isColimit_of_bijective_desc — Mathlib

Lean4
/-- If `c` is a cocone of `F` such that `Quot.desc F c` is bijective, then `c` is a colimit
cocone of `F`.
-/
noncomputable def isColimit_of_bijective_desc [DecidableEq J] (h : Function.Bijective (Quot.desc F c)) : IsColimit c
    where
  desc s := AddCommGrpCat.ofHom ((Quot.desc F s).comp (AddEquiv.ofBijective (Quot.desc F c) h).symm.toAddMonoidHom)
  fac s
    j := by
    ext x
    dsimp
    conv_lhs => erw [← Quot.ι_desc F c j x]
    rw [← AddEquiv.ofBijective_apply _ h, AddEquiv.symm_apply_apply]
    simp only [Quot.ι_desc, Functor.const_obj_obj]
  uniq s m
    hm := by
    ext x
    obtain ⟨x, rfl⟩ := h.2 x
    dsimp
    rw [← AddEquiv.ofBijective_apply _ h, AddEquiv.symm_apply_apply]
    suffices eq : m.hom.comp (AddEquiv.ofBijective (Quot.desc F c) h) = Quot.desc F s by rw [← eq]; rfl
    exact Quot.addMonoidHom_ext F (by simp [← hm])
Похожие утверждения