Linear algebra

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

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

Main definitions

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

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

Main theorems

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

Notations

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

Implementation notes

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

TODO

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

Tags

linear algebra, vector space, module

theorem Finsupp.smul_sum {α : Type u_20} {β : Type u_21} {R : Type u_22} {M : Type u_23} [Zero β] [AddCommMonoid M] [DistribSMul R M] {v : α →₀ β} {c : R} {h : α → β → M} : c • Finsupp.sum v h = Finsupp.sum v fun a b => c • h a b

@[simp]

theorem Finsupp.sum_smul_index_linearMap' {α : Type u_20} {R : Type u_21} {M : Type u_22} {M₂ : Type u_23} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [Module R M₂] {v : α →₀ M} {c : R} {h : α → M →ₗ[R] M₂} : (Finsupp.sum (c • v) fun a => ↑(h a)) = c • Finsupp.sum v fun a => ↑(h a)

@[simp]

theorem Finsupp.linearEquivFunOnFinite_apply (R : Type u_1) (M : Type u_9) (α : Type u_20) [Finite α] [AddCommMonoid M] [Semiring R] [Module R M] : ∀ (a : α →₀ M) (a_1 : α), ↑(Finsupp.linearEquivFunOnFinite R M α) a a_1 = ↑a a_1

noncomputable def Finsupp.linearEquivFunOnFinite (R : Type u_1) (M : Type u_9) (α : Type u_20) [Finite α] [AddCommMonoid M] [Semiring R] [Module R M] : (α →₀ M) ≃ₗ[R] α → M

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

Equations

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

@[simp]

theorem Finsupp.linearEquivFunOnFinite_single (R : Type u_1) (M : Type u_9) (α : Type u_20) [Finite α] [AddCommMonoid M] [Semiring R] [Module R M] [DecidableEq α] (x : α) (m : M) : (↑(Finsupp.linearEquivFunOnFinite R M α) fun₀ | x => m) = Pi.single x m

@[simp]

theorem Finsupp.linearEquivFunOnFinite_symm_single (R : Type u_1) (M : Type u_9) (α : Type u_20) [Finite α] [AddCommMonoid M] [Semiring R] [Module R M] [DecidableEq α] (x : α) (m : M) : ↑(LinearEquiv.symm (Finsupp.linearEquivFunOnFinite R M α)) (Pi.single x m) = fun₀ | x => m

@[simp]

theorem Finsupp.linearEquivFunOnFinite_symm_coe (R : Type u_1) (M : Type u_9) (α : Type u_20) [Finite α] [AddCommMonoid M] [Semiring R] [Module R M] (f : α →₀ M) : ↑(LinearEquiv.symm (Finsupp.linearEquivFunOnFinite R M α)) ↑f = f

noncomputable def Finsupp.LinearEquiv.finsuppUnique (R : Type u_1) (M : Type u_9) [AddCommMonoid M] [Semiring R] [Module R M] (α : Type u_21) [Unique α] : (α →₀ M) ≃ₗ[R] M

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

Equations

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

@[simp]

theorem Finsupp.LinearEquiv.finsuppUnique_apply {R : Type u_1} {M : Type u_9} [AddCommMonoid M] [Semiring R] [Module R M] (α : Type u_21) [Unique α] (f : α →₀ M) : ↑(Finsupp.LinearEquiv.finsuppUnique R M α) f = ↑f default

@[simp]

theorem Finsupp.LinearEquiv.finsuppUnique_symm_apply {R : Type u_1} {M : Type u_9} [AddCommMonoid M] [Semiring R] [Module R M] {α : Type u_21} [Unique α] (m : M) : ↑(LinearEquiv.symm (Finsupp.LinearEquiv.finsuppUnique R M α)) m = fun₀ | default => m

theorem pi_eq_sum_univ {ι : Type u_20} [Fintype ι] [DecidableEq ι] {R : Type u_21} [Semiring R] (x : ι → R) : x = Finset.sum Finset.univ fun i => x i • fun j => if i = j then 1 else 0

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

Properties of linear maps

def LinearMap.domRestrict {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₂) (p : Submodule R M) : { x // x ∈ p } →ₛₗ[σ₁₂] M₂

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

Equations

• LinearMap.domRestrict f p = LinearMap.comp f (Submodule.subtype p)

@[simp]

theorem LinearMap.domRestrict_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₂} (f : M →ₛₗ[σ₁₂] M₂) (p : Submodule R M) (x : { x // x ∈ p }) : ↑(LinearMap.domRestrict f p) x = ↑f ↑x

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

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

Equations

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

@[simp]

theorem LinearMap.codRestrict_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₂} (p : Submodule R₂ M₂) (f : M →ₛₗ[σ₁₂] M₂) {h : ∀ (c : M), ↑f c ∈ p} (x : M) : ↑(↑(LinearMap.codRestrict p f h) x) = ↑f x

@[simp]

theorem LinearMap.comp_codRestrict {R : Type u_1} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_9} {M₂ : Type u_12} {M₃ : Type u_13} [Semiring R] [Semiring R₂] [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₃) (p : Submodule R₃ M₃) (h : ∀ (b : M₂), ↑g b ∈ p) : LinearMap.comp (LinearMap.codRestrict p g h) f = LinearMap.codRestrict p (LinearMap.comp g f) fun x => h (↑f x)

@[simp]

