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.
-/
def isColimitOfEffectiveEpiStruct {X Y : C} (f : Y ⟶ X) (Hf : EffectiveEpiStruct f) :
IsColimit (Sieve.generateSingleton f : Presieve X).cocone :=
letI D := ObjectProperty.FullSubcategory fun T : Over X => Sieve.generateSingleton f T.hom
letI F : D ⥤ _ := (Sieve.generateSingleton f).arrows.diagram
{ desc := fun S =>
Hf.desc (S.ι.app ⟨Over.mk f, ⟨𝟙 _, by simp⟩⟩) <| by
intro Z g₁ g₂ h
let Y' : D := ⟨Over.mk f, 𝟙 _, by simp⟩
let Z' : D := ⟨Over.mk (g₁ ≫ f), g₁, rfl⟩
let g₁' : Z' ⟶ Y' := Over.homMk g₁
let g₂' : Z' ⟶ Y' := Over.homMk g₂ (by simp [Y', Z', h])
change F.map g₁' ≫ _ = F.map g₂' ≫ _
simp only [Y', F, S.w]
fac := by
rintro S ⟨T, g, hT⟩
dsimp
nth_rewrite 1 [← hT, Category.assoc, Hf.fac]
let y : D := ⟨Over.mk f, 𝟙 _, by simp⟩
let x : D := ⟨Over.mk T.hom, g, hT⟩
let g' : x ⟶ y := Over.homMk g
change F.map g' ≫ _ = _
rw [S.w]
rfl
uniq := by
intro S m hm
dsimp
generalize_proofs h1 h2
apply Hf.uniq _ h2
exact hm ⟨Over.mk f, 𝟙 _, by simp⟩ }
