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_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

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

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 ℤ).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

• addMonoidEndRingEquivInt A = let __src := addMonoidHomLequivInt ℤ; { toEquiv := { toFun := __src.toFun, invFun := __src.invFun, left_inv := ⋯, right_inv := ⋯ }, map_mul' := ⋯, map_add' := ⋯ }

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] [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) ⋯

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

• LinearMap.iterateRange f = { toFun := fun (n : ℕ) => LinearMap.range (f ^ n), monotone' := ⋯ }

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

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

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

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.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 = ⊤

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

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

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 := ⋯ } = 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} {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 (LinearMap.rangeRestrict f) = ⊤

theorem LinearMap.surjective_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₂) : Function.Surjective ⇑(LinearMap.rangeRestrict f)

@[simp]

theorem LinearMap.ker_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₂) : 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 := ⋯ }

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

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 ⋯

@[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 ⋯ = 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

• LinearEquiv.ofSubmodule' f U = LinearEquiv.symm (LinearEquiv.ofSubmodules (LinearEquiv.symm f) U (Submodule.comap (↑(LinearEquiv.symm (LinearEquiv.symm f))) U) ⋯)

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)) ⋯

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

• LinearEquiv.ofTop p h = let __src := Submodule.subtype p; { toLinearMap := __src, invFun := fun (x : M) => { val := x, property := ⋯ }, left_inv := ⋯, right_inv := ⋯ }

@[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 := ⋯ }

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

• LinearEquiv.ofLinear f g h₁ h₂ = { toLinearMap := f, invFun := ⇑g, left_inv := ⋯, right_inv := ⋯ }

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

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 ⋯

@[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 ⋯) (LinearEquiv.ofTop (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_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

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

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))) ⋯) 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

• Submodule.comap_equiv_self_of_inj_of_le hf h = LinearEquiv.ofBijective (LinearMap.codRestrict p (LinearMap.comp f (Submodule.subtype (Submodule.comap f p))) ⋯) ⋯

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

• LinearMap.funLeft R M f = { toAddHom := { toFun := fun (x : n → M) => x ∘ f, map_add' := ⋯ }, map_smul' := ⋯ }

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

• LinearEquiv.funCongrLeft R M e = LinearEquiv.ofLinear (LinearMap.funLeft R M ⇑e) (LinearMap.funLeft R M ⇑e.symm) ⋯ ⋯

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