theorem LinearMap.subtype_comp_codRestrict {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (f : M →ₛₗ[σ₁₂] M₂) (p : Submodule R₂ M₂) (h : ∀ (b : M), ↑f b ∈ p) : LinearMap.comp (Submodule.subtype p) (LinearMap.codRestrict p f h) = f

def LinearMap.restrict {R : Type u_1} {M : Type u_9} {M₁ : Type u_11} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₁] [Module R M] [Module R M₁] (f : M →ₗ[R] M₁) {p : Submodule R M} {q : Submodule R M₁} (hf : ∀ (x : M), x ∈ p → ↑f x ∈ q) : { x // x ∈ p } →ₗ[R] { x // x ∈ q }

Restrict domain and codomain of a linear map.

Equations

• LinearMap.restrict f hf = LinearMap.codRestrict q (LinearMap.domRestrict f p) (_ : ∀ (x : { x // x ∈ p }), ↑(LinearMap.domRestrict f p) x ∈ q)

@[simp]

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

theorem LinearMap.restrict_apply {R : Type u_1} {M : Type u_9} {M₁ : Type u_11} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₁] [Module R M] [Module R M₁] {f : M →ₗ[R] M₁} {p : Submodule R M} {q : Submodule R M₁} (hf : ∀ (x : M), x ∈ p → ↑f x ∈ q) (x : { x // x ∈ p }) : ↑(LinearMap.restrict f hf) x = { val := ↑f ↑x, property := hf ↑x (_ : ↑x ∈ p) }

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

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

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

instance LinearMap.uniqueOfLeft {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₂} [Subsingleton M] : Unique (M →ₛₗ[σ₁₂] M₂)

Equations

• LinearMap.uniqueOfLeft = let src := inferInstanceAs (Inhabited (M →ₛₗ[σ₁₂] M₂)); { toInhabited := { default := default }, uniq := (_ : ∀ (f : M →ₛₗ[σ₁₂] M₂), f = default) }

instance LinearMap.uniqueOfRight {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₂} [Subsingleton M₂] : Unique (M →ₛₗ[σ₁₂] M₂)

Equations

• LinearMap.uniqueOfRight = Function.Injective.unique (_ : Function.Injective FunLike.coe)

def LinearMap.evalAddMonoidHom {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₂} (a : M) : (M →ₛₗ[σ₁₂] M₂) →+ M₂

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

Equations

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

def LinearMap.toAddMonoidHom' {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₂} : (M →ₛₗ[σ₁₂] M₂) →+ M →+ M₂

LinearMap.toAddMonoidHom promoted to a AddMonoidHom

Equations

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

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

def LinearMap.smulRight {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₁ : Type u_11} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₁] [Module R M] [Module R M₁] [Semiring S] [Module R S] [Module S M] [IsScalarTower R S M] (f : M₁ →ₗ[R] S) (x : M) : M₁ →ₗ[R] M

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

Equations

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

@[simp]

theorem LinearMap.coe_smulRight {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₁ : Type u_11} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₁] [Module R M] [Module R M₁] [Semiring S] [Module R S] [Module S M] [IsScalarTower R S M] (f : M₁ →ₗ[R] S) (x : M) : ↑(LinearMap.smulRight f x) = fun c => ↑f c • x

theorem LinearMap.smulRight_apply {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₁ : Type u_11} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₁] [Module R M] [Module R M₁] [Semiring S] [Module R S] [Module S M] [IsScalarTower R S M] (f : M₁ →ₗ[R] S) (x : M) (c : M₁) : ↑(LinearMap.smulRight f x) c = ↑f c • x

instance LinearMap.instNontrivialEnd {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial M] : Nontrivial (Module.End R M)

Equations

• @LinearMap.instNontrivialEnd = @LinearMap.instNontrivialEnd.proof_1

@[simp]

theorem LinearMap.coeFn_sum {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₂} {ι : Type u_20} (t : Finset ι) (f : ι → M →ₛₗ[σ₁₂] M₂) : ↑(Finset.sum t fun i => f i) = Finset.sum t fun i => ↑(f i)

theorem LinearMap.submodule_pow_eq_zero_of_pow_eq_zero {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} {g : Module.End R { x // x ∈ N }} {G : Module.End R M} (h : LinearMap.comp G (Submodule.subtype N) = LinearMap.comp (Submodule.subtype N) g) {k : ℕ} (hG : G ^ k = 0) : g ^ k = 0

theorem LinearMap.pow_apply_mem_of_forall_mem {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] {f' : M →ₗ[R] M} {p : Submodule R M} (n : ℕ) (h : ∀ (x : M), x ∈ p → ↑f' x ∈ p) (x : M) (hx : x ∈ p) : ↑(f' ^ n) x ∈ p

theorem LinearMap.pow_restrict {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] {f' : M →ₗ[R] M} {p : Submodule R M} (n : ℕ) (h : ∀ (x : M), x ∈ p → ↑f' x ∈ p) (h' : optParam (∀ (x : M), x ∈ p → ↑(f' ^ n) x ∈ p) (_ : ∀ (x : M), x ∈ p → ↑(f' ^ n) x ∈ p)) : LinearMap.restrict f' h ^ n = LinearMap.restrict (f' ^ n) h'

theorem LinearMap.pi_apply_eq_sum_univ {R : Type u_1} {M : Type u_9} {ι : Type u_17} [Semiring R] [AddCommMonoid M] [Module R M] [Fintype ι] [DecidableEq ι] (f : (ι → R) →ₗ[R] M) (x : ι → R) : ↑f x = Finset.sum Finset.univ fun i => x i • ↑f fun j => if i = j then 1 else 0

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

@[simp]

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

def LinearMap.applyₗ' {R : Type u_1} (S : Type u_6) {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M₂] [SMulCommClass R S M₂] : M →+ (M →ₗ[R] M₂) →ₗ[S] M₂

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

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

Equations

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

@[simp]

theorem LinearMap.ringLmapEquivSelf_symm_apply (R : Type u_1) (S : Type u_6) (M : Type u_9) [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMulCommClass R S M] (x : M) : ↑(LinearEquiv.symm (LinearMap.ringLmapEquivSelf R S M)) x = LinearMap.smulRight 1 x

@[simp]

theorem LinearMap.ringLmapEquivSelf_apply (R : Type u_1) (S : Type u_6) (M : Type u_9) [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMulCommClass R S M] (f : R →ₗ[R] M) : ↑(LinearMap.ringLmapEquivSelf R S M) f = ↑f 1

def LinearMap.ringLmapEquivSelf (R : Type u_1) (S : Type u_6) (M : Type u_9) [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMulCommClass R S M] : (R →ₗ[R] M) ≃ₗ[S] M

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

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

Equations

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

def LinearMap.compRight {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₃

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

Equations

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

@[simp]

theorem LinearMap.compRight_apply {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₃) (g : M →ₗ[R] M₂) : ↑(LinearMap.compRight f) g = LinearMap.comp f g

@[simp]

theorem LinearMap.applyₗ_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₂] (v : M) (f : M →ₗ[R] M₂) : ↑(↑LinearMap.applyₗ v) f = ↑f v

def LinearMap.applyₗ {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] : M →ₗ[R] (M →ₗ[R] M₂) →ₗ[R] M₂

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

This is the LinearMap version of toAddMonoidHom.eval.

Equations

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

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

Alternative version of domRestrict as a linear map.

Equations

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

@[simp]

theorem LinearMap.domRestrict'_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₂] (f : M →ₗ[R] M₂) (p : Submodule R M) (x : { x // x ∈ p }) : ↑(↑(LinearMap.domRestrict' p) f) x = ↑f ↑x

def LinearMap.smulRightₗ {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] : (M₂ →ₗ[R] R) →ₗ[R] M →ₗ[R] M₂ →ₗ[R] M

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

Equations

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

@[simp]

theorem LinearMap.smulRightₗ_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₂] (f : M₂ →ₗ[R] R) (x : M) (c : M₂) : ↑(↑(↑LinearMap.smulRightₗ f) x) c = ↑f c • x

@[simp]

theorem addMonoidHomLequivNat_apply {A : Type u_20} {B : Type u_21} (R : Type u_22) [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.

Properties of submodules

def Submodule.ofLe {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') : { x // x ∈ p } →ₗ[R] { x // x ∈ p' }

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

Equations

• Submodule.ofLe h = LinearMap.codRestrict p' (Submodule.subtype p) (_ : ∀ (x : { x // x ∈ p }), ↑(Submodule.subtype p) x ∈ p')

@[simp]

theorem Submodule.coe_ofLe {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') (x : { x // x ∈ p }) : ↑(↑(Submodule.ofLe h) x) = ↑x

theorem Submodule.ofLe_apply {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') (x : { x // x ∈ p }) : ↑(Submodule.ofLe h) x = { val := ↑x, property := h ↑x (_ : ↑x ∈ p) }

theorem Submodule.ofLe_injective {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') : Function.Injective ↑(Submodule.ofLe h)

theorem Submodule.subtype_comp_ofLe {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.comp (Submodule.subtype q) (Submodule.ofLe h) = Submodule.subtype p

def Submodule.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₂} [RingHomSurjective σ₁₂] {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] (f : F) (p : Submodule R M) : Submodule R₂ M₂

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

Equations

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

@[simp]

theorem Submodule.map_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₂} [RingHomSurjective σ₁₂] {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] (f : F) (p : Submodule R M) : ↑(Submodule.map f p) = ↑f '' ↑p

theorem Submodule.map_toAddSubmonoid {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [RingHomSurjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (p : Submodule R M) : (Submodule.map f p).toAddSubmonoid = AddSubmonoid.map (↑f) p.toAddSubmonoid

theorem Submodule.map_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₂) (p : Submodule R M) : (Submodule.map f p).toAddSubmonoid = AddSubmonoid.map f p.toAddSubmonoid

@[simp]

theorem Submodule.mem_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₂} [RingHomSurjective σ₁₂] {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] {f : F} {p : Submodule R M} {x : M₂} : x ∈ Submodule.map f p ↔ ∃ y, y ∈ p ∧ ↑f y = x

theorem Submodule.mem_map_of_mem {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [RingHomSurjective σ₁₂] {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] {f : F} {p : Submodule R M} {r : M} (h : r ∈ p) : ↑f r ∈ Submodule.map f p

theorem Submodule.apply_coe_mem_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₂} [RingHomSurjective σ₁₂] {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] (f : F) {p : Submodule R M} (r : { x // x ∈ p }) : ↑f ↑r ∈ Submodule.map f p

@[simp]

theorem Submodule.map_id {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) : Submodule.map LinearMap.id p = p

theorem Submodule.map_comp {R : Type u_1} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_9} {M₂ : Type u_12} {M₃ : Type u_13} [Semiring R] [Semiring R₂] [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₃) (p : Submodule R M) : Submodule.map (LinearMap.comp g f) p = Submodule.map g (Submodule.map f p)

theorem Submodule.map_mono {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 : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] {f : F} {p : Submodule R M} {p' : Submodule R M} : p ≤ p' → Submodule.map f p ≤ Submodule.map f p'

@[simp]

theorem Submodule.map_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₂} (p : Submodule R M) [RingHomSurjective σ₁₂] : Submodule.map 0 p = ⊥

theorem Submodule.map_add_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₂} (p : Submodule R M) [RingHomSurjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (g : M →ₛₗ[σ₁₂] M₂) : Submodule.map (f + g) p ≤ Submodule.map f p ⊔ Submodule.map g p

theorem Submodule.range_map_nonempty {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 σ₁₂] (N : Submodule R M) : Set.Nonempty (Set.range fun ϕ => Submodule.map ϕ N)

noncomputable def Submodule.equivMapOfInjective {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 σ₂₁ σ₁₂] {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] (f : F) (i : Function.Injective ↑f) (p : Submodule R M) : { x // x ∈ p } ≃ₛₗ[σ₁₂] { x // x ∈ Submodule.map f p }

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

Equations

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

@[simp]

theorem Submodule.coe_equivMapOfInjective_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 σ₂₁ σ₁₂] {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] (f : F) (i : Function.Injective ↑f) (p : Submodule R M) (x : { x // x ∈ p }) : ↑(↑(Submodule.equivMapOfInjective f i p) x) = ↑f ↑x

def Submodule.comap {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] (f : F) (p : Submodule R₂ M₂) : Submodule R M

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

Equations

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

@[simp]

theorem Submodule.comap_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} [sc : SemilinearMapClass F σ₁₂ M M₂] (f : F) (p : Submodule R₂ M₂) : ↑(Submodule.comap f p) = ↑f ⁻¹' ↑p

@[simp]

theorem Submodule.mem_comap {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {x : M} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] {f : F} {p : Submodule R₂ M₂} : x ∈ Submodule.comap f p ↔ ↑f x ∈ p

@[simp]

theorem Submodule.comap_id {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) : Submodule.comap LinearMap.id p = p

theorem Submodule.comap_comp {R : Type u_1} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_9} {M₂ : Type u_12} {M₃ : Type u_13} [Semiring R] [Semiring R₂] [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₃) (p : Submodule R₃ M₃) : Submodule.comap (LinearMap.comp g f) p = Submodule.comap f (Submodule.comap g p)

theorem Submodule.comap_mono {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} [sc : SemilinearMapClass F σ₁₂ M M₂] {f : F} {q : Submodule R₂ M₂} {q' : Submodule R₂ M₂} : q ≤ q' → Submodule.comap f q ≤ Submodule.comap f q'

theorem Submodule.le_comap_pow_of_le_comap {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) {f : M →ₗ[R] M} (h : p ≤ Submodule.comap f p) (k : ℕ) : p ≤ Submodule.comap (f ^ k) p

theorem Submodule.map_le_iff_le_comap {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} {p : Submodule R M} {q : Submodule R₂ M₂} : Submodule.map f p ≤ q ↔ p ≤ Submodule.comap f q

theorem Submodule.gc_map_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} [sc : SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] (f : F) : GaloisConnection (Submodule.map f) (Submodule.comap f)

@[simp]

theorem Submodule.map_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} [sc : SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] (f : F) : Submodule.map f ⊥ = ⊥

@[simp]

theorem Submodule.map_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₂} (p : Submodule R M) (p' : Submodule R M) {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] (f : F) : Submodule.map f (p ⊔ p') = Submodule.map f p ⊔ Submodule.map f p'

@[simp]

theorem Submodule.map_iSup {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} [sc : SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {ι : Sort u_21} (f : F) (p : ι → Submodule R M) : Submodule.map f (⨆ (i : ι), p i) = ⨆ (i : ι), Submodule.map f (p i)

@[simp]

theorem Submodule.comap_top {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] (f : F) : Submodule.comap f ⊤ = ⊤

@[simp]

theorem Submodule.comap_inf {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₂} (q : Submodule R₂ M₂) (q' : Submodule R₂ M₂) {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] (f : F) : Submodule.comap f (q ⊓ q') = Submodule.comap f q ⊓ Submodule.comap f q'

@[simp]

theorem Submodule.comap_iInf {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} [sc : SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {ι : Sort u_21} (f : F) (p : ι → Submodule R₂ M₂) : Submodule.comap f (⨅ (i : ι), p i) = ⨅ (i : ι), Submodule.comap f (p i)

@[simp]

theorem Submodule.comap_zero {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (q : Submodule R₂ M₂) : Submodule.comap 0 q = ⊤

theorem Submodule.map_comap_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} [sc : SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] (f : F) (q : Submodule R₂ M₂) : Submodule.map f (Submodule.comap f q) ≤ q

theorem Submodule.le_comap_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} [sc : SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] (f : F) (p : Submodule R M) : p ≤ Submodule.comap f (Submodule.map f p)

def Submodule.giMapComap {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} [sc : SemilinearMapClass F σ₁₂ M M₂] {f : F} (hf : Function.Surjective ↑f) [RingHomSurjective σ₁₂] : GaloisInsertion (Submodule.map f) (Submodule.comap f)

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

Equations

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

theorem Submodule.map_comap_eq_of_surjective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] {f : F} (hf : Function.Surjective ↑f) [RingHomSurjective σ₁₂] (p : Submodule R₂ M₂) : Submodule.map f (Submodule.comap f p) = p

theorem Submodule.map_surjective_of_surjective {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} [sc : SemilinearMapClass F σ₁₂ M M₂] {f : F} (hf : Function.Surjective ↑f) [RingHomSurjective σ₁₂] : Function.Surjective (Submodule.map f)

theorem Submodule.comap_injective_of_surjective {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} [sc : SemilinearMapClass F σ₁₂ M M₂] {f : F} (hf : Function.Surjective ↑f) [RingHomSurjective σ₁₂] : Function.Injective (Submodule.comap f)

theorem Submodule.map_sup_comap_of_surjective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] {f : F} (hf : Function.Surjective ↑f) [RingHomSurjective σ₁₂] (p : Submodule R₂ M₂) (q : Submodule R₂ M₂) : Submodule.map f (Submodule.comap f p ⊔ Submodule.comap f q) = p ⊔ q

theorem Submodule.map_iSup_comap_of_sujective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] {f : F} (hf : Function.Surjective ↑f) [RingHomSurjective σ₁₂] {ι : Sort u_21} (S : ι → Submodule R₂ M₂) : Submodule.map f (⨆ (i : ι), Submodule.comap f (S i)) = iSup S

theorem Submodule.map_inf_comap_of_surjective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] {f : F} (hf : Function.Surjective ↑f) [RingHomSurjective σ₁₂] (p : Submodule R₂ M₂) (q : Submodule R₂ M₂) : Submodule.map f (Submodule.comap f p ⊓ Submodule.comap f q) = p ⊓ q

theorem Submodule.map_iInf_comap_of_surjective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] {f : F} (hf : Function.Surjective ↑f) [RingHomSurjective σ₁₂] {ι : Sort u_21} (S : ι → Submodule R₂ M₂) : Submodule.map f (⨅ (i : ι), Submodule.comap f (S i)) = iInf S

theorem Submodule.comap_le_comap_iff_of_surjective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] {f : F} (hf : Function.Surjective ↑f) [RingHomSurjective σ₁₂] (p : Submodule R₂ M₂) (q : Submodule R₂ M₂) : Submodule.comap f p ≤ Submodule.comap f q ↔ p ≤ q

