ker_comapₗ — Mathlib

English

If f is surjective, the kernel of comapₗ is the zero subspace, i.e., comapₗ is injective when restricted to LocallyConstant with surjective base map.

Русский

Если отображение f сюръективно, то ядро comapₗ равно нулевому подпространству; то есть comapₗ инъективно при сюръективности базового отображения.

LaTeX

$$$\ker(\operatorname{comap}_{\ell} R f) = \{0\}$$$

Lean4

theorem ker_comapₗ [Semiring R] [AddCommMonoid Z] [Module R Z] (f : C(X, Y)) (hfs : Function.Surjective f) :
    LinearMap.ker (comapₗ R f : LocallyConstant Y Z →ₗ[R] LocallyConstant X Z) = ⊥ :=
  LinearMap.ker_eq_bot_of_injective <| comap_injective _ hfs

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