isLimitKer — Mathlib

English

The composition kerι φ followed by φ is zero.

Русский

Составление kerι φ затем φ равно нулю.

LaTeX

$$$\ker\iota_\varphi \;\; \xrightarrow{\varphi} \; N = 0$$$

Lean4

/-- `TopModuleCat.ker` is indeed the kernel in `TopModuleCat R`. -/
def isLimitKer : IsLimit (KernelFork.ofι (kerι φ) (kerι_comp φ)) :=
  isLimitAux (KernelFork.ofι (kerι φ) (kerι_comp φ))
    (fun s ↦
      ofHom <|
        (Fork.ι s).hom.codRestrict (LinearMap.ker φ.hom) fun m ↦ by
          rw [LinearMap.mem_ker, ← ConcreteCategory.comp_apply (Fork.ι s) φ, KernelFork.condition, hom_zero_apply])
    (fun s ↦ rfl) (fun s m h ↦ by dsimp at h ⊢; rw [← cancel_mono (kerι φ), h]; rfl)

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