theorem Submodule.comap_strictMono_of_surjective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] {f : F} (hf : Function.Surjective ↑f) [RingHomSurjective σ₁₂] : StrictMono (Submodule.comap f)

def Submodule.gciMapComap {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} [sc : SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Injective ↑f) : GaloisCoinsertion (Submodule.map f) (Submodule.comap f)

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

Equations

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

theorem Submodule.comap_map_eq_of_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Injective ↑f) (p : Submodule R M) : Submodule.comap f (Submodule.map f p) = p

theorem Submodule.comap_surjective_of_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Injective ↑f) : Function.Surjective (Submodule.comap f)

theorem Submodule.map_injective_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} [sc : SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Injective ↑f) : Function.Injective (Submodule.map f)

theorem Submodule.comap_inf_map_of_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Injective ↑f) (p : Submodule R M) (q : Submodule R M) : Submodule.comap f (Submodule.map f p ⊓ Submodule.map f q) = p ⊓ q

theorem Submodule.comap_iInf_map_of_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Injective ↑f) {ι : Sort u_21} (S : ι → Submodule R M) : Submodule.comap f (⨅ (i : ι), Submodule.map f (S i)) = iInf S

theorem Submodule.comap_sup_map_of_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Injective ↑f) (p : Submodule R M) (q : Submodule R M) : Submodule.comap f (Submodule.map f p ⊔ Submodule.map f q) = p ⊔ q

