kernelIsLimit — Mathlib

English

The kernel of a linear map is a kernel in the categorical sense; the kernel cone is a limit cone.

Русский

Ядро линейного отображения является ядром в категориальном смысле; конус ядра является пределом.

LaTeX

$$$$ \\text{IsLimit}(\\text{kernelCone}(f)) $$$$

Lean4

/-- The kernel of a linear map is a kernel in the categorical sense. -/
def kernelIsLimit : IsLimit (kernelCone f) :=
  Fork.IsLimit.mk _
    (fun s =>
      ofHom <|
        -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11036): broken dot notation on LinearMap.ker
        LinearMap.codRestrict (LinearMap.ker f.hom) (Fork.ι s).hom fun c =>
          LinearMap.mem_ker.2 <| by
            -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644

            erw [← ConcreteCategory.comp_apply]
            rw [Fork.condition, HasZeroMorphisms.comp_zero (Fork.ι s) N]
            rfl)
    (fun _ => hom_ext <| LinearMap.subtype_comp_codRestrict _ _ _) fun s m h =>
    hom_ext <| LinearMap.ext fun x => Subtype.ext_iff.2 (by simp [← h]; rfl)

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