# 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

### Properties of linear maps #

@[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.

Equations
• One or more equations did not get rendered due to their size.
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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem addMonoidEndRingEquivInt_apply (A : Type u_20) [] :
∀ (a : A →+ A), = .toFun a
@[simp]
theorem addMonoidEndRingEquivInt_symm_apply (A : Type u_20) [] :
∀ (a : A →ₗ[] A), = .invFun a
def addMonoidEndRingEquivInt (A : Type u_20) [] :

Ring equivalence between additive group endomorphisms of an AddCommGroup A and ℤ-module endomorphisms of A.

Equations
• = let __src := ; { toEquiv := { toFun := __src.toFun, invFun := __src.invFun, left_inv := , right_inv := }, map_mul' := , map_add' := }
Instances For

### Properties of linear maps #

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} [FunLike F M M₂] [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].

Equations
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} [FunLike F M M₂] [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} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [] {f : F} {x : M₂} :
∃ (y : M), 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} [FunLike F M M₂] [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} [FunLike F M M₂] [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} [FunLike F M M₂] [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} [FunLike F M M₂] [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} [FunLike F M M₂] [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₂) :
theorem LinearMap.range_domRestrict_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 : M →ₛₗ[τ₁₂] M₂) (S : ) :
@[simp]
theorem AddMonoidHom.coe_toIntLinearMap_range {M : Type u_21} {M₂ : Type u_22} [] [] (f : M →+ M₂) :
theorem Submodule.map_comap_eq_of_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} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [] {f : F} {p : Submodule R₂ M₂} (h : ) :
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} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] (f : F) (g : F) :

A linear map version of AddMonoidHom.eqLocusM

Equations
• One or more equations did not get rendered due to their size.
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} [FunLike F M M₂] [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} [FunLike F M M₂] [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} [FunLike F M M₂] [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} [FunLike F M M₂] [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} [FunLike F M M₂] [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} [FunLike F M M₂] [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} [FunLike F M M₂] [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 : ) :
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.

Equations
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 →ₛₗ[τ₁₂] ()

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

This is the bundled version of Set.rangeFactorization.

Equations
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₂) :

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₂.

Equations
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 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} [FunLike F M M₂] [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} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [] {f : F} {q : Submodule R₂ M₂} (h : ) :
@[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.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} [FunLike F M M₂] [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} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [] {f : F} (hf : ) :
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.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.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} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] {f : F} [] {p : } :
∃ y ∈ , f ⁻¹' {y} p
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 : M × M) => x.1 + x.2
theorem IsLinearMap.isLinearMap_sub {R : Type u_20} {M : Type u_21} [] [] [Module R M] :
IsLinearMap R fun (x : M × M) => x.1 - x.2
@[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} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [] (f : F) :
@[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 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 : ) :
theorem Submodule.range_inclusion {R : Type u_1} {M : Type u_9} [] [] [Module R M] (p : ) (q : ) (h : p q) :
@[simp]
theorem Submodule.map_subtype_range_inclusion {R : Type u_1} {M : Type u_9} [] [] [Module R M] {p : } {p' : } (h : p p') :
def Submodule.MapSubtype.relIso {R : Type u_1} {M : Type u_9} [] [] [Module R M] (p : ) :
Submodule R p ≃o { p' : // p' p }

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def Submodule.MapSubtype.orderEmbedding {R : Type u_1} {M : Type u_9} [] [] [Module R M] (p : ) :
Submodule R p ↪o

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Submodule.map_subtype_embedding_eq {R : Type u_1} {M : Type u_9} [] [] [Module R M] (p : ) (p' : Submodule R 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 : () →ₗ[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 : ) :
def LinearMap.submoduleImage {R : Type u_1} {M : Type u_9} [] [] [Module R M] {M' : Type u_20} [] [Module R M'] {O : } (ϕ : 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'

Equations
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 : } {ϕ : O →ₗ[R] M'} {N : } {x : M'} :
∃ (y : M) (yO : y O), y N ϕ { 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 : } {ϕ : O →ₗ[R] M'} {N : } (hNO : N O) {x : M'} :
∃ (y : M) (yN : y N), ϕ { val := y, property := } = x
theorem LinearMap.submoduleImage_apply_of_le {R : Type u_1} {M : Type u_9} [] [] [Module R M] {M' : Type u_20} [] [Module R M'] {O : } (ϕ : O →ₗ[R] M') (N : ) (hNO : N O) :
= LinearMap.range (ϕ ∘ₗ )
@[simp]
theorem LinearMap.range_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₂) :
theorem LinearMap.surjective_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₂) :
@[simp]
theorem LinearMap.ker_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₂) :