theorem Submodule.comap_iSup_map_of_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Injective ↑f) {ι : Sort u_21} (S : ι → Submodule R M) : Submodule.comap f (⨆ (i : ι), Submodule.map f (S i)) = iSup S

theorem Submodule.map_le_map_iff_of_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Injective ↑f) (p : Submodule R M) (q : Submodule R M) : Submodule.map f p ≤ Submodule.map f q ↔ p ≤ q

theorem Submodule.map_strictMono_of_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Injective ↑f) : StrictMono (Submodule.map f)

@[simp]

theorem Submodule.orderIsoMapComap_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 σ₂₁ σ₁₂] {F : Type u_20} [SemilinearEquivClass F σ₁₂ M M₂] (f : F) (p : Submodule R M) : ↑(Submodule.orderIsoMapComap f) p = Submodule.map f p

@[simp]

theorem Submodule.orderIsoMapComap_symm_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {F : Type u_20} [SemilinearEquivClass F σ₁₂ M M₂] (f : F) (p : Submodule R₂ M₂) : ↑(RelIso.symm (Submodule.orderIsoMapComap f)) p = Submodule.comap f p

def Submodule.orderIsoMapComap {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 σ₂₁ σ₁₂] {F : Type u_20} [SemilinearEquivClass F σ₁₂ M M₂] (f : F) : Submodule R M ≃o Submodule R₂ M₂

