moduleCatToCycles — Mathlib

English

There is a canonical linear map from X1 to the kernel of g induced by f, i.e., the map sending x to f(x) considered in ker(g).

Русский

Существует каноническое линейное отображение из X1 в ядро g, индуцированное f, отправляющее x в f(x) как элемент ker(g).

LaTeX

$$$\\mathrm{moduleCatToCycles}: S.X_1 \\to \\ker S.g.hom$$$

Lean4

/-- The canonical linear map `S.X₁ →ₗ[R] LinearMap.ker S.g` induced by `S.f`. -/
abbrev moduleCatToCycles : S.X₁ →ₗ[R] LinearMap.ker S.g.hom :=
  S.f.hom.codRestrict _ <| S.moduleCat_zero_apply

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