effectiveEpiFamilyStructOfIsIsoDesc

Lean4
/-- A family of morphisms with the same target inducing an isomorphism from the coproduct to the target
is an `EffectiveEpiFamily`.
-/
noncomputable def effectiveEpiFamilyStructOfIsIsoDesc {B : C} {α : Type*} (X : α → C) (π : (a : α) → (X a ⟶ B))
    [HasCoproduct X] [IsIso (Sigma.desc π)] : EffectiveEpiFamilyStruct X π
    where
  desc e _ := (asIso (Sigma.desc π)).inv ≫ (Sigma.desc e)
  fac e
    h := by
    intro a
    have : π a = Sigma.ι X a ≫ (asIso (Sigma.desc π)).hom := by
      simp only [asIso_hom, colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app]
    rw [this, Category.assoc]
    simp only [asIso_hom, asIso_inv, IsIso.hom_inv_id_assoc, colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app]
  uniq e h m
    hm := by
    simp only [asIso_inv, IsIso.eq_inv_comp]
    ext a
    simp only [colimit.ι_desc_assoc, Discrete.functor_obj, Cofan.mk_pt, Cofan.mk_ι_app, colimit.ι_desc]
    exact hm a
Похожие утверждения