A linear isomorphism induces an order isomorphism of submodules.

Equations

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

theorem Submodule.map_inf_eq_map_inf_comap {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_20} [sc : SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} {p : Submodule R M} {p' : Submodule R₂ M₂} : Submodule.map f p ⊓ p' = Submodule.map f (p ⊓ Submodule.comap f p')

theorem Submodule.map_comap_subtype {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) (p' : Submodule R M) : Submodule.map (Submodule.subtype p) (Submodule.comap (Submodule.subtype p) p') = p ⊓ p'

theorem Submodule.eq_zero_of_bot_submodule {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : { x // x ∈ ⊥ }) : b = 0

theorem LinearMap.iInf_invariant {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] {σ : R →+* R} [RingHomSurjective σ] {ι : Sort u_21} (f : M →ₛₗ[σ] M) {p : ι → Submodule R M} (hf : ∀ (i : ι) (v : M), v ∈ p i → ↑f v ∈ p i) (v : M) : v ∈ iInf p → ↑f v ∈ iInf p

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

theorem Submodule.neg_coe {R : Type u_1} {M : Type u_9} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) : -↑p = ↑p

@[simp]

theorem Submodule.map_neg {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) [AddCommGroup M₂] [Module R M₂] (f : M →ₗ[R] M₂) : Submodule.map (-f) p = Submodule.map f p

theorem Submodule.comap_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₂) (p : Submodule K V₂) (a : K) (h : a ≠ 0) : Submodule.comap (a • f) p = Submodule.comap f p

theorem Submodule.map_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₂) (p : Submodule K V) (a : K) (h : a ≠ 0) : Submodule.map (a • f) p = Submodule.map f p

theorem Submodule.comap_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₂) (p : Submodule K V₂) (a : K) : Submodule.comap (a • f) p = ⨅ (_ : a ≠ 0), Submodule.comap f p

