isColimit_iff_bijective_desc — Mathlib

English

For a functor F: J → AddCommGrpCat, F has a colimit iff the quotient object Quot F is small in universe w.

Русский

Пусть F: J → AddCommGrpCat; тогда F имеет колимит iff объект Quot F мал по вселенной w.

LaTeX

$$$ \\text{HasColimit}(F) \\iff \\mathrm{Small}^{(w)}(\\mathrm{Quot} F) $$$

Lean4

/-- If `c` is a cocone of `F` such that `Quot.desc F c` is bijective, then `c` is a colimit
cocone of `F`.
-/
theorem isColimit_iff_bijective_desc [DecidableEq J] : Nonempty (IsColimit c) ↔ Function.Bijective (Quot.desc F c) :=
  by
  refine ⟨fun ⟨hc⟩ => ?_, fun h ↦ Nonempty.intro (isColimit_of_bijective_desc F c h)⟩
  change Function.Bijective (Quot.desc F c).toIntLinearMap
  rw [← CharacterModule.dual_bijective_iff_bijective]
  refine ⟨fun χ ψ eq ↦ ?_, fun χ ↦ ?_⟩
  · apply AddEquiv.ulift.symm.addMonoidHomCongrRightEquiv.injective
    apply ofHom_injective
    refine hc.hom_ext (fun j ↦ ?_)
    ext x
    rw [ConcreteCategory.comp_apply, ConcreteCategory.comp_apply, ← Quot.ι_desc _ c j x]
    exact DFunLike.congr_fun eq (Quot.ι F j x)
  · set c' : Cocone F :=
      { pt := AddCommGrpCat.of (ULift (AddCircle (1 : ℚ)))
        ι :=
          { app j := AddCommGrpCat.ofHom (((@AddEquiv.ulift _ _).symm.toAddMonoidHom.comp χ).comp (Quot.ι F j))
            naturality {j j'}
              u := by
              ext
              dsimp
              rw [Quot.map_ι F (f := u)] } }
    use AddEquiv.ulift.toAddMonoidHom.comp (hc.desc c').hom
    refine Quot.addMonoidHom_ext _ (fun j x ↦ ?_)
    dsimp
    rw [Quot.ι_desc]
    change AddEquiv.ulift ((c.ι.app j ≫ hc.desc c') x) = _
    rw [hc.fac]
    dsimp [c']
    rw [AddEquiv.apply_symm_apply]

Похожие утверждения