feat(CategoryTheory): equivalences of categories preserve effective e…

…pis (#10421)

Mathlib/CategoryTheory/Equivalence.lean

@@ -149,13 +149,13 @@ theorem Equivalence_mk'_counitInv (functor inverse unit_iso counit_iso f) :
   rfl
 #align category_theory.equivalence.equivalence_mk'_counit_inv CategoryTheory.Equivalence.Equivalence_mk'_counitInv
 
-@[simp]
+@[reassoc (attr := 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_unitIso_comp X
 #align category_theory.equivalence.functor_unit_comp CategoryTheory.Equivalence.functor_unit_comp
 
-@[simp]
+@[reassoc (attr := 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))
@@ -178,7 +178,7 @@ theorem counit_app_functor (e : C ≌ D) (X : C) :
 
 /-- The other triangle equality. The proof follows the following proof in Globular:
   http://globular.science/1905.001 -/
-@[simp]
+@[reassoc (attr := 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]
@@ -203,7 +203,7 @@ theorem unit_inverse_comp (e : C ≌ D) (Y : D) :
   erw [id_comp, (e.unitIso.app _).hom_inv_id]; rfl
 #align category_theory.equivalence.unit_inverse_comp CategoryTheory.Equivalence.unit_inverse_comp
 
-@[simp]
+@[reassoc (attr := simp)]
 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))
@@ -224,13 +224,13 @@ theorem unitInv_app_inverse (e : C ≌ D) (Y : D) :
   rfl
 #align category_theory.equivalence.unit_inv_app_inverse CategoryTheory.Equivalence.unitInv_app_inverse
 
-@[simp]
+@[reassoc, 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]
+@[reassoc, 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
@@ -255,6 +255,7 @@ def adjointifyη : 𝟭 C ≅ F ⋙ G := by
     _ ≅ F ⋙ G := leftUnitor (F ⋙ G)
 #align category_theory.equivalence.adjointify_η CategoryTheory.Equivalence.adjointifyη
 
+@[reassoc]
 theorem adjointify_η_ε (X : C) :
     F.map ((adjointifyη η ε).hom.app X) ≫ ε.hom.app (F.obj X) = 𝟙 (F.obj X) := by
   dsimp [adjointifyη,Trans.trans]

Mathlib/CategoryTheory/Sites/EffectiveEpimorphic.lean

@@ -717,4 +717,141 @@ lemma effectiveEpi_iff_epi {X Y : C} (f : X ⟶ Y) : EffectiveEpi f ↔ Epi f :=
 
 end Epi
 
+noncomputable section Equivalence
+
+variable {D : Type*} [Category D] (e : C ≌ D) {B : C}
+
+variable {α : Type*} (X : α → C) (π : (a : α) → (X a ⟶ B)) [EffectiveEpiFamily X π]
+
+theorem effectiveEpiFamilyStructOfEquivalence_aux {W : D} (ε : (a : α) → e.functor.obj (X a) ⟶ W)
+    (h : ∀ {Z : D} (a₁ a₂ : α) (g₁ : Z ⟶ e.functor.obj (X a₁)) (g₂ : Z ⟶ e.functor.obj (X a₂)),
+      g₁ ≫ e.functor.map (π a₁) = g₂ ≫ e.functor.map (π a₂) → g₁ ≫ ε a₁ = g₂ ≫ ε a₂)
+    {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂) (hg : g₁ ≫ π a₁ = g₂ ≫ π a₂) :
+    g₁ ≫ (fun a ↦ e.unit.app (X a) ≫ e.inverse.map (ε a)) a₁ =
+    g₂ ≫ (fun a ↦ e.unit.app (X a) ≫ e.inverse.map (ε a)) a₂ := by
+  have := h a₁ a₂ (e.functor.map g₁) (e.functor.map g₂)
+  simp only [← Functor.map_comp, hg] at this
+  simpa using congrArg e.inverse.map (this (by trivial))
+
+/-- Equivalences preserve effective epimorphic families -/
+def effectiveEpiFamilyStructOfEquivalence : EffectiveEpiFamilyStruct (fun a ↦ e.functor.obj (X a))
+    (fun a ↦ e.functor.map (π a)) where
+  desc ε h := (e.toAdjunction.homEquiv _ _).symm
+      (EffectiveEpiFamily.desc X π (fun a ↦ e.unit.app _ ≫ e.inverse.map (ε a))
+      (effectiveEpiFamilyStructOfEquivalence_aux e X π ε h))
+  fac ε h a := by
+    simp only [Functor.comp_obj, Adjunction.homEquiv_counit, Functor.id_obj,
+      Equivalence.toAdjunction_counit]
+    have := congrArg ((fun f ↦ f ≫ e.counit.app _) ∘ e.functor.map)
+      (EffectiveEpiFamily.fac X π (fun a ↦ e.unit.app _ ≫ e.inverse.map (ε a))
+      (effectiveEpiFamilyStructOfEquivalence_aux e X π ε h) a)
+    simp only [Functor.id_obj, Functor.comp_obj, Function.comp_apply, Functor.map_comp,
+        Category.assoc, Equivalence.fun_inv_map, Iso.inv_hom_id_app, Category.comp_id] at this
+    simp [this]
+  uniq ε h m hm := by
+    simp only [Functor.comp_obj, Adjunction.homEquiv_counit, Functor.id_obj,
+      Equivalence.toAdjunction_counit]
+    have := EffectiveEpiFamily.uniq X π (fun a ↦ e.unit.app _ ≫ e.inverse.map (ε a))
+      (effectiveEpiFamilyStructOfEquivalence_aux e X π ε h)
+    specialize this (e.unit.app _ ≫ e.inverse.map m) fun a ↦ ?_
+    · rw [← congrArg e.inverse.map (hm a)]
+      simp
+    · simp [← this]
+
+instance (F : C ⥤ D) [IsEquivalence F] :
+    EffectiveEpiFamily (fun a ↦ F.obj (X a)) (fun a ↦ F.map (π a)) :=
+  ⟨⟨effectiveEpiFamilyStructOfEquivalence F.asEquivalence _ _⟩⟩
+
+example {X B : C} (π : X ⟶ B) (F : C ⥤ D) [IsEquivalence F] [EffectiveEpi π] :
+    EffectiveEpi <| F.map π := inferInstance
+
+end Equivalence
+
+section CompIso
+
+variable {B B' : C} {α : Type*} (X : α → C) (π : (a : α) → (X a ⟶ B)) [EffectiveEpiFamily X π]
+  (i : B ⟶ B') [IsIso i]
+
+theorem effectiveEpiFamilyStructCompIso_aux
+    {W : C} (e : (a : α) → X a ⟶ W)
+    (h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
+      g₁ ≫ π a₁ ≫ i = g₂ ≫ π a₂ ≫ i → g₁ ≫ e a₁ = g₂ ≫ e a₂)
+    {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂) (hg : g₁ ≫ π a₁ = g₂ ≫ π a₂) :
+    g₁ ≫ e a₁ = g₂ ≫ e a₂ := by
+  apply h
+  rw [← Category.assoc, hg]
+  simp
+
+/-- An effective epi family followed by an iso is an effective epi family. -/
+noncomputable
+def effectiveEpiFamilyStructCompIso : EffectiveEpiFamilyStruct X (fun a ↦ π a ≫ i) where
+  desc e h := inv i ≫ EffectiveEpiFamily.desc X π e (effectiveEpiFamilyStructCompIso_aux X π i e h)
+  fac _ _ _ := by simp
+  uniq e h m hm := by
+    simp only [Category.assoc] at hm
+    simp [← EffectiveEpiFamily.uniq X π e
+      (effectiveEpiFamilyStructCompIso_aux X π i e h) (i ≫ m) hm]
+
+instance : EffectiveEpiFamily X (fun a ↦ π a ≫ i) := ⟨⟨effectiveEpiFamilyStructCompIso X π i⟩⟩
+
+end CompIso
+
+section IsoComp
+
+variable {B : C} {α : Type*} (X Y : α → C) (π : (a : α) → (X a ⟶ B)) [EffectiveEpiFamily X π]
+  (i : (a : α) → Y a ⟶ X a) [∀ a, IsIso (i a)]
+
+theorem effectiveEpiFamilyStructIsoComp_aux {W : C} (e : (a : α) → Y a ⟶ W)
+    (h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂),
+      g₁ ≫ i a₁ ≫ π a₁ = g₂ ≫ i a₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂)
+    {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂) (hg : g₁ ≫ π a₁ = g₂ ≫ π a₂) :
+    g₁ ≫ (fun a ↦ inv (i a) ≫ e a) a₁ = g₂ ≫ (fun a ↦ inv (i a) ≫ e a) a₂ := by
+  simp only [← Category.assoc]
+  apply h
+  simp [hg]
+
+/-- An effective epi family preceded by a family of isos is an effective epi family. -/
+noncomputable
+def effectiveEpiFamilyStructIsoComp : EffectiveEpiFamilyStruct Y (fun a ↦ i a ≫ π a) where
+  desc e h := EffectiveEpiFamily.desc X π (fun a ↦ inv (i a) ≫ e a)
+    (effectiveEpiFamilyStructIsoComp_aux X Y π i e h)
+  fac _ _ _ := by simp
+  uniq e h m hm := by
+    simp only [Category.assoc] at hm
+    simp [← EffectiveEpiFamily.uniq X π (fun a ↦ inv (i a) ≫ e a)
+      (effectiveEpiFamilyStructIsoComp_aux X Y π i e h) m fun a ↦ by simpa using hm a]
+
+instance effectiveEpiFamilyIsoComp : EffectiveEpiFamily Y (fun a ↦ i a ≫ π a) :=
+  ⟨⟨effectiveEpiFamilyStructIsoComp X Y π i⟩⟩
+
+end IsoComp
+
+section Preserves
+
+variable {D : Type*} [Category D]
+
+namespace Functor
+
+/--
+A functor preserves effective epimorphisms if it maps effective epimorphisms to effective
+epimorphisms.
+-/
+class PreservesEffectiveEpis (F : C ⥤ D) : Prop where
+  /--
+  A functor preserves effective epimorphisms if it maps effective
+  epimorphisms to effective epimorphisms.
+  -/
+  preserves : ∀ {X Y : C} (f : X ⟶ Y) [EffectiveEpi f], EffectiveEpi (F.map f)
+
+instance map_effectiveEpi (F : C ⥤ D) [F.PreservesEffectiveEpis] {X Y : C} (f : X ⟶ Y)
+    [EffectiveEpi f] : EffectiveEpi (F.map f) :=
+  PreservesEffectiveEpis.preserves f
+
+instance (F : C ⥤ D) [IsEquivalence F] : F.PreservesEffectiveEpis where
+  preserves _ := inferInstance
+
+end Functor
+
+end Preserves
+
 end CategoryTheory