# Documentation

Mathlib.LinearAlgebra.Basic

# Linear algebra #

This file defines the basics of linear algebra. It sets up the "categorical/lattice structure" of modules over a ring, submodules, and linear maps.

Many of the relevant definitions, including Module, Submodule, and LinearMap, are found in Algebra/Module.

## Main definitions #

• Many constructors for (semi)linear maps
• The kernel ker and range range of a linear map are submodules of the domain and codomain respectively.

See LinearAlgebra.Span for the span of a set (as a submodule), and LinearAlgebra.Quotient for quotients by submodules.

## Main theorems #

See LinearAlgebra.Isomorphisms for Noether's three isomorphism theorems for modules.

## Notations #

• We continue to use the notations M →ₛₗ[σ] M₂ and M →ₗ[R] M₂ for the type of semilinear (resp. linear) maps from M to M₂ over the ring homomorphism σ (resp. over the ring R).

## Implementation notes #

We note that, when constructing linear maps, it is convenient to use operations defined on bundled maps (LinearMap.prod, LinearMap.coprod, arithmetic operations like +) instead of defining a function and proving it is linear.

## TODO #

• Parts of this file have not yet been generalized to semilinear maps

## Tags #

linear algebra, vector space, module

theorem Finsupp.smul_sum {α : Type u_20} {β : Type u_21} {R : Type u_22} {M : Type u_23} [Zero β] [] [] {v : α →₀ β} {c : R} {h : αβM} :
c = Finsupp.sum v fun a b => c h a b
@[simp]
theorem Finsupp.sum_smul_index_linearMap' {α : Type u_20} {R : Type u_21} {M : Type u_22} {M₂ : Type u_23} [] [] [Module R M] [] [Module R M₂] {v : α →₀ M} {c : R} {h : αM →ₗ[R] M₂} :
(Finsupp.sum (c v) fun a => ↑(h a)) = c Finsupp.sum v fun a => ↑(h a)
@[simp]
theorem Finsupp.linearEquivFunOnFinite_apply (R : Type u_1) (M : Type u_9) (α : Type u_20) [] [] [] [Module R M] :
∀ (a : α →₀ M) (a_1 : α), ↑() a a_1 = a a_1
noncomputable def Finsupp.linearEquivFunOnFinite (R : Type u_1) (M : Type u_9) (α : Type u_20) [] [] [] [Module R M] :
(α →₀ M) ≃ₗ[R] αM

Given Finite α, linearEquivFunOnFinite R is the natural R-linear equivalence between α →₀ β and α → β.

Instances For
@[simp]
theorem Finsupp.linearEquivFunOnFinite_single (R : Type u_1) (M : Type u_9) (α : Type u_20) [] [] [] [Module R M] [] (x : α) (m : M) :
(↑() fun₀ | x => m) =
@[simp]
theorem Finsupp.linearEquivFunOnFinite_symm_single (R : Type u_1) (M : Type u_9) (α : Type u_20) [] [] [] [Module R M] [] (x : α) (m : M) :
↑() () = fun₀ | x => m
@[simp]
theorem Finsupp.linearEquivFunOnFinite_symm_coe (R : Type u_1) (M : Type u_9) (α : Type u_20) [] [] [] [Module R M] (f : α →₀ M) :
↑() f = f
noncomputable def Finsupp.LinearEquiv.finsuppUnique (R : Type u_1) (M : Type u_9) [] [] [Module R M] (α : Type u_21) [] :
(α →₀ M) ≃ₗ[R] M

If α has a unique term, then the type of finitely supported functions α →₀ M is R-linearly equivalent to M.

Instances For
@[simp]
theorem Finsupp.LinearEquiv.finsuppUnique_apply {R : Type u_1} {M : Type u_9} [] [] [Module R M] (α : Type u_21) [] (f : α →₀ M) :
↑() f = f default
@[simp]
theorem Finsupp.LinearEquiv.finsuppUnique_symm_apply {R : Type u_1} {M : Type u_9} [] [] [Module R M] {α : Type u_21} [] (m : M) :
↑() m = fun₀ | default => m
theorem pi_eq_sum_univ {ι : Type u_20} [] [] {R : Type u_21} [] (x : ιR) :
x = Finset.sum Finset.univ fun i => x i fun j => if i = j then 1 else 0

decomposing x : ι → R as a sum along the canonical basis

### Properties of linear maps #

