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) [Semiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R B] (f : A →+ B) : (addMonoidHomLequivNat R) f = AddMonoidHom.toNatLinearMap f

@[simp]

theorem addMonoidHomLequivNat_symm_apply {A : Type u_20} {B : Type u_21} (R : Type u_22) [Semiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R B] (f : A →ₗ[ℕ] B) : (LinearEquiv.symm (addMonoidHomLequivNat R)) f = LinearMap.toAddMonoidHom f

def addMonoidHomLequivNat {A : Type u_20} {B : Type u_21} (R : Type u_22) [Semiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R B] : (A →+ B) ≃ₗ[R] A →ₗ[ℕ] 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.

@[simp]

theorem addMonoidHomLequivInt_apply {A : Type u_20} {B : Type u_21} (R : Type u_22) [Semiring R] [AddCommGroup A] [AddCommGroup B] [Module R B] (f : A →+ B) : (addMonoidHomLequivInt R) f = AddMonoidHom.toIntLinearMap f

@[simp]

theorem addMonoidHomLequivInt_symm_apply {A : Type u_20} {B : Type u_21} (R : Type u_22) [Semiring R] [AddCommGroup A] [AddCommGroup B] [Module R B] (f : A →ₗ[ℤ] B) : (LinearEquiv.symm (addMonoidHomLequivInt R)) f = LinearMap.toAddMonoidHom f

def addMonoidHomLequivInt {A : Type u_20} {B : Type u_21} (R : Type u_22) [Semiring R] [AddCommGroup A] [AddCommGroup B] [Module R B] : (A →+ B) ≃ₗ[R] A →ₗ[ℤ] 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.

@[simp]

theorem addMonoidEndRingEquivInt_apply (A : Type u_20) [AddCommGroup A] : ∀ (a : A →+ A), (addMonoidEndRingEquivInt A) a = (↑(addMonoidHomLequivInt ℤ)).toAddHom.toFun a

@[simp]

theorem addMonoidEndRingEquivInt_symm_apply (A : Type u_20) [AddCommGroup A] : ∀ (a : A →ₗ[ℤ] A), (RingEquiv.symm (addMonoidEndRingEquivInt A)) a = (addMonoidHomLequivInt ℤ).invFun a

def addMonoidEndRingEquivInt (A : Type u_20) [AddCommGroup A] : AddMonoid.End A ≃+* Module.End ℤ A

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

Equations

• One or more equations did not get rendered due to their size.

Properties of linear maps

