feat(CategoryTheory): reindex effective epi families (#11568)

Co-authored-by: Adam Topaz @adamtopaz <topaz@ualberta.ca>

Mathlib/CategoryTheory/EffectiveEpi/Basic.lean

@@ -267,3 +267,31 @@ def effectiveEpiStructOfIsIso {X Y : C} (f : X ⟶ Y) [IsIso f] : EffectiveEpiSt
 instance {X Y : C} (f : X ⟶ Y) [IsIso f] : EffectiveEpi f := ⟨⟨effectiveEpiStructOfIsIso f⟩⟩
 
 example {X : C} : EffectiveEpiFamily (fun _ => X : Unit → C) (fun _ => 𝟙 X) := inferInstance
+
+/--
+Reindex the indexing type of an effective epi family struct.
+-/
+def EffectiveEpiFamilyStruct.reindex
+    {B : C} {α α' : Type*}
+    (X : α → C)
+    (π : (a : α) → (X a ⟶ B))
+    (e : α' ≃ α)
+    (P : EffectiveEpiFamilyStruct (fun a => X (e a)) (fun a => π (e a))) :
+    EffectiveEpiFamilyStruct X π where
+  desc := fun f h => P.desc (fun a => f _) (fun a₁ a₂ => h _ _)
+  fac _ _ a := by
+    obtain ⟨a,rfl⟩ := e.surjective a
+    apply P.fac
+  uniq _ _ m hm := P.uniq _ _ _ fun a => hm _
+
+/--
+Reindex the indexing type of an effective epi family.
+-/
+lemma EffectiveEpiFamily.reindex
+    {B : C} {α α' : Type*}
+    (X : α → C)
+    (π : (a : α) → (X a ⟶ B))
+    (e : α' ≃ α)
+    (h : EffectiveEpiFamily (fun a => X (e a)) (fun a => π (e a))) :
+    EffectiveEpiFamily X π :=
+  .mk <| .intro <| @EffectiveEpiFamily.getStruct _ _ _ _ _ _ h |>.reindex _ _ e

Mathlib/CategoryTheory/Sites/Coherent/CoherentTopology.lean

@@ -72,6 +72,14 @@ theorem EffectiveEpiFamily.transitive_of_finite {α : Type} [Finite α] {Y : α
     exact ⟨β i, inferInstance, Y_n i, π_n i, H i, fun b ↦
       ⟨Y_n i b, (𝟙 _), π_n i b ≫ π i, ⟨(⟨i, b⟩ : Σ (i : α), β i)⟩, by simp⟩⟩
 
+instance precoherentEffectiveEpiFamilyCompEffectiveEpis
+    {α : Type} [Finite α] {Y Z : α → C} (π : (a : α) → (Y a ⟶ X)) [EffectiveEpiFamily Y π]
+    (f : (a : α) → Z a ⟶ Y a) [h : ∀ a, EffectiveEpi (f a)] :
+    EffectiveEpiFamily _ fun a ↦ f a ≫ π a := by
+  simp_rw [effectiveEpi_iff_effectiveEpiFamily] at h
+  exact EffectiveEpiFamily.reindex (e := Equiv.sigmaPUnit α) _ _
+    (EffectiveEpiFamily.transitive_of_finite (β := fun _ ↦ Unit) _ inferInstance _ h)
+
 /--
 A sieve belongs to the coherent topology if and only if it contains a finite
 `EffectiveEpiFamily`.