kernelCone — Mathlib

English

There is an isomorphism between the categorical kernel of f and the module-theoretic kernel of f.hom: kernel f ≅ ModuleCat.of(R, ker f.hom).

Русский

Существует изоморфизм между категориальным ядром morphism f и модульным ядром линейного отображения f.hom: kernel f ≅ ModuleCat.of(R, ker f.hom).

LaTeX

$$$$ \\ker( f ) \\cong_ModuleCat\\!\\!\\!\\!\\!\\! \\; \\ker(f^{\\mathrm{hom}}) $$$$

Lean4

/-- The kernel cone induced by the concrete kernel. -/
def kernelCone : KernelFork f :=
  KernelFork.ofι (ofHom (LinearMap.ker f.hom).subtype) <| by aesop

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