theorem LinearMap.map_codRestrict {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₂₁ : R₂ →+* R} [RingHomSurjective σ₂₁] (p : Submodule R M) (f : M₂ →ₛₗ[σ₂₁] M) (h : ∀ (c : M₂), f c ∈ p) (p' : Submodule R₂ M₂) : Submodule.map (LinearMap.codRestrict p f h) p' = Submodule.comap (Submodule.subtype p) (Submodule.map f p')

theorem LinearMap.comap_codRestrict {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₂₁ : R₂ →+* R} (p : Submodule R M) (f : M₂ →ₛₗ[σ₂₁] M) (hf : ∀ (c : M₂), f c ∈ p) (p' : Submodule R ↥p) : Submodule.comap (LinearMap.codRestrict p f hf) p' = Submodule.comap f (Submodule.map (Submodule.subtype p) p')

def LinearMap.range {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [RingHomSurjective τ₁₂] (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

• LinearMap.range f = Submodule.copy (Submodule.map f ⊤) (Set.range ⇑f) (_ : Set.range ⇑f = ⇑f '' Set.univ)

theorem LinearMap.range_coe {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [RingHomSurjective τ₁₂] (f : F) : ↑(LinearMap.range f) = Set.range ⇑f

theorem LinearMap.range_toAddSubmonoid {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) : (LinearMap.range f).toAddSubmonoid = AddMonoidHom.mrange f

@[simp]

theorem LinearMap.mem_range {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [RingHomSurjective τ₁₂] {f : F} {x : M₂} : x ∈ LinearMap.range f ↔ ∃ (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] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [RingHomSurjective τ₁₂] (f : F) : LinearMap.range f = Submodule.map f ⊤

theorem LinearMap.mem_range_self {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [RingHomSurjective τ₁₂] (f : F) (x : M) : f x ∈ LinearMap.range f

@[simp]

theorem LinearMap.range_id {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [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₂] [Semiring R₃] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R₂ M₂] [Module R₃ M₃] {τ₁₂ : R →+* R₂} {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [RingHomCompTriple τ₁₂ τ₂₃ τ₁₃] [RingHomSurjective τ₁₂] [RingHomSurjective τ₂₃] [RingHomSurjective τ₁₃] (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) : LinearMap.range (LinearMap.comp g f) = Submodule.map g (LinearMap.range f)

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₂] [Semiring R₃] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R₂ M₂] [Module R₃ M₃] {τ₁₂ : R →+* R₂} {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [RingHomCompTriple τ₁₂ τ₂₃ τ₁₃] [RingHomSurjective τ₂₃] [RingHomSurjective τ₁₃] (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) : LinearMap.range (LinearMap.comp g f) ≤ LinearMap.range g

theorem LinearMap.range_eq_top {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [RingHomSurjective τ₁₂] {f : F} : LinearMap.range f = ⊤ ↔ Function.Surjective ⇑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] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [RingHomSurjective τ₁₂] {f : F} {p : Submodule R₂ M₂} : LinearMap.range f ≤ p ↔ Submodule.comap f p = ⊤

theorem LinearMap.map_le_range {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [RingHomSurjective τ₁₂] {f : F} {p : Submodule R M} : Submodule.map f p ≤ LinearMap.range f

@[simp]

theorem LinearMap.range_neg {R : Type u_21} {R₂ : Type u_22} {M : Type u_23} {M₂ : Type u_24} [Semiring R] [Ring R₂] [AddCommMonoid M] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) : LinearMap.range (-f) = LinearMap.range f

theorem LinearMap.range_domRestrict_le_range {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) (S : Submodule R M) : LinearMap.range (LinearMap.domRestrict f S) ≤ LinearMap.range f

@[simp]

theorem AddMonoidHom.coe_toIntLinearMap_range {M : Type u_21} {M₂ : Type u_22} [AddCommGroup M] [AddCommGroup M₂] (f : M →+ M₂) : LinearMap.range (AddMonoidHom.toIntLinearMap f) = AddSubgroup.toIntSubmodule (AddMonoidHom.range f)

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] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [RingHomSurjective τ₁₂] {f : F} {p : Submodule R₂ M₂} (h : p ≤ LinearMap.range f) : Submodule.map f (Submodule.comap f p) = p

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

A linear map version of AddMonoidHom.eqLocusM

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LinearMap.mem_eqLocus {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [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 ∈ LinearMap.eqLocus f g ↔ 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] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] (f : F) (g : F) : (LinearMap.eqLocus f g).toAddSubmonoid = AddMonoidHom.eqLocusM ↑f ↑g

@[simp]

theorem LinearMap.eqLocus_eq_top {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] {f : F} {g : F} : LinearMap.eqLocus f g = ⊤ ↔ 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] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] (f : F) : LinearMap.eqLocus f f = ⊤

theorem LinearMap.le_eqLocus {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [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 : Submodule R M} : S ≤ LinearMap.eqLocus f g ↔ 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] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [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 : Submodule R M} {T : Submodule R M} (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] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [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 : Submodule R M} {T : Submodule R M} (hST : Codisjoint S T) (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} [Semiring R] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] M) (n : ℕ) : (LinearMap.iterateRange f) n = LinearMap.range (f ^ n)

def LinearMap.iterateRange {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] M) : ℕ →o (Submodule R M)ᵒᵈ

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

Equations

• One or more equations did not get rendered due to their size.

@[reducible]

def LinearMap.rangeRestrict {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) : M →ₛₗ[τ₁₂] ↥(LinearMap.range f)

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

This is the bundled version of Set.rangeFactorization.

Equations

• LinearMap.rangeRestrict f = LinearMap.codRestrict (LinearMap.range f) f (_ : ∀ (x : M), f x ∈ LinearMap.range f)

instance LinearMap.fintypeRange {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [Fintype M] [DecidableEq M₂] [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) : Fintype ↥(LinearMap.range f)

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

• LinearMap.fintypeRange f = Set.fintypeRange ⇑f

def LinearMap.ker {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [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 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.

Equations

• LinearMap.ker f = Submodule.comap f ⊥

@[simp]

theorem LinearMap.mem_ker {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] {f : F} {y : M} : y ∈ LinearMap.ker f ↔ f y = 0

@[simp]

theorem LinearMap.ker_id {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [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] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] (f : F) (x : ↥(LinearMap.ker f)) : 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] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) : (LinearMap.ker f).toAddSubmonoid = AddMonoidHom.mker f

theorem LinearMap.comp_ker_subtype {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) : LinearMap.comp f (Submodule.subtype (LinearMap.ker f)) = 0

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₂] [Semiring R₃] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R₂ M₂] [Module R₃ M₃] {τ₁₂ : R →+* R₂} {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [RingHomCompTriple τ₁₂ τ₂₃ τ₁₃] (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) : LinearMap.ker (LinearMap.comp g f) = Submodule.comap f (LinearMap.ker g)

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₂] [Semiring R₃] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R₂ M₂] [Module R₃ M₃] {τ₁₂ : R →+* R₂} {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [RingHomCompTriple τ₁₂ τ₂₃ τ₁₃] (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) : LinearMap.ker f ≤ LinearMap.ker (LinearMap.comp g f)

theorem LinearMap.ker_sup_ker_le_ker_comp_of_commute {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] {f : M →ₗ[R] M} {g : M →ₗ[R] M} (h : Commute f g) : LinearMap.ker f ⊔ LinearMap.ker g ≤ LinearMap.ker (f ∘ₗ g)

@[simp]

theorem LinearMap.ker_le_comap {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {p : Submodule R₂ M₂} (f : M →ₛₗ[τ₁₂] M₂) : LinearMap.ker f ≤ Submodule.comap f p

theorem LinearMap.disjoint_ker {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [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} : Disjoint p (LinearMap.ker f) ↔ ∀ x ∈ p, f x = 0 → x = 0

theorem LinearMap.ker_eq_bot' {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] {f : F} : LinearMap.ker f = ⊥ ↔ ∀ (m : M), f m = 0 → m = 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] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁] {f : M →ₛₗ[τ₁₂] M₂} {g : M₂ →ₛₗ[τ₂₁] M} (h : LinearMap.comp g f = LinearMap.id) : LinearMap.ker f = ⊥

theorem LinearMap.le_ker_iff_map {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [RingHomSurjective τ₁₂] {f : F} {p : Submodule R M} : p ≤ LinearMap.ker f ↔ Submodule.map f p = ⊥

theorem LinearMap.ker_codRestrict {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₂₁ : R₂ →+* R} (p : Submodule R M) (f : M₂ →ₛₗ[τ₂₁] M) (hf : ∀ (c : M₂), f c ∈ p) : LinearMap.ker (LinearMap.codRestrict p f hf) = LinearMap.ker f

theorem LinearMap.range_codRestrict {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₂₁ : R₂ →+* R} [RingHomSurjective τ₂₁] (p : Submodule R M) (f : M₂ →ₛₗ[τ₂₁] M) (hf : ∀ (c : M₂), f c ∈ p) : LinearMap.range (LinearMap.codRestrict p f hf) = Submodule.comap (Submodule.subtype p) (LinearMap.range f)

theorem LinearMap.ker_restrict {R : Type u_1} {M : Type u_9} {M₁ : Type u_11} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₁] [Module R M₁] {p : Submodule R M} {q : Submodule R M₁} {f : M →ₗ[R] M₁} (hf : ∀ x ∈ p, f x ∈ q) : LinearMap.ker (LinearMap.restrict f hf) = LinearMap.ker (LinearMap.domRestrict f p)

theorem Submodule.map_comap_eq {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [RingHomSurjective τ₁₂] (f : F) (q : Submodule R₂ M₂) : Submodule.map f (Submodule.comap f q) = LinearMap.range f ⊓ q

theorem Submodule.map_comap_eq_self {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [RingHomSurjective τ₁₂] {f : F} {q : Submodule R₂ M₂} (h : q ≤ LinearMap.range f) : Submodule.map f (Submodule.comap f q) = q

@[simp]

theorem LinearMap.ker_zero {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} : LinearMap.ker 0 = ⊤

@[simp]

theorem LinearMap.range_zero {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] : LinearMap.range 0 = ⊥

theorem LinearMap.ker_eq_top {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {f : M →ₛₗ[τ₁₂] M₂} : LinearMap.ker f = ⊤ ↔ f = 0

@[simp]

theorem AddMonoidHom.coe_toIntLinearMap_ker {M : Type u_21} {M₂ : Type u_22} [AddCommGroup M] [AddCommGroup M₂] (f : M →+ M₂) : LinearMap.ker (AddMonoidHom.toIntLinearMap f) = AddSubgroup.toIntSubmodule (AddMonoidHom.ker f)

theorem LinearMap.range_le_bot_iff {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) : LinearMap.range f ≤ ⊥ ↔ 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] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} : LinearMap.range f = ⊥ ↔ 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₂] [Semiring R₃] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R₂ M₂] [Module R₃ M₃] {τ₁₂ : R →+* R₂} {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [RingHomCompTriple τ₁₂ τ₂₃ τ₁₃] [RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} {g : M₂ →ₛₗ[τ₂₃] M₃} : LinearMap.range f ≤ LinearMap.ker g ↔ LinearMap.comp g f = 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] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [RingHomSurjective τ₁₂] {f : F} (hf : LinearMap.range f = ⊤) {p : Submodule R₂ M₂} {p' : Submodule R₂ M₂} : Submodule.comap f p ≤ Submodule.comap f p' ↔ p ≤ p'

theorem LinearMap.comap_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [RingHomSurjective τ₁₂] {f : F} (hf : LinearMap.range f = ⊤) : Function.Injective (Submodule.comap f)

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] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] {f : F} (hf : Function.Injective ⇑f) : LinearMap.ker f = ⊥

@[simp]

theorem LinearMap.iterateKer_coe {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] M) (n : ℕ) : (LinearMap.iterateKer f) n = LinearMap.ker (f ^ n)

def LinearMap.iterateKer {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] M) : ℕ →o Submodule R M

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