theorem Submodule.map_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₂) (p : Submodule K V) (a : K) : Submodule.map (a • f) p = ⨆ (_ : a ≠ 0), Submodule.map f p

Properties of linear maps

theorem LinearMap.coe_finsupp_sum {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} {ι : Type u_17} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {σ₁₂ : R →+* R₂} [Module R M] [Module R₂ M₂] {γ : Type u_20} [Zero γ] (t : ι →₀ γ) (g : ι → γ → M →ₛₗ[σ₁₂] M₂) : ↑(Finsupp.sum t g) = ↑(Finsupp.sum t fun i d => g i d)

@[simp]

theorem LinearMap.finsupp_sum_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} {ι : Type u_17} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {σ₁₂ : R →+* R₂} [Module R M] [Module R₂ M₂] {γ : Type u_20} [Zero γ] (t : ι →₀ γ) (g : ι → γ → M →ₛₗ[σ₁₂] M₂) (b : M) : ↑(Finsupp.sum t g) b = Finsupp.sum t fun i d => ↑(g i d) b

theorem LinearMap.coe_dfinsupp_sum {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} {ι : Type u_17} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {σ₁₂ : R →+* R₂} [Module R M] [Module R₂ M₂] {γ : ι → Type u_20} [DecidableEq ι] [(i : ι) → Zero (γ i)] [(i : ι) → (x : γ i) → Decidable (x ≠ 0)] (t : Π₀ (i : ι), γ i) (g : (i : ι) → γ i → M →ₛₗ[σ₁₂] M₂) : ↑(DFinsupp.sum t g) = ↑(DFinsupp.sum t fun i d => g i d)

@[simp]

theorem LinearMap.dfinsupp_sum_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} {ι : Type u_17} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {σ₁₂ : R →+* R₂} [Module R M] [Module R₂ M₂] {γ : ι → Type u_20} [DecidableEq ι] [(i : ι) → Zero (γ i)] [(i : ι) → (x : γ i) → Decidable (x ≠ 0)] (t : Π₀ (i : ι), γ i) (g : (i : ι) → γ i → M →ₛₗ[σ₁₂] M₂) (b : M) : ↑(DFinsupp.sum t g) b = DFinsupp.sum t fun i d => ↑(g i d) b

@[simp]