### 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.

Equations
• One or more equations did not get rendered due to their size.
@[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.

Equations
• LinearEquiv.instUniqueLinearEquiv = { toInhabited := { default := 0 }, uniq := }
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₂)
Equations
• LinearEquiv.uniqueOfSubsingleton = inferInstance
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.

Equations
• One or more equations did not get rendered due to their size.
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) :
p ≃ₗ[R] q

Linear equivalence between two equal submodules.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem LinearEquiv.coe_ofEq_apply {R : Type u_1} {M : Type u_9} [] [] {module_M : Module R M} {p : } {q : } (h : p = q) (x : p) :
(() x) = x
@[simp]
theorem LinearEquiv.ofEq_symm {R : Type u_1} {M : Type u_9} [] [] {module_M : Module R M} {p : } {q : } (h : p = q) :
@[simp]
theorem LinearEquiv.ofEq_rfl {R : Type u_1} {M : Type u_9} [] [] {module_M : Module R M} {p : } :
=
def LinearEquiv.ofSubmodules {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 : ) (q : Submodule R₂ M₂) (h : Submodule.map (e) p = q) :
p ≃ₛₗ[σ₁₂] q

A linear equivalence which maps a submodule of one module onto another, restricts to a linear equivalence of the two submodules.

Equations
Instances For
@[simp]
theorem LinearEquiv.ofSubmodules_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 : } {q : Submodule R₂ M₂} (h : = q) (x : p) :
(() x) = e x
@[simp]
theorem LinearEquiv.ofSubmodules_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 : } {q : Submodule R₂ M₂} (h : = q) (x : q) :
((LinearEquiv.symm ()) x) = () x
def LinearEquiv.ofSubmodule' {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} [Module R M] [Module R₂ M₂] (f : M ≃ₛₗ[σ₁₂] M₂) (U : Submodule R₂ M₂) :
(Submodule.comap (f) U) ≃ₛₗ[σ₁₂] U

A linear equivalence of two modules restricts to a linear equivalence from the preimage of any submodule to that submodule.

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

Equations
Instances For
theorem LinearEquiv.ofSubmodule'_toLinearMap {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} [Module R M] [Module R₂ M₂] (f : M ≃ₛₗ[σ₁₂] M₂) (U : Submodule R₂ M₂) :
@[simp]
theorem LinearEquiv.ofSubmodule'_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} [Module R M] [Module R₂ M₂] (f : M ≃ₛₗ[σ₁₂] M₂) (U : Submodule R₂ M₂) (x : (Submodule.comap (f) U)) :
(() x) = f x
@[simp]
theorem LinearEquiv.ofSubmodule'_symm_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} [Module R M] [Module R₂ M₂] (f : M ≃ₛₗ[σ₁₂] M₂) (U : Submodule R₂ M₂) (x : U) :
( x) = () x
def LinearEquiv.ofTop {R : Type u_1} {M : Type u_9} [] [] {module_M : Module R M} (p : ) (h : p = ) :
p ≃ₗ[R] M

The top submodule of M is linearly equivalent to M.

