Lean4
/-- Implementation: This is a construction which will be used in the proof that
the sieve generated by a family of arrows is effective epimorphic if and only if
the family is an effective epi.
-/
noncomputable def effectiveEpiFamilyStructOfIsColimit {B : C} {α : Type*} (X : α → C) (π : (a : α) → (X a ⟶ B))
(H : IsColimit (Sieve.generateFamily X π : Presieve B).cocone) : EffectiveEpiFamilyStruct X π :=
let aux {W : C} (e : (a : α) → (X a ⟶ W))
(h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π _ = g₂ ≫ π _ → g₁ ≫ e _ = g₂ ≫ e _) :
Cocone (Sieve.generateFamily X π).arrows.diagram :=
{ pt := W
ι :=
{ app := fun ⟨_, hT⟩ => hT.choose_spec.choose ≫ e hT.choose
naturality := by
intro ⟨A, a, (g₁ : A.left ⟶ _), ha⟩ ⟨B, b, (g₂ : B.left ⟶ _), hb⟩ (q : A ⟶ B)
dsimp; rw [Category.comp_id, ← Category.assoc]
apply h; rw [Category.assoc]
generalize_proofs h1 h2 h3 h4
rw [h2.choose_spec, h4.choose_spec, Over.w] } }
{ desc := fun {_} e h => H.desc (aux e h)
fac := by
intro W e h a
dsimp
have := H.fac (aux e h) ⟨Over.mk (π a), a, 𝟙 _, by simp⟩
dsimp [aux] at this; rw [this]; clear this
conv_rhs => rw [← Category.id_comp (e a)]
apply h
generalize_proofs h1 h2
rw [h2.choose_spec, Category.id_comp]
uniq := by
intro W e h m hm
apply H.uniq (aux e h)
rintro ⟨T, a, (g : T.left ⟶ _), ha⟩
dsimp
nth_rewrite 1 [← ha, Category.assoc, hm]
apply h
generalize_proofs h1 h2
rwa [h2.choose_spec] }
