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 α → β.

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

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

@[simp]

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

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

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

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

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

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

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.

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

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.

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

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

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

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

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

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

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

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.

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

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

@[simp]

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

@[simp]

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

def addMonoidHomLequivInt {A : Type u_20} {B : Type u_21} (R : Type u_22) [Semiring R] [AddCommGroup A] [AddCommGroup B] [Module R B] : (A →+ B) ≃ₗ[R] A →ₗ[ℤ] B

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

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.

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

@[simp]

theorem Submodule.subsingleton_iff (R : Type u_1) {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] : Subsingleton (Submodule R M) ↔ Subsingleton M

@[simp]

theorem Submodule.nontrivial_iff (R : Type u_1) {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] : Nontrivial (Submodule R M) ↔ Nontrivial M

instance Submodule.instUniqueSubmodule {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] [Subsingleton M] : Unique (Submodule R M)

instance Submodule.unique' {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] [Subsingleton R] : Unique (Submodule R M)

instance Submodule.instNontrivialSubmodule {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial M] : Nontrivial (Submodule R M)

theorem Submodule.mem_right_iff_eq_zero_of_disjoint {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {p' : Submodule R M} (h : Disjoint p p') {x : { x // x ∈ p }} : ↑x ∈ p' ↔ x = 0

theorem Submodule.mem_left_iff_eq_zero_of_disjoint {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {p' : Submodule R M} (h : Disjoint p p') {x : { x // x ∈ p' }} : ↑x ∈ p ↔ x = 0

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

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

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

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

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.

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.

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

@[simp]

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

theorem LinearMap.coe_finsupp_sum {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} {ι : Type u_17} [Semiring R] [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].

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

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

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

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

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

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.

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

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

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

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.

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

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

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

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

@[simp]

theorem LinearEquiv.map_sum {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} {ι : Type u_17} [Semiring R] [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₂) {s : Finset ι} (u : ι → M) : ↑e (Finset.sum s fun i => u i) = Finset.sum s fun i => ↑e (u i)

theorem LinearEquiv.map_eq_comap {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [Semiring R] [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.

@[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_finsupp_sum {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} {ι : Type u_17} {γ : Type u_20} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] [Zero γ] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁] [RingHomInvPair τ₂₁ τ₁₂] (f : M ≃ₛₗ[τ₁₂] M₂) {t : ι →₀ γ} {g : ι → γ → M} : ↑f (Finsupp.sum t g) = Finsupp.sum t fun i d => ↑f (g i d)

@[simp]

theorem LinearEquiv.map_dfinsupp_sumAddHom {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} {ι : Type u_17} [Semiring R] [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.

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

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