Equations
• = let __src := ; { toLinearMap := __src, invFun := fun (x : M) => { val := x, property := }, left_inv := , right_inv := }
Instances For
@[simp]
theorem LinearEquiv.ofTop_apply {R : Type u_1} {M : Type u_9} [] [] {module_M : Module R M} (p : ) {h : p = } (x : p) :
() x = x
@[simp]
theorem LinearEquiv.coe_ofTop_symm_apply {R : Type u_1} {M : Type u_9} [] [] {module_M : Module R M} (p : ) {h : p = } (x : M) :
(() x) = x
theorem LinearEquiv.ofTop_symm_apply {R : Type u_1} {M : Type u_9} [] [] {module_M : Module R M} (p : ) {h : p = } (x : M) :
() x = { val := x, property := }
def LinearEquiv.ofLinear {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 σ₂₁ σ₁₂} (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₁] M) (h₁ : = LinearMap.id) (h₂ : = LinearMap.id) :
M ≃ₛₗ[σ₁₂] M₂

If a linear map has an inverse, it is a linear equivalence.

Equations
• LinearEquiv.ofLinear f g h₁ h₂ = { toLinearMap := f, invFun := g, left_inv := , right_inv := }
Instances For
@[simp]
theorem LinearEquiv.ofLinear_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 σ₂₁ σ₁₂} (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₁] M) {h₁ : = LinearMap.id} {h₂ : = LinearMap.id} (x : M) :
(LinearEquiv.ofLinear f g h₁ h₂) x = f x
@[simp]
theorem LinearEquiv.ofLinear_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 σ₂₁ σ₁₂} (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₁] M) {h₁ : = LinearMap.id} {h₂ : = LinearMap.id} (x : M₂) :
(LinearEquiv.symm (LinearEquiv.ofLinear f g h₁ h₂)) x = g x
@[simp]
theorem LinearEquiv.range {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₂) :
@[simp]
theorem LinearEquivClass.range {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} [Module R M] [Module R₂ M₂] {F : Type u_20} [EquivLike F M M₂] [SemilinearEquivClass F σ₁₂ M M₂] (e : F) :
theorem LinearEquiv.eq_bot_of_equiv {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [] [Semiring R₂] [] [] {module_M : Module R M} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (p : ) [Module R₂ M₂] (e : p ≃ₛₗ[σ₁₂] ) :
p =
@[simp]
theorem LinearEquiv.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_M : Module R M} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) (h : M₂ →ₛₗ[σ₂₃] M₃) [] [] :
def LinearEquiv.ofLeftInverse {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} {f : M →ₛₗ[σ₁₂] M₂} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {g : M₂M} (h : ) :
M ≃ₛₗ[σ₁₂] ()

A linear map f : M →ₗ[R] M₂ with a left-inverse g : M₂ →ₗ[R] M defines a linear equivalence between M and f.range.

