effectiveEpiStructIsColimitDescOfEffectiveEpiFamily

Lean4
/-- Given an `EffectiveEpiFamily X π` and a corresponding coproduct cocone, the family descends to an
`EffectiveEpi` from the coproduct.
-/
noncomputable def effectiveEpiStructIsColimitDescOfEffectiveEpiFamily {B : C} {α : Type*} (X : α → C) (c : Cofan X)
    (hc : IsColimit c) (π : (a : α) → (X a ⟶ B)) [EffectiveEpiFamily X π] : EffectiveEpiStruct (hc.desc (Cofan.mk B π))
    where
  desc e
    h :=
    EffectiveEpiFamily.desc X π (fun a ↦ c.ι.app ⟨a⟩ ≫ e)
      (fun a₁ a₂ g₁ g₂ hg ↦ by
        simp only [← Category.assoc]
        exact h (g₁ ≫ c.ι.app ⟨a₁⟩) (g₂ ≫ c.ι.app ⟨a₂⟩) (by simpa))
  fac e h := hc.hom_ext (fun ⟨j⟩ ↦ (by simp))
  uniq e _ m
    hm :=
    EffectiveEpiFamily.uniq X π (fun a ↦ c.ι.app ⟨a⟩ ≫ e) (fun _ _ _ _ hg ↦ (by simp [← hm, reassoc_of% hg])) m
      (fun _ ↦ (by simp [← hm]))
Похожие утверждения