Lean4
/-- Implementation: This is a construction which will be used in the proof that
the sieve generated by a single arrow is effective epimorphic if and only if
the arrow is an effective epi.
-/
noncomputable def effectiveEpiStructOfIsColimit {X Y : C} (f : Y ⟶ X)
(Hf : IsColimit (Sieve.generateSingleton f : Presieve X).cocone) : EffectiveEpiStruct f :=
let aux {W : C} (e : Y ⟶ W) (h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e) :
Cocone (Sieve.generateSingleton f).arrows.diagram :=
{ pt := W
ι :=
{ app := fun ⟨_, hT⟩ => hT.choose ≫ e
naturality := by
rintro ⟨A, hA⟩ ⟨B, hB⟩ (q : A ⟶ B)
dsimp; simp only [← Category.assoc, Category.comp_id]
apply h
rw [Category.assoc, hB.choose_spec, hA.choose_spec, Over.w] } }
{ desc := fun {_} e h => Hf.desc (aux e h)
fac := by
intro W e h
dsimp
have := Hf.fac (aux e h) ⟨Over.mk f, 𝟙 _, by simp⟩
dsimp [aux] at this; rw [this]; clear this
nth_rewrite 2 [← Category.id_comp e]
apply h
generalize_proofs hh
rw [hh.choose_spec, Category.id_comp]
uniq := by
intro W e h m hm
dsimp
apply Hf.uniq (aux e h)
rintro ⟨A, g, hA⟩
dsimp
nth_rewrite 1 [← hA, Category.assoc, hm]
apply h
generalize_proofs hh
rwa [hh.choose_spec] }