Equations

• One or more equations did not get rendered due to their size.

theorem LinearMap.range_toAddSubgroup {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Ring R] [Ring R₂] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) : Submodule.toAddSubgroup (LinearMap.range f) = AddMonoidHom.range (LinearMap.toAddMonoidHom f)

theorem LinearMap.ker_toAddSubgroup {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Ring R] [Ring R₂] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) : Submodule.toAddSubgroup (LinearMap.ker f) = AddMonoidHom.ker (LinearMap.toAddMonoidHom f)

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₂] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) (g : M →ₛₗ[τ₁₂] M₂) : LinearMap.eqLocus f g = LinearMap.ker (f - g)

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₂] [AddCommGroup M] [AddCommGroup M₂] [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} : x - y ∈ LinearMap.ker f ↔ 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₂] [AddCommGroup M] [AddCommGroup M₂] [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} : Disjoint p (LinearMap.ker f) ↔ ∀ x ∈ p, ∀ y ∈ p, f x = f y → x = 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₂] [AddCommGroup M] [AddCommGroup M₂] [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} {s : Set M} (h : s ⊆ ↑p) (hd : Disjoint p (LinearMap.ker f)) : 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₂] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (F : Type u_20) [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] {f : F} : LinearMap.ker f = ⊥ ↔ Function.Injective ⇑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₂] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {f : M →ₛₗ[τ₁₂] M₂} : LinearMap.ker f = ⊥ ↔ Function.Injective ⇑f

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₂] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] {f : F} [RingHomSurjective τ₁₂] {p : Submodule R M} : LinearMap.ker f ≤ p ↔ ∃ y ∈ LinearMap.range f, ⇑f ⁻¹' {y} ⊆ ↑p

@[simp]

theorem LinearMap.injective_domRestrict_iff {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Ring R] [Ring R₂] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {f : M →ₛₗ[τ₁₂] M₂} {S : Submodule R M} : Function.Injective ⇑(LinearMap.domRestrict f S) ↔ S ⊓ LinearMap.ker f = ⊥

@[simp]

theorem LinearMap.injective_restrict_iff_disjoint {R : Type u_1} {M : Type u_9} [Ring R] [AddCommGroup M] [Module R M] {p : Submodule R M} {f : M →ₗ[R] M} (hf : ∀ x ∈ p, f x ∈ p) : Function.Injective ⇑(LinearMap.restrict f hf) ↔ Disjoint p (LinearMap.ker f)