This is a computable alternative to LinearEquiv.ofInjective, and a bidirectional version of LinearMap.rangeRestrict.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem LinearEquiv.ofLeftInverse_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} {f : M →ₛₗ[σ₁₂] M₂} {g : M₂ →ₛₗ[σ₂₁] M} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (h : ) (x : M) :
() = f x
@[simp]
theorem LinearEquiv.ofLeftInverse_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} {f : M →ₛₗ[σ₁₂] M₂} {g : M₂ →ₛₗ[σ₂₁] M} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (h : ) (x : ()) :
= g x
noncomputable def LinearEquiv.ofInjective {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} (f : M →ₛₗ[σ₁₂] M₂) [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (h : ) :
M ≃ₛₗ[σ₁₂] ()

An Injective linear map f : M →ₗ[R] M₂ defines a linear equivalence between M and f.range. See also LinearMap.ofLeftInverse.

Equations
Instances For
@[simp]
theorem LinearEquiv.ofInjective_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} (f : M →ₛₗ[σ₁₂] M₂) [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {h : } (x : M) :
(() x) = f x
noncomputable def LinearEquiv.ofBijective {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} (f : M →ₛₗ[σ₁₂] M₂) [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (hf : ) :
M ≃ₛₗ[σ₁₂] M₂

A bijective linear map is a linear equivalence.

Equations
Instances For
@[simp]
theorem LinearEquiv.ofBijective_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} (f : M →ₛₗ[σ₁₂] M₂) [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {hf : } (x : M) :
() x = f x
@[simp]
theorem LinearEquiv.ofBijective_symm_apply_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} (f : M →ₛₗ[σ₁₂] M₂) [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {h : } (x : M) :
(f x) = x
theorem LinearEquiv.map_neg {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₂) (a : M) :
e (-a) = -e a
theorem LinearEquiv.map_sub {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₂) (a : M) (b : M) :
e (a - b) = e a - e b
def LinearEquiv.neg (R : Type u_1) {M : Type u_9} [] [] [Module R M] :

x ↦ -x as a LinearEquiv

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem LinearEquiv.coe_neg {R : Type u_1} {M : Type u_9} [] [] [Module R M] :
() = -id
theorem LinearEquiv.neg_apply {R : Type u_1} {M : Type u_9} [] [] [Module R M] (x : M) :
() x = -x
@[simp]
theorem LinearEquiv.symm_neg {R : Type u_1} {M : Type u_9} [] [] [Module R M] :
def LinearEquiv.smulOfUnit {R : Type u_1} {M : Type u_9} [] [] [Module R M] (a : Rˣ) :

Multiplying by a unit a of the ring R is a linear equivalence.

Equations
Instances For
def LinearEquiv.arrowCongr {R : Type u_20} {M₁ : Type u_21} {M₂ : Type u_22} {M₂₁ : Type u_23} {M₂₂ : Type u_24} [] [] [] [] [] [Module R M₁] [Module R M₂] [Module R M₂₁] [Module R M₂₂] (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : M₂₁ ≃ₗ[R] M₂₂) :
(M₁ →ₗ[R] M₂₁) ≃ₗ[R] M₂ →ₗ[R] M₂₂

A linear isomorphism between the domains and codomains of two spaces of linear maps gives a linear isomorphism between the two function spaces.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem LinearEquiv.arrowCongr_apply {R : Type u_20} {M₁ : Type u_21} {M₂ : Type u_22} {M₂₁ : Type u_23} {M₂₂ : Type u_24} [] [] [] [] [] [Module R M₁] [Module R M₂] [Module R M₂₁] [Module R M₂₂] (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : M₂₁ ≃ₗ[R] M₂₂) (f : M₁ →ₗ[R] M₂₁) (x : M₂) :
(() f) x = e₂ (f (() x))
@[simp]
theorem LinearEquiv.arrowCongr_symm_apply {R : Type u_20} {M₁ : Type u_21} {M₂ : Type u_22} {M₂₁ : Type u_23} {M₂₂ : Type u_24} [] [] [] [] [] [Module R M₁] [Module R M₂] [Module R M₂₁] [Module R M₂₂] (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : M₂₁ ≃ₗ[R] M₂₂) (f : M₂ →ₗ[R] M₂₂) (x : M₁) :
(() f) x = () (f (e₁ x))
theorem LinearEquiv.arrowCongr_comp {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₃] {N : Type u_20} {N₂ : Type u_21} {N₃ : Type u_22} [] [] [] [Module R N] [Module R N₂] [Module R N₃] (e₁ : M ≃ₗ[R] N) (e₂ : M₂ ≃ₗ[R] N₂) (e₃ : M₃ ≃ₗ[R] N₃) (f : M →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) :
() (g ∘ₗ f) = () g ∘ₗ () f
theorem LinearEquiv.arrowCongr_trans {R : Type u_1} [] {M₁ : Type u_20} {M₂ : Type u_21} {M₃ : Type u_22} {N₁ : Type u_23} {N₂ : Type u_24} {N₃ : Type u_25} [] [Module R M₁] [] [Module R M₂] [] [Module R M₃] [] [Module R N₁] [] [Module R N₂] [] [Module R N₃] (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : N₁ ≃ₗ[R] N₂) (e₃ : M₂ ≃ₗ[R] M₃) (e₄ : N₂ ≃ₗ[R] N₃) :
≪≫ₗ = LinearEquiv.arrowCongr (e₁ ≪≫ₗ e₃) (e₂ ≪≫ₗ e₄)
def LinearEquiv.congrRight {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₃

If M₂ and M₃ are linearly isomorphic then the two spaces of linear maps from M into M₂ and M into M₃ are linearly isomorphic.

Equations
Instances For
def LinearEquiv.conj {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [] [] [] [Module R M] [Module R M₂] (e : M ≃ₗ[R] M₂) :

If M and M₂ are linearly isomorphic then the two spaces of linear maps from M and M₂ to themselves are linearly isomorphic.

Equations
Instances For
theorem LinearEquiv.conj_apply {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [] [] [] [Module R M] [Module R M₂] (e : M ≃ₗ[R] M₂) (f : ) :
() f = (e ∘ₗ f) ∘ₗ ()
theorem LinearEquiv.conj_apply_apply {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [] [] [] [Module R M] [Module R M₂] (e : M ≃ₗ[R] M₂) (f : ) (x : M₂) :
(() f) x = e (f (() x))
theorem LinearEquiv.symm_conj_apply {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [] [] [] [Module R M] [Module R M₂] (e : M ≃ₗ[R] M₂) (f : Module.End R M₂) :
f = (() ∘ₗ f) ∘ₗ e
theorem LinearEquiv.conj_comp {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [] [] [] [Module R M] [Module R M₂] (e : M ≃ₗ[R] M₂) (f : ) (g : ) :
() (g ∘ₗ f) = () g ∘ₗ () f
theorem LinearEquiv.conj_trans {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₃] (e₁ : M ≃ₗ[R] M₂) (e₂ : M₂ ≃ₗ[R] M₃) :
≪≫ₗ = LinearEquiv.conj (e₁ ≪≫ₗ e₂)
@[simp]
theorem LinearEquiv.conj_id {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [] [] [] [Module R M] [Module R M₂] (e : M ≃ₗ[R] M₂) :
() LinearMap.id = LinearMap.id
def LinearEquiv.congrLeft (M : Type u_9) {M₂ : Type u_12} {M₃ : Type u_13} [] [] [] {R : Type u_20} (S : Type u_21) [] [] [Module R M₂] [Module R M₃] [Module R M] [Module S M] [] (e : M₂ ≃ₗ[R] M₃) :
(M₂ →ₗ[R] M) ≃ₗ[S] M₃ →ₗ[R] M

An R-linear isomorphism between two R-modules M₂ and M₃ induces an S-linear isomorphism between M₂ →ₗ[R] M and M₃ →ₗ[R] M, if M is both an R-module and an S-module and their actions commute.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem LinearEquiv.smulOfNeZero_symm_apply (K : Type u_7) (M : Type u_9) [] [] [Module K M] (a : K) (ha : a 0) :
∀ (a_1 : M), (LinearEquiv.symm ()) a_1 = (Units.mk0 a ha)⁻¹ a_1
@[simp]
theorem LinearEquiv.smulOfNeZero_apply (K : Type u_7) (M : Type u_9) [] [] [Module K M] (a : K) (ha : a 0) :
∀ (a_1 : M), () a_1 = a a_1
def LinearEquiv.smulOfNeZero (K : Type u_7) (M : Type u_9) [] [] [Module K M] (a : K) (ha : a 0) :

Multiplying by a nonzero element a of the field K is a linear equivalence.

Equations
Instances For
def Submodule.equivSubtypeMap {R : Type u_1} {M : Type u_9} [] [] [Module R M] (p : ) (q : Submodule R p) :
q ≃ₗ[R] ()

Given p a submodule of the module M and q a submodule of p, p.equivSubtypeMap q is the natural LinearEquiv between q and q.map p.subtype.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Submodule.equivSubtypeMap_apply {R : Type u_1} {M : Type u_9} [] [] [Module R M] {p : } {q : Submodule R p} (x : q) :
( x) = x
@[simp]
theorem Submodule.equivSubtypeMap_symm_apply {R : Type u_1} {M : Type u_9} [] [] [Module R M] {p : } {q : Submodule R p} (x : ()) :
() = x
@[simp]
theorem Submodule.comap_equiv_self_of_inj_of_le_apply {R : Type u_1} {M : Type u_9} {N : Type u_15} [] [] [Module R M] [] [Module R N] {f : M →ₗ[R] N} {p : } (hf : ) (h : ) :
∀ (a : ()), = () a
noncomputable def Submodule.comap_equiv_self_of_inj_of_le {R : Type u_1} {M : Type u_9} {N : Type u_15} [] [] [Module R M] [] [Module R N] {f : M →ₗ[R] N} {p : } (hf : ) (h : ) :
() ≃ₗ[R] p

A linear injection M ↪ N restricts to an equivalence f⁻¹ p ≃ p for any submodule p contained in its range.

Equations
Instances For
def Equiv.toLinearEquiv {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [] [] [Module R M] [] [Module R M₂] (e : M M₂) (h : IsLinearMap R e) :
M ≃ₗ[R] M₂

An equivalence whose underlying function is linear is a linear equivalence.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def LinearMap.funLeft (R : Type u_1) (M : Type u_9) [] [] [Module R M] {m : Type u_20} {n : Type u_21} (f : mn) :
(nM) →ₗ[R] mM

Given an R-module M and a function m → n between arbitrary types, construct a linear map (n → M) →ₗ[R] (m → M)

Equations
• = { toAddHom := { toFun := fun (x : nM) => x f, map_add' := }, map_smul' := }
Instances For
@[simp]
theorem LinearMap.funLeft_apply (R : Type u_1) (M : Type u_9) [] [] [Module R M] {m : Type u_20} {n : Type u_21} (f : mn) (g : nM) (i : m) :
() g i = g (f i)
@[simp]
theorem LinearMap.funLeft_id (R : Type u_1) (M : Type u_9) [] [] [Module R M] {n : Type u_21} (g : nM) :
() g = g
theorem LinearMap.funLeft_comp (R : Type u_1) (M : Type u_9) [] [] [Module R M] {m : Type u_20} {n : Type u_21} {p : Type u_22} (f₁ : np) (f₂ : mn) :
LinearMap.funLeft R M (f₁ f₂) = ∘ₗ
theorem LinearMap.funLeft_surjective_of_injective (R : Type u_1) (M : Type u_9) [] [] [Module R M] {m : Type u_20} {n : Type u_21} (f : mn) (hf : ) :
theorem LinearMap.funLeft_injective_of_surjective (R : Type u_1) (M : Type u_9) [] [] [Module R M] {m : Type u_20} {n : Type u_21} (f : mn) (hf : ) :
def LinearEquiv.funCongrLeft (R : Type u_1) (M : Type u_9) [] [] [Module R M] {m : Type u_20} {n : Type u_21} (e : m n) :
(nM) ≃ₗ[R] mM

Given an R-module M and an equivalence m ≃ n between arbitrary types, construct a linear equivalence (n → M) ≃ₗ[R] (m → M)

Equations
Instances For
@[simp]
theorem LinearEquiv.funCongrLeft_apply (R : Type u_1) (M : Type u_9) [] [] [Module R M] {m : Type u_20} {n : Type u_21} (e : m n) (x : nM) :
() x = () x
@[simp]
theorem LinearEquiv.funCongrLeft_id (R : Type u_1) (M : Type u_9) [] [] [Module R M] {n : Type u_21} :
= LinearEquiv.refl R (nM)
@[simp]
theorem LinearEquiv.funCongrLeft_comp (R : Type u_1) (M : Type u_9) [] [] [Module R M] {m : Type u_20} {n : Type u_21} {p : Type u_22} (e₁ : m n) (e₂ : n p) :
LinearEquiv.funCongrLeft R M (e₁.trans e₂) = ≪≫ₗ
@[simp]
theorem LinearEquiv.funCongrLeft_symm (R : Type u_1) (M : Type u_9) [] [] [Module R M] {m : Type u_20} {n : Type u_21} (e : m n) :