cokernelIsColimit — Mathlib

English

The projection onto the quotient is a cokernel in the categorical sense; the cokernel cocone is a colimit cocone.

Русский

Проекция на кваторку является коканелом в категориальном смысле; коканел-конон образует колимитный кокон.

LaTeX

$$$$ \\text{IsColimit}(\\text{cokernelCocone}(f)) $$$$

Lean4

/-- The projection onto the quotient is a cokernel in the categorical sense. -/
def cokernelIsColimit : IsColimit (cokernelCocone f) :=
  Cofork.IsColimit.mk _
    (fun s =>
      ofHom <|
        (LinearMap.range f.hom).liftQ (Cofork.π s).hom <|
          LinearMap.range_le_ker_iff.2 <| ModuleCat.hom_ext_iff.mp <| CokernelCofork.condition s)
    (fun s => hom_ext <| (LinearMap.range f.hom).liftQ_mkQ (Cofork.π s).hom _) fun s m h => by
    -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11036): broken dot notation

    haveI : Epi (ofHom (LinearMap.range f.hom).mkQ) :=
      (epi_iff_range_eq_top _).mpr
        (Submodule.range_mkQ _)
          -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11036): broken dot notation

    apply (cancel_epi (ofHom (LinearMap.range f.hom).mkQ)).1
    exact h

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