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.
-/
def isColimitOfEffectiveEpiFamilyStruct {B : C} {α : Type*} (X : α → C) (π : (a : α) → (X a ⟶ B))
(H : EffectiveEpiFamilyStruct X π) : IsColimit (Sieve.generateFamily X π : Presieve B).cocone :=
letI D := ObjectProperty.FullSubcategory fun T : Over B => Sieve.generateFamily X π T.hom
letI F : D ⥤ _ := (Sieve.generateFamily X π).arrows.diagram
{ desc := fun S =>
H.desc (fun a => S.ι.app ⟨Over.mk (π a), ⟨a, 𝟙 _, by simp⟩⟩) <|
by
intro Z a₁ a₂ g₁ g₂ h
dsimp
let A₁ : D := ⟨Over.mk (π a₁), a₁, 𝟙 _, by simp⟩
let A₂ : D := ⟨Over.mk (π a₂), a₂, 𝟙 _, by simp⟩
let Z' : D := ⟨Over.mk (g₁ ≫ π a₁), a₁, g₁, rfl⟩
let i₁ : Z' ⟶ A₁ := Over.homMk g₁
let i₂ : Z' ⟶ A₂ := Over.homMk g₂
change F.map i₁ ≫ _ = F.map i₂ ≫ _
simp only [F, A₁, A₂, S.w]
fac := by
intro S ⟨T, a, (g : T.left ⟶ X a), hT⟩
dsimp
nth_rewrite 1 [← hT, Category.assoc, H.fac]
let A : D := ⟨Over.mk (π a), a, 𝟙 _, by simp⟩
let B : D := ⟨Over.mk T.hom, a, g, hT⟩
let i : B ⟶ A := Over.homMk g
change F.map i ≫ _ = _
rw [S.w]
rfl
uniq := by
intro S m hm; dsimp
apply H.uniq
intro a
exact hm ⟨Over.mk (π a), a, 𝟙 _, by simp⟩ }
