search

b-mehta / topos

Topos theory in lean
56 stars 2 forks source link

Uniqueness of adjunctions #14

Closed b-mehta closed 4 years ago

b-mehta commented 4 years ago

If F ⊣ G and F ⊣ H, then G ≅ H, and similarly on the other side.

thjread commented 4 years ago

Most of the way there with 4ede163ad5b622d6a6f590017822b4f733a4bdaa -- I'll see if I can finish it off later.

thjread commented 4 years ago

Uniqueness of left adjoints finished in b40d0e638898e919cef94fa4be34d0a65b553594 - just need to finish proving that if F is left adjoint to G then G.op is left adjoint to F.op (don't think this is in mathlib?) If anyone want to have a go at that feel free.

I'll also make a mathlib PR for def iso_unop {F F' : C ⥤ D} (α : F'.op ≅ F.op) : F ≅ F' since it's just a copy paste to fill an obvious hole.

b-mehta commented 4 years ago 

def adjunction_op {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) : G.op ⊣ F.op :=
adjunction.mk_of_hom_equiv
{ hom_equiv := λ X Y,
    { to_fun := λ f, ((adj.hom_equiv (Y.unop) (X.unop)).inv_fun f.unop).op,
      inv_fun := λ g, ((adj.hom_equiv (Y.unop) (X.unop)).to_fun g.unop).op,
      left_inv := λ f, begin dsimp, rw (adj.hom_equiv _ _).right_inv, refl end,
      right_inv := λ f, begin dsimp, rw (adj.hom_equiv _ _).left_inv, refl end },
  hom_equiv_naturality_left_symm' := λ X' X Y f g, begin dsimp, apply has_hom.hom.unop_inj, simp, apply adj.hom_equiv_naturality_right end,
  hom_equiv_naturality_right' := λ Y' Y X f g, begin dsimp, apply has_hom.hom.unop_inj, simp, apply adj.hom_equiv_naturality_left_symm end
}```
thjread commented 4 years ago

Thanks! I've made a PR