@[simp]
theorem LinearMap.map_sum {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (f : M →ₛₗ[σ₁₂] M₂) {ι : Type u_20} {t : } {g : ιM} :
f (Finset.sum t fun i => g i) = Finset.sum t fun i => f (g i)
def LinearMap.domRestrict {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (f : M →ₛₗ[σ₁₂] M₂) (p : ) :
{ x // x p } →ₛₗ[σ₁₂] M₂

The restriction of a linear map f : M → M₂ to a submodule p ⊆ M gives a linear map p → M₂.

Instances For
@[simp]
theorem LinearMap.domRestrict_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (f : M →ₛₗ[σ₁₂] M₂) (p : ) (x : { x // x p }) :
↑() x = f x
def LinearMap.codRestrict {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (p : Submodule R₂ M₂) (f : M →ₛₗ[σ₁₂] M₂) (h : ∀ (c : M), f c p) :
M →ₛₗ[σ₁₂] { x // x p }

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

Instances For
@[simp]
theorem LinearMap.codRestrict_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (p : Submodule R₂ M₂) (f : M →ₛₗ[σ₁₂] M₂) {h : ∀ (c : M), f c p} (x : M) :
↑(↑() x) = f x
@[simp]
theorem LinearMap.comp_codRestrict {R : Type u_1} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_9} {M₂ : Type u_12} {M₃ : Type u_13} [] [Semiring R₂] [Semiring R₃] [] [] [] [Module R M] [Module R₂ M₂] [Module R₃ M₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] M₃) (p : Submodule R₃ M₃) (h : ∀ (b : M₂), g b p) :
LinearMap.comp () f = LinearMap.codRestrict p () fun x => h (f x)
@[simp]
theorem LinearMap.subtype_comp_codRestrict {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (f : M →ₛₗ[σ₁₂] M₂) (p : Submodule R₂ M₂) (h : ∀ (b : M), f b p) :
def LinearMap.restrict {R : Type u_1} {M : Type u_9} {M₁ : Type u_11} [] [] [] [Module R M] [Module R M₁] (f : M →ₗ[R] M₁) {p : } {q : Submodule R M₁} (hf : ∀ (x : M), x pf x q) :
{ x // x p } →ₗ[R] { x // x q }

Restrict domain and codomain of a linear map.

Instances For
@[simp]
theorem LinearMap.restrict_coe_apply {R : Type u_1} {M : Type u_9} {M₁ : Type u_11} [] [] [] [Module R M] [Module R M₁] (f : M →ₗ[R] M₁) {p : } {q : Submodule R M₁} (hf : ∀ (x : M), x pf x q) (x : { x // x p }) :
↑(↑() x) = f x
theorem LinearMap.restrict_apply {R : Type u_1} {M : Type u_9} {M₁ : Type u_11} [] [] [] [Module R M] [Module R M₁] {f : M →ₗ[R] M₁} {p : } {q : Submodule R M₁} (hf : ∀ (x : M), x pf x q) (x : { x // x p }) :
↑() x = { val := f x, property := hf x (_ : x p) }
theorem LinearMap.subtype_comp_restrict {R : Type u_1} {M : Type u_9} {M₁ : Type u_11} [] [] [] [Module R M] [Module R M₁] {f : M →ₗ[R] M₁} {p : } {q : Submodule R M₁} (hf : ∀ (x : M), x pf x q) :
theorem LinearMap.restrict_eq_codRestrict_domRestrict {R : Type u_1} {M : Type u_9} {M₁ : Type u_11} [] [] [] [Module R M] [Module R M₁] {f : M →ₗ[R] M₁} {p : } {q : Submodule R M₁} (hf : ∀ (x : M), x pf x q) :
= LinearMap.codRestrict q () fun x => hf x (_ : x p)
theorem LinearMap.restrict_eq_domRestrict_codRestrict {R : Type u_1} {M : Type u_9} {M₁ : Type u_11} [] [] [] [Module R M] [Module R M₁] {f : M →ₗ[R] M₁} {p : } {q : Submodule R M₁} (hf : ∀ (x : M), f x q) :
(LinearMap.restrict f fun x x_1 => hf x) =
instance LinearMap.uniqueOfLeft {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] :
Unique (M →ₛₗ[σ₁₂] M₂)
instance LinearMap.uniqueOfRight {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] :
Unique (M →ₛₗ[σ₁₂] M₂)
def LinearMap.evalAddMonoidHom {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (a : M) :
(M →ₛₗ[σ₁₂] M₂) →+ M₂

Evaluation of a σ₁₂-linear map at a fixed a, as an AddMonoidHom.

Instances For
def LinearMap.toAddMonoidHom' {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} :
(M →ₛₗ[σ₁₂] M₂) →+ M →+ M₂

LinearMap.toAddMonoidHom promoted to a AddMonoidHom

Instances For
theorem LinearMap.sum_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} {ι : Type u_17} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (t : ) (f : ιM →ₛₗ[σ₁₂] M₂) (b : M) :
↑(Finset.sum t fun d => f d) b = Finset.sum t fun d => ↑(f d) b
def LinearMap.smulRight {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₁ : Type u_11} [] [] [] [Module R M] [Module R M₁] [] [Module R S] [Module S M] [] (f : M₁ →ₗ[R] S) (x : M) :
M₁ →ₗ[R] M

When f is an R-linear map taking values in S, then fun ↦ b, f b • x is an R-linear map.

Instances For
@[simp]
theorem LinearMap.coe_smulRight {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₁ : Type u_11} [] [] [] [Module R M] [Module R M₁] [] [Module R S] [Module S M] [] (f : M₁ →ₗ[R] S) (x : M) :
↑() = fun c => f c x
theorem LinearMap.smulRight_apply {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₁ : Type u_11} [] [] [] [Module R M] [Module R M₁] [] [Module R S] [Module S M] [] (f : M₁ →ₗ[R] S) (x : M) (c : M₁) :
↑() c = f c x
instance LinearMap.instNontrivialEnd {R : Type u_1} {M : Type u_9} [] [] [Module R M] [] :
@[simp]
theorem LinearMap.coeFn_sum {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {ι : Type u_20} (t : ) (f : ιM →ₛₗ[σ₁₂] M₂) :
↑(Finset.sum t fun i => f i) = Finset.sum t fun i => ↑(f i)
theorem LinearMap.submodule_pow_eq_zero_of_pow_eq_zero {R : Type u_1} {M : Type u_9} [] [] [Module R M] {N : } {g : Module.End R { x // x N }} {G : } (h : ) {k : } (hG : G ^ k = 0) :
g ^ k = 0
theorem LinearMap.pow_apply_mem_of_forall_mem {R : Type u_1} {M : Type u_9} [] [] [Module R M] {f' : M →ₗ[R] M} {p : } (n : ) (h : ∀ (x : M), x pf' x p) (x : M) (hx : x p) :
↑(f' ^ n) x p
theorem LinearMap.pow_restrict {R : Type u_1} {M : Type u_9} [] [] [Module R M] {f' : M →ₗ[R] M} {p : } (n : ) (h : ∀ (x : M), x pf' x p) (h' : optParam (∀ (x : M), x p↑(f' ^ n) x p) (_ : ∀ (x : M), x p↑(f' ^ n) x p)) :
^ n = LinearMap.restrict (f' ^ n) h'
theorem LinearMap.pi_apply_eq_sum_univ {R : Type u_1} {M : Type u_9} {ι : Type u_17} [] [] [Module R M] [] [] (f : (ιR) →ₗ[R] M) (x : ιR) :
f x = Finset.sum Finset.univ fun i => x i f fun j => if i = j then 1 else 0

A linear map f applied to x : ι → R can be computed using the image under f of elements of the canonical basis.

@[simp]
theorem LinearMap.applyₗ'_apply_apply {R : Type u_1} (S : Type u_6) {M : Type u_9} {M₂ : Type u_12} [] [] [] [] [Module R M] [Module R M₂] [Module S M₂] [SMulCommClass R S M₂] (v : M) (f : M →ₗ[R] M₂) :
↑(↑() v) f = f v
def LinearMap.applyₗ' {R : Type u_1} (S : Type u_6) {M : Type u_9} {M₂ : Type u_12} [] [] [] [] [Module R M] [Module R M₂] [Module S M₂] [SMulCommClass R S M₂] :
M →+ (M →ₗ[R] M₂) →ₗ[S] M₂

Applying a linear map at v : M, seen as S-linear map from M →ₗ[R] M₂ to M₂.

See LinearMap.applyₗ for a version where S = R.

Instances For
@[simp]
theorem LinearMap.ringLmapEquivSelf_apply (R : Type u_1) (S : Type u_6) (M : Type u_9) [] [] [] [Module R M] [Module S M] [] (f : R →ₗ[R] M) :
↑() f = f 1
@[simp]
theorem LinearMap.ringLmapEquivSelf_symm_apply (R : Type u_1) (S : Type u_6) (M : Type u_9) [] [] [] [Module R M] [Module S M] [] (x : M) :
↑() x =
def LinearMap.ringLmapEquivSelf (R : Type u_1) (S : Type u_6) (M : Type u_9) [] [] [] [Module R M] [Module S M] [] :
(R →ₗ[R] M) ≃ₗ[S] M

The equivalence between R-linear maps from R to M, and points of M itself. This says that the forgetful functor from R-modules to types is representable, by R.

This as an S-linear equivalence, under the assumption that S acts on M commuting with R. When R is commutative, we can take this to be the usual action with S = R. Otherwise, S = ℕ shows that the equivalence is additive. See note [bundled maps over different rings].

Instances For
def LinearMap.compRight {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} {M₃ : Type u_13} [] [] [] [] [Module R M] [Module R M₂] [Module R M₃] (f : M₂ →ₗ[R] M₃) :
(M →ₗ[R] M₂) →ₗ[R] M →ₗ[R] M₃

Composition by f : M₂ → M₃ is a linear map from the space of linear maps M → M₂ to the space of linear maps M₂ → M₃.

Instances For
@[simp]
theorem LinearMap.compRight_apply {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} {M₃ : Type u_13} [] [] [] [] [Module R M] [Module R M₂] [Module R M₃] (f : M₂ →ₗ[R] M₃) (g : M →ₗ[R] M₂) :
↑() g =
@[simp]
theorem LinearMap.applyₗ_apply_apply {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [] [] [] [Module R M] [Module R M₂] (v : M) (f : M →ₗ[R] M₂) :
↑(LinearMap.applyₗ v) f = f v
def LinearMap.applyₗ {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [] [] [] [Module R M] [Module R M₂] :
M →ₗ[R] (M →ₗ[R] M₂) →ₗ[R] M₂

Applying a linear map at v : M, seen as a linear map from M →ₗ[R] M₂ to M₂. See also LinearMap.applyₗ' for a version that works with two different semirings.

This is the LinearMap version of toAddMonoidHom.eval.

Instances For
def LinearMap.domRestrict' {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [] [] [] [Module R M] [Module R M₂] (p : ) :
(M →ₗ[R] M₂) →ₗ[R] { x // x p } →ₗ[R] M₂

Alternative version of domRestrict as a linear map.

Instances For
@[simp]
theorem LinearMap.domRestrict'_apply {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [] [] [] [Module R M] [Module R M₂] (f : M →ₗ[R] M₂) (p : ) (x : { x // x p }) :
↑(↑() f) x = f x
def LinearMap.smulRightₗ {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [] [] [] [Module R M] [Module R M₂] :
(M₂ →ₗ[R] R) →ₗ[R] M →ₗ[R] M₂ →ₗ[R] M

The family of linear maps M₂ → M parameterised by f ∈ M₂ → R, x ∈ M, is linear in f, x.

Instances For
@[simp]
theorem LinearMap.smulRightₗ_apply {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [] [] [] [Module R M] [Module R M₂] (f : M₂ →ₗ[R] R) (x : M) (c : M₂) :
↑(↑(LinearMap.smulRightₗ f) x) c = f c x
@[simp]
theorem addMonoidHomLequivNat_apply {A : Type u_20} {B : Type u_21} (R : Type u_22) [] [] [] [Module R B] (f : A →+ B) :
@[simp]
theorem addMonoidHomLequivNat_symm_apply {A : Type u_20} {B : Type u_21} (R : Type u_22) [] [] [] [Module R B] (f : A →ₗ[] B) :
def addMonoidHomLequivNat {A : Type u_20} {B : Type u_21} (R : Type u_22) [] [] [] [Module R B] :

The R-linear equivalence between additive morphisms A →+ B and ℕ-linear morphisms A →ₗ[ℕ] B.

Instances For
@[simp]
theorem addMonoidHomLequivInt_symm_apply {A : Type u_20} {B : Type u_21} (R : Type u_22) [] [] [] [Module R B] (f : A →ₗ[] B) :
@[simp]
theorem addMonoidHomLequivInt_apply {A : Type u_20} {B : Type u_21} (R : Type u_22) [] [] [] [Module R B] (f : A →+ B) :
def addMonoidHomLequivInt {A : Type u_20} {B : Type u_21} (R : Type u_22) [] [] [] [Module R B] :

The R-linear equivalence between additive morphisms A →+ B and ℤ-linear morphisms A →ₗ[ℤ] B.

Instances For

### Properties of submodules #

def Submodule.ofLe {R : Type u_1} {M : Type u_9} [] [] [Module R M] {p : } {p' : } (h : p p') :
{ x // x p } →ₗ[R] { x // x p' }

If two submodules p and p' satisfy p ⊆ p', then ofLe p p' is the linear map version of this inclusion.

Instances For
@[simp]
theorem Submodule.coe_ofLe {R : Type u_1} {M : Type u_9} [] [] [Module R M] {p : } {p' : } (h : p p') (x : { x // x p }) :
↑(↑() x) = x
theorem Submodule.ofLe_apply {R : Type u_1} {M : Type u_9} [] [] [Module R M] {p : } {p' : } (h : p p') (x : { x // x p }) :
↑() x = { val := x, property := h x (_ : x p) }
theorem Submodule.ofLe_injective {R : Type u_1} {M : Type u_9} [] [] [Module R M] {p : } {p' : } (h : p p') :
theorem Submodule.subtype_comp_ofLe {R : Type u_1} {M : Type u_9} [] [] [Module R M] (p : ) (q : ) (h : p q) :
@[simp]
theorem Submodule.subsingleton_iff (R : Type u_1) {M : Type u_9} [] [] [Module R M] :
@[simp]
theorem Submodule.nontrivial_iff (R : Type u_1) {M : Type u_9} [] [] [Module R M] :
instance Submodule.instUniqueSubmodule {R : Type u_1} {M : Type u_9} [] [] [Module R M] [] :
instance Submodule.unique' {R : Type u_1} {M : Type u_9} [] [] [Module R M] [] :
instance Submodule.instNontrivialSubmodule {R : Type u_1} {M : Type u_9} [] [] [Module R M] [] :
theorem Submodule.mem_right_iff_eq_zero_of_disjoint {R : Type u_1} {M : Type u_9} [] [] [Module R M] {p : } {p' : } (h : Disjoint p p') {x : { x // x p }} :
x p' x = 0
theorem Submodule.mem_left_iff_eq_zero_of_disjoint {R : Type u_1} {M : Type u_9} [] [] [Module R M] {p : } {p' : } (h : Disjoint p p') {x : { x // x p' }} :
x p x = 0
def Submodule.map {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] (f : F) (p : ) :
Submodule R₂ M₂

The pushforward of a submodule p ⊆ M by f : M → M₂

Instances For
@[simp]
theorem Submodule.map_coe {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] (f : F) (p : ) :
↑() = f '' p
theorem Submodule.map_toAddSubmonoid {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] (f : M →ₛₗ[σ₁₂] M₂) (p : ) :
theorem Submodule.map_toAddSubmonoid' {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] (f : M →ₛₗ[σ₁₂] M₂) (p : ) :
@[simp]
theorem Submodule.mem_map {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] {f : F} {p : } {x : M₂} :
x y, y p f y = x
theorem Submodule.mem_map_of_mem {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] {f : F} {p : } {r : M} (h : r p) :
f r
theorem Submodule.apply_coe_mem_map {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] (f : F) {p : } (r : { x // x p }) :
f r
@[simp]
theorem Submodule.map_id {R : Type u_1} {M : Type u_9} [] [] [Module R M] (p : ) :
Submodule.map LinearMap.id p = p
theorem Submodule.map_comp {R : Type u_1} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_9} {M₂ : Type u_12} {M₃ : Type u_13} [] [Semiring R₂] [Semiring R₃] [] [] [] [Module R M] [Module R₂ M₂] [Module R₃ M₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [] [] [] (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] M₃) (p : ) :
theorem Submodule.map_mono {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] {f : F} {p : } {p' : } :
p p'
@[simp]
theorem Submodule.map_zero {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (p : ) [] :
theorem Submodule.map_add_le {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (p : ) [] (f : M →ₛₗ[σ₁₂] M₂) (g : M →ₛₗ[σ₁₂] M₂) :
theorem Submodule.range_map_nonempty {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] (N : ) :
Set.Nonempty (Set.range fun ϕ => )
noncomputable def Submodule.equivMapOfInjective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] (f : F) (i : ) (p : ) :
{ x // x p } ≃ₛₗ[σ₁₂] { x // x }

The pushforward of a submodule by an injective linear map is linearly equivalent to the original submodule. See also LinearEquiv.submoduleMap for a computable version when f has an explicit inverse.

Instances For
@[simp]
theorem Submodule.coe_equivMapOfInjective_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] (f : F) (i : ) (p : ) (x : { x // x p }) :
↑(↑() x) = f x
def Submodule.comap {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] (f : F) (p : Submodule R₂ M₂) :

The pullback of a submodule p ⊆ M₂ along f : M → M₂

Instances For
@[simp]
theorem Submodule.comap_coe {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] (f : F) (p : Submodule R₂ M₂) :
↑() = f ⁻¹' p
@[simp]
theorem Submodule.mem_comap {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {x : M} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] {f : F} {p : Submodule R₂ M₂} :
x f x p
@[simp]
theorem Submodule.comap_id {R : Type u_1} {M : Type u_9} [] [] [Module R M] (p : ) :
Submodule.comap LinearMap.id p = p
theorem Submodule.comap_comp {R : Type u_1} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_9} {M₂ : Type u_12} {M₃ : Type u_13} [] [Semiring R₂] [Semiring R₃] [] [] [] [Module R M] [Module R₂ M₂] [Module R₃ M₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] M₃) (p : Submodule R₃ M₃) :
=
theorem Submodule.comap_mono {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] {f : F} {q : Submodule R₂ M₂} {q' : Submodule R₂ M₂} :
q q'
theorem Submodule.le_comap_pow_of_le_comap {R : Type u_1} {M : Type u_9} [] [] [Module R M] (p : ) {f : M →ₗ[R] M} (h : p ) (k : ) :
theorem Submodule.map_le_iff_le_comap {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] [] {f : F} {p : } {q : Submodule R₂ M₂} :
q p
theorem Submodule.gc_map_comap {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] [] (f : F) :
@[simp]
theorem Submodule.map_bot {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] [] (f : F) :
@[simp]
theorem Submodule.map_sup {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (p : ) (p' : ) {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] [] (f : F) :
@[simp]
theorem Submodule.map_iSup {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] [] {ι : Sort u_21} (f : F) (p : ι) :
Submodule.map f (⨆ (i : ι), p i) = ⨆ (i : ι), Submodule.map f (p i)
@[simp]
theorem Submodule.comap_top {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] (f : F) :
@[simp]
theorem Submodule.comap_inf {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (q : Submodule R₂ M₂) (q' : Submodule R₂ M₂) {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] (f : F) :
@[simp]
theorem Submodule.comap_iInf {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] [] {ι : Sort u_21} (f : F) (p : ιSubmodule R₂ M₂) :
Submodule.comap f (⨅ (i : ι), p i) = ⨅ (i : ι), Submodule.comap f (p i)
@[simp]
theorem Submodule.comap_zero {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (q : Submodule R₂ M₂) :
theorem Submodule.map_comap_le {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] [] (f : F) (q : Submodule R₂ M₂) :
theorem Submodule.le_comap_map {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] [] (f : F) (p : ) :
def Submodule.giMapComap {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] {f : F} (hf : ) [] :

map f and comap f form a GaloisInsertion when f is surjective.

Instances For
theorem Submodule.map_comap_eq_of_surjective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] {f : F} (hf : ) [] (p : Submodule R₂ M₂) :
theorem Submodule.map_surjective_of_surjective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] {f : F} (hf : ) [] :
theorem Submodule.comap_injective_of_surjective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] {f : F} (hf : ) [] :
theorem Submodule.map_sup_comap_of_surjective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] {f : F} (hf : ) [] (p : Submodule R₂ M₂) (q : Submodule R₂ M₂) :
theorem Submodule.map_iSup_comap_of_sujective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] {f : F} (hf : ) [] {ι : Sort u_21} (S : ιSubmodule R₂ M₂) :
Submodule.map f (⨆ (i : ι), Submodule.comap f (S i)) = iSup S
theorem Submodule.map_inf_comap_of_surjective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] {f : F} (hf : ) [] (p : Submodule R₂ M₂) (q : Submodule R₂ M₂) :
theorem Submodule.map_iInf_comap_of_surjective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] {f : F} (hf : ) [] {ι : Sort u_21} (S : ιSubmodule R₂ M₂) :
Submodule.map f (⨅ (i : ι), Submodule.comap f (S i)) = iInf S
theorem Submodule.comap_le_comap_iff_of_surjective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] {f : F} (hf : ) [] (p : Submodule R₂ M₂) (q : Submodule R₂ M₂) :
p q
theorem Submodule.comap_strictMono_of_surjective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] {f : F} (hf : ) [] :
def Submodule.gciMapComap {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] [] {f : F} (hf : ) :

map f and comap f form a GaloisCoinsertion when f is injective.

Instances For
theorem Submodule.comap_map_eq_of_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] [] {f : F} (hf : ) (p : ) :
theorem Submodule.comap_surjective_of_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] [] {f : F} (hf : ) :
theorem Submodule.map_injective_of_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] [] {f : F} (hf : ) :
theorem Submodule.comap_inf_map_of_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] [] {f : F} (hf : ) (p : ) (q : ) :
theorem Submodule.comap_iInf_map_of_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] [] {f : F} (hf : ) {ι : Sort u_21} (S : ι) :
Submodule.comap f (⨅ (i : ι), Submodule.map f (S i)) = iInf S
theorem Submodule.comap_sup_map_of_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] [] {f : F} (hf : ) (p : ) (q : ) :
theorem Submodule.comap_iSup_map_of_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] [] {f : F} (hf : ) {ι : Sort u_21} (S : ι) :
Submodule.comap f (⨆ (i : ι), Submodule.map f (S i)) = iSup S
theorem Submodule.map_le_map_iff_of_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] [] {f : F} (hf : ) (p : ) (q : ) :
p q
theorem Submodule.map_strictMono_of_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] [] {f : F} (hf : ) :
@[simp]
theorem Submodule.orderIsoMapComap_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {F : Type u_20} [SemilinearEquivClass F σ₁₂ M M₂] (f : F) (p : ) :
=
@[simp]
theorem Submodule.orderIsoMapComap_symm_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {F : Type u_20} [SemilinearEquivClass F σ₁₂ M M₂] (f : F) (p : Submodule R₂ M₂) :
=
def Submodule.orderIsoMapComap {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {F : Type u_20} [SemilinearEquivClass F σ₁₂ M M₂] (f : F) :
≃o Submodule R₂ M₂

A linear isomorphism induces an order isomorphism of submodules.

Instances For
theorem Submodule.map_inf_eq_map_inf_comap {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] [] {f : F} {p : } {p' : Submodule R₂ M₂} :
p' = Submodule.map f (p )
theorem Submodule.map_comap_subtype {R : Type u_1} {M : Type u_9} [] [] [Module R M] (p : ) (p' : ) :
= p p'
theorem Submodule.eq_zero_of_bot_submodule {R : Type u_1} {M : Type u_9} [] [] [Module R M] (b : { x // x }) :
b = 0
theorem LinearMap.iInf_invariant {R : Type u_1} {M : Type u_9} [] [] [Module R M] {σ : R →+* R} {ι : Sort u_21} (f : M →ₛₗ[σ] M) {p : ι} (hf : ∀ (i : ι) (v : M), v p if v p i) (v : M) :
v iInf pf v iInf p

The infimum of a family of invariant submodule of an endomorphism is also an invariant submodule.

theorem Submodule.neg_coe {R : Type u_1} {M : Type u_9} [Ring R] [] [Module R M] (p : ) :
-p = p
@[simp]
theorem Submodule.map_neg {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [Ring R] [] [Module R M] (p : ) [] [Module R M₂] (f : M →ₗ[R] M₂) :
theorem Submodule.comap_smul {K : Type u_7} {V : Type u_18} {V₂ : Type u_19} [] [] [Module K V] [] [Module K V₂] (f : V →ₗ[K] V₂) (p : Submodule K V₂) (a : K) (h : a 0) :
theorem Submodule.map_smul {K : Type u_7} {V : Type u_18} {V₂ : Type u_19} [] [] [Module K V] [] [Module K V₂] (f : V →ₗ[K] V₂) (p : ) (a : K) (h : a 0) :
theorem Submodule.comap_smul' {K : Type u_7} {V : Type u_18} {V₂ : Type u_19} [] [] [Module K V] [] [Module K V₂] (f : V →ₗ[K] V₂) (p : Submodule K V₂) (a : K) :
Submodule.comap (a f) p = ⨅ (_ : a 0),
theorem Submodule.map_smul' {K : Type u_7} {V : Type u_18} {V₂ : Type u_19} [] [] [Module K V] [] [Module K V₂] (f : V →ₗ[K] V₂) (p : ) (a : K) :
Submodule.map (a f) p = ⨆ (_ : a 0),

### Properties of linear maps #

@[simp]
theorem LinearMap.map_finsupp_sum {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} {ι : Type u_17} [] [Semiring R₂] [] [] {σ₁₂ : R →+* R₂} [Module R M] [Module R₂ M₂] {γ : Type u_20} [Zero γ] (f : M →ₛₗ[σ₁₂] M₂) {t : ι →₀ γ} {g : ιγM} :
f () = Finsupp.sum t fun i d => f (g i d)
theorem LinearMap.coe_finsupp_sum {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} {ι : Type u_17} [] [Semiring R₂] [] [] {σ₁₂ : R →+* R₂} [Module R M] [Module R₂ M₂] {γ : Type u_20} [Zero γ] (t : ι →₀ γ) (g : ιγM →ₛₗ[σ₁₂] M₂) :
↑() = ↑(Finsupp.sum t fun i d => g i d)
@[simp]
theorem LinearMap.finsupp_sum_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} {ι : Type u_17} [] [Semiring R₂] [] [] {σ₁₂ : R →+* R₂} [Module R M] [Module R₂ M₂] {γ : Type u_20} [Zero γ] (t : ι →₀ γ) (g : ιγM →ₛₗ[σ₁₂] M₂) (b : M) :
↑() b = Finsupp.sum t fun i d => ↑(g i d) b
theorem LinearMap.coe_dfinsupp_sum {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} {ι : Type u_17} [] [Semiring R₂] [] [] {σ₁₂ : R →+* R₂} [Module R M] [Module R₂ M₂] {γ : ιType u_20} [] [(i : ι) → Zero (γ i)] [(i : ι) → (x : γ i) → Decidable (x 0)] (t : Π₀ (i : ι), γ i) (g : (i : ι) → γ iM →ₛₗ[σ₁₂] M₂) :
↑() = ↑(DFinsupp.sum t fun i d => g i d)
@[simp]
theorem LinearMap.dfinsupp_sum_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} {ι : Type u_17} [] [Semiring R₂] [] [] {σ₁₂ : R →+* R₂} [Module R M] [Module R₂ M₂] {γ : ιType u_20} [] [(i : ι) → Zero (γ i)] [(i : ι) → (x : γ i) → Decidable (x 0)] (t : Π₀ (i : ι), γ i) (g : (i : ι) → γ iM →ₛₗ[σ₁₂] M₂) (b : M) :
↑() b = DFinsupp.sum t fun i d => ↑(g i d) b
@[simp]
theorem LinearMap.map_dfinsupp_sumAddHom {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} {ι : Type u_17} [] [Semiring R₂] [] [] {σ₁₂ : R →+* R₂} [Module R M] [Module R₂ M₂] {γ : ιType u_20} [] [(i : ι) → AddZeroClass (γ i)] (f : M →ₛₗ[σ₁₂] M₂) {t : Π₀ (i : ι), γ i} {g : (i : ι) → γ i →+ M} :
f (↑() t) = ↑(DFinsupp.sumAddHom fun i => ) t
theorem LinearMap.map_codRestrict {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₂₁ : R₂ →+* R} [] (p : ) (f : M₂ →ₛₗ[σ₂₁] M) (h : ∀ (c : M₂), f c p) (p' : Submodule R₂ M₂) :
theorem LinearMap.comap_codRestrict {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₂₁ : R₂ →+* R} (p : ) (f : M₂ →ₛₗ[σ₂₁] M) (hf : ∀ (c : M₂), f c p) (p' : Submodule R { x // x p }) :
def LinearMap.range {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F τ₁₂ M M₂] [] (f : F) :
Submodule R₂ M₂

The range of a linear map f : M → M₂ is a submodule of M₂. See Note [range copy pattern].

Instances For
theorem LinearMap.range_coe {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F τ₁₂ M M₂] [] (f : F) :
↑() =
theorem LinearMap.range_toAddSubmonoid {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [] (f : M →ₛₗ[τ₁₂] M₂) :
@[simp]
theorem LinearMap.mem_range {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F τ₁₂ M M₂] [] {f : F} {x : M₂} :
y, f y = x
theorem LinearMap.range_eq_map {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F τ₁₂ M M₂] [] (f : F) :
theorem LinearMap.mem_range_self {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F τ₁₂ M M₂] [] (f : F) (x : M) :
f x
@[simp]
theorem LinearMap.range_id {R : Type u_1} {M : Type u_9} [] [] [Module R M] :
LinearMap.range LinearMap.id =
theorem LinearMap.range_comp {R : Type u_1} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_9} {M₂ : Type u_12} {M₃ : Type u_13} [] [Semiring R₂] [Semiring R₃] [] [] [] [Module R M] [Module R₂ M₂] [Module R₃ M₃] {τ₁₂ : R →+* R₂} {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [RingHomCompTriple τ₁₂ τ₂₃ τ₁₃] [] [] [] (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) :
theorem LinearMap.range_comp_le_range {R : Type u_1} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_9} {M₂ : Type u_12} {M₃ : Type u_13} [] [Semiring R₂] [Semiring R₃] [] [] [] [Module R M] [Module R₂ M₂] [Module R₃ M₃] {τ₁₂ : R →+* R₂} {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [RingHomCompTriple τ₁₂ τ₂₃ τ₁₃] [] [] (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) :
theorem LinearMap.range_eq_top {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F τ₁₂ M M₂] [] {f : F} :
theorem LinearMap.range_le_iff_comap {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F τ₁₂ M M₂] [] {f : F} {p : Submodule R₂ M₂} :
theorem LinearMap.map_le_range {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F τ₁₂ M M₂] [] {f : F} {p : } :
@[simp]
theorem LinearMap.range_neg {R : Type u_21} {R₂ : Type u_22} {M : Type u_23} {M₂ : Type u_24} [] [Ring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [] (f : M →ₛₗ[τ₁₂] M₂) :
def LinearMap.eqLocus {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F τ₁₂ M M₂] (f : F) (g : F) :

A linear map version of AddMonoidHom.eqLocusM

Instances For
@[simp]
theorem LinearMap.mem_eqLocus {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F τ₁₂ M M₂] {x : M} {f : F} {g : F} :
x f x = g x
theorem LinearMap.eqLocus_toAddSubmonoid {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F τ₁₂ M M₂] (f : F) (g : F) :
@[simp]
theorem LinearMap.eqLocus_eq_top {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F τ₁₂ M M₂] {f : F} {g : F} :
f = g
@[simp]
theorem LinearMap.eqLocus_same {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F τ₁₂ M M₂] (f : F) :
theorem LinearMap.le_eqLocus {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F τ₁₂ M M₂] {f : F} {g : F} {S : } :
S Set.EqOn f g S
theorem LinearMap.eqOn_sup {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F τ₁₂ M M₂] {f : F} {g : F} {S : } {T : } (hS : Set.EqOn f g S) (hT : Set.EqOn f g T) :
Set.EqOn f g ↑(S T)
theorem LinearMap.ext_on_codisjoint {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F τ₁₂ M M₂] {f : F} {g : F} {S : } {T : } (hST : ) (hS : Set.EqOn f g S) (hT : Set.EqOn f g T) :
f = g
@[simp]
theorem LinearMap.iterateRange_coe {R : Type u_1} {M : Type u_9} [] [] [Module R M] (f : M →ₗ[R] M) (n : ) :
↑() n = LinearMap.range (f ^ n)
def LinearMap.iterateRange {R : Type u_1} {M : Type u_9} [] [] [Module R M] (f : M →ₗ[R] M) :

The decreasing sequence of submodules consisting of the ranges of the iterates of a linear map.

Instances For
@[reducible]
def LinearMap.rangeRestrict {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [] (f : M →ₛₗ[τ₁₂] M₂) :
M →ₛₗ[τ₁₂] { x // }

Restrict the codomain of a linear map f to f.range.

This is the bundled version of Set.rangeFactorization.

Instances For
instance LinearMap.fintypeRange {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [] [] [] (f : M →ₛₗ[τ₁₂] M₂) :
Fintype { x // }

The range of a linear map is finite if the domain is finite. Note: this instance can form a diamond with Subtype.fintype in the presence of Fintype M₂.

def LinearMap.ker {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F τ₁₂ M M₂] (f : F) :

The kernel of a linear map f : M → M₂ is defined to be comap f ⊥. This is equivalent to the set of x : M such that f x = 0. The kernel is a submodule of M.

Instances For
@[simp]
theorem LinearMap.mem_ker {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F τ₁₂ M M₂] {f : F} {y : M} :
f y = 0
@[simp]
theorem LinearMap.ker_id {R : Type u_1} {M : Type u_9} [] [] [Module R M] :
LinearMap.ker LinearMap.id =
@[simp]
theorem LinearMap.map_coe_ker {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F τ₁₂ M M₂] (f : F) (x : { x // }) :
f x = 0
theorem LinearMap.ker_toAddSubmonoid {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) :
theorem LinearMap.comp_ker_subtype {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) :
theorem LinearMap.ker_comp {R : Type u_1} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_9} {M₂ : Type u_12} {M₃ : Type u_13} [] [Semiring R₂] [Semiring R₃] [] [] [] [Module R M] [Module R₂ M₂] [Module R₃ M₃] {τ₁₂ : R →+* R₂} {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [RingHomCompTriple τ₁₂ τ₂₃ τ₁₃] (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) :
=
theorem LinearMap.ker_le_ker_comp {R : Type u_1} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_9} {M₂ : Type u_12} {M₃ : Type u_13} [] [Semiring R₂] [Semiring R₃] [] [] [] [Module R M] [Module R₂ M₂] [Module R₃ M₃] {τ₁₂ : R →+* R₂} {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [RingHomCompTriple τ₁₂ τ₂₃ τ₁₃] (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) :
theorem LinearMap.disjoint_ker {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F τ₁₂ M M₂] {f : F} {p : } :
∀ (x : M), x pf x = 0x = 0
theorem LinearMap.ker_eq_bot' {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F τ₁₂ M M₂] {f : F} :
∀ (m : M), f m = 0m = 0
theorem LinearMap.ker_eq_bot_of_inverse {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁] {f : M →ₛₗ[τ₁₂] M₂} {g : M₂ →ₛₗ[τ₂₁] M} (h : = LinearMap.id) :
theorem LinearMap.le_ker_iff_map {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F τ₁₂ M M₂] [] {f : F} {p : } :
theorem LinearMap.ker_codRestrict {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₂₁ : R₂ →+* R} (p : ) (f : M₂ →ₛₗ[τ₂₁] M) (hf : ∀ (c : M₂), f c p) :
theorem LinearMap.range_codRestrict {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₂₁ : R₂ →+* R} [] (p : ) (f : M₂ →ₛₗ[τ₂₁] M) (hf : ∀ (c : M₂), f c p) :
theorem LinearMap.ker_restrict {R : Type u_1} {M : Type u_9} {M₁ : Type u_11} [] [] [Module R M] [] [Module R M₁] {p : } {q : Submodule R M₁} {f : M →ₗ[R] M₁} (hf : ∀ (x : M), x pf x q) :
theorem Submodule.map_comap_eq {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F τ₁₂ M M₂] [] (f : F) (q : Submodule R₂ M₂) :
theorem Submodule.map_comap_eq_self {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F τ₁₂ M M₂] [] {f : F} {q : Submodule R₂ M₂} (h : ) :
@[simp]
theorem LinearMap.ker_zero {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} :
@[simp]
theorem LinearMap.range_zero {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [] :
theorem LinearMap.ker_eq_top {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {f : M →ₛₗ[τ₁₂] M₂} :
f = 0
theorem LinearMap.range_le_bot_iff {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [] (f : M →ₛₗ[τ₁₂] M₂) :
f = 0
theorem LinearMap.range_eq_bot {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [] {f : M →ₛₗ[τ₁₂] M₂} :
f = 0
theorem LinearMap.range_le_ker_iff {R : Type u_1} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_9} {M₂ : Type u_12} {M₃ : Type u_13} [] [Semiring R₂] [Semiring R₃] [] [] [] [Module R M] [Module R₂ M₂] [Module R₃ M₃] {τ₁₂ : R →+* R₂} {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [RingHomCompTriple τ₁₂ τ₂₃ τ₁₃] [] {f : M →ₛₗ[τ₁₂] M₂} {g : M₂ →ₛₗ[τ₂₃] M₃} :
= 0
theorem LinearMap.comap_le_comap_iff {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F τ₁₂ M M₂] [] {f : F} (hf : ) {p : Submodule R₂ M₂} {p' : Submodule R₂ M₂} :
p p'
theorem LinearMap.comap_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F τ₁₂ M M₂] [] {f : F} (hf : ) :
theorem LinearMap.ker_eq_bot_of_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F τ₁₂ M M₂] {f : F} (hf : ) :
@[simp]
theorem LinearMap.iterateKer_coe {R : Type u_1} {M : Type u_9} [] [] [Module R M] (f : M →ₗ[R] M) (n : ) :
↑() n = LinearMap.ker (f ^ n)
def LinearMap.iterateKer {R : Type u_1} {M : Type u_9} [] [] [Module R M] (f : M →ₗ[R] M) :

The increasing sequence of submodules consisting of the kernels of the iterates of a linear map.

Instances For
theorem LinearMap.range_toAddSubgroup {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Ring R] [Ring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [] (f : M →ₛₗ[τ₁₂] M₂) :
theorem LinearMap.ker_toAddSubgroup {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Ring R] [Ring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) :
theorem LinearMap.eqLocus_eq_ker_sub {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Ring R] [Ring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) (g : M →ₛₗ[τ₁₂] M₂) :
theorem LinearMap.sub_mem_ker_iff {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Ring R] [Ring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F τ₁₂ M M₂] {f : F} {x : M} {y : M} :
x - y f x = f y
theorem LinearMap.disjoint_ker' {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Ring R] [Ring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F τ₁₂ M M₂] {f : F} {p : } :
∀ (x : M), x p∀ (y : M), y pf x = f yx = y
theorem LinearMap.injOn_of_disjoint_ker {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Ring R] [Ring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F τ₁₂ M M₂] {f : F} {p : } {s : Set M} (h : s p) (hd : ) :
Set.InjOn (f) s
theorem LinearMapClass.ker_eq_bot {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Ring R] [Ring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (F : Type u_20) [sc : SemilinearMapClass F τ₁₂ M M₂] {f : F} :
theorem LinearMap.ker_eq_bot {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Ring R] [Ring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {f : M →ₛₗ[τ₁₂] M₂} :
theorem LinearMap.ker_le_iff {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Ring R] [Ring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F τ₁₂ M M₂] {f : F} [] {p : } :
y, f ⁻¹' {y} p
theorem LinearMap.ker_smul {K : Type u_7} {V : Type u_18} {V₂ : Type u_19} [] [] [Module K V] [] [Module K V₂] (f : V →ₗ[K] V₂) (a : K) (h : a 0) :
theorem LinearMap.ker_smul' {K : Type u_7} {V : Type u_18} {V₂ : Type u_19} [] [] [Module K V] [] [Module K V₂] (f : V →ₗ[K] V₂) (a : K) :
LinearMap.ker (a f) = ⨅ (_ : a 0),
theorem LinearMap.range_smul {K : Type u_7} {V : Type u_18} {V₂ : Type u_19} [] [] [Module K V] [] [Module K V₂] (f : V →ₗ[K] V₂) (a : K) (h : a 0) :
theorem LinearMap.range_smul' {K : Type u_7} {V : Type u_18} {V₂ : Type u_19} [] [] [Module K V] [] [Module K V₂] (f : V →ₗ[K] V₂) (a : K) :
LinearMap.range (a f) = ⨆ (_ : a 0),
theorem IsLinearMap.isLinearMap_add {R : Type u_1} {M : Type u_9} [] [] [Module R M] :
IsLinearMap R fun x => x.fst + x.snd
theorem IsLinearMap.isLinearMap_sub {R : Type u_20} {M : Type u_21} [] [] [Module R M] :
IsLinearMap R fun x => x.fst - x.snd
@[simp]
theorem Submodule.map_top {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F τ₁₂ M M₂] [] (f : F) :
@[simp]
theorem Submodule.comap_bot {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F τ₁₂ M M₂] (f : F) :
@[simp]
theorem Submodule.ker_subtype {R : Type u_1} {M : Type u_9} [] [] [Module R M] (p : ) :
@[simp]
theorem Submodule.range_subtype {R : Type u_1} {M : Type u_9} [] [] [Module R M] (p : ) :
theorem Submodule.map_subtype_le {R : Type u_1} {M : Type u_9} [] [] [Module R M] (p : ) (p' : Submodule R { x // x p }) :
p
theorem Submodule.map_subtype_top {R : Type u_1} {M : Type u_9} [] [] [Module R M] (p : ) :

Under the canonical linear map from a submodule p to the ambient space M, the image of the maximal submodule of p is just p .

@[simp]
theorem Submodule.comap_subtype_eq_top {R : Type u_1} {M : Type u_9} [] [] [Module R M] {p : } {p' : } :
p p'
@[simp]
theorem Submodule.comap_subtype_self {R : Type u_1} {M : Type u_9} [] [] [Module R M] (p : ) :
@[simp]
theorem Submodule.ker_ofLe {R : Type u_1} {M : Type u_9} [] [] [Module R M] (p : ) (p' : ) (h : p p') :
theorem Submodule.range_ofLe {R : Type u_1} {M : Type u_9} [] [] [Module R M] (p : ) (q : ) (h : p q) :
@[simp]
theorem Submodule.map_subtype_range_ofLe {R : Type u_1} {M : Type u_9} [] [] [Module R M] {p : } {p' : } (h : p p') :
= p
theorem Submodule.disjoint_iff_comap_eq_bot {R : Type u_1} {M : Type u_9} [] [] [Module R M] {p : } {q : } :
def Submodule.MapSubtype.relIso {R : Type u_1} {M : Type u_9} [] [] [Module R M] (p : ) :
Submodule R { x // x p } ≃o { p' // p' p }

If N ⊆ M then submodules of N are the same as submodules of M contained in N

Instances For
def Submodule.MapSubtype.orderEmbedding {R : Type u_1} {M : Type u_9} [] [] [Module R M] (p : ) :
Submodule R { x // x p } ↪o

If p ⊆ M is a submodule, the ordering of submodules of p is embedded in the ordering of submodules of M.

Instances For
@[simp]
theorem Submodule.map_subtype_embedding_eq {R : Type u_1} {M : Type u_9} [] [] [Module R M] (p : ) (p' : Submodule R { x // x p }) :
theorem LinearMap.ker_eq_bot_of_cancel {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {f : M →ₛₗ[τ₁₂] M₂} (h : ∀ (u v : { x // } →ₗ[R] M), = u = v) :

A monomorphism is injective.

theorem LinearMap.range_comp_of_range_eq_top {R : Type u_1} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_9} {M₂ : Type u_12} {M₃ : Type u_13} [] [Semiring R₂] [Semiring R₃] [] [] [] [Module R M] [Module R₂ M₂] [Module R₃ M₃] {τ₁₂ : R →+* R₂} {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [RingHomCompTriple τ₁₂ τ₂₃ τ₁₃] [] [] [] {f : M →ₛₗ[τ₁₂] M₂} (g : M₂ →ₛₗ[τ₂₃] M₃) (hf : ) :
theorem LinearMap.ker_comp_of_ker_eq_bot {R : Type u_1} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_9} {M₂ : Type u_12} {M₃ : Type u_13} [] [Semiring R₂] [Semiring R₃] [] [] [] [Module R M] [Module R₂ M₂] [Module R₃ M₃] {τ₁₂ : R →+* R₂} {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [RingHomCompTriple τ₁₂ τ₂₃ τ₁₃] (f : M →ₛₗ[τ₁₂] M₂) {g : M₂ →ₛₗ[τ₂₃] M₃} (hg : ) :
def LinearMap.submoduleImage {R : Type u_1} {M : Type u_9} [] [] [Module R M] {M' : Type u_20} [] [Module R M'] {O : } (ϕ : { x // x O } →ₗ[R] M') (N : ) :

If O is a submodule of M, and Φ : O →ₗ M' is a linear map, then (ϕ : O →ₗ M').submoduleImage N is ϕ(N) as a submodule of M'

Instances For
@[simp]
theorem LinearMap.mem_submoduleImage {R : Type u_1} {M : Type u_9} [] [] [Module R M] {M' : Type u_20} [] [Module R M'] {O : } {ϕ : { x // x O } →ₗ[R] M'} {N : } {x : M'} :
y yO x, ϕ { val := y, property := yO } = x
theorem LinearMap.mem_submoduleImage_of_le {R : Type u_1} {M : Type u_9} [] [] [Module R M] {M' : Type u_20} [] [Module R M'] {O : } {ϕ : { x // x O } →ₗ[R] M'} {N : } (hNO : N O) {x : M'} :
y yN, ϕ { val := y, property := hNO y yN } = x
theorem LinearMap.submoduleImage_apply_ofLe {R : Type u_1} {M : Type u_9} [] [] [Module R M] {M' : Type u_20} [] [Module R M'] {O : } (ϕ : { x // x O } →ₗ[R] M') (N : ) (hNO : N O) :
@[simp]
theorem LinearMap.range_rangeRestrict {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [] [] [] [Module R M] [Module R M₂] (f : M →ₗ[R] M₂) :
@[simp]
theorem LinearMap.ker_rangeRestrict {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [] [] [] [Module R M] [Module R M₂] (f : M →ₗ[R] M₂) :

### Linear equivalences #

instance LinearEquiv.instZeroLinearEquiv {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [] [] :
Zero (M ≃ₛₗ[σ₁₂] M₂)

Between two zero modules, the zero map is an equivalence.

@[simp]
theorem LinearEquiv.zero_symm {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [] [] :
@[simp]
theorem LinearEquiv.coe_zero {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [] [] :
0 = 0
theorem LinearEquiv.zero_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [] [] (x : M) :
0 x = 0
instance LinearEquiv.instUniqueLinearEquiv {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [] [] :
Unique (M ≃ₛₗ[σ₁₂] M₂)

Between two zero modules, the zero map is the only equivalence.

instance LinearEquiv.uniqueOfSubsingleton {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [] [] :
Unique (M ≃ₛₗ[σ₁₂] M₂)
@[simp]
theorem LinearEquiv.map_sum {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} {ι : Type u_17} [] [Semiring R₂] [] [] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) {s : } (u : ιM) :
e (Finset.sum s fun i => u i) = Finset.sum s fun i => e (u i)
theorem LinearEquiv.map_eq_comap {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) {p : } :
Submodule.map (e) p = Submodule.comap (↑()) p
def LinearEquiv.submoduleMap {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) (p : ) :
{ x // x p } ≃ₛₗ[σ₁₂] { x // x Submodule.map (e) p }

A linear equivalence of two modules restricts to a linear equivalence from any submodule p of the domain onto the image of that submodule.

This is the linear version of AddEquiv.submonoidMap and AddEquiv.subgroupMap.

This is LinearEquiv.ofSubmodule' but with map on the right instead of comap on the left.

Instances For
@[simp]
theorem LinearEquiv.submoduleMap_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) (p : ) (x : { x // x p }) :
↑(↑() x) = e x
@[simp]
theorem LinearEquiv.submoduleMap_symm_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) (p : ) (x : { x // x Submodule.map (e) p }) :
↑(↑() x) = ↑() x
@[simp]
theorem LinearEquiv.map_finsupp_sum {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} {ι : Type u_17} {γ : Type u_20} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] [Zero γ] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁] [RingHomInvPair τ₂₁ τ₁₂] (f : M ≃ₛₗ[τ₁₂] M₂) {t : ι →₀ γ} {g : ιγM} :
f () = Finsupp.sum t fun i d => f (g i d)
@[simp]
theorem LinearEquiv.map_dfinsupp_sumAddHom {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} {ι : Type u_17} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁] [RingHomInvPair τ₂₁ τ₁₂] {γ : ιType u_20} [] [(i : ι) → AddZeroClass (γ i)] (f : M ≃ₛₗ[τ₁₂] M₂) (t : Π₀ (i : ι), γ i) (g : (i : ι) → γ i →+ M) :
f (↑() t) = ↑(DFinsupp.sumAddHom fun i => ) t
def LinearEquiv.curry (R : Type u_1) (V : Type u_18) (V₂ : Type u_19) [] :
(V × V₂R) ≃ₗ[R] VV₂R

Linear equivalence between a curried and uncurried function. Differs from TensorProduct.curry.

Instances For
@[simp]
theorem LinearEquiv.coe_curry (R : Type u_1) (V : Type u_18) (V₂ : Type u_19) [] :
↑() = Function.curry
@[simp]
theorem LinearEquiv.coe_curry_symm (R : Type u_1) (V : Type u_18) (V₂ : Type u_19) [] :
↑(LinearEquiv.symm ()) = Function.uncurry
def LinearEquiv.ofEq {R : Type u_1} {M : Type u_9} [] [] {module_M : Module R M} (p : ) (q : ) (h : p = q) :
{ x // x p } ≃ₗ[R] { x // x q }

Linear equivalence between two equal submodules.

Instances For
@[simp]
theorem LinearEquiv.coe_ofEq_apply {R : Type u_1} {M : Type u_9} [] [] {module_M : Module R M} {p : }