theorem LinearMap.map_dfinsupp_sumAddHom {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} {ι : Type u_17} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {σ₁₂ : R →+* R₂} [Module R M] [Module R₂ M₂] {γ : ι → Type u_20} [DecidableEq ι] [(i : ι) → AddZeroClass (γ i)] (f : M →ₛₗ[σ₁₂] M₂) {t : Π₀ (i : ι), γ i} {g : (i : ι) → γ i →+ M} : ↑f (↑(DFinsupp.sumAddHom g) t) = ↑(DFinsupp.sumAddHom fun i => AddMonoidHom.comp (LinearMap.toAddMonoidHom f) (g i)) t

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 { x // x ∈ 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} [sc : 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} [sc : 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} [sc : SemilinearMapClass F τ₁₂ M M₂] [RingHomSurjective τ₁₂] {f : F} {x : M₂} : x ∈ LinearMap.range f ↔ ∃ y, ↑f y = x

theorem LinearMap.range_eq_map {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : 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} [sc : 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} [sc : 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} [sc : 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} [sc : 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

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} [sc : 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} [sc : 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} [sc : 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} [sc : 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} [sc : 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} [sc : 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} [sc : 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} [sc : 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 →ₛₗ[τ₁₂] { x // x ∈ 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 { x // x ∈ 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} [sc : 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} [sc : 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} [sc : SemilinearMapClass F τ₁₂ M M₂] (f : F) (x : { x // 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.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} [sc : SemilinearMapClass F τ₁₂ M M₂] {f : F} {p : Submodule R M} : Disjoint p (LinearMap.ker f) ↔ ∀ (x : M), 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} [sc : 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} [sc : 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 : M), 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} [sc : 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} [sc : 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

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} [sc : 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} [sc : 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} [sc : 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} [sc : 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} [sc : SemilinearMapClass F τ₁₂ M M₂] {f : F} {p : Submodule R M} : Disjoint p (LinearMap.ker f) ↔ ∀ (x : M), x ∈ p → ∀ (y : M), 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} [sc : 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) [sc : 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} [sc : SemilinearMapClass F τ₁₂ M M₂] {f : F} [RingHomSurjective τ₁₂] {p : Submodule R M} : LinearMap.ker f ≤ p ↔ ∃ y, 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 = ⊥

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 => x.fst + x.snd

theorem IsLinearMap.isLinearMap_sub {R : Type u_20} {M : Type u_21} [Semiring R] [AddCommGroup M] [Module R M] : IsLinearMap R fun x => x.fst - x.snd

@[simp]

theorem Submodule.map_top {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_20} [sc : 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} [sc : 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 { x // x ∈ 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_ofLe {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.ofLe h) = ⊥

theorem Submodule.range_ofLe {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.ofLe h) = Submodule.comap (Submodule.subtype q) p

@[simp]

theorem Submodule.map_subtype_range_ofLe {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.ofLe 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 { x // x ∈ p } ≃o { p' // p' ≤ p }

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

Equations

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

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 { x // x ∈ 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

• Submodule.MapSubtype.orderEmbedding p = RelEmbedding.trans (RelIso.toRelEmbedding (Submodule.MapSubtype.relIso p)) (Subtype.relEmbedding (fun p p' => p ≤ p') fun p' => p' ≤ p)

@[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 { x // x ∈ 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 : { x // x ∈ 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} (ϕ : { x // x ∈ 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} {ϕ : { x // x ∈ O } →ₗ[R] M'} {N : Submodule R M} {x : M'} : x ∈ LinearMap.submoduleImage ϕ N ↔ ∃ y yO x, ↑ϕ { 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} {ϕ : { x // x ∈ O } →ₗ[R] M'} {N : Submodule R M} (hNO : N ≤ O) {x : M'} : x ∈ LinearMap.submoduleImage ϕ N ↔ ∃ y yN, ↑ϕ { val := y, property := hNO y yN } = x

theorem LinearMap.submoduleImage_apply_ofLe {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} (ϕ : { x // x ∈ O } →ₗ[R] M') (N : Submodule R M) (hNO : N ≤ O) : LinearMap.submoduleImage ϕ N = LinearMap.range (LinearMap.comp ϕ (Submodule.ofLe 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) : { x // x ∈ p } ≃ₛₗ[σ₁₂] { x // x ∈ Submodule.map (↑e) p }

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

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

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

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 : { x // 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 : { x // x ∈ Submodule.map (↑e) p }) : ↑(↑(LinearEquiv.symm (LinearEquiv.submoduleMap e p)) x) = ↑(LinearEquiv.symm e) ↑x

@[simp]

theorem LinearEquiv.map_dfinsupp_sumAddHom {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} {ι : Type u_17} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁] [RingHomInvPair τ₂₁ τ₁₂] {γ : ι → Type u_20} [DecidableEq ι] [(i : ι) → AddZeroClass (γ i)] (f : M ≃ₛₗ[τ₁₂] M₂) (t : Π₀ (i : ι), γ i) (g : (i : ι) → γ i →+ M) : ↑f (↑(DFinsupp.sumAddHom g) t) = ↑(DFinsupp.sumAddHom fun i => AddMonoidHom.comp (AddEquiv.toAddMonoidHom (LinearEquiv.toAddEquiv f)) (g i)) t

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) : { x // x ∈ p } ≃ₗ[R] { x // x ∈ 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 : { x // 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 { x // x ∈ 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) : { x // x ∈ p } ≃ₛₗ[σ₁₂] { x // x ∈ 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 : { x // 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 : { x // 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₂) : { x // x ∈ Submodule.comap (↑f) U } ≃ₛₗ[σ₁₂] { x // x ∈ 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 : { x // 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 : { x // 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 : { x // 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 = ⊤) : { x // x ∈ 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 : { x // 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} [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 : { x // x ∈ p } ≃ₛₗ[σ₁₂] { x // x ∈ ⊥ }) : 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 ≃ₛₗ[σ₁₂] { x // x ∈ 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 : { x // 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 ≃ₛₗ[σ₁₂] { x // x ∈ 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

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₃) (LinearMap.comp g f) = LinearMap.comp (↑(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.trans (LinearEquiv.arrowCongr e₁ e₂) (LinearEquiv.arrowCongr e₃ e₄) = LinearEquiv.arrowCongr (LinearEquiv.trans e₁ e₃) (LinearEquiv.trans 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 = LinearMap.comp (LinearMap.comp (↑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 = LinearMap.comp (LinearMap.comp (↑(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) (LinearMap.comp g f) = LinearMap.comp (↑(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.trans (LinearEquiv.conj e₁) (LinearEquiv.conj e₂) = LinearEquiv.conj (LinearEquiv.trans 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

@[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 : M), ↑(LinearEquiv.smulOfNeZero K M a ha) a = a • a

@[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 : M), ↑(LinearEquiv.symm (LinearEquiv.smulOfNeZero K M a ha)) a = (Units.mk0 a ha)⁻¹ • a

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 { x // x ∈ p }) : { x // x ∈ q } ≃ₗ[R] { x // x ∈ 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 { x // x ∈ p }} (x : { x // 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 { x // x ∈ p }} (x : { x // x ∈ Submodule.map (Submodule.subtype p) q }) : ↑↑(↑(LinearEquiv.symm (Submodule.equivSubtypeMap p q)) x) = ↑x

@[simp]

theorem Submodule.comapSubtypeEquivOfLe_symm_apply {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {q : Submodule R M} (hpq : p ≤ q) (x : { x // x ∈ p }) : ↑(LinearEquiv.symm (Submodule.comapSubtypeEquivOfLe hpq)) x = { val := { val := ↑x, property := (_ : ↑x ∈ q) }, property := (_ : ↑x ∈ p) }

def Submodule.comapSubtypeEquivOfLe {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {q : Submodule R M} (hpq : p ≤ q) : { x // x ∈ Submodule.comap (Submodule.subtype q) p } ≃ₗ[R] { x // x ∈ p }

If s ≤ t, then we can view s as a submodule of t by taking the comap of t.subtype.

Equations

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

@[simp]

theorem Submodule.comapSubtypeEquivOfLe_apply_coe {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {q : Submodule R M} (hpq : p ≤ q) (x : { x // x ∈ Submodule.comap (Submodule.subtype q) p }) : ↑(↑(Submodule.comapSubtypeEquivOfLe hpq) x) = ↑↑x

@[simp]

theorem Submodule.mem_map_equiv {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [CommSemiring R] [CommSemiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁] [RingHomInvPair τ₂₁ τ₁₂] (p : Submodule R M) {e : M ≃ₛₗ[τ₁₂] M₂} {x : M₂} : x ∈ Submodule.map (↑e) p ↔ ↑(LinearEquiv.symm e) x ∈ p

theorem Submodule.map_equiv_eq_comap_symm {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [CommSemiring R] [CommSemiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁] [RingHomInvPair τ₂₁ τ₁₂] (e : M ≃ₛₗ[τ₁₂] M₂) (K : Submodule R M) : Submodule.map (↑e) K = Submodule.comap (↑(LinearEquiv.symm e)) K

theorem Submodule.comap_equiv_eq_map_symm {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [CommSemiring R] [CommSemiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁] [RingHomInvPair τ₂₁ τ₁₂] (e : M ≃ₛₗ[τ₁₂] M₂) (K : Submodule R₂ M₂) : Submodule.comap (↑e) K = Submodule.map (↑(LinearEquiv.symm e)) K

theorem Submodule.map_symm_eq_iff {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [CommSemiring R] [CommSemiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁] [RingHomInvPair τ₂₁ τ₁₂] {p : Submodule R M} (e : M ≃ₛₗ[τ₁₂] M₂) {K : Submodule R₂ M₂} : Submodule.map (LinearEquiv.symm e) K = p ↔ Submodule.map e p = K

theorem Submodule.orderIsoMapComap_apply' {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [CommSemiring R] [CommSemiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁] [RingHomInvPair τ₂₁ τ₁₂] (e : M ≃ₛₗ[τ₁₂] M₂) (p : Submodule R M) : ↑(Submodule.orderIsoMapComap e) p = Submodule.comap (LinearEquiv.symm e) p

theorem Submodule.orderIsoMapComap_symm_apply' {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [CommSemiring R] [CommSemiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁] [RingHomInvPair τ₂₁ τ₁₂] (e : M ≃ₛₗ[τ₁₂] M₂) (p : Submodule R₂ M₂) : ↑(OrderIso.symm (Submodule.orderIsoMapComap e)) p = Submodule.map (LinearEquiv.symm e) p

theorem Submodule.comap_le_comap_smul {R : Type u_1} {N : Type u_15} {N₂ : Type u_16} [CommSemiring R] [AddCommMonoid N] [AddCommMonoid N₂] [Module R N] [Module R N₂] (qₗ : Submodule R N₂) (fₗ : N →ₗ[R] N₂) (c : R) : Submodule.comap fₗ qₗ ≤ Submodule.comap (c • fₗ) qₗ

theorem Submodule.inf_comap_le_comap_add {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [CommSemiring R] [CommSemiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (q : Submodule R₂ M₂) (f₁ : M →ₛₗ[τ₁₂] M₂) (f₂ : M →ₛₗ[τ₁₂] M₂) : Submodule.comap f₁ q ⊓ Submodule.comap f₂ q ≤ Submodule.comap (f₁ + f₂) q

def Submodule.compatibleMaps {R : Type u_1} {N : Type u_15} {N₂ : Type u_16} [CommSemiring R] [AddCommMonoid N] [AddCommMonoid N₂] [Module R N] [Module R N₂] (pₗ : Submodule R N) (qₗ : Submodule R N₂) : Submodule R (N →ₗ[R] N₂)

Given modules M, M₂ over a commutative ring, together with submodules p ⊆ M, q ⊆ M₂, the set of maps ${f ∈ Hom(M, M₂) | f(p) ⊆ q }$ is a submodule of Hom(M, M₂).

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.comp (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.trans (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