diff --git a/Mathlib/CategoryTheory/Adjunction/Basic.lean b/Mathlib/CategoryTheory/Adjunction/Basic.lean index a5b65f05aaa50..610789b9be365 100644 --- a/Mathlib/CategoryTheory/Adjunction/Basic.lean +++ b/Mathlib/CategoryTheory/Adjunction/Basic.lean @@ -177,14 +177,14 @@ theorem homEquiv_naturality_right_symm (f : X ⟶ G.obj Y) (g : Y ⟶ Y') : #align category_theory.adjunction.hom_equiv_naturality_right_symm CategoryTheory.Adjunction.homEquiv_naturality_right_symm @[simp] -theorem left_triangle : whiskerRight adj.unit F ≫ whiskerLeft F adj.counit = NatTrans.id _ := by +theorem left_triangle : whiskerRight adj.unit F ≫ whiskerLeft F adj.counit = 𝟙 _ := by ext; dsimp erw [← adj.homEquiv_counit, Equiv.symm_apply_eq, adj.homEquiv_unit] simp #align category_theory.adjunction.left_triangle CategoryTheory.Adjunction.left_triangle @[simp] -theorem right_triangle : whiskerLeft G adj.unit ≫ whiskerRight adj.counit G = NatTrans.id _ := by +theorem right_triangle : whiskerLeft G adj.unit ≫ whiskerRight adj.counit G = 𝟙 _ := by ext; dsimp erw [← adj.homEquiv_unit, ← Equiv.eq_symm_apply, adj.homEquiv_counit] simp @@ -387,10 +387,10 @@ def mkOfUnitCounit (adj : CoreUnitCounit F G) : F ⊣ G := exact t } } #align category_theory.adjunction.mk_of_unit_counit CategoryTheory.Adjunction.mkOfUnitCounit -/- Porting note: simpNF linter claims these are solved by simp but that +/- Porting note: simpNF linter claims these are solved by simp but that is not true -/ -attribute [nolint simpNF] CategoryTheory.Adjunction.mkOfUnitCounit_homEquiv_symm_apply -attribute [nolint simpNF] CategoryTheory.Adjunction.mkOfUnitCounit_homEquiv_apply +attribute [nolint simpNF] CategoryTheory.Adjunction.mkOfUnitCounit_homEquiv_symm_apply +attribute [nolint simpNF] CategoryTheory.Adjunction.mkOfUnitCounit_homEquiv_apply /-- The adjunction between the identity functor on a category and itself. -/ def id : 𝟭 C ⊣ 𝟭 C where diff --git a/Mathlib/CategoryTheory/DiscreteCategory.lean b/Mathlib/CategoryTheory/DiscreteCategory.lean index 14cc5ef7c9f13..9518b44d11cdb 100644 --- a/Mathlib/CategoryTheory/DiscreteCategory.lean +++ b/Mathlib/CategoryTheory/DiscreteCategory.lean @@ -44,7 +44,7 @@ universe v₁ v₂ v₃ u₁ u₁' u₂ u₃ -- This is intentionally a structure rather than a type synonym -- to enforce using `DiscreteEquiv` (or `Discrete.mk` and `Discrete.as`) to move between --- `discrete α` and `α`. Otherwise there is too much API leakage. +-- `Discrete α` and `α`. Otherwise there is too much API leakage. /-- A wrapper for promoting any type to a category, with the only morphisms being equalities. -/ @@ -64,8 +64,7 @@ theorem Discrete.mk_as {α : Type u₁} (X : Discrete α) : Discrete.mk X.as = X /-- `Discrete α` is equivalent to the original type `α`.-/ @[simps] -def discreteEquiv {α : Type u₁} : Discrete α ≃ α - where +def discreteEquiv {α : Type u₁} : Discrete α ≃ α where toFun := Discrete.as invFun := Discrete.mk left_inv := by aesop_cat @@ -82,8 +81,7 @@ somewhat annoyingly we have to define `X ⟶ Y` as `ULift (PLift (X = Y))`. See -/ -instance discreteCategory (α : Type u₁) : SmallCategory (Discrete α) - where +instance discreteCategory (α : Type u₁) : SmallCategory (Discrete α) where Hom X Y := ULift (PLift (X.as = Y.as)) id X := ULift.up (PLift.up rfl) comp {X Y Z} g f := by @@ -166,8 +164,7 @@ instance {I : Type u₁} {i j : Discrete I} (f : i ⟶ j) : IsIso f := ⟨⟨Discrete.eqToHom (eq_of_hom f).symm, by aesop_cat⟩⟩ /-- Any function `I → C` gives a functor `Discrete I ⥤ C`.-/ -def functor {I : Type u₁} (F : I → C) : Discrete I ⥤ C - where +def functor {I : Type u₁} (F : I → C) : Discrete I ⥤ C where obj := F ∘ Discrete.as map {X Y} f := by dsimp @@ -249,8 +246,7 @@ def compNatIsoDiscrete {I : Type u₁} {D : Type u₃} [Category.{v₃} D] (F : an equivalence between the corresponding `discrete` categories. -/ @[simps] -def equivalence {I : Type u₁} {J : Type u₂} (e : I ≃ J) : Discrete I ≌ Discrete J - where +def equivalence {I : Type u₁} {J : Type u₂} (e : I ≃ J) : Discrete I ≌ Discrete J where functor := Discrete.functor (Discrete.mk ∘ (e : I → J)) inverse := Discrete.functor (Discrete.mk ∘ (e.symm : J → I)) unitIso := @@ -269,8 +265,7 @@ def equivalence {I : Type u₁} {J : Type u₂} (e : I ≃ J) : Discrete I ≌ D /-- We can convert an equivalence of `discrete` categories to a type-level `Equiv`. -/ @[simps] -def equivOfEquivalence {α : Type u₁} {β : Type u₂} (h : Discrete α ≌ Discrete β) : α ≃ β - where +def equivOfEquivalence {α : Type u₁} {β : Type u₂} (h : Discrete α ≌ Discrete β) : α ≃ β where toFun := Discrete.as ∘ h.functor.obj ∘ Discrete.mk invFun := Discrete.as ∘ h.inverse.obj ∘ Discrete.mk left_inv a := by simpa using eq_of_hom (h.unitIso.app (Discrete.mk a)).2 diff --git a/Mathlib/CategoryTheory/Equivalence.lean b/Mathlib/CategoryTheory/Equivalence.lean index 50f19437dec10..e647b92d214c8 100644 --- a/Mathlib/CategoryTheory/Equivalence.lean +++ b/Mathlib/CategoryTheory/Equivalence.lean @@ -48,9 +48,9 @@ if it is full, faithful and essentially surjective. ## Main results * `Equivalence.mk`: upgrade an equivalence to a (half-)adjoint equivalence -* `IsEquivalence.equiv_of_iso`: when `F` and `G` are isomorphic functors, `F` is an equivalence +* `IsEquivalence.equivOfIso`: when `F` and `G` are isomorphic functors, `F` is an equivalence iff `G` is. -* `Equivalence.of_fully_faithfully_essSurj`: a fully faithful essentially surjective functor is an +* `Equivalence.ofFullyFaithfullyEssSurj`: a fully faithful essentially surjective functor is an equivalence. ## Notations @@ -96,7 +96,7 @@ structure Equivalence (C : Type u₁) (D : Type u₂) [Category.{v₁} C] [Categ /-- We infix the usual notation for an equivalence -/ infixr:10 " ≌ " => Equivalence - + variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D] namespace Equivalence @@ -127,29 +127,25 @@ preventing structure projections from unfolding. -/ theorem Equivalence_mk'_unit (functor inverse unit_iso counit_iso f) : (⟨functor, inverse, unit_iso, counit_iso, f⟩ : C ≌ D).unit = unit_iso.hom := rfl -#align - category_theory.equivalence.equivalence_mk'_unit CategoryTheory.Equivalence.equivalence_mk'_unit +#align category_theory.equivalence.equivalence_mk'_unit CategoryTheory.Equivalence.Equivalence_mk'_unit @[simp] -theorem equivalence_mk'_counit (functor inverse unit_iso counit_iso f) : +theorem Equivalence_mk'_counit (functor inverse unit_iso counit_iso f) : (⟨functor, inverse, unit_iso, counit_iso, f⟩ : C ≌ D).counit = counit_iso.hom := rfl -#align category_theory.equivalence.equivalence_mk'_counit - CategoryTheory.Equivalence.equivalence_mk'_counit +#align category_theory.equivalence.equivalence_mk'_counit CategoryTheory.Equivalence.Equivalence_mk'_counit @[simp] -theorem equivalence_mk'_unitInv (functor inverse unit_iso counit_iso f) : +theorem Equivalence_mk'_unitInv (functor inverse unit_iso counit_iso f) : (⟨functor, inverse, unit_iso, counit_iso, f⟩ : C ≌ D).unitInv = unit_iso.inv := rfl -#align category_theory.equivalence.equivalence_mk'_unit_inv - CategoryTheory.Equivalence.equivalence_mk'_unitInv +#align category_theory.equivalence.equivalence_mk'_unit_inv CategoryTheory.Equivalence.Equivalence_mk'_unitInv @[simp] -theorem equivalence_mk'_counitInv (functor inverse unit_iso counit_iso f) : +theorem Equivalence_mk'_counitInv (functor inverse unit_iso counit_iso f) : (⟨functor, inverse, unit_iso, counit_iso, f⟩ : C ≌ D).counitInv = counit_iso.inv := rfl -#align category_theory.equivalence.equivalence_mk'_counit_inv - CategoryTheory.Equivalence.equivalence_mk'_counitInv +#align category_theory.equivalence.equivalence_mk'_counit_inv CategoryTheory.Equivalence.Equivalence_mk'_counitInv @[simp] theorem functor_unit_comp (e : C ≌ D) (X : C) : @@ -164,25 +160,22 @@ theorem counitInv_functor_comp (e : C ≌ D) (X : C) : erw [Iso.inv_eq_inv (e.functor.mapIso (e.unitIso.app X) ≪≫ e.counitIso.app (e.functor.obj X)) (Iso.refl _)] exact e.functor_unit_comp X -#align category_theory.equivalence.counit_inv_functor_comp - CategoryTheory.Equivalence.counitInv_functor_comp +#align category_theory.equivalence.counit_inv_functor_comp CategoryTheory.Equivalence.counitInv_functor_comp -theorem counit_inv_app_functor (e : C ≌ D) (X : C) : +theorem counitInv_app_functor (e : C ≌ D) (X : C) : e.counitInv.app (e.functor.obj X) = e.functor.map (e.unit.app X) := by symm erw [← Iso.comp_hom_eq_id (e.counitIso.app _), functor_unit_comp] rfl -#align category_theory.equivalence.counit_inv_app_functor - CategoryTheory.Equivalence.counit_inv_app_functor +#align category_theory.equivalence.counit_inv_app_functor CategoryTheory.Equivalence.counitInv_app_functor theorem counit_app_functor (e : C ≌ D) (X : C) : e.counit.app (e.functor.obj X) = e.functor.map (e.unitInv.app X) := by erw [← Iso.hom_comp_eq_id (e.functor.mapIso (e.unitIso.app X)), functor_unit_comp] rfl -#align - category_theory.equivalence.counit_app_functor CategoryTheory.Equivalence.counit_app_functor +#align category_theory.equivalence.counit_app_functor CategoryTheory.Equivalence.counit_app_functor /-- The other triangle equality. The proof follows the following proof in Globular: http://globular.science/1905.001 -/ @@ -213,14 +206,13 @@ theorem unit_inverse_comp (e : C ≌ D) (Y : D) : #align category_theory.equivalence.unit_inverse_comp CategoryTheory.Equivalence.unit_inverse_comp @[simp] -theorem inverse_counit_inv_comp (e : C ≌ D) (Y : D) : +theorem inverse_counitInv_comp (e : C ≌ D) (Y : D) : e.inverse.map (e.counitInv.app Y) ≫ e.unitInv.app (e.inverse.obj Y) = 𝟙 (e.inverse.obj Y) := by erw [Iso.inv_eq_inv (e.unitIso.app (e.inverse.obj Y) ≪≫ e.inverse.mapIso (e.counitIso.app Y)) (Iso.refl _)] exact e.unit_inverse_comp Y -#align category_theory.equivalence.inverse_counit_inv_comp - CategoryTheory.Equivalence.inverse_counit_inv_comp +#align category_theory.equivalence.inverse_counit_inv_comp CategoryTheory.Equivalence.inverse_counitInv_comp theorem unit_app_inverse (e : C ≌ D) (Y : D) : e.unit.app (e.inverse.obj Y) = e.inverse.map (e.counitInv.app Y) := by @@ -228,13 +220,12 @@ theorem unit_app_inverse (e : C ≌ D) (Y : D) : dsimp #align category_theory.equivalence.unit_app_inverse CategoryTheory.Equivalence.unit_app_inverse -theorem unit_inv_app_inverse (e : C ≌ D) (Y : D) : +theorem unitInv_app_inverse (e : C ≌ D) (Y : D) : e.unitInv.app (e.inverse.obj Y) = e.inverse.map (e.counit.app Y) := by symm erw [← Iso.hom_comp_eq_id (e.unitIso.app _), unit_inverse_comp] rfl -#align - category_theory.equivalence.unit_inv_app_inverse CategoryTheory.Equivalence.unit_inv_app_inverse +#align category_theory.equivalence.unit_inv_app_inverse CategoryTheory.Equivalence.unitInv_app_inverse @[simp] theorem fun_inv_map (e : C ≌ D) (X Y : D) (f : X ⟶ Y) : @@ -254,9 +245,9 @@ section variable {F : C ⥤ D} {G : D ⥤ C} (η : 𝟭 C ≅ F ⋙ G) (ε : G ⋙ F ≅ 𝟭 D) /-- If `η : 𝟭 C ≅ F ⋙ G` is part of a (not necessarily half-adjoint) equivalence, we can upgrade it -to a refined natural isomorphism `adjointify_η η : 𝟭 C ≅ F ⋙ G` which exhibits the properties -required for a half-adjoint equivalence. See `equivalence.mk`. -/ -def adjointifyη : 𝟭 C ≅ F ⋙ G := by +to a refined natural isomorphism `adjointifyη η : 𝟭 C ≅ F ⋙ G` which exhibits the properties +required for a half-adjoint equivalence. See `Equivalence.mk`. -/ +def adjointifyη : 𝟭 C ≅ F ⋙ G := by calc 𝟭 C ≅ F ⋙ G := η _ ≅ F ⋙ 𝟭 D ⋙ G := isoWhiskerLeft F (leftUnitor G).symm @@ -265,7 +256,6 @@ def adjointifyη : 𝟭 C ≅ F ⋙ G := by _ ≅ (F ⋙ G) ⋙ F ⋙ G := (associator F G (F ⋙ G)).symm _ ≅ 𝟭 C ⋙ F ⋙ G := isoWhiskerRight η.symm (F ⋙ G) _ ≅ F ⋙ G := leftUnitor (F ⋙ G) - #align category_theory.equivalence.adjointify_η CategoryTheory.Equivalence.adjointifyη theorem adjointify_η_ε (X : C) : @@ -291,7 +281,7 @@ protected def mk (F : C ⥤ D) (G : D ⥤ C) (η : 𝟭 C ≅ F ⋙ G) (ε : G /-- Equivalence of categories is reflexive. -/ @[refl, simps] -def refl : C ≌ C := +def refl : C ≌ C := ⟨𝟭 C, 𝟭 C, Iso.refl _, Iso.refl _, fun _ => Category.id_comp _⟩ #align category_theory.equivalence.refl CategoryTheory.Equivalence.refl @@ -301,7 +291,7 @@ instance : Inhabited (C ≌ C) := /-- Equivalence of categories is symmetric. -/ @[symm, simps] def symm (e : C ≌ D) : D ≌ C := - ⟨e.inverse, e.functor, e.counitIso.symm, e.unitIso.symm, e.inverse_counit_inv_comp⟩ + ⟨e.inverse, e.functor, e.counitIso.symm, e.unitIso.symm, e.inverse_counitInv_comp⟩ #align category_theory.equivalence.symm CategoryTheory.Equivalence.symm variable {E : Type u₃} [Category.{v₃} E] @@ -318,12 +308,12 @@ def trans (e : C ≌ D) (f : D ≌ E) : C ≌ E counitIso := by refine' Iso.trans _ f.counitIso exact isoWhiskerLeft f.inverse (isoWhiskerRight e.counitIso f.functor) - -- We wouldn't have needed to give this proof if we'd used `equivalence.mk`, + -- We wouldn't have needed to give this proof if we'd used `Equivalence.mk`, -- but we choose to avoid using that here, for the sake of good structure projection `simp` -- lemmas. functor_unitIso_comp X := by dsimp - rw [← f.functor.map_comp_assoc, e.functor.map_comp, ← counit_inv_app_functor, fun_inv_map, + rw [← f.functor.map_comp_assoc, e.functor.map_comp, ← counitInv_app_functor, fun_inv_map, Iso.inv_hom_id_app_assoc, assoc, Iso.inv_hom_id_app, counit_app_functor, ← Functor.map_comp] erw [comp_id, Iso.hom_inv_id_app, Functor.map_id] #align category_theory.equivalence.trans CategoryTheory.Equivalence.trans @@ -335,22 +325,20 @@ def funInvIdAssoc (e : C ≌ D) (F : C ⥤ E) : e.functor ⋙ e.inverse ⋙ F #align category_theory.equivalence.fun_inv_id_assoc CategoryTheory.Equivalence.funInvIdAssoc @[simp] -theorem fun_inv_id_assoc_hom_app (e : C ≌ D) (F : C ⥤ E) (X : C) : +theorem funInvIdAssoc_hom_app (e : C ≌ D) (F : C ⥤ E) (X : C) : (funInvIdAssoc e F).hom.app X = F.map (e.unitInv.app X) := by dsimp [funInvIdAssoc] aesop_cat -#align category_theory.equivalence.fun_inv_id_assoc_hom_app - CategoryTheory.Equivalence.fun_inv_id_assoc_hom_app +#align category_theory.equivalence.fun_inv_id_assoc_hom_app CategoryTheory.Equivalence.funInvIdAssoc_hom_app @[simp] -theorem fun_inv_id_assoc_inv_app (e : C ≌ D) (F : C ⥤ E) (X : C) : +theorem funInvIdAssoc_inv_app (e : C ≌ D) (F : C ⥤ E) (X : C) : (funInvIdAssoc e F).inv.app X = F.map (e.unit.app X) := by dsimp [funInvIdAssoc] aesop_cat -#align category_theory.equivalence.fun_inv_id_assoc_inv_app - CategoryTheory.Equivalence.fun_inv_id_assoc_inv_app +#align category_theory.equivalence.fun_inv_id_assoc_inv_app CategoryTheory.Equivalence.funInvIdAssoc_inv_app /-- Composing a functor with both functors of an equivalence yields a naturally isomorphic functor. -/ @@ -359,22 +347,20 @@ def invFunIdAssoc (e : C ≌ D) (F : D ⥤ E) : e.inverse ⋙ e.functor ⋙ F #align category_theory.equivalence.inv_fun_id_assoc CategoryTheory.Equivalence.invFunIdAssoc @[simp] -theorem inv_fun_id_assoc_hom_app (e : C ≌ D) (F : D ⥤ E) (X : D) : +theorem invFunIdAssoc_hom_app (e : C ≌ D) (F : D ⥤ E) (X : D) : (invFunIdAssoc e F).hom.app X = F.map (e.counit.app X) := by dsimp [invFunIdAssoc] aesop_cat -#align category_theory.equivalence.inv_fun_id_assoc_hom_app - CategoryTheory.Equivalence.inv_fun_id_assoc_hom_app +#align category_theory.equivalence.inv_fun_id_assoc_hom_app CategoryTheory.Equivalence.invFunIdAssoc_hom_app @[simp] -theorem inv_fun_id_assoc_inv_app (e : C ≌ D) (F : D ⥤ E) (X : D) : +theorem invFunIdAssoc_inv_app (e : C ≌ D) (F : D ⥤ E) (X : D) : (invFunIdAssoc e F).inv.app X = F.map (e.counitInv.app X) := by dsimp [invFunIdAssoc] aesop_cat -#align category_theory.equivalence.inv_fun_id_assoc_inv_app - CategoryTheory.Equivalence.inv_fun_id_assoc_inv_app +#align category_theory.equivalence.inv_fun_id_assoc_inv_app CategoryTheory.Equivalence.invFunIdAssoc_inv_app /-- If `C` is equivalent to `D`, then `C ⥤ E` is equivalent to `D ⥤ E`. -/ @[simps! functor inverse unitIso counitIso] @@ -400,9 +386,9 @@ section CancellationLemmas variable (e : C ≌ D) -/- We need special forms of `cancel_nat_iso_hom_right(_assoc)` and -`cancel_nat_iso_inv_right(_assoc)` for units and counits, because neither `simp` or `rw` will apply -those lemmas in this setting without providing `e.unit_iso` (or similar) as an explicit argument. +/- We need special forms of `cancel_natIso_hom_right(_assoc)` and +`cancel_natIso_inv_right(_assoc)` for units and counits, because neither `simp` or `rw` will apply +those lemmas in this setting without providing `e.unitIso` (or similar) as an explicit argument. We also provide the lemmas for length four compositions, since they're occasionally useful. (e.g. in proving that equivalences take monos to monos) -/ @[simp] @@ -411,52 +397,45 @@ theorem cancel_unit_right {X Y : C} (f f' : X ⟶ Y) : #align category_theory.equivalence.cancel_unit_right CategoryTheory.Equivalence.cancel_unit_right @[simp] -theorem cancel_unit_inv_right {X Y : C} (f f' : X ⟶ e.inverse.obj (e.functor.obj Y)) : +theorem cancel_unitInv_right {X Y : C} (f f' : X ⟶ e.inverse.obj (e.functor.obj Y)) : f ≫ e.unitInv.app Y = f' ≫ e.unitInv.app Y ↔ f = f' := by simp only [cancel_mono] -#align - category_theory.equivalence.cancel_unit_inv_right CategoryTheory.Equivalence.cancel_unit_inv_right +#align category_theory.equivalence.cancel_unit_inv_right CategoryTheory.Equivalence.cancel_unitInv_right @[simp] theorem cancel_counit_right {X Y : D} (f f' : X ⟶ e.functor.obj (e.inverse.obj Y)) : f ≫ e.counit.app Y = f' ≫ e.counit.app Y ↔ f = f' := by simp only [cancel_mono] -#align - category_theory.equivalence.cancel_counit_right CategoryTheory.Equivalence.cancel_counit_right +#align category_theory.equivalence.cancel_counit_right CategoryTheory.Equivalence.cancel_counit_right @[simp] -theorem cancel_counit_inv_right {X Y : D} (f f' : X ⟶ Y) : +theorem cancel_counitInv_right {X Y : D} (f f' : X ⟶ Y) : f ≫ e.counitInv.app Y = f' ≫ e.counitInv.app Y ↔ f = f' := by simp only [cancel_mono] -#align category_theory.equivalence.cancel_counit_inv_right - CategoryTheory.Equivalence.cancel_counit_inv_right +#align category_theory.equivalence.cancel_counit_inv_right CategoryTheory.Equivalence.cancel_counitInv_right @[simp] theorem cancel_unit_right_assoc {W X X' Y : C} (f : W ⟶ X) (g : X ⟶ Y) (f' : W ⟶ X') (g' : X' ⟶ Y) : f ≫ g ≫ e.unit.app Y = f' ≫ g' ≫ e.unit.app Y ↔ f ≫ g = f' ≫ g' := by simp only [← Category.assoc, cancel_mono] -#align category_theory.equivalence.cancel_unit_right_assoc - CategoryTheory.Equivalence.cancel_unit_right_assoc +#align category_theory.equivalence.cancel_unit_right_assoc CategoryTheory.Equivalence.cancel_unit_right_assoc @[simp] -theorem cancel_counit_inv_right_assoc {W X X' Y : D} (f : W ⟶ X) (g : X ⟶ Y) (f' : W ⟶ X') +theorem cancel_counitInv_right_assoc {W X X' Y : D} (f : W ⟶ X) (g : X ⟶ Y) (f' : W ⟶ X') (g' : X' ⟶ Y) : f ≫ g ≫ e.counitInv.app Y = f' ≫ g' ≫ e.counitInv.app Y ↔ f ≫ g = f' ≫ g' := by simp only [← Category.assoc, cancel_mono] -#align category_theory.equivalence.cancel_counit_inv_right_assoc - CategoryTheory.Equivalence.cancel_counit_inv_right_assoc +#align category_theory.equivalence.cancel_counit_inv_right_assoc CategoryTheory.Equivalence.cancel_counitInv_right_assoc @[simp] theorem cancel_unit_right_assoc' {W X X' Y Y' Z : C} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z) (f' : W ⟶ X') (g' : X' ⟶ Y') (h' : Y' ⟶ Z) : f ≫ g ≫ h ≫ e.unit.app Z = f' ≫ g' ≫ h' ≫ e.unit.app Z ↔ f ≫ g ≫ h = f' ≫ g' ≫ h' := by simp only [← Category.assoc, cancel_mono] -#align category_theory.equivalence.cancel_unit_right_assoc' - CategoryTheory.Equivalence.cancel_unit_right_assoc' +#align category_theory.equivalence.cancel_unit_right_assoc' CategoryTheory.Equivalence.cancel_unit_right_assoc' @[simp] -theorem cancel_counit_inv_right_assoc' {W X X' Y Y' Z : D} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z) +theorem cancel_counitInv_right_assoc' {W X X' Y Y' Z : D} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z) (f' : W ⟶ X') (g' : X' ⟶ Y') (h' : Y' ⟶ Z) : f ≫ g ≫ h ≫ e.counitInv.app Z = f' ≫ g' ≫ h' ≫ e.counitInv.app Z ↔ f ≫ g ≫ h = f' ≫ g' ≫ h' := by simp only [← Category.assoc, cancel_mono] -#align category_theory.equivalence.cancel_counit_inv_right_assoc' - CategoryTheory.Equivalence.cancel_counit_inv_right_assoc' +#align category_theory.equivalence.cancel_counit_inv_right_assoc' CategoryTheory.Equivalence.cancel_counitInv_right_assoc' end CancellationLemmas @@ -528,8 +507,7 @@ instance ofEquivalence (F : C ≌ D) : IsEquivalence F.functor := instance ofEquivalenceInverse (F : C ≌ D) : IsEquivalence F.inverse := IsEquivalence.ofEquivalence F.symm -#align category_theory.is_equivalence.of_equivalence_inverse - CategoryTheory.IsEquivalence.ofEquivalenceInverse +#align category_theory.is_equivalence.of_equivalence_inverse CategoryTheory.IsEquivalence.ofEquivalenceInverse open Equivalence @@ -563,26 +541,26 @@ instance isEquivalenceInv (F : C ⥤ D) [IsEquivalence F] : IsEquivalence F.inv #align category_theory.functor.is_equivalence_inv CategoryTheory.Functor.isEquivalenceInv @[simp] -theorem as_equivalence_functor (F : C ⥤ D) [IsEquivalence F] : F.asEquivalence.functor = F := +theorem asEquivalence_functor (F : C ⥤ D) [IsEquivalence F] : F.asEquivalence.functor = F := rfl -#align category_theory.functor.as_equivalence_functor CategoryTheory.Functor.as_equivalence_functor +#align category_theory.functor.as_equivalence_functor CategoryTheory.Functor.asEquivalence_functor @[simp] -theorem as_equivalence_inverse (F : C ⥤ D) [IsEquivalence F] : F.asEquivalence.inverse = inv F := +theorem asEquivalence_inverse (F : C ⥤ D) [IsEquivalence F] : F.asEquivalence.inverse = inv F := rfl -#align category_theory.functor.as_equivalence_inverse CategoryTheory.Functor.as_equivalence_inverse +#align category_theory.functor.as_equivalence_inverse CategoryTheory.Functor.asEquivalence_inverse @[simp] -theorem as_equivalence_unit {F : C ⥤ D} [IsEquivalence F] : +theorem asEquivalence_unit {F : C ⥤ D} [IsEquivalence F] : F.asEquivalence.unitIso = IsEquivalence.unitIso := rfl -#align category_theory.functor.as_equivalence_unit CategoryTheory.Functor.as_equivalence_unit +#align category_theory.functor.as_equivalence_unit CategoryTheory.Functor.asEquivalence_unit @[simp] -theorem as_equivalence_counit {F : C ⥤ D} [IsEquivalence F] : +theorem asEquivalence_counit {F : C ⥤ D} [IsEquivalence F] : F.asEquivalence.counitIso = IsEquivalence.counitIso := rfl -#align category_theory.functor.as_equivalence_counit CategoryTheory.Functor.as_equivalence_counit +#align category_theory.functor.as_equivalence_counit CategoryTheory.Functor.asEquivalence_counit @[simp] theorem inv_inv (F : C ⥤ D) [IsEquivalence F] : inv (inv F) = F := @@ -611,20 +589,18 @@ theorem inverse_inv (E : C ≌ D) : E.inverse.inv = E.functor := #align category_theory.equivalence.inverse_inv CategoryTheory.Equivalence.inverse_inv @[simp] -theorem functor_as_equivalence (E : C ≌ D) : E.functor.asEquivalence = E := +theorem functor_asEquivalence (E : C ≌ D) : E.functor.asEquivalence = E := by cases E congr -#align category_theory.equivalence.functor_as_equivalence - CategoryTheory.Equivalence.functor_as_equivalence +#align category_theory.equivalence.functor_as_equivalence CategoryTheory.Equivalence.functor_asEquivalence @[simp] -theorem inverse_as_equivalence (E : C ≌ D) : E.inverse.asEquivalence = E.symm := +theorem inverse_asEquivalence (E : C ≌ D) : E.inverse.asEquivalence = E.symm := by cases E congr -#align category_theory.equivalence.inverse_as_equivalence - CategoryTheory.Equivalence.inverse_as_equivalence +#align category_theory.equivalence.inverse_as_equivalence CategoryTheory.Equivalence.inverse_asEquivalence end Equivalence @@ -666,25 +642,25 @@ def ofIso {F G : C ⥤ D} (e : F ≅ G) (hF : IsEquivalence F) : IsEquivalence G simp only [Functor.id_map, id_comp] #align category_theory.is_equivalence.of_iso CategoryTheory.IsEquivalence.ofIso -/-- Compatibility of `of_iso` with the composition of isomorphisms of functors -/ -theorem of_iso_trans {F G H : C ⥤ D} (e : F ≅ G) (e' : G ≅ H) (hF : IsEquivalence F) : +/-- Compatibility of `ofIso` with the composition of isomorphisms of functors -/ +theorem ofIso_trans {F G H : C ⥤ D} (e : F ≅ G) (e' : G ≅ H) (hF : IsEquivalence F) : ofIso e' (ofIso e hF) = ofIso (e ≪≫ e') hF := by dsimp [ofIso] congr 1 <;> ext X <;> dsimp [NatIso.hcomp] · simp only [id_comp, assoc, Functor.map_comp] · simp only [Functor.map_id, comp_id, id_comp, assoc] -#align category_theory.is_equivalence.of_iso_trans CategoryTheory.IsEquivalence.of_iso_trans +#align category_theory.is_equivalence.of_iso_trans CategoryTheory.IsEquivalence.ofIso_trans -/-- Compatibility of `of_iso` with identity isomorphisms of functors -/ -theorem of_iso_refl (F : C ⥤ D) (hF : IsEquivalence F) : ofIso (Iso.refl F) hF = hF := +/-- Compatibility of `ofIso` with identity isomorphisms of functors -/ +theorem ofIso_refl (F : C ⥤ D) (hF : IsEquivalence F) : ofIso (Iso.refl F) hF = hF := by rcases hF with ⟨Finv, Funit, Fcounit, Fcomp⟩ dsimp [ofIso] congr 1 <;> ext X <;> dsimp [NatIso.hcomp] · simp only [comp_id, map_id] · simp only [id_comp, map_id] -#align category_theory.is_equivalence.of_iso_refl CategoryTheory.IsEquivalence.of_iso_refl +#align category_theory.is_equivalence.of_iso_refl CategoryTheory.IsEquivalence.ofIso_refl /-- When `F` and `G` are two isomorphic functors, then `F` is an equivalence iff `G` is. -/ @[simps] @@ -692,8 +668,8 @@ def equivOfIso {F G : C ⥤ D} (e : F ≅ G) : IsEquivalence F ≃ IsEquivalence where toFun := ofIso e invFun := ofIso e.symm - left_inv hF := by rw [of_iso_trans, Iso.self_symm_id, of_iso_refl] - right_inv hF := by rw [of_iso_trans, Iso.symm_self_id, of_iso_refl] + left_inv hF := by rw [ofIso_trans, Iso.self_symm_id, ofIso_refl] + right_inv hF := by rw [ofIso_trans, Iso.symm_self_id, ofIso_refl] #align category_theory.is_equivalence.equiv_of_iso CategoryTheory.IsEquivalence.equivOfIso /-- If `G` and `F ⋙ G` are equivalence of categories, then `F` is also an equivalence. -/ @@ -721,22 +697,20 @@ namespace Equivalence See . -/ -theorem ess_surj_of_equivalence (F : C ⥤ D) [IsEquivalence F] : EssSurj F := +theorem essSurj_of_equivalence (F : C ⥤ D) [IsEquivalence F] : EssSurj F := ⟨fun Y => ⟨F.inv.obj Y, ⟨F.asEquivalence.counitIso.app Y⟩⟩⟩ -#align category_theory.equivalence.ess_surj_of_equivalence - CategoryTheory.Equivalence.ess_surj_of_equivalence +#align category_theory.equivalence.ess_surj_of_equivalence CategoryTheory.Equivalence.essSurj_of_equivalence -- see Note [lower instance priority] /-- An equivalence is faithful. See . -/ -instance (priority := 100) faithful_of_equivalence (F : C ⥤ D) [IsEquivalence F] : Faithful F where +instance (priority := 100) faithfulOfEquivalence (F : C ⥤ D) [IsEquivalence F] : Faithful F where map_injective := @fun X Y f g h => by - have p : F.inv.map (F.map f) = F.inv.map (F.map g) := congrArg F.inv.map h + have p : F.inv.map (F.map f) = F.inv.map (F.map g) := congrArg F.inv.map h simpa only [cancel_epi, cancel_mono, IsEquivalence.inv_fun_map] using p -#align category_theory.equivalence.faithful_of_equivalence - CategoryTheory.Equivalence.faithful_of_equivalence +#align category_theory.equivalence.faithful_of_equivalence CategoryTheory.Equivalence.faithfulOfEquivalence -- see Note [lower instance priority] /-- An equivalence is full. @@ -745,8 +719,8 @@ See . -/ instance (priority := 100) fullOfEquivalence (F : C ⥤ D) [IsEquivalence F] : Full F where - preimage := @fun X Y f => F.asEquivalence.unit.app X ≫ F.inv.map f ≫ F.asEquivalence.unitInv.app Y - witness := @fun X Y f => + preimage {X Y} f := F.asEquivalence.unit.app X ≫ F.inv.map f ≫ F.asEquivalence.unitInv.app Y + witness {X Y} f := F.inv.map_injective <| by simpa only [IsEquivalence.inv_fun_map, assoc, Iso.inv_hom_id_app_assoc, Iso.inv_hom_id_app] using comp_id _ @@ -756,11 +730,10 @@ instance (priority := 100) fullOfEquivalence (F : C ⥤ D) [IsEquivalence F] : F private noncomputable def equivalenceInverse (F : C ⥤ D) [Full F] [Faithful F] [EssSurj F] : D ⥤ C where obj X := F.objPreimage X - map := @fun X Y f => F.preimage ((F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv) + map {X Y} f := F.preimage ((F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv) map_id X := by apply F.map_injective; aesop_cat - map_comp := @fun X Y Z f g => by apply F.map_injective; simp --- #align --- category_theory.equivalence.equivalence_inverse CategoryTheory.Equivalence.equivalenceInverse + map_comp {X Y Z} f g := by apply F.map_injective; simp +-- #align category_theory.equivalence.equivalence_inverse CategoryTheory.Equivalence.equivalenceInverse /- Porting note: this is a private def in mathlib -/ -- @@ -772,44 +745,37 @@ noncomputable def ofFullyFaithfullyEssSurj (F : C ⥤ D) [Full F] [Faithful F] [ IsEquivalence F := IsEquivalence.mk (equivalenceInverse F) (NatIso.ofComponents (fun X => (F.preimageIso <| F.objObjPreimageIso <| F.obj X).symm) - @fun X Y f => by + fun f => by apply F.map_injective aesop_cat) (NatIso.ofComponents F.objObjPreimageIso (by aesop_cat)) -#align category_theory.equivalence.of_fully_faithfully_ess_surj - CategoryTheory.Equivalence.ofFullyFaithfullyEssSurj +#align category_theory.equivalence.of_fully_faithfully_ess_surj CategoryTheory.Equivalence.ofFullyFaithfullyEssSurj @[simp] theorem functor_map_inj_iff (e : C ≌ D) {X Y : C} (f g : X ⟶ Y) : e.functor.map f = e.functor.map g ↔ f = g := ⟨fun h => e.functor.map_injective h, fun h => h ▸ rfl⟩ -#align - category_theory.equivalence.functor_map_inj_iff CategoryTheory.Equivalence.functor_map_inj_iff +#align category_theory.equivalence.functor_map_inj_iff CategoryTheory.Equivalence.functor_map_inj_iff @[simp] theorem inverse_map_inj_iff (e : C ≌ D) {X Y : D} (f g : X ⟶ Y) : e.inverse.map f = e.inverse.map g ↔ f = g := functor_map_inj_iff e.symm f g -#align - category_theory.equivalence.inverse_map_inj_iff CategoryTheory.Equivalence.inverse_map_inj_iff +#align category_theory.equivalence.inverse_map_inj_iff CategoryTheory.Equivalence.inverse_map_inj_iff -instance ess_surj_induced_functor {C' : Type _} (e : C' ≃ D) : EssSurj (inducedFunctor e) - where mem_essImage Y := - ⟨e.symm Y, by simp only [inducedFunctor_obj,Equiv.apply_symm_apply]; exact ⟨default⟩⟩ -#align category_theory.equivalence.ess_surj_induced_functor - CategoryTheory.Equivalence.ess_surj_induced_functor +instance essSurjInducedFunctor {C' : Type _} (e : C' ≃ D) : EssSurj (inducedFunctor e) where + mem_essImage Y := ⟨e.symm Y, by simpa using ⟨default⟩⟩ +#align category_theory.equivalence.ess_surj_induced_functor CategoryTheory.Equivalence.essSurjInducedFunctor noncomputable instance inducedFunctorOfEquiv {C' : Type _} (e : C' ≃ D) : IsEquivalence (inducedFunctor e) := Equivalence.ofFullyFaithfullyEssSurj _ -#align category_theory.equivalence.induced_functor_of_equiv - CategoryTheory.Equivalence.inducedFunctorOfEquiv +#align category_theory.equivalence.induced_functor_of_equiv CategoryTheory.Equivalence.inducedFunctorOfEquiv noncomputable instance fullyFaithfulToEssImage (F : C ⥤ D) [Full F] [Faithful F] : IsEquivalence F.toEssImage := ofFullyFaithfullyEssSurj F.toEssImage -#align category_theory.equivalence.fully_faithful_to_ess_image - CategoryTheory.Equivalence.fullyFaithfulToEssImage +#align category_theory.equivalence.fully_faithful_to_ess_image CategoryTheory.Equivalence.fullyFaithfulToEssImage end Equivalence diff --git a/Mathlib/CategoryTheory/Equivalence.lean.orig b/Mathlib/CategoryTheory/Equivalence.lean.orig deleted file mode 100644 index 5d3e6dc2db975..0000000000000 --- a/Mathlib/CategoryTheory/Equivalence.lean.orig +++ /dev/null @@ -1,813 +0,0 @@ -/- -Copyright (c) 2017 Scott Morrison. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Tim Baumann, Stephen Morgan, Scott Morrison, Floris van Doorn - -! This file was ported from Lean 3 source module category_theory.equivalence -! leanprover-community/mathlib commit 9aba7801eeecebb61f58a5763c2b6dd1b47dc6ef -! Please do not edit these lines, except to modify the commit id -! if you have ported upstream changes. --/ -import Mathlib.CategoryTheory.Functor.FullyFaithful -import Mathlib.CategoryTheory.FullSubcategory -import Mathlib.CategoryTheory.Whiskering -import Mathlib.CategoryTheory.EssentialImage -import Mathlib.Tactic.Slice -import Mathlib.Tactic.Relation.Rfl -import Mathlib.Tactic.Relation.Trans --- TODO: remove -set_option autoImplicit false -/-! -# Equivalence of categories - -An equivalence of categories `C` and `D` is a pair of functors `F : C ⥤ D` and `G : D ⥤ C` such -that `η : 𝟭 C ≅ F ⋙ G` and `ε : G ⋙ F ≅ 𝟭 D`. In many situations, equivalences are a better -notion of "sameness" of categories than the stricter isomorphims of categories. - -Recall that one way to express that two functors `F : C ⥤ D` and `G : D ⥤ C` are adjoint is using -two natural transformations `η : 𝟭 C ⟶ F ⋙ G` and `ε : G ⋙ F ⟶ 𝟭 D`, called the unit and the -counit, such that the compositions `F ⟶ FGF ⟶ F` and `G ⟶ GFG ⟶ G` are the identity. Unfortunately, -it is not the case that the natural isomorphisms `η` and `ε` in the definition of an equivalence -automatically give an adjunction. However, it is true that -* if one of the two compositions is the identity, then so is the other, and -* given an equivalence of categories, it is always possible to refine `η` in such a way that the - identities are satisfied. - -For this reason, in mathlib we define an equivalence to be a "half-adjoint equivalence", which is -a tuple `(F, G, η, ε)` as in the first paragraph such that the composite `F ⟶ FGF ⟶ F` is the -identity. By the remark above, this already implies that the tuple is an "adjoint equivalence", -i.e., that the composite `G ⟶ GFG ⟶ G` is also the identity. - -We also define essentially surjective functors and show that a functor is an equivalence if and only -if it is full, faithful and essentially surjective. - -## Main definitions - -* `Equivalence`: bundled (half-)adjoint equivalences of categories -* `IsEquivalence`: type class on a functor `F` containing the data of the inverse `G` as well as - the natural isomorphisms `η` and `ε`. -* `EssSurj`: type class on a functor `F` containing the data of the preimages and the isomorphisms - `F.obj (preimage d) ≅ d`. - -## Main results - -* `Equivalence.mk`: upgrade an equivalence to a (half-)adjoint equivalence -* `IsEquivalence.equiv_of_iso`: when `F` and `G` are isomorphic functors, `F` is an equivalence -iff `G` is. -* `Equivalence.of_fully_faithfully_essSurj`: a fully faithful essentially surjective functor is an - equivalence. - -## Notations - -We write `C ≌ D` (`\backcong`, not to be confused with `≅`/`\cong`) for a bundled equivalence. - --/ - -namespace CategoryTheory - -open CategoryTheory.Functor NatIso Category - --- declare the `v`'s first; see `CategoryTheory.Category` for an explanation -universe v₁ v₂ v₃ u₁ u₂ u₃ - -/-- We define an equivalence as a (half)-adjoint equivalence, a pair of functors with - a unit and counit which are natural isomorphisms and the triangle law `Fη ≫ εF = 1`, or in other - words the composite `F ⟶ FGF ⟶ F` is the identity. - - In `unit_inverse_comp`, we show that this is actually an adjoint equivalence, i.e., that the - composite `G ⟶ GFG ⟶ G` is also the identity. - - The triangle equation is written as a family of equalities between morphisms, it is more - complicated if we write it as an equality of natural transformations, because then we would have - to insert natural transformations like `F ⟶ F1`. - -See --/ -structure Equivalence (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category.{v₂} D] where mk' :: - functor : C ⥤ D - inverse : D ⥤ C - unitIso : 𝟭 C ≅ functor ⋙ inverse - counitIso : inverse ⋙ functor ≅ 𝟭 D - functor_unit_iso_comp' : ∀ X : C, functor.map (unitIso.hom.app X) ≫ counitIso.hom.app (functor.obj X) = 𝟙 (functor.obj X) := by aesop_cat -#align category_theory.equivalence CategoryTheory.Equivalence - -restate_axiom Equivalence.functor_unit_iso_comp' - --- mathport name: «expr ≌ » -infixr:10 " ≌ " => Equivalence - -variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D] - -namespace Equivalence - -/-- The unit of an equivalence of categories. -/ -abbrev unit (e : C ≌ D) : 𝟭 C ⟶ e.functor ⋙ e.inverse := - e.unitIso.hom -#align category_theory.equivalence.unit CategoryTheory.Equivalence.unit - -/-- The counit of an equivalence of categories. -/ -abbrev counit (e : C ≌ D) : e.inverse ⋙ e.functor ⟶ 𝟭 D := - e.counitIso.hom -#align category_theory.equivalence.counit CategoryTheory.Equivalence.counit - -/-- The inverse of the unit of an equivalence of categories. -/ -abbrev unitInv (e : C ≌ D) : e.functor ⋙ e.inverse ⟶ 𝟭 C := - e.unitIso.inv -#align category_theory.equivalence.unit_inv CategoryTheory.Equivalence.unitInv - -/-- The inverse of the counit of an equivalence of categories. -/ -abbrev counitInv (e : C ≌ D) : 𝟭 D ⟶ e.inverse ⋙ e.functor := - e.counitIso.inv -#align category_theory.equivalence.counit_inv CategoryTheory.Equivalence.counitInv - -/- While these abbreviations are convenient, they also cause some trouble, -preventing structure projections from unfolding. -/ -@[simp] -theorem equivalence_mk'_unit (functor inverse unit_iso counit_iso f) : - (⟨functor, inverse, unit_iso, counit_iso, f⟩ : C ≌ D).unit = unit_iso.hom := - rfl -#align - category_theory.equivalence.equivalence_mk'_unit CategoryTheory.Equivalence.equivalence_mk'_unit - -@[simp] -theorem equivalence_mk'_counit (functor inverse unit_iso counit_iso f) : - (⟨functor, inverse, unit_iso, counit_iso, f⟩ : C ≌ D).counit = counit_iso.hom := - rfl -#align - category_theory.equivalence.equivalence_mk'_counit CategoryTheory.Equivalence.equivalence_mk'_counit - -@[simp] -theorem equivalence_mk'_unitInv (functor inverse unit_iso counit_iso f) : - (⟨functor, inverse, unit_iso, counit_iso, f⟩ : C ≌ D).unitInv = unit_iso.inv := - rfl -#align - category_theory.equivalence.equivalence_mk'_unit_inv CategoryTheory.Equivalence.equivalence_mk'_unitInv - -@[simp] -theorem equivalence_mk'_counitInv (functor inverse unit_iso counit_iso f) : - (⟨functor, inverse, unit_iso, counit_iso, f⟩ : C ≌ D).counitInv = counit_iso.inv := - rfl -#align - category_theory.equivalence.equivalence_mk'_counit_inv CategoryTheory.Equivalence.equivalence_mk'_counitInv - -@[simp] -theorem functor_unit_comp (e : C ≌ D) (X : C) : - e.functor.map (e.unit.app X) ≫ e.counit.app (e.functor.obj X) = 𝟙 (e.functor.obj X) := - e.functor_unit_iso_comp X -#align category_theory.equivalence.functor_unit_comp CategoryTheory.Equivalence.functor_unit_comp - -@[simp] -theorem counitInv_functor_comp (e : C ≌ D) (X : C) : - e.counitInv.app (e.functor.obj X) ≫ e.functor.map (e.unitInv.app X) = 𝟙 (e.functor.obj X) := - by - erw [Iso.inv_eq_inv (e.functor.mapIso (e.unitIso.app X) ≪≫ e.counitIso.app (e.functor.obj X)) - (Iso.refl _)] - exact e.functor_unit_comp X -#align - category_theory.equivalence.counit_inv_functor_comp CategoryTheory.Equivalence.counitInv_functor_comp - -theorem counit_inv_app_functor (e : C ≌ D) (X : C) : - e.counitInv.app (e.functor.obj X) = e.functor.map (e.unit.app X) := - by - symm - erw [← Iso.comp_hom_eq_id (e.counitIso.app _), functor_unit_comp] - rfl -#align - category_theory.equivalence.counit_inv_app_functor CategoryTheory.Equivalence.counit_inv_app_functor - -theorem counit_app_functor (e : C ≌ D) (X : C) : - e.counit.app (e.functor.obj X) = e.functor.map (e.unitInv.app X) := - by - erw [← Iso.hom_comp_eq_id (e.functor.mapIso (e.unitIso.app X)), functor_unit_comp] - rfl -#align category_theory.equivalence.counit_app_functor CategoryTheory.Equivalence.counit_app_functor - -/-- The other triangle equality. The proof follows the following proof in Globular: - http://globular.science/1905.001 -/ -@[simp] -theorem unit_inverse_comp (e : C ≌ D) (Y : D) : - e.unit.app (e.inverse.obj Y) ≫ e.inverse.map (e.counit.app Y) = 𝟙 (e.inverse.obj Y) := - by - rw [← id_comp (e.inverse.map _), ← map_id e.inverse, ← counitInv_functor_comp, map_comp] - dsimp - rw [← Iso.hom_inv_id_assoc (e.unitIso.app _) (e.inverse.map (e.functor.map _)), app_hom, app_inv] - sliceLHS 2 3 => erw [e.unit.naturality] - sliceLHS 1 2 => erw [e.unit.naturality] - sliceLHS 4 4 => - rw [← Iso.hom_inv_id_assoc (e.inverse.mapIso (e.counitIso.app _)) (e.unitInv.app _)] - sliceLHS 3 4 => - erw [← map_comp e.inverse, e.counit.naturality] - erw [(e.counitIso.app _).hom_inv_id, map_id] - erw [id_comp] - sliceLHS 2 3 => erw [← map_comp e.inverse, e.counitIso.inv.naturality, map_comp] - sliceLHS 3 4 => erw [e.unitInv.naturality] - sliceLHS 4 5 => erw [← map_comp (e.functor ⋙ e.inverse), (e.unitIso.app _).hom_inv_id, map_id] - erw [id_comp] - sliceLHS 3 4 => erw [← e.unitInv.naturality] - sliceLHS 2 3 => - erw [← map_comp e.inverse, ← e.counitIso.inv.naturality, (e.counitIso.app _).hom_inv_id, - map_id] - erw [id_comp, (e.unitIso.app _).hom_inv_id]; rfl -#align category_theory.equivalence.unit_inverse_comp CategoryTheory.Equivalence.unit_inverse_comp - -@[simp] -theorem inverse_counit_inv_comp (e : C ≌ D) (Y : D) : - e.inverse.map (e.counitInv.app Y) ≫ e.unitInv.app (e.inverse.obj Y) = 𝟙 (e.inverse.obj Y) := - by - erw [Iso.inv_eq_inv (e.unitIso.app (e.inverse.obj Y) ≪≫ e.inverse.mapIso (e.counitIso.app Y)) - (Iso.refl _)] - exact e.unit_inverse_comp Y -#align - category_theory.equivalence.inverse_counit_inv_comp CategoryTheory.Equivalence.inverse_counit_inv_comp - -theorem unit_app_inverse (e : C ≌ D) (Y : D) : - e.unit.app (e.inverse.obj Y) = e.inverse.map (e.counitInv.app Y) := by - erw [← Iso.comp_hom_eq_id (e.inverse.mapIso (e.counitIso.app Y)), unit_inverse_comp] - dsimp -#align category_theory.equivalence.unit_app_inverse CategoryTheory.Equivalence.unit_app_inverse - -theorem unit_inv_app_inverse (e : C ≌ D) (Y : D) : - e.unitInv.app (e.inverse.obj Y) = e.inverse.map (e.counit.app Y) := by - symm - erw [← Iso.hom_comp_eq_id (e.unitIso.app _), unit_inverse_comp] - rfl -#align - category_theory.equivalence.unit_inv_app_inverse CategoryTheory.Equivalence.unit_inv_app_inverse - -@[simp] -theorem fun_inv_map (e : C ≌ D) (X Y : D) (f : X ⟶ Y) : - e.functor.map (e.inverse.map f) = e.counit.app X ≫ f ≫ e.counitInv.app Y := - (NatIso.naturality_2 e.counitIso f).symm -#align category_theory.equivalence.fun_inv_map CategoryTheory.Equivalence.fun_inv_map - -@[simp] -theorem inv_fun_map (e : C ≌ D) (X Y : C) (f : X ⟶ Y) : - e.inverse.map (e.functor.map f) = e.unitInv.app X ≫ f ≫ e.unit.app Y := - (NatIso.naturality_1 e.unitIso f).symm -#align category_theory.equivalence.inv_fun_map CategoryTheory.Equivalence.inv_fun_map - -section - --- In this section we convert an arbitrary equivalence to a half-adjoint equivalence. -variable {F : C ⥤ D} {G : D ⥤ C} (η : 𝟭 C ≅ F ⋙ G) (ε : G ⋙ F ≅ 𝟭 D) - -/-- If `η : 𝟭 C ≅ F ⋙ G` is part of a (not necessarily half-adjoint) equivalence, we can upgrade it -to a refined natural isomorphism `adjointify_η η : 𝟭 C ≅ F ⋙ G` which exhibits the properties -required for a half-adjoint equivalence. See `equivalence.mk`. -/ -def adjointifyη : 𝟭 C ≅ F ⋙ G := by - calc - 𝟭 C ≅ F ⋙ G := η - _ ≅ F ⋙ 𝟭 D ⋙ G := isoWhiskerLeft F (leftUnitor G).symm - _ ≅ F ⋙ (G ⋙ F) ⋙ G := isoWhiskerLeft F (isoWhiskerRight ε.symm G) - _ ≅ F ⋙ G ⋙ F ⋙ G := isoWhiskerLeft F (associator G F G) - _ ≅ (F ⋙ G) ⋙ F ⋙ G := (associator F G (F ⋙ G)).symm - _ ≅ 𝟭 C ⋙ F ⋙ G := isoWhiskerRight η.symm (F ⋙ G) - _ ≅ F ⋙ G := leftUnitor (F ⋙ G) - -#align category_theory.equivalence.adjointify_η CategoryTheory.Equivalence.adjointifyη - -theorem adjointify_η_ε (X : C) : - F.map ((adjointifyη η ε).hom.app X) ≫ ε.hom.app (F.obj X) = 𝟙 (F.obj X) := - by - dsimp [adjointifyη,Trans.trans] - simp - have := ε.hom.naturality (F.map (η.inv.app X)); dsimp at this; rw [this]; clear this - rw [← assoc _ _ (F.map _)] - have := ε.hom.naturality (ε.inv.app <| F.obj X); dsimp at this; rw [this]; clear this - have := (ε.app <| F.obj X).hom_inv_id; dsimp at this; rw [this]; clear this - rw [id_comp]; have := (F.mapIso <| η.app X).hom_inv_id; dsimp at this; rw [this] -#align category_theory.equivalence.adjointify_η_ε CategoryTheory.Equivalence.adjointify_η_ε - -end - -/-- Every equivalence of categories consisting of functors `F` and `G` such that `F ⋙ G` and - `G ⋙ F` are naturally isomorphic to identity functors can be transformed into a half-adjoint - equivalence without changing `F` or `G`. -/ -protected def mk (F : C ⥤ D) (G : D ⥤ C) (η : 𝟭 C ≅ F ⋙ G) (ε : G ⋙ F ≅ 𝟭 D) : C ≌ D := - ⟨F, G, adjointifyη η ε, ε, adjointify_η_ε η ε⟩ -#align category_theory.equivalence.mk CategoryTheory.Equivalence.mk - -/-- Equivalence of categories is reflexive. -/ -@[refl, simps] -def refl : C ≌ C := - ⟨𝟭 C, 𝟭 C, Iso.refl _, Iso.refl _, fun X => Category.id_comp _⟩ -#align category_theory.equivalence.refl CategoryTheory.Equivalence.refl - -instance : Inhabited (C ≌ C) := - ⟨refl⟩ - -/-- Equivalence of categories is symmetric. -/ -@[symm, simps] -def symm (e : C ≌ D) : D ≌ C := - ⟨e.inverse, e.functor, e.counitIso.symm, e.unitIso.symm, e.inverse_counit_inv_comp⟩ -#align category_theory.equivalence.symm CategoryTheory.Equivalence.symm - -variable {E : Type u₃} [Category.{v₃} E] - -/-- Equivalence of categories is transitive. -/ -@[trans, simps] -def trans (e : C ≌ D) (f : D ≌ E) : C ≌ E - where - functor := e.functor ⋙ f.functor - inverse := f.inverse ⋙ e.inverse - unitIso := by - refine' Iso.trans e.unitIso _ - exact isoWhiskerLeft e.functor (isoWhiskerRight f.unitIso e.inverse) - counitIso := by - refine' Iso.trans _ f.counitIso - exact isoWhiskerLeft f.inverse (isoWhiskerRight e.counitIso f.functor) - -- We wouldn't have needed to give this proof if we'd used `equivalence.mk`, - -- but we choose to avoid using that here, for the sake of good structure projection `simp` - -- lemmas. - functor_unit_iso_comp' X := by - dsimp - rw [← f.functor.map_comp_assoc, e.functor.map_comp, ← counit_inv_app_functor, fun_inv_map, - Iso.inv_hom_id_app_assoc, assoc, Iso.inv_hom_id_app, counit_app_functor, ← Functor.map_comp] - erw [comp_id, Iso.hom_inv_id_app, Functor.map_id] -#align category_theory.equivalence.trans CategoryTheory.Equivalence.trans - -/-- Composing a functor with both functors of an equivalence yields a naturally isomorphic -functor. -/ -def funInvIdAssoc (e : C ≌ D) (F : C ⥤ E) : e.functor ⋙ e.inverse ⋙ F ≅ F := - (Functor.associator _ _ _).symm ≪≫ isoWhiskerRight e.unitIso.symm F ≪≫ F.leftUnitor -#align category_theory.equivalence.fun_inv_id_assoc CategoryTheory.Equivalence.funInvIdAssoc - -@[simp] -theorem fun_inv_id_assoc_hom_app (e : C ≌ D) (F : C ⥤ E) (X : C) : - (funInvIdAssoc e F).hom.app X = F.map (e.unitInv.app X) := - by - dsimp [funInvIdAssoc] - aesop_cat -#align - category_theory.equivalence.fun_inv_id_assoc_hom_app CategoryTheory.Equivalence.fun_inv_id_assoc_hom_app - -@[simp] -theorem fun_inv_id_assoc_inv_app (e : C ≌ D) (F : C ⥤ E) (X : C) : - (funInvIdAssoc e F).inv.app X = F.map (e.unit.app X) := - by - dsimp [funInvIdAssoc] - aesop_cat -#align - category_theory.equivalence.fun_inv_id_assoc_inv_app CategoryTheory.Equivalence.fun_inv_id_assoc_inv_app - -/-- Composing a functor with both functors of an equivalence yields a naturally isomorphic -functor. -/ -def invFunIdAssoc (e : C ≌ D) (F : D ⥤ E) : e.inverse ⋙ e.functor ⋙ F ≅ F := - (Functor.associator _ _ _).symm ≪≫ isoWhiskerRight e.counitIso F ≪≫ F.leftUnitor -#align category_theory.equivalence.inv_fun_id_assoc CategoryTheory.Equivalence.invFunIdAssoc - -@[simp] -theorem inv_fun_id_assoc_hom_app (e : C ≌ D) (F : D ⥤ E) (X : D) : - (invFunIdAssoc e F).hom.app X = F.map (e.counit.app X) := - by - dsimp [invFunIdAssoc] - aesop_cat -#align - category_theory.equivalence.inv_fun_id_assoc_hom_app CategoryTheory.Equivalence.inv_fun_id_assoc_hom_app - -@[simp] -theorem inv_fun_id_assoc_inv_app (e : C ≌ D) (F : D ⥤ E) (X : D) : - (invFunIdAssoc e F).inv.app X = F.map (e.counitInv.app X) := - by - dsimp [invFunIdAssoc] - aesop_cat -#align - category_theory.equivalence.inv_fun_id_assoc_inv_app CategoryTheory.Equivalence.inv_fun_id_assoc_inv_app - -/-- If `C` is equivalent to `D`, then `C ⥤ E` is equivalent to `D ⥤ E`. -/ -@[simps! functor inverse unitIso counitIso] -def congrLeft (e : C ≌ D) : C ⥤ E ≌ D ⥤ E := - Equivalence.mk ((whiskeringLeft _ _ _).obj e.inverse) ((whiskeringLeft _ _ _).obj e.functor) - (NatIso.ofComponents (fun F => (e.funInvIdAssoc F).symm) (by aesop_cat)) - (NatIso.ofComponents (fun F => e.invFunIdAssoc F) (by aesop_cat)) -#align category_theory.equivalence.congr_left CategoryTheory.Equivalence.congrLeft - -/-- If `C` is equivalent to `D`, then `E ⥤ C` is equivalent to `E ⥤ D`. -/ -@[simps! functor inverse unitIso counitIso] -def congrRight (e : C ≌ D) : E ⥤ C ≌ E ⥤ D := - Equivalence.mk ((whiskeringRight _ _ _).obj e.functor) ((whiskeringRight _ _ _).obj e.inverse) - (NatIso.ofComponents - (fun F => F.rightUnitor.symm ≪≫ isoWhiskerLeft F e.unitIso ≪≫ Functor.associator _ _ _) - (by aesop_cat)) - (NatIso.ofComponents - (fun F => Functor.associator _ _ _ ≪≫ isoWhiskerLeft F e.counitIso ≪≫ F.rightUnitor) - (by aesop_cat)) -#align category_theory.equivalence.congr_right CategoryTheory.Equivalence.congrRight - -section CancellationLemmas - -variable (e : C ≌ D) - -/- We need special forms of `cancel_nat_iso_hom_right(_assoc)` and -`cancel_nat_iso_inv_right(_assoc)` for units and counits, because neither `simp` or `rw` will apply -those lemmas in this setting without providing `e.unit_iso` (or similar) as an explicit argument. -We also provide the lemmas for length four compositions, since they're occasionally useful. -(e.g. in proving that equivalences take monos to monos) -/ -@[simp] -theorem cancel_unit_right {X Y : C} (f f' : X ⟶ Y) : - f ≫ e.unit.app Y = f' ≫ e.unit.app Y ↔ f = f' := by simp only [cancel_mono] -#align category_theory.equivalence.cancel_unit_right CategoryTheory.Equivalence.cancel_unit_right - -@[simp] -theorem cancel_unit_inv_right {X Y : C} (f f' : X ⟶ e.inverse.obj (e.functor.obj Y)) : - f ≫ e.unitInv.app Y = f' ≫ e.unitInv.app Y ↔ f = f' := by simp only [cancel_mono] -#align - category_theory.equivalence.cancel_unit_inv_right CategoryTheory.Equivalence.cancel_unit_inv_right - -@[simp] -theorem cancel_counit_right {X Y : D} (f f' : X ⟶ e.functor.obj (e.inverse.obj Y)) : - f ≫ e.counit.app Y = f' ≫ e.counit.app Y ↔ f = f' := by simp only [cancel_mono] -#align - category_theory.equivalence.cancel_counit_right CategoryTheory.Equivalence.cancel_counit_right - -@[simp] -theorem cancel_counit_inv_right {X Y : D} (f f' : X ⟶ Y) : - f ≫ e.counitInv.app Y = f' ≫ e.counitInv.app Y ↔ f = f' := by simp only [cancel_mono] -#align - category_theory.equivalence.cancel_counit_inv_right CategoryTheory.Equivalence.cancel_counit_inv_right - -@[simp] -theorem cancel_unit_right_assoc {W X X' Y : C} (f : W ⟶ X) (g : X ⟶ Y) (f' : W ⟶ X') (g' : X' ⟶ Y) : - f ≫ g ≫ e.unit.app Y = f' ≫ g' ≫ e.unit.app Y ↔ f ≫ g = f' ≫ g' := by - simp only [← Category.assoc, cancel_mono] -#align - category_theory.equivalence.cancel_unit_right_assoc CategoryTheory.Equivalence.cancel_unit_right_assoc - -@[simp] -theorem cancel_counit_inv_right_assoc {W X X' Y : D} (f : W ⟶ X) (g : X ⟶ Y) (f' : W ⟶ X') - (g' : X' ⟶ Y) : f ≫ g ≫ e.counitInv.app Y = f' ≫ g' ≫ e.counitInv.app Y ↔ f ≫ g = f' ≫ g' := by - simp only [← Category.assoc, cancel_mono] -#align - category_theory.equivalence.cancel_counit_inv_right_assoc CategoryTheory.Equivalence.cancel_counit_inv_right_assoc - -@[simp] -theorem cancel_unit_right_assoc' {W X X' Y Y' Z : C} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z) - (f' : W ⟶ X') (g' : X' ⟶ Y') (h' : Y' ⟶ Z) : - f ≫ g ≫ h ≫ e.unit.app Z = f' ≫ g' ≫ h' ≫ e.unit.app Z ↔ f ≫ g ≫ h = f' ≫ g' ≫ h' := by - simp only [← Category.assoc, cancel_mono] -#align - category_theory.equivalence.cancel_unit_right_assoc' CategoryTheory.Equivalence.cancel_unit_right_assoc' - -@[simp] -theorem cancel_counit_inv_right_assoc' {W X X' Y Y' Z : D} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z) - (f' : W ⟶ X') (g' : X' ⟶ Y') (h' : Y' ⟶ Z) : - f ≫ g ≫ h ≫ e.counitInv.app Z = f' ≫ g' ≫ h' ≫ e.counitInv.app Z ↔ f ≫ g ≫ h = f' ≫ g' ≫ h' := - by simp only [← Category.assoc, cancel_mono] -#align - category_theory.equivalence.cancel_counit_inv_right_assoc' CategoryTheory.Equivalence.cancel_counit_inv_right_assoc' - -end CancellationLemmas - -section - --- There's of course a monoid structure on `C ≌ C`, --- but let's not encourage using it. --- The power structure is nevertheless useful. -/-- Natural number powers of an auto-equivalence. Use `(^)` instead. -/ -def powNat (e : C ≌ C) : ℕ → (C ≌ C) - | 0 => Equivalence.refl - | 1 => e - | n + 2 => e.trans (powNat e (n + 1)) -#align category_theory.equivalence.pow_nat CategoryTheory.Equivalence.powNat - -/-- Powers of an auto-equivalence. Use `(^)` instead. -/ -def pow (e : C ≌ C) : ℤ → (C ≌ C) - | Int.ofNat n => e.powNat n - | Int.negSucc n => e.symm.powNat (n + 1) -#align category_theory.equivalence.pow CategoryTheory.Equivalence.pow - -instance : Pow (C ≌ C) ℤ := - ⟨pow⟩ - -@[simp] -theorem pow_zero (e : C ≌ C) : e ^ (0 : ℤ) = Equivalence.refl := - rfl -#align category_theory.equivalence.pow_zero CategoryTheory.Equivalence.pow_zero - -@[simp] -theorem pow_one (e : C ≌ C) : e ^ (1 : ℤ) = e := - rfl -#align category_theory.equivalence.pow_one CategoryTheory.Equivalence.pow_one - -@[simp] -theorem pow_neg_one (e : C ≌ C) : e ^ (-1 : ℤ) = e.symm := - rfl -#align category_theory.equivalence.pow_neg_one CategoryTheory.Equivalence.pow_neg_one - --- TODO as necessary, add the natural isomorphisms `(e^a).trans e^b ≅ e^(a+b)`. --- At this point, we haven't even defined the category of equivalences. -end - -end Equivalence - -/-- A functor that is part of a (half) adjoint equivalence -/ -class IsEquivalence (F : C ⥤ D) where mk' :: - inverse : D ⥤ C - unitIso : 𝟭 C ≅ F ⋙ inverse - counitIso : inverse ⋙ F ≅ 𝟭 D - functor_unit_iso_comp' : - ∀ X : C, - F.map ((unitIso.hom : 𝟭 C ⟶ F ⋙ inverse).app X) ≫ counitIso.hom.app (F.obj X) = - 𝟙 (F.obj X) := by - aesop_cat -#align category_theory.is_equivalence CategoryTheory.IsEquivalence - -restate_axiom IsEquivalence.functor_unit_iso_comp' - -attribute [reassoc (attr := simp)] IsEquivalence.functor_unit_iso_comp - -namespace IsEquivalence - -instance ofEquivalence (F : C ≌ D) : IsEquivalence F.functor := - { F with } -#align category_theory.is_equivalence.of_equivalence CategoryTheory.IsEquivalence.ofEquivalence - -instance ofEquivalenceInverse (F : C ≌ D) : IsEquivalence F.inverse := - IsEquivalence.ofEquivalence F.symm -#align - category_theory.is_equivalence.of_equivalence_inverse CategoryTheory.IsEquivalence.ofEquivalenceInverse - -open Equivalence - -/-- To see that a functor is an equivalence, it suffices to provide an inverse functor `G` such that - `F ⋙ G` and `G ⋙ F` are naturally isomorphic to identity functors. -/ -protected def mk {F : C ⥤ D} (G : D ⥤ C) (η : 𝟭 C ≅ F ⋙ G) (ε : G ⋙ F ≅ 𝟭 D) : IsEquivalence F := - ⟨G, adjointifyη η ε, ε, adjointify_η_ε η ε⟩ -#align category_theory.is_equivalence.mk CategoryTheory.IsEquivalence.mk - -end IsEquivalence - -namespace Functor - -/-- Interpret a functor that is an equivalence as an equivalence. -/ -def asEquivalence (F : C ⥤ D) [IsEquivalence F] : C ≌ D := - ⟨F, IsEquivalence.inverse F, IsEquivalence.unitIso, IsEquivalence.counitIso, - IsEquivalence.functor_unit_iso_comp⟩ -#align category_theory.functor.as_equivalence CategoryTheory.Functor.asEquivalence - -instance isEquivalenceRefl : IsEquivalence (𝟭 C) := - IsEquivalence.ofEquivalence Equivalence.refl -#align category_theory.functor.is_equivalence_refl CategoryTheory.Functor.isEquivalenceRefl - -/-- The inverse functor of a functor that is an equivalence. -/ -def inv (F : C ⥤ D) [IsEquivalence F] : D ⥤ C := - IsEquivalence.inverse F -#align category_theory.functor.inv CategoryTheory.Functor.inv - -instance isEquivalenceInv (F : C ⥤ D) [IsEquivalence F] : IsEquivalence F.inv := - IsEquivalence.ofEquivalence F.asEquivalence.symm -#align category_theory.functor.is_equivalence_inv CategoryTheory.Functor.isEquivalenceInv - -@[simp] -theorem as_equivalence_functor (F : C ⥤ D) [IsEquivalence F] : F.asEquivalence.functor = F := - rfl -#align category_theory.functor.as_equivalence_functor CategoryTheory.Functor.as_equivalence_functor - -@[simp] -theorem as_equivalence_inverse (F : C ⥤ D) [IsEquivalence F] : F.asEquivalence.inverse = inv F := - rfl -#align category_theory.functor.as_equivalence_inverse CategoryTheory.Functor.as_equivalence_inverse - -@[simp] -theorem as_equivalence_unit {F : C ⥤ D} [IsEquivalence F] : - F.asEquivalence.unitIso = IsEquivalence.unitIso := - rfl -#align category_theory.functor.as_equivalence_unit CategoryTheory.Functor.as_equivalence_unit - -@[simp] -theorem as_equivalence_counit {F : C ⥤ D} [IsEquivalence F] : - F.asEquivalence.counitIso = IsEquivalence.counitIso := - rfl -#align category_theory.functor.as_equivalence_counit CategoryTheory.Functor.as_equivalence_counit - -@[simp] -theorem inv_inv (F : C ⥤ D) [IsEquivalence F] : inv (inv F) = F := - rfl -#align category_theory.functor.inv_inv CategoryTheory.Functor.inv_inv - -variable {E : Type u₃} [Category.{v₃} E] - -instance isEquivalenceTrans (F : C ⥤ D) (G : D ⥤ E) [IsEquivalence F] [IsEquivalence G] : - IsEquivalence (F ⋙ G) := - IsEquivalence.ofEquivalence (Equivalence.trans (asEquivalence F) (asEquivalence G)) -#align category_theory.functor.is_equivalence_trans CategoryTheory.Functor.isEquivalenceTrans - -end Functor - -namespace Equivalence - -@[simp] -theorem functor_inv (E : C ≌ D) : E.functor.inv = E.inverse := - rfl -#align category_theory.equivalence.functor_inv CategoryTheory.Equivalence.functor_inv - -@[simp] -theorem inverse_inv (E : C ≌ D) : E.inverse.inv = E.functor := - rfl -#align category_theory.equivalence.inverse_inv CategoryTheory.Equivalence.inverse_inv - -@[simp] -theorem functor_as_equivalence (E : C ≌ D) : E.functor.asEquivalence = E := - by - cases E - congr -#align - category_theory.equivalence.functor_as_equivalence CategoryTheory.Equivalence.functor_as_equivalence - -@[simp] -theorem inverse_as_equivalence (E : C ≌ D) : E.inverse.asEquivalence = E.symm := - by - cases E - congr -#align - category_theory.equivalence.inverse_as_equivalence CategoryTheory.Equivalence.inverse_as_equivalence - -end Equivalence - -namespace IsEquivalence - -@[simp] -theorem fun_inv_map (F : C ⥤ D) [IsEquivalence F] (X Y : D) (f : X ⟶ Y) : - F.map (F.inv.map f) = F.asEquivalence.counit.app X ≫ f ≫ F.asEquivalence.counitInv.app Y := - by - erw [NatIso.naturality_2] - rfl -#align category_theory.is_equivalence.fun_inv_map CategoryTheory.IsEquivalence.fun_inv_map - -@[simp] -theorem inv_fun_map (F : C ⥤ D) [IsEquivalence F] (X Y : C) (f : X ⟶ Y) : - F.inv.map (F.map f) = F.asEquivalence.unitInv.app X ≫ f ≫ F.asEquivalence.unit.app Y := - by - erw [NatIso.naturality_1] - rfl -#align category_theory.is_equivalence.inv_fun_map CategoryTheory.IsEquivalence.inv_fun_map - -/-- When a functor `F` is an equivalence of categories, and `G` is isomorphic to `F`, then -`G` is also an equivalence of categories. -/ -@[simps] -def ofIso {F G : C ⥤ D} (e : F ≅ G) (hF : IsEquivalence F) : IsEquivalence G - where - inverse := hF.inverse - unitIso := hF.unitIso ≪≫ NatIso.hcomp e (Iso.refl hF.inverse) - counitIso := NatIso.hcomp (Iso.refl hF.inverse) e.symm ≪≫ hF.counitIso - functor_unit_iso_comp' X := by - dsimp [NatIso.hcomp] - erw [id_comp, F.map_id, comp_id] - apply (cancel_epi (e.hom.app X)).mp - sliceLHS 1 2 => rw [← e.hom.naturality] - sliceLHS 2 3 => rw [← NatTrans.vcomp_app', e.hom_inv_id] - simp only [NatTrans.id_app, id_comp, comp_id, F.map_comp, assoc] - erw [hF.counitIso.hom.naturality] - sliceLHS 1 2 => rw [functor_unit_iso_comp] - simp only [Functor.id_map, id_comp] -#align category_theory.is_equivalence.of_iso CategoryTheory.IsEquivalence.ofIso - -/-- Compatibility of `of_iso` with the composition of isomorphisms of functors -/ -theorem of_iso_trans {F G H : C ⥤ D} (e : F ≅ G) (e' : G ≅ H) (hF : IsEquivalence F) : - ofIso e' (ofIso e hF) = ofIso (e ≪≫ e') hF := - by - dsimp [ofIso] - congr 1 <;> ext X <;> dsimp [NatIso.hcomp] - · simp only [id_comp, assoc, Functor.map_comp] - · simp only [Functor.map_id, comp_id, id_comp, assoc] -#align category_theory.is_equivalence.of_iso_trans CategoryTheory.IsEquivalence.of_iso_trans - -/-- Compatibility of `of_iso` with identity isomorphisms of functors -/ -theorem of_iso_refl (F : C ⥤ D) (hF : IsEquivalence F) : ofIso (Iso.refl F) hF = hF := - by - rcases hF with ⟨Finv, Funit, Fcounit, Fcomp⟩ - dsimp [ofIso] - congr 1 <;> ext X <;> dsimp [NatIso.hcomp] - · simp only [comp_id, map_id] - · simp only [id_comp, map_id] -#align category_theory.is_equivalence.of_iso_refl CategoryTheory.IsEquivalence.of_iso_refl - -/-- When `F` and `G` are two isomorphic functors, then `F` is an equivalence iff `G` is. -/ -@[simps] -def equivOfIso {F G : C ⥤ D} (e : F ≅ G) : IsEquivalence F ≃ IsEquivalence G - where - toFun := ofIso e - invFun := ofIso e.symm - left_inv hF := by rw [of_iso_trans, Iso.self_symm_id, of_iso_refl] - right_inv hF := by rw [of_iso_trans, Iso.symm_self_id, of_iso_refl] -#align category_theory.is_equivalence.equiv_of_iso CategoryTheory.IsEquivalence.equivOfIso - -/-- If `G` and `F ⋙ G` are equivalence of categories, then `F` is also an equivalence. -/ -@[simp] -def cancelCompRight {E : Type _} [Category E] (F : C ⥤ D) (G : D ⥤ E) (hG : IsEquivalence G) - (_ : IsEquivalence (F ⋙ G)) : IsEquivalence F := - ofIso (Functor.associator F G G.inv ≪≫ NatIso.hcomp (Iso.refl F) hG.unitIso.symm ≪≫ rightUnitor F) - (Functor.isEquivalenceTrans (F ⋙ G) G.inv) -#align category_theory.is_equivalence.cancel_comp_right CategoryTheory.IsEquivalence.cancelCompRight - -/-- If `F` and `F ⋙ G` are equivalence of categories, then `G` is also an equivalence. -/ -@[simp] -def cancelCompLeft {E : Type _} [Category E] (F : C ⥤ D) (G : D ⥤ E) (hF : IsEquivalence F) - (_ : IsEquivalence (F ⋙ G)) : IsEquivalence G := - ofIso - ((Functor.associator F.inv F G).symm ≪≫ NatIso.hcomp hF.counitIso (Iso.refl G) ≪≫ leftUnitor G) - (Functor.isEquivalenceTrans F.inv (F ⋙ G)) -#align category_theory.is_equivalence.cancel_comp_left CategoryTheory.IsEquivalence.cancelCompLeft - -end IsEquivalence - -namespace Equivalence - -/-- An equivalence is essentially surjective. - -See . --/ -theorem ess_surj_of_equivalence (F : C ⥤ D) [IsEquivalence F] : EssSurj F := - ⟨fun Y => ⟨F.inv.obj Y, ⟨F.asEquivalence.counitIso.app Y⟩⟩⟩ -#align - category_theory.equivalence.ess_surj_of_equivalence CategoryTheory.Equivalence.ess_surj_of_equivalence - --- see Note [lower instance priority] -/-- An equivalence is faithful. - -See . --/ -instance (priority := 100) faithful_of_equivalence (F : C ⥤ D) [IsEquivalence F] : Faithful F where - map_injective := @fun X Y f g h => by - have p : F.inv.map (F.map f) = F.inv.map (F.map g) := congrArg F.inv.map h - simpa only [cancel_epi, cancel_mono, IsEquivalence.inv_fun_map] using p -#align - category_theory.equivalence.faithful_of_equivalence CategoryTheory.Equivalence.faithful_of_equivalence - --- see Note [lower instance priority] -/-- An equivalence is full. - -See . --/ -instance (priority := 100) fullOfEquivalence (F : C ⥤ D) [IsEquivalence F] : Full F - where - preimage := @fun X Y f => F.asEquivalence.unit.app X ≫ F.inv.map f ≫ F.asEquivalence.unitInv.app Y - witness := @fun X Y f => - F.inv.map_injective <| by - simpa only [IsEquivalence.inv_fun_map, assoc, Iso.inv_hom_id_app_assoc, - Iso.inv_hom_id_app] using comp_id _ -#align category_theory.equivalence.full_of_equivalence CategoryTheory.Equivalence.fullOfEquivalence - -@[simps] -private noncomputable def equivalenceInverse (F : C ⥤ D) [Full F] [Faithful F] [EssSurj F] : D ⥤ C - where - obj X := F.objPreimage X - map := @fun X Y f => F.preimage ((F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv) - map_id X := by apply F.map_injective; aesop_cat - map_comp := @fun X Y Z f g => by apply F.map_injective; simp --- #align --- category_theory.equivalence.equivalence_inverse CategoryTheory.Equivalence.equivalenceInverse -/- Porting note: this is a private def in mathlib -/ - --- -/-- A functor which is full, faithful, and essentially surjective is an equivalence. - -See . --/ -noncomputable def ofFullyFaithfullyEssSurj (F : C ⥤ D) [Full F] [Faithful F] [EssSurj F] : - IsEquivalence F := - IsEquivalence.mk (equivalenceInverse F) - (NatIso.ofComponents (fun X => (F.preimageIso <| F.objObjPreimageIso <| F.obj X).symm) - @fun X Y f => by - apply F.map_injective - aesop_cat) - (NatIso.ofComponents F.objObjPreimageIso (by aesop_cat)) -#align - category_theory.equivalence.of_fully_faithfully_ess_surj CategoryTheory.Equivalence.ofFullyFaithfullyEssSurj - -@[simp] -theorem functor_map_inj_iff (e : C ≌ D) {X Y : C} (f g : X ⟶ Y) : - e.functor.map f = e.functor.map g ↔ f = g := - ⟨fun h => e.functor.map_injective h, fun h => h ▸ rfl⟩ -#align - category_theory.equivalence.functor_map_inj_iff CategoryTheory.Equivalence.functor_map_inj_iff - -@[simp] -theorem inverse_map_inj_iff (e : C ≌ D) {X Y : D} (f g : X ⟶ Y) : - e.inverse.map f = e.inverse.map g ↔ f = g := - functor_map_inj_iff e.symm f g -#align - category_theory.equivalence.inverse_map_inj_iff CategoryTheory.Equivalence.inverse_map_inj_iff - -instance ess_surj_induced_functor {C' : Type _} (e : C' ≃ D) : EssSurj (inducedFunctor e) - where mem_essImage Y := - ⟨e.symm Y, by simp only [inducedFunctor_obj,Equiv.apply_symm_apply]; exact ⟨default⟩⟩ -#align - category_theory.equivalence.ess_surj_induced_functor CategoryTheory.Equivalence.ess_surj_induced_functor - -noncomputable instance inducedFunctorOfEquiv {C' : Type _} (e : C' ≃ D) : - IsEquivalence (inducedFunctor e) := - Equivalence.ofFullyFaithfullyEssSurj _ -#align - category_theory.equivalence.induced_functor_of_equiv CategoryTheory.Equivalence.inducedFunctorOfEquiv - -noncomputable instance fullyFaithfulToEssImage (F : C ⥤ D) [Full F] [Faithful F] : - IsEquivalence F.toEssImage := - ofFullyFaithfullyEssSurj F.toEssImage -#align - category_theory.equivalence.fully_faithful_to_ess_image CategoryTheory.Equivalence.fullyFaithfulToEssImage - -end Equivalence - -end CategoryTheory - diff --git a/Mathlib/CategoryTheory/Functor/Currying.lean b/Mathlib/CategoryTheory/Functor/Currying.lean index 3eec08d7ff1f3..8c747e20a3e04 100644 --- a/Mathlib/CategoryTheory/Functor/Currying.lean +++ b/Mathlib/CategoryTheory/Functor/Currying.lean @@ -116,8 +116,8 @@ def uncurryObjFlip (F : C ⥤ D ⥤ E) : uncurry.obj F.flip ≅ Prod.swap _ _ variable (B C D E) -/-- A version of `category_theory.whiskering_right` for bifunctors, obtained by uncurrying, -applying `whiskering_right` and currying back +/-- A version of `CategoryTheory.whiskeringRight` for bifunctors, obtained by uncurrying, +applying `whiskeringRight` and currying back -/ @[simps!] def whiskeringRight₂ : (C ⥤ D ⥤ E) ⥤ (B ⥤ C) ⥤ (B ⥤ D) ⥤ B ⥤ E := diff --git a/Mathlib/CategoryTheory/Groupoid.lean b/Mathlib/CategoryTheory/Groupoid.lean index 8ebf75d278f76..02333aed46bec 100644 --- a/Mathlib/CategoryTheory/Groupoid.lean +++ b/Mathlib/CategoryTheory/Groupoid.lean @@ -17,7 +17,7 @@ import Mathlib.Combinatorics.Quiver.ConnectedComponent /-! # Groupoids -We define `groupoid` as a typeclass extending `category`, +We define `Groupoid` as a typeclass extending `category`, asserting that all morphisms have inverses. The instance `IsIso.ofGroupoid (f : X ⟶ Y) : IsIso f` means that you can then write @@ -40,7 +40,7 @@ namespace CategoryTheory universe v v₂ u u₂ -- morphism levels before object levels. See note [CategoryTheory universes]. -/-- A `groupoid` is a category such that all morphisms are isomorphisms. -/ +/-- A `Groupoid` is a category such that all morphisms are isomorphisms. -/ class Groupoid (obj : Type u) extends Category.{v} obj : Type max u (v + 1) where /-- The inverse morphism -/ inv : ∀ {X Y : obj}, (X ⟶ Y) → (Y ⟶ X) @@ -78,7 +78,7 @@ theorem Groupoid.inv_eq_inv (f : X ⟶ Y) : Groupoid.inv f = CategoryTheory.inv IsIso.eq_inv_of_hom_inv_id <| Groupoid.comp_inv f #align category_theory.groupoid.inv_eq_inv CategoryTheory.Groupoid.inv_eq_inv -/-- `groupoid.inv` is involutive. -/ +/-- `Groupoid.inv` is involutive. -/ @[simps] def Groupoid.invEquiv : (X ⟶ Y) ≃ (Y ⟶ X) := ⟨Groupoid.inv, Groupoid.inv, fun f => by simp, fun f => by simp⟩ diff --git a/Mathlib/CategoryTheory/Iso.lean b/Mathlib/CategoryTheory/Iso.lean index 3c4a7a7de8990..acc0ac8f88af6 100644 --- a/Mathlib/CategoryTheory/Iso.lean +++ b/Mathlib/CategoryTheory/Iso.lean @@ -142,7 +142,7 @@ def refl (X : C) : X ≅ X where instance : Inhabited (X ≅ X) := ⟨Iso.refl X⟩ -theorem nonempty_iso_refl (X : C) : Nonempty (X ≅ X) := ⟨default⟩ +theorem nonempty_iso_refl (X : C) : Nonempty (X ≅ X) := ⟨default⟩ @[simp] theorem refl_symm (X : C) : (Iso.refl X).symm = Iso.refl X := rfl @@ -159,8 +159,9 @@ def trans (α : X ≅ Y) (β : Y ≅ Z) : X ≅ Z where #align category_theory.iso.trans_hom CategoryTheory.Iso.trans_hom #align category_theory.iso.trans_inv CategoryTheory.Iso.trans_inv -instance : Trans (· ≅ ·) (· ≅ ·) ((·:C) ≅ ·) where - trans := trans +@[simps] +instance : Trans (α := C) (· ≅ ·) (· ≅ ·) (· ≅ ·) where + trans := trans /-- Notation for composition of isomorphisms. -/ infixr:80 " ≪≫ " => Iso.trans -- type as `\ll \gg`. diff --git a/Mathlib/CategoryTheory/Limits/Cones.lean b/Mathlib/CategoryTheory/Limits/Cones.lean index abf5a7c42648a..158e8eb08eb8a 100644 --- a/Mathlib/CategoryTheory/Limits/Cones.lean +++ b/Mathlib/CategoryTheory/Limits/Cones.lean @@ -19,13 +19,13 @@ import Mathlib.CategoryTheory.Functor.ReflectsIso We define `Cone F`, a cone over a functor `F`, and `F.cones : Cᵒᵖ ⥤ Type`, the functor associating to `X` the cones over `F` with cone point `X`. -A cone `c` is defined by specifying its cone point `c.X` and a natural transformation `c.π` -from the constant `c.X` valued functor to `F`. +A cone `c` is defined by specifying its cone point `c.pt` and a natural transformation `c.π` +from the constant `c.pt` valued functor to `F`. We provide `c.w f : c.π.app j ≫ F.map f = c.π.app j'` for any `f : j ⟶ j'` as a wrapper for `c.π.naturality f` avoiding unneeded identity morphisms. -We define `c.extend f`, where `c : cone F` and `f : Y ⟶ c.X` for some other `Y`, +We define `c.extend f`, where `c : cone F` and `f : Y ⟶ c.pt` for some other `Y`, which replaces the cone point by `Y` and inserts `f` into each of the components of the cone. Similarly we have `c.whisker F` producing a `Cone (E ⋙ F)` @@ -115,20 +115,20 @@ namespace Limits section /-- A `c : Cone F` is: -* an object `c.X` and -* a natural transformation `c.π : c.X ⟶ F` from the constant `c.X` functor to `F`. +* an object `c.pt` and +* a natural transformation `c.π : c.pt ⟶ F` from the constant `c.pt` functor to `F`. `Cone F` is equivalent, via `cone.equiv` below, to `Σ X, F.cones.obj X`. -/ structure Cone (F : J ⥤ C) where /-- An object of `C` -/ - X : C + pt : C /-- A natural transformation from the constant functor at `X` to `F` -/ - π : (const J).obj X ⟶ F + π : (const J).obj pt ⟶ F #align category_theory.limits.cone CategoryTheory.Limits.Cone instance inhabitedCone (F : Discrete PUnit ⥤ C) : Inhabited (Cone F) := - ⟨{ X := F.obj ⟨⟨⟩⟩ + ⟨{ pt := F.obj ⟨⟨⟩⟩ π := { app := fun ⟨⟨⟩⟩ => 𝟙 _ naturality := by intro X Y f @@ -147,20 +147,20 @@ theorem Cone.w {F : J ⥤ C} (c : Cone F) {j j' : J} (f : j ⟶ j') : #align category_theory.limits.cone.w CategoryTheory.Limits.Cone.w /-- A `c : Cocone F` is -* an object `c.X` and -* a natural transformation `c.ι : F ⟶ c.X` from `F` to the constant `c.X` functor. +* an object `c.pt` and +* a natural transformation `c.ι : F ⟶ c.pt` from `F` to the constant `c.pt` functor. `Cocone F` is equivalent, via `cone.equiv` below, to `Σ X, F.cocones.obj X`. -/ structure Cocone (F : J ⥤ C) where /-- An object of `C` -/ - X : C + pt : C /-- A natural transformation from `F` to the constant functor at `X` -/ - ι : F ⟶ (const J).obj X + ι : F ⟶ (const J).obj pt #align category_theory.limits.cocone CategoryTheory.Limits.Cocone instance inhabitedCocone (F : Discrete PUnit ⥤ C) : Inhabited (Cocone F) := - ⟨{ X := F.obj ⟨⟨⟩⟩ + ⟨{ pt := F.obj ⟨⟨⟩⟩ ι := { app := fun ⟨⟨⟩⟩ => 𝟙 _ naturality := by intro X Y f @@ -188,9 +188,9 @@ namespace Cone @[simps!] def equiv (F : J ⥤ C) : Cone F ≅ ΣX, F.cones.obj X where - hom c := ⟨op c.X, c.π⟩ + hom c := ⟨op c.pt, c.π⟩ inv c := - { X := c.1.unop + { pt := c.1.unop π := c.2 } hom_inv_id := by funext X @@ -204,7 +204,7 @@ def equiv (F : J ⥤ C) : Cone F ≅ ΣX, F.cones.obj X /-- A map to the vertex of a cone naturally induces a cone by composition. -/ @[simps] -def extensions (c : Cone F) : yoneda.obj c.X ⋙ uliftFunctor.{u₁} ⟶ F.cones where +def extensions (c : Cone F) : yoneda.obj c.pt ⋙ uliftFunctor.{u₁} ⟶ F.cones where app X f := (const J).map f.down ≫ c.π naturality := by intros X Y f @@ -215,8 +215,8 @@ def extensions (c : Cone F) : yoneda.obj c.X ⋙ uliftFunctor.{u₁} ⟶ F.cones /-- A map to the vertex of a cone induces a cone by composition. -/ @[simps] -def extend (c : Cone F) {X : C} (f : X ⟶ c.X) : Cone F := - { X := X +def extend (c : Cone F) {X : C} (f : X ⟶ c.pt) : Cone F := + { pt := X π := c.extensions.app (op X) ⟨f⟩ } #align category_theory.limits.cone.extend CategoryTheory.Limits.Cone.extend @@ -224,7 +224,7 @@ def extend (c : Cone F) {X : C} (f : X ⟶ c.X) : Cone F := @[simps] def whisker (E : K ⥤ J) (c : Cone F) : Cone (E ⋙ F) where - X := c.X + pt := c.pt π := whiskerLeft E c.π #align category_theory.limits.cone.whisker CategoryTheory.Limits.Cone.whisker @@ -235,9 +235,9 @@ namespace Cocone /-- The isomorphism between a cocone on `F` and an element of the functor `F.cocones`. -/ def equiv (F : J ⥤ C) : Cocone F ≅ ΣX, F.cocones.obj X where - hom c := ⟨c.X, c.ι⟩ + hom c := ⟨c.pt, c.ι⟩ inv c := - { X := c.1 + { pt := c.1 ι := c.2 } hom_inv_id := by funext X @@ -251,7 +251,7 @@ def equiv (F : J ⥤ C) : Cocone F ≅ ΣX, F.cocones.obj X /-- A map from the vertex of a cocone naturally induces a cocone by composition. -/ @[simps] -def extensions (c : Cocone F) : coyoneda.obj (op c.X) ⋙ uliftFunctor.{u₁} ⟶ F.cocones where +def extensions (c : Cocone F) : coyoneda.obj (op c.pt) ⋙ uliftFunctor.{u₁} ⟶ F.cocones where app X f := c.ι ≫ (const J).map f.down naturality := fun {X} {Y} f => by dsimp [coyoneda,const] @@ -261,8 +261,8 @@ def extensions (c : Cocone F) : coyoneda.obj (op c.X) ⋙ uliftFunctor.{u₁} /-- A map from the vertex of a cocone induces a cocone by composition. -/ @[simps] -def extend (c : Cocone F) {Y : C} (f : c.X ⟶ Y) : Cocone F where - X := Y +def extend (c : Cocone F) {Y : C} (f : c.pt ⟶ Y) : Cocone F where + pt := Y ι := c.extensions.app Y ⟨f⟩ #align category_theory.limits.cocone.extend CategoryTheory.Limits.Cocone.extend @@ -272,7 +272,7 @@ version. @[simps] def whisker (E : K ⥤ J) (c : Cocone F) : Cocone (E ⋙ F) where - X := c.X + pt := c.pt ι := whiskerLeft E c.ι #align category_theory.limits.cocone.whisker CategoryTheory.Limits.Cocone.whisker @@ -283,7 +283,7 @@ commutes with the cone legs. -/ @[ext] structure ConeMorphism (A B : Cone F) where /-- A morphism between the two vertex objects of the cones -/ - Hom : A.X ⟶ B.X + Hom : A.pt ⟶ B.pt /-- The triangle consisting of the two natural tranformations and `Hom` commutes -/ w : ∀ j : J, Hom ≫ B.π.app j = A.π.app j := by aesop_cat #align category_theory.limits.cone_morphism CategoryTheory.Limits.ConeMorphism @@ -300,7 +300,7 @@ instance inhabitedConeMorphism (A : Cone F) : Inhabited (ConeMorphism A A) := instance Cone.category : Category (Cone F) where Hom A B := ConeMorphism A B comp f g := { Hom := f.Hom ≫ g.Hom } - id B := { Hom := 𝟙 B.X } + id B := { Hom := 𝟙 B.pt } #align category_theory.limits.cone.category CategoryTheory.Limits.Cone.category namespace Cones @@ -310,7 +310,7 @@ namespace Cones maps. -/ -- Porting note: `@[ext]` used to accept lemmas like this. Now we add an aesop rule @[aesop apply safe (rule_sets [CategoryTheory]), simps] -def ext {c c' : Cone F} (φ : c.X ≅ c'.X) (w : ∀ j, c.π.app j = φ.hom ≫ c'.π.app j) : c ≅ c' where +def ext {c c' : Cone F} (φ : c.pt ≅ c'.pt) (w : ∀ j, c.π.app j = φ.hom ≫ c'.π.app j) : c ≅ c' where hom := { Hom := φ.hom } inv := { Hom := φ.inv @@ -319,7 +319,7 @@ def ext {c c' : Cone F} (φ : c.X ≅ c'.X) (w : ∀ j, c.π.app j = φ.hom ≫ /-- Eta rule for cones. -/ @[simps!] -def eta (c : Cone F) : c ≅ ⟨c.X, c.π⟩ := +def eta (c : Cone F) : c ≅ ⟨c.pt, c.π⟩ := Cones.ext (Iso.refl _) (by aesop_cat) #align category_theory.limits.cones.eta CategoryTheory.Limits.Cones.eta @@ -338,7 +338,7 @@ Functorially postcompose a cone for `F` by a natural transformation `F ⟶ G` to def postcompose {G : J ⥤ C} (α : F ⟶ G) : Cone F ⥤ Cone G where obj c := - { X := c.X + { pt := c.pt π := c.π ≫ α } map f := { Hom := f.Hom } #align category_theory.limits.cones.postcompose CategoryTheory.Limits.Cones.postcompose @@ -413,7 +413,7 @@ variable (F) /-- Forget the cone structure and obtain just the cone point. -/ @[simps] def forget : Cone F ⥤ C where - obj t := t.X + obj t := t.pt map f := f.Hom #align category_theory.limits.cones.forget CategoryTheory.Limits.Cones.forget @@ -423,7 +423,7 @@ variable (G : C ⥤ D) @[simps] def functoriality : Cone F ⥤ Cone (F ⋙ G) where obj A := - { X := G.obj A.X + { pt := G.obj A.pt π := { app := fun j => G.map (A.π.app j) naturality := by intros; erw [← G.map_comp]; aesop_cat } } @@ -483,7 +483,7 @@ which commutes with the cocone legs. -/ @[ext] structure CoconeMorphism (A B : Cocone F) where /-- A morphism between the (co)vertex objects in `C` -/ - Hom : A.X ⟶ B.X + Hom : A.pt ⟶ B.pt /-- The triangle made from the two natural transformations and `Hom` commutes -/ w : ∀ j : J, A.ι.app j ≫ Hom = B.ι.app j := by aesop_cat #align category_theory.limits.cocone_morphism CategoryTheory.Limits.CoconeMorphism @@ -499,7 +499,7 @@ attribute [reassoc (attr := simp)] CoconeMorphism.w instance Cocone.category : Category (Cocone F) where Hom A B := CoconeMorphism A B comp f g := { Hom := f.Hom ≫ g.Hom } - id B := { Hom := 𝟙 B.X } + id B := { Hom := 𝟙 B.pt } #align category_theory.limits.cocone.category CategoryTheory.Limits.Cocone.category namespace Cocones @@ -509,7 +509,7 @@ namespace Cocones maps. -/ -- Porting note: `@[ext]` used to accept lemmas like this. Now we add an aesop rule @[aesop apply safe (rule_sets [CategoryTheory]), simps] -def ext {c c' : Cocone F} (φ : c.X ≅ c'.X) (w : ∀ j, c.ι.app j ≫ φ.hom = c'.ι.app j) +def ext {c c' : Cocone F} (φ : c.pt ≅ c'.pt) (w : ∀ j, c.ι.app j ≫ φ.hom = c'.ι.app j) : c ≅ c' where hom := { Hom := φ.hom } inv := @@ -519,7 +519,7 @@ def ext {c c' : Cocone F} (φ : c.X ≅ c'.X) (w : ∀ j, c.ι.app j ≫ φ.hom /-- Eta rule for cocones. -/ @[simps!] -def eta (c : Cocone F) : c ≅ ⟨c.X, c.ι⟩ := +def eta (c : Cocone F) : c ≅ ⟨c.pt, c.ι⟩ := Cocones.ext (Iso.refl _) (by aesop_cat) #align category_theory.limits.cocones.eta CategoryTheory.Limits.Cocones.eta @@ -537,7 +537,7 @@ for `G`. -/ @[simps] def precompose {G : J ⥤ C} (α : G ⟶ F) : Cocone F ⥤ Cocone G where obj c := - { X := c.X + { pt := c.pt ι := α ≫ c.ι } map f := { Hom := f.Hom } #align category_theory.limits.cocones.precompose CategoryTheory.Limits.Cocones.precompose @@ -613,7 +613,7 @@ variable (F) /-- Forget the cocone structure and obtain just the cocone point. -/ @[simps] def forget : Cocone F ⥤ C where - obj t := t.X + obj t := t.pt map f := f.Hom #align category_theory.limits.cocones.forget CategoryTheory.Limits.Cocones.forget @@ -623,7 +623,7 @@ variable (G : C ⥤ D) @[simps] def functoriality : Cocone F ⥤ Cocone (F ⋙ G) where obj A := - { X := G.obj A.X + { pt := G.obj A.pt ι := { app := fun j => G.map (A.ι.app j) naturality := by intros; erw [← G.map_comp]; aesop_cat } } @@ -701,7 +701,6 @@ variable {F : J ⥤ C} {G : J ⥤ C} (H : C ⥤ D) open CategoryTheory.Limits -/- Porting note: dot notation on the functor is broken for `mapCone` -/ /-- The image of a cone in C under a functor G : C ⥤ D is a cone in D. -/ @[simps!] def mapCone (c : Cone F) : Cone (F ⋙ H) := @@ -714,6 +713,7 @@ def mapCocone (c : Cocone F) : Cocone (F ⋙ H) := (Cocones.functoriality F H).obj c #align category_theory.functor.map_cocone CategoryTheory.Functor.mapCocone +/- Porting note: dot notation on the functor is broken for `mapCone` -/ /-- Given a cone morphism `c ⟶ c'`, construct a cone morphism on the mapped cones functorially. -/ def mapConeMorphism {c c' : Cone F} (f : c ⟶ c') : mapCone H c ⟶ mapCone _ c' := (Cones.functoriality F H).map f @@ -866,14 +866,14 @@ variable {F : J ⥤ C} /-- Change a `Cocone F` into a `Cone F.op`. -/ @[simps] def Cocone.op (c : Cocone F) : Cone F.op where - X := Opposite.op c.X + pt := Opposite.op c.pt π := NatTrans.op c.ι #align category_theory.limits.cocone.op CategoryTheory.Limits.Cocone.op /-- Change a `Cone F` into a `Cocone F.op`. -/ @[simps] def Cone.op (c : Cone F) : Cocone F.op where - X := Opposite.op c.X + pt := Opposite.op c.pt ι := NatTrans.op c.π #align category_theory.limits.cone.op CategoryTheory.Limits.Cone.op @@ -881,7 +881,7 @@ def Cone.op (c : Cone F) : Cocone F.op where @[simps] def Cocone.unop (c : Cocone F.op) : Cone F where - X := Opposite.unop c.X + pt := Opposite.unop c.pt π := NatTrans.removeOp c.ι #align category_theory.limits.cocone.unop CategoryTheory.Limits.Cocone.unop @@ -889,7 +889,7 @@ def Cocone.unop (c : Cocone F.op) : Cone F @[simps] def Cone.unop (c : Cone F.op) : Cocone F where - X := Opposite.unop c.X + pt := Opposite.unop c.pt ι := NatTrans.removeOp c.π #align category_theory.limits.cone.unop CategoryTheory.Limits.Cone.unop @@ -970,7 +970,7 @@ and replace with `@[simps]`-/ @[simps!] def coneOfCoconeLeftOp (c : Cocone F.leftOp) : Cone F where - X := op c.X + pt := op c.pt π := NatTrans.removeLeftOp c.ι #align category_theory.limits.cone_of_cocone_left_op CategoryTheory.Limits.coneOfCoconeLeftOp @@ -978,7 +978,7 @@ def coneOfCoconeLeftOp (c : Cocone F.leftOp) : Cone F @[simps!] def coconeLeftOpOfCone (c : Cone F) : Cocone F.leftOp where - X := unop c.X + pt := unop c.pt ι := NatTrans.leftOp c.π #align category_theory.limits.cocone_left_op_of_cone CategoryTheory.Limits.coconeLeftOpOfCone @@ -986,10 +986,10 @@ def coconeLeftOpOfCone (c : Cone F) : Cocone F.leftOp reduce the RHS using `expr.dsimp` and `expr.simp`, but for some reason the expression is not being simplified properly. -/ /-- Change a cone on `F.leftOp : Jᵒᵖ ⥤ C` to a cocone on `F : J ⥤ Cᵒᵖ`. -/ -@[simps X] +@[simps pt] def coconeOfConeLeftOp (c : Cone F.leftOp) : Cocone F where - X := op c.X + pt := op c.pt ι := NatTrans.removeLeftOp c.π #align category_theory.limits.cocone_of_cone_left_op CategoryTheory.Limits.coconeOfConeLeftOp @@ -1004,7 +1004,7 @@ theorem coconeOfConeLeftOp_ι_app (c : Cone F.leftOp) (j) : @[simps!] def coneLeftOpOfCocone (c : Cocone F) : Cone F.leftOp where - X := unop c.X + pt := unop c.pt π := NatTrans.leftOp c.ι #align category_theory.limits.cone_left_op_of_cocone CategoryTheory.Limits.coneLeftOpOfCocone @@ -1018,7 +1018,7 @@ variable {F : Jᵒᵖ ⥤ C} @[simps] def coneOfCoconeRightOp (c : Cocone F.rightOp) : Cone F where - X := unop c.X + pt := unop c.pt π := NatTrans.removeRightOp c.ι #align category_theory.limits.cone_of_cocone_right_op CategoryTheory.Limits.coneOfCoconeRightOp @@ -1026,7 +1026,7 @@ def coneOfCoconeRightOp (c : Cocone F.rightOp) : Cone F @[simps] def coconeRightOpOfCone (c : Cone F) : Cocone F.rightOp where - X := op c.X + pt := op c.pt ι := NatTrans.rightOp c.π #align category_theory.limits.cocone_right_op_of_cone CategoryTheory.Limits.coconeRightOpOfCone @@ -1034,7 +1034,7 @@ def coconeRightOpOfCone (c : Cone F) : Cocone F.rightOp @[simps] def coconeOfConeRightOp (c : Cone F.rightOp) : Cocone F where - X := unop c.X + pt := unop c.pt ι := NatTrans.removeRightOp c.π #align category_theory.limits.cocone_of_cone_right_op CategoryTheory.Limits.coconeOfConeRightOp @@ -1042,7 +1042,7 @@ def coconeOfConeRightOp (c : Cone F.rightOp) : Cocone F @[simps] def coneRightOpOfCocone (c : Cocone F) : Cone F.rightOp where - X := op c.X + pt := op c.pt π := NatTrans.rightOp c.ι #align category_theory.limits.cone_right_op_of_cocone CategoryTheory.Limits.coneRightOpOfCocone @@ -1056,7 +1056,7 @@ variable {F : Jᵒᵖ ⥤ Cᵒᵖ} @[simps] def coneOfCoconeUnop (c : Cocone F.unop) : Cone F where - X := op c.X + pt := op c.pt π := NatTrans.removeUnop c.ι #align category_theory.limits.cone_of_cocone_unop CategoryTheory.Limits.coneOfCoconeUnop @@ -1064,7 +1064,7 @@ def coneOfCoconeUnop (c : Cocone F.unop) : Cone F @[simps] def coconeUnopOfCone (c : Cone F) : Cocone F.unop where - X := unop c.X + pt := unop c.pt ι := NatTrans.unop c.π #align category_theory.limits.cocone_unop_of_cone CategoryTheory.Limits.coconeUnopOfCone @@ -1072,7 +1072,7 @@ def coconeUnopOfCone (c : Cone F) : Cocone F.unop @[simps] def coconeOfConeUnop (c : Cone F.unop) : Cocone F where - X := op c.X + pt := op c.pt ι := NatTrans.removeUnop c.π #align category_theory.limits.cocone_of_cone_unop CategoryTheory.Limits.coconeOfConeUnop @@ -1080,7 +1080,7 @@ def coconeOfConeUnop (c : Cone F.unop) : Cocone F @[simps] def coneUnopOfCocone (c : Cocone F) : Cone F.unop where - X := unop c.X + pt := unop c.pt π := NatTrans.unop c.ι #align category_theory.limits.cone_unop_of_cocone CategoryTheory.Limits.coneUnopOfCocone diff --git a/Mathlib/CategoryTheory/Limits/Shapes/StrongEpi.lean b/Mathlib/CategoryTheory/Limits/Shapes/StrongEpi.lean index a71d94949664b..ef32f913c8954 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/StrongEpi.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/StrongEpi.lean @@ -26,7 +26,7 @@ Besides the definition, we show that * if `f ≫ g` is a strong epimorphism, then so is `g`, * if `f` is both a strong epimorphism and a monomorphism, then it is an isomorphism -We also define classes `strong_mono_category` and `strong_epi_category` for categories in which +We also define classes `StrongMonoCategory` and `StrongEpiCategory` for categories in which every monomorphism or epimorphism is strong, and deduce that these categories are balanced. ## TODO @@ -59,11 +59,11 @@ class StrongEpi (f : P ⟶ Q) : Prop where theorem StrongEpi.mk' {f : P ⟶ Q} [Epi f] - (hf : ∀ (X Y : C) (z : X ⟶ Y) + (hf : ∀ (X Y : C) (z : X ⟶ Y) (_ : Mono z) (u : P ⟶ X) (v : Q ⟶ Y) (sq : CommSq u f z v), sq.HasLift) : StrongEpi f := { epi := inferInstance - llp := fun {X} {Y} z hz => ⟨fun {u} {v} sq => hf X Y z hz u v sq⟩ } + llp := fun {X Y} z hz => ⟨fun {u v} sq => hf X Y z hz u v sq⟩ } #align category_theory.strong_epi.mk' CategoryTheory.StrongEpi.mk' /-- A strong monomorphism `f` is a monomorphism which has the right lifting property @@ -76,10 +76,10 @@ class StrongMono (f : P ⟶ Q) : Prop where #align category_theory.strong_mono CategoryTheory.StrongMono theorem StrongMono.mk' {f : P ⟶ Q} [Mono f] - (hf : ∀ (X Y : C) (z : X ⟶ Y) (_ : Epi z) (u : X ⟶ P) - (v : Y ⟶ Q) (sq : CommSq u z f v), sq.HasLift) : StrongMono f where + (hf : ∀ (X Y : C) (z : X ⟶ Y) (_ : Epi z) (u : X ⟶ P) + (v : Y ⟶ Q) (sq : CommSq u z f v), sq.HasLift) : StrongMono f where mono := inferInstance - rlp := fun {X} {Y} z hz => ⟨fun {u} {v} sq => hf X Y z hz u v sq⟩ + rlp := fun {X Y} z hz => ⟨fun {u v} sq => hf X Y z hz u v sq⟩ #align category_theory.strong_mono.mk' CategoryTheory.StrongMono.mk' attribute [instance] StrongEpi.llp @@ -117,7 +117,7 @@ theorem strongMono_comp [StrongMono f] [StrongMono g] : StrongMono (f ≫ g) := /-- If `f ≫ g` is a strong epimorphism, then so is `g`. -/ theorem strongEpi_of_strongEpi [StrongEpi (f ≫ g)] : StrongEpi g := { epi := epi_of_epi f g - llp := fun {X} {Y} z _ => by + llp := fun {X Y} z _ => by constructor intro u v sq have h₀ : (f ≫ u) ≫ z = (f ≫ g) ≫ v := by simp only [Category.assoc, sq.w] @@ -130,27 +130,25 @@ theorem strongEpi_of_strongEpi [StrongEpi (f ≫ g)] : StrongEpi g := /-- If `f ≫ g` is a strong monomorphism, then so is `f`. -/ theorem strongMono_of_strongMono [StrongMono (f ≫ g)] : StrongMono f := { mono := mono_of_mono f g - rlp := fun {X} {Y} z => by + rlp := fun {X Y} z => by intros constructor intro u v sq - have h₀ : u ≫ f ≫ g = z ≫ v ≫ g := by + have h₀ : u ≫ f ≫ g = z ≫ v ≫ g := by rw [←Category.assoc, eq_whisker sq.w, Category.assoc] exact CommSq.HasLift.mk' ⟨(CommSq.mk h₀).lift, by simp, by simp [← cancel_epi z, sq.w]⟩ } #align category_theory.strong_mono_of_strong_mono CategoryTheory.strongMono_of_strongMono /-- An isomorphism is in particular a strong epimorphism. -/ -instance (priority := 100) strongEpi_of_isIso [IsIso f] : StrongEpi f - where +instance (priority := 100) strongEpi_of_isIso [IsIso f] : StrongEpi f where epi := by infer_instance - llp {X} {Y} z := HasLiftingProperty.of_left_iso _ _ + llp {X Y} z := HasLiftingProperty.of_left_iso _ _ #align category_theory.strong_epi_of_is_iso CategoryTheory.strongEpi_of_isIso /-- An isomorphism is in particular a strong monomorphism. -/ -instance (priority := 100) strongMono_of_isIso [IsIso f] : StrongMono f - where +instance (priority := 100) strongMono_of_isIso [IsIso f] : StrongMono f where mono := by infer_instance - rlp {X} {Y} z := HasLiftingProperty.of_right_iso _ _ + rlp {X Y} z := HasLiftingProperty.of_right_iso _ _ #align category_theory.strong_mono_of_is_iso CategoryTheory.strongMono_of_isIso theorem StrongEpi.of_arrow_iso {A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'} @@ -159,7 +157,7 @@ theorem StrongEpi.of_arrow_iso {A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'} rw [Arrow.iso_w' e] haveI := epi_comp f e.hom.right apply epi_comp - llp := fun {X} {Y} z => by + llp := fun {X Y} z => by intro apply HasLiftingProperty.of_arrow_iso_left e z } #align category_theory.strong_epi.of_arrow_iso CategoryTheory.StrongEpi.of_arrow_iso @@ -170,7 +168,7 @@ theorem StrongMono.of_arrow_iso {A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'} rw [Arrow.iso_w' e] haveI := mono_comp f e.hom.right apply mono_comp - rlp := fun {X} {Y} z => by + rlp := fun {X Y} z => by intro apply HasLiftingProperty.of_arrow_iso_right z e } #align category_theory.strong_mono.of_arrow_iso CategoryTheory.StrongMono.of_arrow_iso @@ -178,13 +176,13 @@ theorem StrongMono.of_arrow_iso {A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'} theorem StrongEpi.iff_of_arrow_iso {A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'} (e : Arrow.mk f ≅ Arrow.mk g) : StrongEpi f ↔ StrongEpi g := by constructor <;> intro - exacts[StrongEpi.of_arrow_iso e, StrongEpi.of_arrow_iso e.symm] + exacts [StrongEpi.of_arrow_iso e, StrongEpi.of_arrow_iso e.symm] #align category_theory.strong_epi.iff_of_arrow_iso CategoryTheory.StrongEpi.iff_of_arrow_iso theorem StrongMono.iff_of_arrow_iso {A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'} (e : Arrow.mk f ≅ Arrow.mk g) : StrongMono f ↔ StrongMono g := by constructor <;> intro - exacts[StrongMono.of_arrow_iso e, StrongMono.of_arrow_iso e.symm] + exacts [StrongMono.of_arrow_iso e, StrongMono.of_arrow_iso e.symm] #align category_theory.strong_mono.iff_of_arrow_iso CategoryTheory.StrongMono.iff_of_arrow_iso end @@ -208,12 +206,14 @@ class StrongEpiCategory : Prop where /-- A strong epi category is a category in which every epimorphism is strong. -/ strongEpi_of_epi : ∀ {X Y : C} (f : X ⟶ Y) [Epi f], StrongEpi f #align category_theory.strong_epi_category CategoryTheory.StrongEpiCategory +#align category_theory.strong_epi_category.strong_epi_of_epi CategoryTheory.StrongEpiCategory.strongEpi_of_epi /-- A strong mono category is a category in which every monomorphism is strong. -/ class StrongMonoCategory : Prop where /-- A strong mono category is a category in which every monomorphism is strong. -/ strongMono_of_mono : ∀ {X Y : C} (f : X ⟶ Y) [Mono f], StrongMono f #align category_theory.strong_mono_category CategoryTheory.StrongMonoCategory +#align category_theory.strong_mono_category.strong_mono_of_mono CategoryTheory.StrongMonoCategory.strongMono_of_mono end @@ -229,8 +229,8 @@ section attribute [local instance] strongEpi_of_epi -instance (priority := 100) balanced_of_strongEpiCategory [StrongEpiCategory C] : Balanced C - where isIso_of_mono_of_epi _ _ _ := isIso_of_mono_of_strongEpi _ +instance (priority := 100) balanced_of_strongEpiCategory [StrongEpiCategory C] : Balanced C where + isIso_of_mono_of_epi _ _ _ := isIso_of_mono_of_strongEpi _ #align category_theory.balanced_of_strong_epi_category CategoryTheory.balanced_of_strongEpiCategory end @@ -239,11 +239,10 @@ section attribute [local instance] strongMono_of_mono -instance (priority := 100) balanced_of_strongMonoCategory [StrongMonoCategory C] : Balanced C - where isIso_of_mono_of_epi _ _ _ := isIso_of_epi_of_strongMono _ +instance (priority := 100) balanced_of_strongMonoCategory [StrongMonoCategory C] : Balanced C where + isIso_of_mono_of_epi _ _ _ := isIso_of_epi_of_strongMono _ #align category_theory.balanced_of_strong_mono_category CategoryTheory.balanced_of_strongMonoCategory end end CategoryTheory -#lint diff --git a/Mathlib/CategoryTheory/Pi/Basic.lean b/Mathlib/CategoryTheory/Pi/Basic.lean index 19d9e10022e0c..dcb2885c5cd47 100644 --- a/Mathlib/CategoryTheory/Pi/Basic.lean +++ b/Mathlib/CategoryTheory/Pi/Basic.lean @@ -29,8 +29,7 @@ variable {I : Type w₀} {J : Type w₁} (C : I → Type u₁) [∀ i, Category. /-- `pi C` gives the cartesian product of an indexed family of categories. -/ -instance pi : Category.{max w₀ v₁} (∀ i, C i) - where +instance pi : Category.{max w₀ v₁} (∀ i, C i) where Hom X Y := ∀ i, X i ⟶ Y i id X i := 𝟙 (X i) comp f g i := f i ≫ g i @@ -71,18 +70,17 @@ section variable {J : Type w₁} -/- Porting note: add this because Lean cannot see directly through the `∘` for +/- Porting note: add this because Lean cannot see directly through the `∘` for `Function.comp` -/ -instance (f : J → I) : (j : J) → Category ((C ∘ f) j) := by +instance (f : J → I) : (j : J) → Category ((C ∘ f) j) := by dsimp - infer_instance + infer_instance /-- Pull back an `I`-indexed family of objects to an `J`-indexed family, along a function `J → I`. -/ @[simps] -def comap (h : J → I) : (∀ i, C i) ⥤ (∀ j, C (h j)) - where +def comap (h : J → I) : (∀ i, C i) ⥤ (∀ j, C (h j)) where obj f i := f (h i) map α i := α (h i) #align category_theory.pi.comap CategoryTheory.Pi.comap @@ -93,13 +91,12 @@ variable (I) pulling back a grading along the identity function, and the identity functor. -/ @[simps] -def comapId : comap C (id : I → I) ≅ 𝟭 (∀ i, C i) - where +def comapId : comap C (id : I → I) ≅ 𝟭 (∀ i, C i) where hom := { app := fun X => 𝟙 X, naturality := by simp only [comap]; aesop_cat} inv := { app := fun X => 𝟙 X } #align category_theory.pi.comap_id CategoryTheory.Pi.comapId -example (g : J → I) : (j : J) → Category (C (g j)) := by infer_instance +example (g : J → I) : (j : J) → Category (C (g j)) := by infer_instance variable {I} @@ -110,21 +107,20 @@ pulling back along two successive functions, and pulling back along their composition -/ @[simps!] -def comapComp (f : K → J) (g : J → I) : comap C g ⋙ comap (C ∘ g) f ≅ comap C (g ∘ f) - where - hom := { - app := fun X b => 𝟙 (X (g (f b))) +def comapComp (f : K → J) (g : J → I) : comap C g ⋙ comap (C ∘ g) f ≅ comap C (g ∘ f) where + hom := { + app := fun X b => 𝟙 (X (g (f b))) naturality := fun X Y f' => by simp only [comap,Function.comp]; funext; simp } - inv := { + inv := { app := fun X b => 𝟙 (X (g (f b))) naturality := fun X Y f' => by simp only [comap,Function.comp]; funext; simp } - hom_inv_id := by - simp only [comap] - ext Y + hom_inv_id := by + simp only [comap] + ext Y simp [CategoryStruct.comp,CategoryStruct.id] - inv_hom_id := by + inv_hom_id := by simp only [comap] ext X simp [CategoryStruct.comp,CategoryStruct.id] @@ -142,23 +138,7 @@ section variable {J : Type w₀} {D : J → Type u₁} [∀ j, Category.{v₁} (D j)] -/- Porting note: We have the following warning but it just looks -to me to be permutation of the universe labels - -warning: category_theory.pi.sum_elim_category -> -\ CategoryTheory.Pi.sumElimCategory is a dubious translation: -lean 3 declaration is forall {I : Type.{u1}} (C : I -> Type.{u3}) [_inst_1 : -forall (i : I), CategoryTheory.Category.{u2, u3} (C i)] {J : Type.{u1}} {D : J --> Type.{u3}} [_inst_2 : forall (j : J), CategoryTheory.Category.{u2, u3} (D -j)] (s : Sum.{u1, u1} I J), CategoryTheory.Category.{u2, u3} (Sum.elim.{u1, u1, -succ (succ u3)} I J Type.{u3} C D s) but is expected to have type forall {I : -Type.{u3}} (C : I -> Type.{u1}) [_inst_1 : forall (i : I), -CategoryTheory.Category.{u2, u1} (C i)] {J : Type.{u3}} {D : J -> Type.{u1}} -[_inst_2 : forall (j : J), CategoryTheory.Category.{u2, u1} (D j)] (s : -Sum.{u3, u3} I J), CategoryTheory.Category.{u2, u1} (Sum.elim.{u3, u3, succ -(succ u1)} I J Type.{u1} C D s) Case conversion may be inaccurate. Consider -using '#align category_theory.pi.sum_elim_category -CategoryTheory.Pi.sumElimCategoryₓ'. -/ +/- Porting note: maybe mixing up universes -/ instance sumElimCategory : ∀ s : Sum I J, Category.{v₁} (Sum.elim C D s) | Sum.inl i => by dsimp @@ -166,43 +146,42 @@ instance sumElimCategory : ∀ s : Sum I J, Category.{v₁} (Sum.elim C D s) | Sum.inr j => by dsimp infer_instance -#align category_theory.pi.sum_elim_category CategoryTheory.Pi.sumElimCategory +#align category_theory.pi.sum_elim_category CategoryTheory.Pi.sumElimCategoryₓ -/- Porting note: replaced `Sum.rec` with `match`'s per the error about -current state of code generation -/ +/- Porting note: replaced `Sum.rec` with `match`'s per the error about +current state of code generation -/ /-- The bifunctor combining an `I`-indexed family of objects with a `J`-indexed family of objects to obtain an `I ⊕ J`-indexed family of objects. -/ @[simps] -def sum : (∀ i, C i) ⥤ (∀ j, D j) ⥤ ∀ s : Sum I J, Sum.elim C D s - where +def sum : (∀ i, C i) ⥤ (∀ j, D j) ⥤ ∀ s : Sum I J, Sum.elim C D s where obj X := - { obj := fun Y s => - match s with - | .inl i => X i + { obj := fun Y s => + match s with + | .inl i => X i | .inr j => Y j - map := fun {Y} {Y'} f s => - match s with - | .inl i => 𝟙 (X i) + map := fun {Y} {Y'} f s => + match s with + | .inl i => 𝟙 (X i) | .inr j => f j - map_id := fun Y => by + map_id := fun Y => by dsimp simp only [CategoryStruct.id] - funext s - match s with - | .inl i => simp - | .inr j => simp + funext s + match s with + | .inl i => simp + | .inr j => simp map_comp := fun {Y₁} {Y₂} {Y₃} f g => by funext s; cases s; repeat {simp} } - map {X} {X'} f := - { app := fun Y s => - match s with - | .inl i => f i - | .inr j => 𝟙 (Y j) + map {X} {X'} f := + { app := fun Y s => + match s with + | .inl i => f i + | .inr j => 𝟙 (Y j) naturality := fun {Y} {Y'} g => by funext s; cases s; repeat {simp} } - map_id := fun X => by + map_id := fun X => by ext Y; dsimp; simp only [CategoryStruct.id]; funext s; cases s; repeat {simp} - map_comp := fun f g => by + map_comp := fun f g => by ext Y; dsimp; simp only [CategoryStruct.comp]; funext s; cases s; repeat {simp} #align category_theory.pi.sum CategoryTheory.Pi.sum @@ -249,8 +228,7 @@ variable {D : I → Type u₁} [∀ i, Category.{v₁} (D i)] {A : Type u₁} [C /-- Assemble an `I`-indexed family of functors into a functor between the pi types. -/ @[simps] -def pi (F : ∀ i, C i ⥤ D i) : (∀ i, C i) ⥤ ∀ i, D i - where +def pi (F : ∀ i, C i ⥤ D i) : (∀ i, C i) ⥤ ∀ i, D i where obj f i := (F i).obj (f i) map α i := (F i).map (α i) #align category_theory.functor.pi CategoryTheory.Functor.pi @@ -258,8 +236,7 @@ def pi (F : ∀ i, C i ⥤ D i) : (∀ i, C i) ⥤ ∀ i, D i /-- Similar to `pi`, but all functors come from the same category `A` -/ @[simps] -def pi' (f : ∀ i, A ⥤ C i) : A ⥤ ∀ i, C i - where +def pi' (f : ∀ i, A ⥤ C i) : A ⥤ ∀ i, C i where obj a i := (f i).obj a map h i := (f i).map h #align category_theory.functor.pi' CategoryTheory.Functor.pi' @@ -279,15 +256,15 @@ end EqToHom -- how `Functor.pi` commutes with `Pi.eval` and `Pi.comap`. @[simp] theorem pi'_eval (f : ∀ i, A ⥤ C i) (i : I) : pi' f ⋙ Pi.eval C i = f i := by - apply Functor.ext - intro _ _ _ - · simp - · intro _ - rfl + apply Functor.ext + intro _ _ _ + · simp + · intro _ + rfl #align category_theory.functor.pi'_eval CategoryTheory.Functor.pi'_eval /-- Two functors to a product category are equal iff they agree on every coordinate. -/ -theorem pi_ext (f f' : A ⥤ ∀ i, C i) (h : ∀ i, f ⋙ (Pi.eval C i) = f' ⋙ (Pi.eval C i)) +theorem pi_ext (f f' : A ⥤ ∀ i, C i) (h : ∀ i, f ⋙ (Pi.eval C i) = f' ⋙ (Pi.eval C i)) : f = f' := by apply Functor.ext; rotate_left · intro X @@ -296,7 +273,7 @@ theorem pi_ext (f f' : A ⥤ ∀ i, C i) (h : ∀ i, f ⋙ (Pi.eval C i) = f' have := congr_obj h X simpa · intro X Y g - dsimp + dsimp funext i specialize h i have := congr_hom h g @@ -316,8 +293,8 @@ variable {F G : ∀ i, C i ⥤ D i} /-- Assemble an `I`-indexed family of natural transformations into a single natural transformation. -/ @[simps!] -def pi (α : ∀ i, F i ⟶ G i) : Functor.pi F ⟶ Functor.pi G where - app f i := (α i).app (f i) +def pi (α : ∀ i, F i ⟶ G i) : Functor.pi F ⟶ Functor.pi G where + app f i := (α i).app (f i) naturality := fun X Y f => by simp [Functor.pi,CategoryStruct.comp] #align category_theory.nat_trans.pi CategoryTheory.NatTrans.pi diff --git a/Mathlib/CategoryTheory/Types.lean b/Mathlib/CategoryTheory/Types.lean index 63f7c04605930..aa3befe7b5b8c 100644 --- a/Mathlib/CategoryTheory/Types.lean +++ b/Mathlib/CategoryTheory/Types.lean @@ -88,8 +88,7 @@ abbrev asHom {α β : Type u} (f : α → β) : α ⟶ β := f #align category_theory.as_hom CategoryTheory.asHom --- If you don't mind some notation you can use fewer keystrokes: -/-- Type as \upr in VScode -/ +@[inherit_doc] scoped notation "↾" f:200 => CategoryTheory.asHom f section diff --git a/Mathlib/Tactic/Core.lean b/Mathlib/Tactic/Core.lean index 0aa9edc66aae9..d240a76eb102c 100644 --- a/Mathlib/Tactic/Core.lean +++ b/Mathlib/Tactic/Core.lean @@ -102,6 +102,39 @@ end Lean namespace Lean.Elab.Tactic +/-- Given a local context and an array of `FVarIds` assumed to be in that local context, remove all +implementation details. -/ +def filterOutImplementationDetails (lctx : LocalContext) (fvarIds : Array FVarId) : Array FVarId := + fvarIds.filter (fun fvar => ! (lctx.fvarIdToDecl.find! fvar).isImplementationDetail) + +/-- Elaborate syntax for an `FVarId` in the local context of the given goal. -/ +def getFVarIdAt (goal : MVarId) (id : Syntax) : TacticM FVarId := withRef id do + -- use apply-like elaboration to suppress insertion of implicit arguments + let e ← goal.withContext do + elabTermForApply id (mayPostpone := false) + match e with + | Expr.fvar fvarId => return fvarId + | _ => throwError "unexpected term '{e}'; expected single reference to variable" + +/-- Get the array of `FVarId`s in the local context of the given `goal`. + +If `ids` is specified, elaborate them in the local context of the given goal to obtain the array of +`FVarId`s. + +If `includeImplementationDetails` is `false` (the default), we filter out implementation details +(`implDecl`s and `auxDecl`s) from the resulting list of `FVarId`s. -/ +def getFVarIdsAt (goal : MVarId) (ids : Option (Array Syntax) := none) + (includeImplementationDetails : Bool := false) : TacticM (Array FVarId) := + goal.withContext do + let lctx := (← goal.getDecl).lctx + let fvarIds ← match ids with + | none => pure lctx.getFVarIds + | some ids => ids.mapM <| getFVarIdAt goal + if includeImplementationDetails then + return fvarIds + else + return filterOutImplementationDetails lctx fvarIds + /-- Run a tactic on all goals, and always succeeds. diff --git a/lean-toolchain b/lean-toolchain index 04ab6c3b09caa..d88e7bc6387b8 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2023-02-03 +leanprover/lean4:nightly-2023-02-23 diff --git a/test/slice.lean b/test/slice.lean index 818c82d6eb420..6d9d47c7aee08 100644 --- a/test/slice.lean +++ b/test/slice.lean @@ -3,16 +3,24 @@ import Mathlib.Tactic.Slice open CategoryTheory variable (C : Type) [Category C] (X Y Z W U : C) -variable (f₁ f₂ : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W) (l : W ⟶ U) +variable (f₁ f₂ : X ⟶ Y) (g g₁ g₂ : Y ⟶ Z) (h : Z ⟶ W) (l : W ⟶ U) -example (h₁ : f₁ = f₂) : f₁ ≫ g ≫ h ≫ l = ((f₂ ≫ g) ≫ h) ≫ l := by +example (hyp : f₁ ≫ g₁ = f₂ ≫ g₂) : f₁ ≫ g₁ ≫ h ≫ l = (f₂ ≫ g₂) ≫ (h ≫ l) := by + conv => + rhs + slice 2 3 + show f₁ ≫ g₁ ≫ h ≫ l = f₂ ≫ (g₂ ≫ h) ≫ l conv => lhs - slice 1 4 + slice 1 2 + rw [hyp] + show ((f₂ ≫ g₂) ≫ h) ≫ l = f₂ ≫ (g₂ ≫ h) ≫ l conv => lhs - slice 1 1 - rw [h₁] + slice 2 3 + +example (hyp : f₁ ≫ g₁ = f₂ ≫ g₂) : f₁ ≫ g₁ ≫ h ≫ l = (f₂ ≫ g₂) ≫ (h ≫ l) := by + slice_lhs 1 2 => { rw [hyp] }; slice_rhs 1 2 => skip example (h₁ : f₁ = f₂) : f₁ ≫ g ≫ h ≫ l = ((f₂ ≫ g) ≫ h) ≫ l := by slice_lhs 1 1 => rw [h₁]