codLift — Mathlib

English

The linear map Submodule.subtype is the embedding of a submodule into M.

Русский

Линейное отображение Submodule.subtype является вложением подмодуля в M.

LaTeX

$$Submodule.subtype : p →ₗ[R] M$$

Lean4

/-- A linear map `f : M → M₂` whose values lie in the image of an injective linear map
`p : M₂' → M₂` admits a unique lift to a linear map `M → M₂'`. -/
noncomputable def codLift : M →ₛₗ[σ₁₂] M₂' where
  toFun c := (h c).choose
  map_add' b c := by apply hp; simp_rw [map_add, (h _).choose_spec, ← map_add, (h _).choose_spec]
  map_smul' r c := by apply hp; simp_rw [map_smul, (h _).choose_spec, LinearMap.map_smulₛₗ]

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