theorem LinearMap.ker_smul {K : Type u_7} {V : Type u_18} {V₂ : Type u_19} [Semifield K] [AddCommMonoid V] [Module K V] [AddCommMonoid V₂] [Module K V₂] (f : V →ₗ[K] V₂) (a : K) (h : a ≠ 0) : LinearMap.ker (a • f) = LinearMap.ker f

theorem LinearMap.ker_smul' {K : Type u_7} {V : Type u_18} {V₂ : Type u_19} [Semifield K] [AddCommMonoid V] [Module K V] [AddCommMonoid V₂] [Module K V₂] (f : V →ₗ[K] V₂) (a : K) : LinearMap.ker (a • f) = ⨅ (_ : a ≠ 0), LinearMap.ker f

theorem LinearMap.range_smul {K : Type u_7} {V : Type u_18} {V₂ : Type u_19} [Semifield K] [AddCommMonoid V] [Module K V] [AddCommMonoid V₂] [Module K V₂] (f : V →ₗ[K] V₂) (a : K) (h : a ≠ 0) : LinearMap.range (a • f) = LinearMap.range f

theorem LinearMap.range_smul' {K : Type u_7} {V : Type u_18} {V₂ : Type u_19} [Semifield K] [AddCommMonoid V] [Module K V] [AddCommMonoid V₂] [Module K V₂] (f : V →ₗ[K] V₂) (a : K) : LinearMap.range (a • f) = ⨆ (_ : a ≠ 0), LinearMap.range f

