From ff66d924928479a5ab9086a45ce1d25771b9371f Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Wed, 30 Sep 2020 09:51:44 +0000 Subject: [PATCH] chore(category_theory/limits): facts about opposites of limit cones (#4250) Simple facts about limit cones and opposite categories. Co-authored-by: Scott Morrison --- src/category_theory/adjunction/opposites.lean | 5 +- src/category_theory/limits/cones.lean | 110 +++++++++++++- src/category_theory/limits/limits.lean | 70 +++++++++ src/category_theory/monad/equiv_mon.lean | 29 +++- src/category_theory/opposites.lean | 134 +++++++++++++++--- src/data/opposite.lean | 2 + 6 files changed, 317 insertions(+), 33 deletions(-) diff --git a/src/category_theory/adjunction/opposites.lean b/src/category_theory/adjunction/opposites.lean index bd4da65aaaf9f..9b528e7773260 100644 --- a/src/category_theory/adjunction/opposites.lean +++ b/src/category_theory/adjunction/opposites.lean @@ -80,11 +80,12 @@ nat_iso.of_components /-- If `F` and `F'` are both left adjoint to `G`, then they are naturally isomorphic. -/ def left_adjoint_uniq {F F' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) : F ≅ F' := -nat_iso.unop (fully_faithful_cancel_right _ (left_adjoints_coyoneda_equiv adj2 adj1)) +nat_iso.remove_op (fully_faithful_cancel_right _ (left_adjoints_coyoneda_equiv adj2 adj1)) /-- If `G` and `G'` are both right adjoint to `F`, then they are naturally isomorphic. -/ def right_adjoint_uniq {F : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') : G ≅ G' := -nat_iso.unop (left_adjoint_uniq (op_adjoint_op_of_adjoint _ F adj2) (op_adjoint_op_of_adjoint _ _ adj1)) +nat_iso.remove_op + (left_adjoint_uniq (op_adjoint_op_of_adjoint _ F adj2) (op_adjoint_op_of_adjoint _ _ adj1)) end adjunction diff --git a/src/category_theory/limits/cones.lean b/src/category_theory/limits/cones.lean index 5f2a80784b953..f5e6230455f20 100644 --- a/src/category_theory/limits/cones.lean +++ b/src/category_theory/limits/cones.lean @@ -512,8 +512,7 @@ begin dsimp, rw [comp_id, H.map_comp, is_equivalence.fun_inv_map H, assoc, nat_iso.cancel_nat_iso_hom_left, assoc, is_equivalence.inv_fun_id_inv_comp], - apply comp_id, - -- annoyingly `dsimp, simp` leaves it as `c.π.app j ≫ 𝟙 _ = c.π.app j` instead of closing... + dsimp, simp, end /-- `map_cone` is the right inverse to `map_cone_inv`. -/ @@ -527,14 +526,88 @@ end category_theory namespace category_theory.limits +section +variables {F : J ⥤ C} + +/-- Change a `cocone F` into a `cone F.op`. -/ +@[simps] def cocone.op (c : cocone F) : cone F.op := +{ X := op c.X, + π := + { app := λ j, (c.ι.app (unop j)).op, + naturality' := λ j j' f, has_hom.hom.unop_inj (by tidy) } } + +/-- Change a `cone F` into a `cocone F.op`. -/ +@[simps] def cone.op (c : cone F) : cocone F.op := +{ X := op c.X, + ι := + { app := λ j, (c.π.app (unop j)).op, + naturality' := λ j j' f, has_hom.hom.unop_inj (by tidy) } } + +/-- Change a `cocone F.op` into a `cone F`. -/ +@[simps] def cocone.unop (c : cocone F.op) : cone F := +{ X := unop c.X, + π := + { app := λ j, (c.ι.app (op j)).unop, + naturality' := λ j j' f, has_hom.hom.op_inj + begin dsimp, simp only [comp_id], exact (c.w f.op).symm, end } } + +/-- Change a `cone F.op` into a `cocone F`. -/ +@[simps] def cone.unop (c : cone F.op) : cocone F := +{ X := unop c.X, + ι := + { app := λ j, (c.π.app (op j)).unop, + naturality' := λ j j' f, has_hom.hom.op_inj + begin dsimp, simp only [id_comp], exact (c.w f.op), end } } + +variables (F) + +/-- +The category of cocones on `F` +is equivalent to the opposite category of +the category of cones on the opposite of `F`. +-/ +@[simps] +def cocone_equivalence_op_cone_op : cocone F ≌ (cone F.op)ᵒᵖ := +{ functor := + { obj := λ c, op (cocone.op c), + map := λ X Y f, has_hom.hom.op + { hom := f.hom.op, + w' := λ j, by { apply has_hom.hom.unop_inj, dsimp, simp, }, } }, + inverse := + { obj := λ c, cone.unop (unop c), + map := λ X Y f, + { hom := f.unop.hom.unop, + w' := λ j, by { apply has_hom.hom.op_inj, dsimp, simp, }, } }, + unit_iso := nat_iso.of_components (λ c, cocones.ext (iso.refl _) (by tidy)) (by tidy), + counit_iso := nat_iso.of_components (λ c, + by { op_induction c, dsimp, apply iso.op, exact cones.ext (iso.refl _) (by tidy), }) + begin + intros, + have hX : X = op (unop X) := rfl, + revert hX, + generalize : unop X = X', + rintro rfl, + have hY : Y = op (unop Y) := rfl, + revert hY, + generalize : unop Y = Y', + rintro rfl, + apply has_hom.hom.unop_inj, + apply cone_morphism.ext, + dsimp, simp, + end, + functor_unit_iso_comp' := λ c, begin apply has_hom.hom.unop_inj, ext, dsimp, simp, end } + +end + +section variables {F : J ⥤ Cᵒᵖ} --- Here and below we only automatically generate the `@[simp]` lemma for the `X` field, --- as we can be a simpler `rfl` lemma for the components of the natural transformation by hand. /-- Change a cocone on `F.left_op : Jᵒᵖ ⥤ C` to a cocone on `F : J ⥤ Cᵒᵖ`. -/ +-- Here and below we only automatically generate the `@[simp]` lemma for the `X` field, +-- as we can write a simpler `rfl` lemma for the components of the natural transformation by hand. @[simps X] def cone_of_cocone_left_op (c : cocone F.left_op) : cone F := { X := op c.X, - π := nat_trans.right_op (c.ι ≫ (const.op_obj_unop (op c.X)).hom) } + π := nat_trans.remove_left_op (c.ι ≫ (const.op_obj_unop (op c.X)).hom) } @[simp] lemma cone_of_cocone_left_op_π_app (c : cocone F.left_op) (j) : (cone_of_cocone_left_op c).π.app j = (c.ι.app (op j)).op := @@ -552,7 +625,7 @@ by { dsimp [cocone_left_op_of_cone], simp } /-- Change a cone on `F.left_op : Jᵒᵖ ⥤ C` to a cocone on `F : J ⥤ Cᵒᵖ`. -/ @[simps X] def cocone_of_cone_left_op (c : cone F.left_op) : cocone F := { X := op c.X, - ι := nat_trans.right_op ((const.op_obj_unop (op c.X)).hom ≫ c.π) } + ι := nat_trans.remove_left_op ((const.op_obj_unop (op c.X)).hom ≫ c.π) } @[simp] lemma cocone_of_cone_left_op_ι_app (c : cone F.left_op) (j) : (cocone_of_cone_left_op c).ι.app j = (c.π.app (op j)).op := @@ -566,4 +639,29 @@ by { dsimp [cocone_of_cone_left_op], simp } @[simp] lemma cone_left_op_of_cocone_π_app (c : cocone F) (j) : (cone_left_op_of_cocone c).π.app j = (c.ι.app (unop j)).unop := by { dsimp [cone_left_op_of_cocone], simp } + +end + end category_theory.limits + +namespace category_theory.functor + +open category_theory.limits + +variables {F : J ⥤ C} +variables {D : Type u'} [category.{v} D] + +section +variables (G : C ⥤ D) + +/-- The opposite cocone of the image of a cone is the image of the opposite cocone. -/ +def map_cone_op (t : cone F) : (G.map_cone t).op ≅ (G.op.map_cocone t.op) := +cocones.ext (iso.refl _) (by tidy) + +/-- The opposite cone of the image of a cocone is the image of the opposite cone. -/ +def map_cocone_op {t : cocone F} : (G.map_cocone t).op ≅ (G.op.map_cone t.op) := +cones.ext (iso.refl _) (by tidy) + +end + +end category_theory.functor diff --git a/src/category_theory/limits/limits.lean b/src/category_theory/limits/limits.lean index 1f095660a75b2..7fafc6de5bdad 100644 --- a/src/category_theory/limits/limits.lean +++ b/src/category_theory/limits/limits.lean @@ -1706,4 +1706,74 @@ by { constructor, intro F, apply has_colimit_of_equivalence_comp e, apply_instan end colimit +section opposite + +/-- +If `t : cone F` is a limit cone, then `t.op : cocone F.op` is a colimit cocone. +-/ +def is_limit.op {t : cone F} (P : is_limit t) : is_colimit t.op := +{ desc := λ s, (P.lift s.unop).op, + fac' := λ s j, congr_arg has_hom.hom.op (P.fac s.unop (unop j)), + uniq' := λ s m w, + begin + rw ← P.uniq s.unop m.unop, + { refl, }, + { dsimp, intro j, rw ← w, refl, } + end } + +/-- +If `t : cocone F` is a colimit cocone, then `t.op : cone F.op` is a limit cone. +-/ +def is_colimit.op {t : cocone F} (P : is_colimit t) : is_limit t.op := +{ lift := λ s, (P.desc s.unop).op, + fac' := λ s j, congr_arg has_hom.hom.op (P.fac s.unop (unop j)), + uniq' := λ s m w, + begin + rw ← P.uniq s.unop m.unop, + { refl, }, + { dsimp, intro j, rw ← w, refl, } + end } + +/-- +If `t : cone F.op` is a limit cone, then `t.unop : cocone F` is a colimit cocone. +-/ +def is_limit.unop {t : cone F.op} (P : is_limit t) : is_colimit t.unop := +{ desc := λ s, (P.lift s.op).unop, + fac' := λ s j, congr_arg has_hom.hom.unop (P.fac s.op (op j)), + uniq' := λ s m w, + begin + rw ← P.uniq s.op m.op, + { refl, }, + { dsimp, intro j, rw ← w, refl, } + end } + +/-- +If `t : cocone F.op` is a colimit cocone, then `t.unop : cone F.` is a limit cone. +-/ +def is_colimit.unop {t : cocone F.op} (P : is_colimit t) : is_limit t.unop := +{ lift := λ s, (P.desc s.op).unop, + fac' := λ s j, congr_arg has_hom.hom.unop (P.fac s.op (op j)), + uniq' := λ s m w, + begin + rw ← P.uniq s.op m.op, + { refl, }, + { dsimp, intro j, rw ← w, refl, } + end } + +/-- +`t : cone F` is a limit cone if and only is `t.op : cocone F.op` is a colimit cocone. +-/ +def is_limit_equiv_is_colimit_op {t : cone F} : is_limit t ≃ is_colimit t.op := +equiv_of_subsingleton_of_subsingleton + is_limit.op (λ P, P.unop.of_iso_limit (cones.ext (iso.refl _) (by tidy))) + +/-- +`t : cocone F` is a colimit cocone if and only is `t.op : cone F.op` is a limit cone. +-/ +def is_colimit_equiv_is_limit_op {t : cocone F} : is_colimit t ≃ is_limit t.op := +equiv_of_subsingleton_of_subsingleton + is_colimit.op (λ P, P.unop.of_iso_colimit (cocones.ext (iso.refl _) (by tidy))) + +end opposite + end category_theory.limits diff --git a/src/category_theory/monad/equiv_mon.lean b/src/category_theory/monad/equiv_mon.lean index 5c561020f1fd9..e812f78f1eda5 100644 --- a/src/category_theory/monad/equiv_mon.lean +++ b/src/category_theory/monad/equiv_mon.lean @@ -87,28 +87,43 @@ def Mon_to_Monad : Mon_ (C ⥤ C) ⥤ Monad C := finish, end, ..f.hom } } + +namespace Monad_Mon_equiv variable {C} /-- Isomorphism of functors used in `Monad_Mon_equiv` -/ @[simps] -def of_to_mon_end_iso : Mon_to_Monad C ⋙ Monad_to_Mon C ≅ 𝟭 _ := +def counit_iso : Mon_to_Monad C ⋙ Monad_to_Mon C ≅ 𝟭 _ := { hom := { app := λ _, { hom := 𝟙 _ } }, inv := { app := λ _, { hom := 𝟙 _ } } } +/-- Auxilliary definition for `Monad_Mon_equiv` -/ +@[simps] +def unit_iso_hom : 𝟭 _ ⟶ Monad_to_Mon C ⋙ Mon_to_Monad C := +{ app := λ _, { app := λ _, 𝟙 _ } } + +/-- Auxilliary definition for `Monad_Mon_equiv` -/ +@[simps] +def unit_iso_inv : Monad_to_Mon C ⋙ Mon_to_Monad C ⟶ 𝟭 _ := +{ app := λ _, { app := λ _, 𝟙 _ } } + /-- Isomorphism of functors used in `Monad_Mon_equiv` -/ @[simps] -def to_of_mon_end_iso : Monad_to_Mon C ⋙ Mon_to_Monad C ≅ 𝟭 _ := -{ hom := { app := λ _, { app := λ _, 𝟙 _ } }, - inv := { app := λ _, { app := λ _, 𝟙 _ } } } +def unit_iso : 𝟭 _ ≅ Monad_to_Mon C ⋙ Mon_to_Monad C := +{ hom := unit_iso_hom, + inv := unit_iso_inv } + +end Monad_Mon_equiv + +open Monad_Mon_equiv -variable (C) /-- Oh, monads are just monoids in the category of endofunctors (equivalence of categories). -/ @[simps] def Monad_Mon_equiv : (Monad C) ≌ (Mon_ (C ⥤ C)) := { functor := Monad_to_Mon _, inverse := Mon_to_Monad _, - unit_iso := to_of_mon_end_iso.symm, - counit_iso := of_to_mon_end_iso } + unit_iso := unit_iso, + counit_iso := counit_iso } -- Sanity check example (A : Monad C) {X : C} : ((Monad_Mon_equiv C).unit_iso.app A).hom.app X = 𝟙 _ := rfl diff --git a/src/category_theory/opposites.lean b/src/category_theory/opposites.lean index e86d5ec02bcc0..1386a9eb0b399 100644 --- a/src/category_theory/opposites.lean +++ b/src/category_theory/opposites.lean @@ -27,7 +27,13 @@ variables [has_hom.{v₁} C] instance has_hom.opposite : has_hom Cᵒᵖ := { hom := λ X Y, unop Y ⟶ unop X } +/-- +The opposite of a morphism in `C`. +-/ def has_hom.hom.op {X Y : C} (f : X ⟶ Y) : op Y ⟶ op X := f +/-- +Given a morphism in `Cᵒᵖ`, we can take the "unopposite" back in `C`. +-/ def has_hom.hom.unop {X Y : Cᵒᵖ} (f : X ⟶ Y) : unop Y ⟶ unop X := f attribute [irreducible] has_hom.opposite @@ -87,6 +93,10 @@ def op_op_equivalence : Cᵒᵖᵒᵖ ≌ C := unit_iso := iso.refl (𝟭 Cᵒᵖᵒᵖ), counit_iso := iso.refl (unop_unop ⋙ op_op) } +/-- +If `f.op` is an isomorphism `f` must be too. +(This cannot be an instance as it would immediately loop!) +-/ def is_iso_of_op {X Y : C} (f : X ⟶ Y) [is_iso f.op] : is_iso f := { inv := (inv (f.op)).unop, hom_inv_id' := has_hom.hom.op_inj (by simp), @@ -100,13 +110,21 @@ variables {D : Type u₂} [category.{v₂} D] variables {C D} +/-- +The opposite of a functor, i.e. considering a functor `F : C ⥤ D` as a functor `Cᵒᵖ ⥤ Dᵒᵖ`. +In informal mathematics no distinction is made between these. +-/ @[simps] -protected definition op (F : C ⥤ D) : Cᵒᵖ ⥤ Dᵒᵖ := +protected def op (F : C ⥤ D) : Cᵒᵖ ⥤ Dᵒᵖ := { obj := λ X, op (F.obj (unop X)), map := λ X Y f, (F.map f.unop).op } +/-- +Given a functor `F : Cᵒᵖ ⥤ Dᵒᵖ` we can take the "unopposite" functor `F : C ⥤ D`. +In informal mathematics no distinction is made between these. +-/ @[simps] -protected definition unop (F : Cᵒᵖ ⥤ Dᵒᵖ) : C ⥤ D := +protected def unop (F : Cᵒᵖ ⥤ Dᵒᵖ) : C ⥤ D := { obj := λ X, unop (F.obj (op X)), map := λ X Y f, (F.map f.op).unop } @@ -120,15 +138,21 @@ nat_iso.of_components (λ X, iso.refl _) (by tidy) variables (C D) +/-- +Taking the opposite of a functor is functorial. +-/ @[simps] -definition op_hom : (C ⥤ D)ᵒᵖ ⥤ (Cᵒᵖ ⥤ Dᵒᵖ) := +def op_hom : (C ⥤ D)ᵒᵖ ⥤ (Cᵒᵖ ⥤ Dᵒᵖ) := { obj := λ F, (unop F).op, map := λ F G α, { app := λ X, (α.unop.app (unop X)).op, naturality' := λ X Y f, has_hom.hom.unop_inj (α.unop.naturality f.unop).symm } } +/-- +Take the "unopposite" of a functor is functorial. +-/ @[simps] -definition op_inv : (Cᵒᵖ ⥤ Dᵒᵖ) ⥤ (C ⥤ D)ᵒᵖ := +def op_inv : (Cᵒᵖ ⥤ Dᵒᵖ) ⥤ (C ⥤ D)ᵒᵖ := { obj := λ F, op F.unop, map := λ F G α, has_hom.hom.op { app := λ X, (α.app (op X)).unop, @@ -138,13 +162,21 @@ definition op_inv : (Cᵒᵖ ⥤ Dᵒᵖ) ⥤ (C ⥤ D)ᵒᵖ := variables {C D} +/-- +Another variant of the opposite of functor, turning a functor `C ⥤ Dᵒᵖ` into a functor `Cᵒᵖ ⥤ D`. +In informal mathematics no distinction is made. +-/ @[simps] -protected definition left_op (F : C ⥤ Dᵒᵖ) : Cᵒᵖ ⥤ D := +protected def left_op (F : C ⥤ Dᵒᵖ) : Cᵒᵖ ⥤ D := { obj := λ X, unop (F.obj (unop X)), map := λ X Y f, (F.map f.unop).unop } +/-- +Another variant of the opposite of functor, turning a functor `Cᵒᵖ ⥤ D` into a functor `C ⥤ Dᵒᵖ`. +In informal mathematics no distinction is made. +-/ @[simps] -protected definition right_op (F : Cᵒᵖ ⥤ D) : C ⥤ Dᵒᵖ := +protected def right_op (F : Cᵒᵖ ⥤ D) : C ⥤ Dᵒᵖ := { obj := λ X, op (F.obj (op X)), map := λ X Y f, (F.map f.op).op } @@ -178,13 +210,25 @@ variables {F G : C ⥤ D} local attribute [semireducible] has_hom.opposite -@[simps] protected definition op (α : F ⟶ G) : G.op ⟶ F.op := +/-- The opposite of a natural transformation. -/ +@[simps] protected def op (α : F ⟶ G) : G.op ⟶ F.op := { app := λ X, (α.app (unop X)).op, naturality' := begin tidy, erw α.naturality, refl, end } @[simp] lemma op_id (F : C ⥤ D) : nat_trans.op (𝟙 F) = 𝟙 (F.op) := rfl -@[simps] protected definition unop (α : F.op ⟶ G.op) : G ⟶ F := +/-- The "unopposite" of a natural transformation. -/ +@[simps] protected def unop {F G : Cᵒᵖ ⥤ Dᵒᵖ} (α : F ⟶ G) : G.unop ⟶ F.unop := +{ app := λ X, (α.app (op X)).unop, + naturality' := begin tidy, erw α.naturality, refl, end } + +@[simp] lemma unop_id (F : Cᵒᵖ ⥤ Dᵒᵖ) : nat_trans.unop (𝟙 F) = 𝟙 (F.unop) := rfl + +/-- +Given a natural transformation `α : F.op ⟶ G.op`, +we can take the "unopposite" of each component obtaining a natural transformation `G ⟶ F`. +-/ +@[simps] protected def remove_op (α : F.op ⟶ G.op) : G ⟶ F := { app := λ X, (α.app (op X)).unop, naturality' := begin @@ -195,7 +239,7 @@ local attribute [semireducible] has_hom.opposite refl, end } -@[simp] lemma unop_id (F : C ⥤ D) : nat_trans.unop (𝟙 F.op) = 𝟙 F := rfl +@[simp] lemma remove_op_id (F : C ⥤ D) : nat_trans.remove_op (𝟙 F.op) = 𝟙 F := rfl end @@ -204,7 +248,11 @@ variables {F G : C ⥤ Dᵒᵖ} local attribute [semireducible] has_hom.opposite -protected definition left_op (α : F ⟶ G) : G.left_op ⟶ F.left_op := +/-- +Given a natural transformation `α : F ⟶ G`, for `F G : C ⥤ Dᵒᵖ`, +taking `unop` of each component gives a natural transformation `G.left_op ⟶ F.left_op`. +-/ +protected def left_op (α : F ⟶ G) : G.left_op ⟶ F.left_op := { app := λ X, (α.app (unop X)).unop, naturality' := begin tidy, erw α.naturality, refl, end } @@ -212,7 +260,11 @@ protected definition left_op (α : F ⟶ G) : G.left_op ⟶ F.left_op := (nat_trans.left_op α).app X = (α.app (unop X)).unop := rfl -protected definition right_op (α : F.left_op ⟶ G.left_op) : G ⟶ F := +/-- +Given a natural transformation `α : F.left_op ⟶ G.left_op`, for `F G : C ⥤ Dᵒᵖ`, +taking `op` of each component gives a natural transformation `G ⟶ F`. +-/ +protected def remove_left_op (α : F.left_op ⟶ G.left_op) : G ⟶ F := { app := λ X, (α.app (op X)).op, naturality' := begin @@ -222,8 +274,8 @@ protected definition right_op (α : F.left_op ⟶ G.left_op) : G ⟶ F := erw this end } -@[simp] lemma right_op_app (α : F.left_op ⟶ G.left_op) (X) : - (nat_trans.right_op α).app X = (α.app (op X)).op := +@[simp] lemma remove_left_op_app (α : F.left_op ⟶ G.left_op) (X) : + (nat_trans.remove_left_op α).app X = (α.app (op X)).op := rfl end @@ -233,7 +285,10 @@ namespace iso variables {X Y : C} -protected definition op (α : X ≅ Y) : op Y ≅ op X := +/-- +The opposite isomorphism. +-/ +protected def op (α : X ≅ Y) : op Y ≅ op X := { hom := α.hom.op, inv := α.inv.op, hom_inv_id' := has_hom.hom.unop_inj α.inv_hom_id, @@ -251,7 +306,7 @@ variables {F G : C ⥤ D} /-- The natural isomorphism between opposite functors `G.op ≅ F.op` induced by a natural isomorphism between the original functors `F ≅ G`. -/ -protected definition op (α : F ≅ G) : G.op ≅ F.op := +protected def op (α : F ≅ G) : G.op ≅ F.op := { hom := nat_trans.op α.hom, inv := nat_trans.op α.inv, hom_inv_id' := begin ext, dsimp, rw ←op_comp, rw α.inv_hom_id_app, refl, end, @@ -262,17 +317,60 @@ protected definition op (α : F ≅ G) : G.op ≅ F.op := /-- The natural isomorphism between functors `G ≅ F` induced by a natural isomorphism between the opposite functors `F.op ≅ G.op`. -/ -protected definition unop (α : F.op ≅ G.op) : G ≅ F := +protected def remove_op (α : F.op ≅ G.op) : G ≅ F := +{ hom := nat_trans.remove_op α.hom, + inv := nat_trans.remove_op α.inv, + hom_inv_id' := begin ext, dsimp, rw ←unop_comp, rw α.inv_hom_id_app, refl, end, + inv_hom_id' := begin ext, dsimp, rw ←unop_comp, rw α.hom_inv_id_app, refl, end } + +@[simp] lemma remove_op_hom (α : F.op ≅ G.op) : + (nat_iso.remove_op α).hom = nat_trans.remove_op α.hom := rfl +@[simp] lemma remove_op_inv (α : F.op ≅ G.op) : + (nat_iso.remove_op α).inv = nat_trans.remove_op α.inv := rfl + +/-- The natural isomorphism between functors `G.unop ≅ F.unop` induced by a natural isomorphism +between the original functors `F ≅ G`. -/ +protected def unop {F G : Cᵒᵖ ⥤ Dᵒᵖ} (α : F ≅ G) : G.unop ≅ F.unop := { hom := nat_trans.unop α.hom, inv := nat_trans.unop α.inv, hom_inv_id' := begin ext, dsimp, rw ←unop_comp, rw α.inv_hom_id_app, refl, end, inv_hom_id' := begin ext, dsimp, rw ←unop_comp, rw α.hom_inv_id_app, refl, end } -@[simp] lemma unop_hom (α : F.op ≅ G.op) : (nat_iso.unop α).hom = nat_trans.unop α.hom := rfl -@[simp] lemma unop_inv (α : F.op ≅ G.op) : (nat_iso.unop α).inv = nat_trans.unop α.inv := rfl +@[simp] lemma unop_hom {F G : Cᵒᵖ ⥤ Dᵒᵖ} (α : F ≅ G) : + (nat_iso.unop α).hom = nat_trans.unop α.hom := rfl +@[simp] lemma unop_inv {F G : Cᵒᵖ ⥤ Dᵒᵖ} (α : F ≅ G) : + (nat_iso.unop α).inv = nat_trans.unop α.inv := rfl + end nat_iso +namespace equivalence + +variables {D : Type u₂} [category.{v₂} D] + +/-- +An equivalence between categories gives an equivalence between the opposite categories. +-/ +@[simps] +def op (e : C ≌ D) : Cᵒᵖ ≌ Dᵒᵖ := +{ functor := e.functor.op, + inverse := e.inverse.op, + unit_iso := (nat_iso.op e.unit_iso).symm, + counit_iso := (nat_iso.op e.counit_iso).symm, + functor_unit_iso_comp' := λ X, by { apply has_hom.hom.unop_inj, dsimp, simp, }, } + +/-- +An equivalence between opposite categories gives an equivalence between the original categories. +-/ +@[simps] +def unop (e : Cᵒᵖ ≌ Dᵒᵖ) : C ≌ D := +{ functor := e.functor.unop, + inverse := e.inverse.unop, + unit_iso := (nat_iso.unop e.unit_iso).symm, + counit_iso := (nat_iso.unop e.counit_iso).symm, + functor_unit_iso_comp' := λ X, by { apply has_hom.hom.op_inj, dsimp, simp, }, } + +end equivalence /-- The equivalence between arrows of the form `A ⟶ B` and `B.unop ⟶ A.unop`. Useful for building adjunctions. diff --git a/src/data/opposite.lean b/src/data/opposite.lean index e0a2d57bbcfe3..d9ee995c3fb3a 100644 --- a/src/data/opposite.lean +++ b/src/data/opposite.lean @@ -77,8 +77,10 @@ equiv_to_opposite.symm.apply_eq_iff_eq_symm_apply _ _ instance [inhabited α] : inhabited αᵒᵖ := ⟨op (default _)⟩ +@[simp] def op_induction {F : Π (X : αᵒᵖ), Sort v} (h : Π X, F (op X)) : Π X, F X := λ X, h (unop X) + end opposite namespace tactic