codRestrict — Mathlib

English

The Submodule.subtype map is a linear map from p to M.

Русский

Карта Submodule.subtype является линейным отображением из p в M.

LaTeX

$${\text{Submodule.subtype} : p →ₗ[R] M}$$

Lean4

/-- A linear map `f : M₂ → M` whose values lie in a submodule `p ⊆ M` can be restricted to a
linear map M₂ → p.

See also `LinearMap.codLift`. -/
def codRestrict (p : Submodule R₂ M₂) (f : M →ₛₗ[σ₁₂] M₂) (h : ∀ c, f c ∈ p) : M →ₛₗ[σ₁₂] p
    where
  toFun c := ⟨f c, h c⟩
  map_add' _ _ := by simp
  map_smul' _ _ := by simp

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