theorem IsLinearMap.isLinearMap_add {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [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} [Semiring R] [AddCommGroup M] [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] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [RingHomSurjective τ₁₂] (f : F) : Submodule.map f ⊤ = LinearMap.range f

@[simp]

theorem Submodule.comap_bot {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] (f : F) : Submodule.comap f ⊥ = LinearMap.ker f

@[simp]

theorem Submodule.ker_subtype {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) : LinearMap.ker (Submodule.subtype p) = ⊥

@[simp]

theorem Submodule.range_subtype {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) : LinearMap.range (Submodule.subtype p) = p

theorem Submodule.map_subtype_le {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) (p' : Submodule R ↥p) : Submodule.map (Submodule.subtype p) p' ≤ p

theorem Submodule.map_subtype_top {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) : Submodule.map (Submodule.subtype p) ⊤ = 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} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {p' : Submodule R M} : Submodule.comap (Submodule.subtype p) p' = ⊤ ↔ p ≤ p'

@[simp]

theorem Submodule.comap_subtype_self {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) : Submodule.comap (Submodule.subtype p) p = ⊤

@[simp]

theorem Submodule.ker_inclusion {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) (p' : Submodule R M) (h : p ≤ p') : LinearMap.ker (Submodule.inclusion h) = ⊥

theorem Submodule.range_inclusion {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) (q : Submodule R M) (h : p ≤ q) : LinearMap.range (Submodule.inclusion h) = Submodule.comap (Submodule.subtype q) p

@[simp]

theorem Submodule.map_subtype_range_inclusion {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {p' : Submodule R M} (h : p ≤ p') : Submodule.map (Submodule.subtype p') (LinearMap.range (Submodule.inclusion h)) = p

theorem Submodule.disjoint_iff_comap_eq_bot {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {q : Submodule R M} : Disjoint p q ↔ Submodule.comap (Submodule.subtype p) q = ⊥

def Submodule.MapSubtype.relIso {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) : Submodule R ↥p ≃o { p' : Submodule R M // 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.

def Submodule.MapSubtype.orderEmbedding {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) : Submodule R ↥p ↪o Submodule R M

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.

@[simp]

theorem Submodule.map_subtype_embedding_eq {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) (p' : Submodule R ↥p) : (Submodule.MapSubtype.orderEmbedding p) p' = Submodule.map (Submodule.subtype p) 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] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {f : M →ₛₗ[τ₁₂] M₂} (h : ∀ (u v : ↥(LinearMap.ker f) →ₗ[R] M), LinearMap.comp f u = LinearMap.comp f v → u = v) : LinearMap.ker f = ⊥

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₂] [Semiring R₃] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R₂ M₂] [Module R₃ M₃] {τ₁₂ : R →+* R₂} {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [RingHomCompTriple τ₁₂ τ₂₃ τ₁₃] [RingHomSurjective τ₁₂] [RingHomSurjective τ₂₃] [RingHomSurjective τ₁₃] {f : M →ₛₗ[τ₁₂] M₂} (g : M₂ →ₛₗ[τ₂₃] M₃) (hf : LinearMap.range f = ⊤) : LinearMap.range (LinearMap.comp g f) = LinearMap.range g

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₂] [Semiring R₃] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R₂ M₂] [Module R₃ M₃] {τ₁₂ : R →+* R₂} {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [RingHomCompTriple τ₁₂ τ₂₃ τ₁₃] (f : M →ₛₗ[τ₁₂] M₂) {g : M₂ →ₛₗ[τ₂₃] M₃} (hg : LinearMap.ker g = ⊥) : LinearMap.ker (LinearMap.comp g f) = LinearMap.ker f

def LinearMap.submoduleImage {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] {M' : Type u_20} [AddCommMonoid M'] [Module R M'] {O : Submodule R M} (ϕ : ↥O →ₗ[R] M') (N : Submodule R M) : Submodule R M'

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

• LinearMap.submoduleImage ϕ N = Submodule.map ϕ (Submodule.comap (Submodule.subtype O) N)

@[simp]

theorem LinearMap.mem_submoduleImage {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] {M' : Type u_20} [AddCommMonoid M'] [Module R M'] {O : Submodule R M} {ϕ : ↥O →ₗ[R] M'} {N : Submodule R M} {x : M'} : x ∈ LinearMap.submoduleImage ϕ N ↔ ∃ (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} [Semiring R] [AddCommMonoid M] [Module R M] {M' : Type u_20} [AddCommMonoid M'] [Module R M'] {O : Submodule R M} {ϕ : ↥O →ₗ[R] M'} {N : Submodule R M} (hNO : N ≤ O) {x : M'} : x ∈ LinearMap.submoduleImage ϕ N ↔ ∃ (y : M) (yN : y ∈ N), ϕ { val := y, property := (_ : y ∈ O) } = x

theorem LinearMap.submoduleImage_apply_of_le {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] {M' : Type u_20} [AddCommGroup M'] [Module R M'] {O : Submodule R M} (ϕ : ↥O →ₗ[R] M') (N : Submodule R M) (hNO : N ≤ O) : LinearMap.submoduleImage ϕ N = LinearMap.range (ϕ ∘ₗ Submodule.inclusion hNO)

@[simp]

theorem LinearMap.range_rangeRestrict {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (f : M →ₗ[R] M₂) : LinearMap.range (LinearMap.rangeRestrict f) = ⊤

@[simp]

theorem LinearMap.ker_rangeRestrict {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (f : M →ₗ[R] M₂) : LinearMap.ker (LinearMap.rangeRestrict f) = LinearMap.ker f

Linear equivalences

instance LinearEquiv.instZeroLinearEquiv {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [Subsingleton M] [Subsingleton M₂] : 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] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [Subsingleton M] [Subsingleton M₂] : LinearEquiv.symm 0 = 0

@[simp]

theorem LinearEquiv.coe_zero {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [Subsingleton M] [Subsingleton M₂] : ⇑0 = 0

theorem LinearEquiv.zero_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [Subsingleton M] [Subsingleton M₂] (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] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [Subsingleton M] [Subsingleton M₂] : Unique (M ≃ₛₗ[σ₁₂] M₂)

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

Equations

• LinearEquiv.instUniqueLinearEquiv = { toInhabited := { default := 0 }, uniq := (_ : ∀ (x : M ≃ₛₗ[σ₁₂] M₂), x = default) }

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

Equations

• LinearEquiv.uniqueOfSubsingleton = inferInstance

theorem LinearEquiv.map_eq_comap {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) {p : Submodule R M} : Submodule.map (↑e) p = Submodule.comap (↑(LinearEquiv.symm e)) p

def LinearEquiv.submoduleMap {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) (p : Submodule R M) : ↥p ≃ₛₗ[σ₁₂] ↥(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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LinearEquiv.submoduleMap_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) (p : Submodule R M) (x : ↥p) : ↑((LinearEquiv.submoduleMap e 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] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) (p : Submodule R M) (x : ↥(Submodule.map (↑e) p)) : ↑((LinearEquiv.symm (LinearEquiv.submoduleMap e p)) x) = (LinearEquiv.symm e) ↑x

def LinearEquiv.curry (R : Type u_1) (V : Type u_18) (V₂ : Type u_19) [Semiring R] : (V × V₂ → R) ≃ₗ[R] V → V₂ → 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.

@[simp]

theorem LinearEquiv.coe_curry (R : Type u_1) (V : Type u_18) (V₂ : Type u_19) [Semiring R] : ⇑(LinearEquiv.curry R V V₂) = Function.curry

@[simp]

theorem LinearEquiv.coe_curry_symm (R : Type u_1) (V : Type u_18) (V₂ : Type u_19) [Semiring R] : ⇑(LinearEquiv.symm (LinearEquiv.curry R V V₂)) = Function.uncurry

def LinearEquiv.ofEq {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) (q : Submodule R M) (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.

@[simp]

theorem LinearEquiv.coe_ofEq_apply {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] {module_M : Module R M} {p : Submodule R M} {q : Submodule R M} (h : p = q) (x : ↥p) : ↑((LinearEquiv.ofEq p q h) x) = ↑x

@[simp]

theorem LinearEquiv.ofEq_symm {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] {module_M : Module R M} {p : Submodule R M} {q : Submodule R M} (h : p = q) : LinearEquiv.symm (LinearEquiv.ofEq p q h) = LinearEquiv.ofEq q p (_ : q = p)

@[simp]

theorem LinearEquiv.ofEq_rfl {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] {module_M : Module R M} {p : Submodule R M} : LinearEquiv.ofEq p p (_ : p = p) = LinearEquiv.refl R ↥p

def LinearEquiv.ofSubmodules {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) (p : Submodule R M) (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

• LinearEquiv.ofSubmodules e p q h = LinearEquiv.trans (LinearEquiv.submoduleMap e p) (LinearEquiv.ofEq (Submodule.map (↑e) p) q h)

@[simp]

theorem LinearEquiv.ofSubmodules_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) {p : Submodule R M} {q : Submodule R₂ M₂} (h : Submodule.map e p = q) (x : ↥p) : ↑((LinearEquiv.ofSubmodules e p q h) 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] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) {p : Submodule R M} {q : Submodule R₂ M₂} (h : Submodule.map e p = q) (x : ↥q) : ↑((LinearEquiv.symm (LinearEquiv.ofSubmodules e p q h)) x) = (LinearEquiv.symm e) ↑x

def LinearEquiv.ofSubmodule' {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {σ₁₂ : 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

• One or more equations did not get rendered due to their size.

theorem LinearEquiv.ofSubmodule'_toLinearMap {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} [Module R M] [Module R₂ M₂] (f : M ≃ₛₗ[σ₁₂] M₂) (U : Submodule R₂ M₂) : ↑(LinearEquiv.ofSubmodule' f U) = LinearMap.codRestrict U (LinearMap.domRestrict (↑f) (Submodule.comap (↑f) U)) (_ : ∀ (x : ↥(Submodule.comap (↑f) U)), ↑x ∈ Submodule.comap (↑f) U)

@[simp]

theorem LinearEquiv.ofSubmodule'_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {σ₁₂ : 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)) : ↑((LinearEquiv.ofSubmodule' 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] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} [Module R M] [Module R₂ M₂] (f : M ≃ₛₗ[σ₁₂] M₂) (U : Submodule R₂ M₂) (x : ↥U) : ↑((LinearEquiv.symm (LinearEquiv.ofSubmodule' f U)) x) = (LinearEquiv.symm f) ↑x

def LinearEquiv.ofTop {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) (h : p = ⊤) : ↥p ≃ₗ[R] M

The top submodule of M is linearly equivalent to M.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LinearEquiv.ofTop_apply {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {h : p = ⊤} (x : ↥p) : (LinearEquiv.ofTop p h) x = ↑x

@[simp]

theorem LinearEquiv.coe_ofTop_symm_apply {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {h : p = ⊤} (x : M) : ↑((LinearEquiv.symm (LinearEquiv.ofTop p h)) x) = x

theorem LinearEquiv.ofTop_symm_apply {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {h : p = ⊤} (x : M) : (LinearEquiv.symm (LinearEquiv.ofTop p h)) x = { val := x, property := (_ : x ∈ p) }

def LinearEquiv.ofLinear {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {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.comp f g = LinearMap.id) (h₂ : LinearMap.comp g f = LinearMap.id) : M ≃ₛₗ[σ₁₂] M₂

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LinearEquiv.ofLinear_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {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.comp f g = LinearMap.id} {h₂ : LinearMap.comp g f = 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] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {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.comp f g = LinearMap.id} {h₂ : LinearMap.comp g f = 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] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) : LinearMap.range ↑e = ⊤

@[simp]

theorem LinearEquivClass.range {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {σ₁₂ : 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) : LinearMap.range e = ⊤

theorem LinearEquiv.eq_bot_of_equiv {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (p : Submodule R M) [Module R₂ M₂] (e : ↥p ≃ₛₗ[σ₁₂] ↥⊥) : p = ⊥

@[simp]

theorem LinearEquiv.ker {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) : LinearMap.ker ↑e = ⊥

@[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₂] [Semiring R₃] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] {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₃) [RingHomSurjective σ₂₃] [RingHomSurjective σ₁₃] : LinearMap.range (LinearMap.comp h ↑e) = LinearMap.range h

@[simp]

theorem LinearEquiv.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₂] [Semiring R₃] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {σ₃₂ : R₃ →+* R₂} {re₂₃ : RingHomInvPair σ₂₃ σ₃₂} {re₃₂ : RingHomInvPair σ₃₂ σ₂₃} (e'' : M₂ ≃ₛₗ[σ₂₃] M₃) (l : M →ₛₗ[σ₁₂] M₂) : LinearMap.ker (LinearMap.comp (↑e'') l) = LinearMap.ker l

def LinearEquiv.ofLeftInverse {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {f : M →ₛₗ[σ₁₂] M₂} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {g : M₂ → M} (h : Function.LeftInverse g ⇑f) : M ≃ₛₗ[σ₁₂] ↥(LinearMap.range f)

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.

@[simp]

theorem LinearEquiv.ofLeftInverse_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {f : M →ₛₗ[σ₁₂] M₂} {g : M₂ →ₛₗ[σ₂₁] M} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (h : Function.LeftInverse ⇑g ⇑f) (x : M) : ↑((LinearEquiv.ofLeftInverse h) x) = 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] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {f : M →ₛₗ[σ₁₂] M₂} {g : M₂ →ₛₗ[σ₂₁] M} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (h : Function.LeftInverse ⇑g ⇑f) (x : ↥(LinearMap.range f)) : (LinearEquiv.symm (LinearEquiv.ofLeftInverse 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] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} (f : M →ₛₗ[σ₁₂] M₂) [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (h : Function.Injective ⇑f) : M ≃ₛₗ[σ₁₂] ↥(LinearMap.range f)

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

Equations

• LinearEquiv.ofInjective f h = LinearEquiv.ofLeftInverse (_ : Function.LeftInverse (Classical.choose (_ : Function.HasLeftInverse ⇑f)) ⇑f)

@[simp]

theorem LinearEquiv.ofInjective_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} (f : M →ₛₗ[σ₁₂] M₂) [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {h : Function.Injective ⇑f} (x : M) : ↑((LinearEquiv.ofInjective f h) 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] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} (f : M →ₛₗ[σ₁₂] M₂) [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (hf : Function.Bijective ⇑f) : M ≃ₛₗ[σ₁₂] M₂

A bijective linear map is a linear equivalence.

Equations

• LinearEquiv.ofBijective f hf = LinearEquiv.trans (LinearEquiv.ofInjective f (_ : Function.Injective ⇑f)) (LinearEquiv.ofTop (LinearMap.range f) (_ : LinearMap.range f = ⊤))

@[simp]

theorem LinearEquiv.ofBijective_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} (f : M →ₛₗ[σ₁₂] M₂) [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {hf : Function.Bijective ⇑f} (x : M) : (LinearEquiv.ofBijective f hf) 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] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} (f : M →ₛₗ[σ₁₂] M₂) [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {h : Function.Bijective ⇑f} (x : M) : (LinearEquiv.symm (LinearEquiv.ofBijective f h)) (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] [Semiring R₂] [AddCommGroup M] [AddCommGroup M₂] {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] [Semiring R₂] [AddCommGroup M] [AddCommGroup M₂] {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} [Semiring R] [AddCommGroup M] [Module R M] : M ≃ₗ[R] M

x ↦ -x as a LinearEquiv

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LinearEquiv.coe_neg {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommGroup M] [Module R M] : ⇑(LinearEquiv.neg R) = -id

theorem LinearEquiv.neg_apply {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommGroup M] [Module R M] (x : M) : (LinearEquiv.neg R) x = -x

@[simp]

theorem LinearEquiv.symm_neg {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommGroup M] [Module R M] : LinearEquiv.symm (LinearEquiv.neg R) = LinearEquiv.neg R

def LinearEquiv.smulOfUnit {R : Type u_1} {M : Type u_9} [CommSemiring R] [AddCommMonoid M] [Module R M] (a : Rˣ) : M ≃ₗ[R] M

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

Equations

• LinearEquiv.smulOfUnit a = DistribMulAction.toLinearEquiv R M a

def LinearEquiv.arrowCongr {R : Type u_20} {M₁ : Type u_21} {M₂ : Type u_22} {M₂₁ : Type u_23} {M₂₂ : Type u_24} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₂₁] [AddCommMonoid M₂₂] [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.

@[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} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₂₁] [AddCommMonoid M₂₂] [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₂) : ((LinearEquiv.arrowCongr e₁ e₂) f) x = e₂ (f ((LinearEquiv.symm e₁) 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} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₂₁] [AddCommMonoid M₂₂] [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₁) : ((LinearEquiv.symm (LinearEquiv.arrowCongr e₁ e₂)) f) x = (LinearEquiv.symm e₂) (f (e₁ x))

theorem LinearEquiv.arrowCongr_comp {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} {M₃ : Type u_13} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] {N : Type u_20} {N₂ : Type u_21} {N₃ : Type u_22} [AddCommMonoid N] [AddCommMonoid N₂] [AddCommMonoid N₃] [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₃) : (LinearEquiv.arrowCongr e₁ e₃) (g ∘ₗ f) = (LinearEquiv.arrowCongr e₂ e₃) g ∘ₗ (LinearEquiv.arrowCongr e₁ e₂) f

theorem LinearEquiv.arrowCongr_trans {R : Type u_1} [CommSemiring R] {M₁ : Type u_20} {M₂ : Type u_21} {M₃ : Type u_22} {N₁ : Type u_23} {N₂ : Type u_24} {N₃ : Type u_25} [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid M₃] [Module R M₃] [AddCommMonoid N₁] [Module R N₁] [AddCommMonoid N₂] [Module R N₂] [AddCommMonoid N₃] [Module R N₃] (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : N₁ ≃ₗ[R] N₂) (e₃ : M₂ ≃ₗ[R] M₃) (e₄ : N₂ ≃ₗ[R] N₃) : LinearEquiv.arrowCongr e₁ e₂ ≪≫ₗ LinearEquiv.arrowCongr e₃ e₄ = 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} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [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

• LinearEquiv.congrRight f = LinearEquiv.arrowCongr (LinearEquiv.refl R M) f

def LinearEquiv.conj {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (e : M ≃ₗ[R] M₂) : Module.End R M ≃ₗ[R] Module.End 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

• LinearEquiv.conj e = LinearEquiv.arrowCongr e e

theorem LinearEquiv.conj_apply {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (e : M ≃ₗ[R] M₂) (f : Module.End R M) : (LinearEquiv.conj e) f = (↑e ∘ₗ f) ∘ₗ ↑(LinearEquiv.symm e)

theorem LinearEquiv.conj_apply_apply {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (e : M ≃ₗ[R] M₂) (f : Module.End R M) (x : M₂) : ((LinearEquiv.conj e) f) x = e (f ((LinearEquiv.symm e) x))

theorem LinearEquiv.symm_conj_apply {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (e : M ≃ₗ[R] M₂) (f : Module.End R M₂) : (LinearEquiv.conj (LinearEquiv.symm e)) f = (↑(LinearEquiv.symm e) ∘ₗ f) ∘ₗ ↑e

theorem LinearEquiv.conj_comp {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (e : M ≃ₗ[R] M₂) (f : Module.End R M) (g : Module.End R M) : (LinearEquiv.conj e) (g ∘ₗ f) = (LinearEquiv.conj e) g ∘ₗ (LinearEquiv.conj e) f

theorem LinearEquiv.conj_trans {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} {M₃ : Type u_13} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] (e₁ : M ≃ₗ[R] M₂) (e₂ : M₂ ≃ₗ[R] M₃) : LinearEquiv.conj e₁ ≪≫ₗ LinearEquiv.conj e₂ = LinearEquiv.conj (e₁ ≪≫ₗ e₂)

@[simp]

theorem LinearEquiv.conj_id {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (e : M ≃ₗ[R] M₂) : (LinearEquiv.conj e) LinearMap.id = LinearMap.id

def LinearEquiv.congrLeft (M : Type u_9) {M₂ : Type u_12} {M₃ : Type u_13} [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] {R : Type u_20} (S : Type u_21) [Semiring R] [Semiring S] [Module R M₂] [Module R M₃] [Module R M] [Module S M] [SMulCommClass R 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.

@[simp]

theorem LinearEquiv.smulOfNeZero_apply (K : Type u_7) (M : Type u_9) [Field K] [AddCommGroup M] [Module K M] (a : K) (ha : a ≠ 0) : ∀ (a_1 : M), (LinearEquiv.smulOfNeZero K M a ha) a_1 = a • a_1

@[simp]

theorem LinearEquiv.smulOfNeZero_symm_apply (K : Type u_7) (M : Type u_9) [Field K] [AddCommGroup M] [Module K M] (a : K) (ha : a ≠ 0) : ∀ (a_1 : M), (LinearEquiv.symm (LinearEquiv.smulOfNeZero K M a ha)) a_1 = (Units.mk0 a ha)⁻¹ • a_1

def LinearEquiv.smulOfNeZero (K : Type u_7) (M : Type u_9) [Field K] [AddCommGroup M] [Module K M] (a : K) (ha : a ≠ 0) : M ≃ₗ[K] M

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

Equations

• LinearEquiv.smulOfNeZero K M a ha = LinearEquiv.smulOfUnit (Units.mk0 a ha)

def Submodule.equivSubtypeMap {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) (q : Submodule R ↥p) : ↥q ≃ₗ[R] ↥(Submodule.map (Submodule.subtype p) q)

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.

@[simp]

theorem Submodule.equivSubtypeMap_apply {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {q : Submodule R ↥p} (x : ↥q) : ↑((Submodule.equivSubtypeMap p q) x) = (LinearMap.domRestrict (Submodule.subtype p) q) x

@[simp]

theorem Submodule.equivSubtypeMap_symm_apply {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {q : Submodule R ↥p} (x : ↥(Submodule.map (Submodule.subtype p) q)) : ↑↑((LinearEquiv.symm (Submodule.equivSubtypeMap p q)) 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} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {f : M →ₗ[R] N} {p : Submodule R N} (hf : Function.Injective ⇑f) (h : p ≤ LinearMap.range f) : ∀ (a : ↥(Submodule.comap f p)), (Submodule.comap_equiv_self_of_inj_of_le hf h) a = (LinearMap.codRestrict p (LinearMap.comp f (Submodule.subtype (Submodule.comap f p))) (_ : ∀ (x : ↥(Submodule.comap f p)), (f ∘ₗ Submodule.subtype (Submodule.comap f p)) x ∈ p)) a

noncomputable def Submodule.comap_equiv_self_of_inj_of_le {R : Type u_1} {M : Type u_9} {N : Type u_15} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {f : M →ₗ[R] N} {p : Submodule R N} (hf : Function.Injective ⇑f) (h : p ≤ LinearMap.range f) : ↥(Submodule.comap f p) ≃ₗ[R] ↥p

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

Equations

• One or more equations did not get rendered due to their size.

def Equiv.toLinearEquiv {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid 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.

def LinearMap.funLeft (R : Type u_1) (M : Type u_9) [Semiring R] [AddCommMonoid M] [Module R M] {m : Type u_20} {n : Type u_21} (f : m → n) : (n → M) →ₗ[R] m → M

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LinearMap.funLeft_apply (R : Type u_1) (M : Type u_9) [Semiring R] [AddCommMonoid M] [Module R M] {m : Type u_20} {n : Type u_21} (f : m → n) (g : n → M) (i : m) : (LinearMap.funLeft R M f) g i = g (f i)

@[simp]

theorem LinearMap.funLeft_id (R : Type u_1) (M : Type u_9) [Semiring R] [AddCommMonoid M] [Module R M] {n : Type u_21} (g : n → M) : (LinearMap.funLeft R M id) g = g

theorem LinearMap.funLeft_comp (R : Type u_1) (M : Type u_9) [Semiring R] [AddCommMonoid M] [Module R M] {m : Type u_20} {n : Type u_21} {p : Type u_22} (f₁ : n → p) (f₂ : m → n) : LinearMap.funLeft R M (f₁ ∘ f₂) = LinearMap.funLeft R M f₂ ∘ₗ LinearMap.funLeft R M f₁

theorem LinearMap.funLeft_surjective_of_injective (R : Type u_1) (M : Type u_9) [Semiring R] [AddCommMonoid M] [Module R M] {m : Type u_20} {n : Type u_21} (f : m → n) (hf : Function.Injective f) : Function.Surjective ⇑(LinearMap.funLeft R M f)

theorem LinearMap.funLeft_injective_of_surjective (R : Type u_1) (M : Type u_9) [Semiring R] [AddCommMonoid M] [Module R M] {m : Type u_20} {n : Type u_21} (f : m → n) (hf : Function.Surjective f) : Function.Injective ⇑(LinearMap.funLeft R M f)

def LinearEquiv.funCongrLeft (R : Type u_1) (M : Type u_9) [Semiring R] [AddCommMonoid M] [Module R M] {m : Type u_20} {n : Type u_21} (e : m ≃ n) : (n → M) ≃ₗ[R] m → M

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LinearEquiv.funCongrLeft_apply (R : Type u_1) (M : Type u_9) [Semiring R] [AddCommMonoid M] [Module R M] {m : Type u_20} {n : Type u_21} (e : m ≃ n) (x : n → M) : (LinearEquiv.funCongrLeft R M e) x = (LinearMap.funLeft R M ⇑e) x

@[simp]

theorem LinearEquiv.funCongrLeft_id (R : Type u_1) (M : Type u_9) [Semiring R] [AddCommMonoid M] [Module R M] {n : Type u_21} : LinearEquiv.funCongrLeft R M (Equiv.refl n) = LinearEquiv.refl R (n → M)

@[simp]

theorem LinearEquiv.funCongrLeft_comp (R : Type u_1) (M : Type u_9) [Semiring R] [AddCommMonoid M] [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₂) = LinearEquiv.funCongrLeft R M e₂ ≪≫ₗ LinearEquiv.funCongrLeft R M e₁

@[simp]

theorem LinearEquiv.funCongrLeft_symm (R : Type u_1) (M : Type u_9) [Semiring R] [AddCommMonoid M] [Module R M] {m : Type u_20} {n : Type u_21} (e : m ≃ n) : LinearEquiv.symm (LinearEquiv.funCongrLeft R M e) = LinearEquiv.funCongrLeft R M e.symm