mathlib documentation

linear_algebra.basic

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 linear_map, are found in src/algebra/module.

Main definitions #

See linear_algebra.quotient for quotients by submodules.

Main theorems #

See linear_algebra.isomorphisms for Noether's three isomorphism theorems for modules.

Notations #

Implementation notes #

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

TODO #

Tags #

linear algebra, vector space, module

theorem finsupp.smul_sum {α : Type u_1} {β : Type u_2} {R : Type u_3} {M : Type u_4} [has_zero β] [monoid R] [add_comm_monoid M] [distrib_mul_action R M] {v : α →₀ β} {c : R} {h : α → β → M} :
c v.sum h = v.sum (λ (a : α) (b : β), c h a b)
@[simp]
theorem finsupp.sum_smul_index_linear_map' {α : Type u_1} {R : Type u_2} {M : Type u_3} {M₂ : Type u_4} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M₂] [module R M₂] {v : α →₀ M} {c : R} {h : α → (M →ₗ[R] M₂)} :
(c v).sum (λ (a : α), (h a)) = c v.sum (λ (a : α), (h a))
@[simp]
theorem finsupp.linear_equiv_fun_on_fintype_apply (R : Type u_1) (M : Type u_9) (α : Type u_20) [fintype α] [add_comm_monoid M] [semiring R] [module R M] (x : α →₀ M) (ᾰ : α) :
noncomputable def finsupp.linear_equiv_fun_on_fintype (R : Type u_1) (M : Type u_9) (α : Type u_20) [fintype α] [add_comm_monoid M] [semiring R] [module R M] :
→₀ M) ≃ₗ[R] α → M

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

Equations
@[simp]
theorem finsupp.linear_equiv_fun_on_fintype_single (R : Type u_1) (M : Type u_9) (α : Type u_20) [fintype α] [add_comm_monoid M] [semiring R] [module R M] [decidable_eq α] (x : α) (m : M) :
@[simp]
theorem finsupp.linear_equiv_fun_on_fintype_symm_single (R : Type u_1) (M : Type u_9) (α : Type u_20) [fintype α] [add_comm_monoid M] [semiring R] [module R M] [decidable_eq α] (x : α) (m : M) :
@[simp]
theorem finsupp.linear_equiv_fun_on_fintype_symm_coe (R : Type u_1) (M : Type u_9) (α : Type u_20) [fintype α] [add_comm_monoid M] [semiring R] [module R M] (f : α →₀ M) :
theorem pi_eq_sum_univ {ι : Type u_1} [fintype ι] {R : Type u_2} [semiring R] (x : ι → R) :
x = ∑ (i : ι), x i λ (j : ι), ite (i = j) 1 0

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

Properties of linear maps #

theorem linear_map.comp_assoc {R : Type u_1} {R₂ : Type u_3} {R₃ : Type u_4} {R₄ : Type u_5} {M : Type u_9} {M₂ : Type u_12} {M₃ : Type u_13} {M₄ : Type u_14} [semiring R] [semiring R₂] [semiring R₃] [semiring R₄] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [add_comm_monoid M₄] [module R M] [module R₂ M₂] [module R₃ M₃] [module R₄ M₄] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₃₄ : R₃ →+* R₄} {σ₁₃ : R →+* R₃} {σ₂₄ : R₂ →+* R₄} {σ₁₄ : R →+* R₄} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] [ring_hom_comp_triple σ₂₃ σ₃₄ σ₂₄] [ring_hom_comp_triple σ₁₃ σ₃₄ σ₁₄] [ring_hom_comp_triple σ₁₂ σ₂₄ σ₁₄] (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] M₃) (h : M₃ →ₛₗ[σ₃₄] M₄) :
(h.comp g).comp f = h.comp (g.comp f)
def linear_map.dom_restrict {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} (f : M →ₛₗ[σ₁₂] M₂) (p : submodule R M) :
p →ₛₗ[σ₁₂] M₂

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

Equations
@[simp]
theorem linear_map.dom_restrict_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} (f : M →ₛₗ[σ₁₂] M₂) (p : submodule R M) (x : p) :
def linear_map.cod_restrict {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} (p : submodule R₂ M₂) (f : M →ₛₗ[σ₁₂] M₂) (h : ∀ (c : M), f c p) :
M →ₛₗ[σ₁₂] 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
@[simp]
theorem linear_map.cod_restrict_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} (p : submodule R₂ M₂) (f : M →ₛₗ[σ₁₂] M₂) {h : ∀ (c : M), f c p} (x : M) :
@[simp]
theorem linear_map.comp_cod_restrict {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₃] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [module R M] [module R₂ M₂] [module R₃ M₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] M₃) (p : submodule R₃ M₃) (h : ∀ (b : M₂), g b p) :
@[simp]
theorem linear_map.subtype_comp_cod_restrict {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} (f : M →ₛₗ[σ₁₂] M₂) (p : submodule R₂ M₂) (h : ∀ (b : M), f b p) :
def linear_map.restrict {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (f : M →ₗ[R] M) {p : submodule R M} (hf : ∀ (x : M), x pf x p) :

Restrict domain and codomain of an endomorphism.

Equations
theorem linear_map.restrict_apply {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {f : M →ₗ[R] M} {p : submodule R M} (hf : ∀ (x : M), x pf x p) (x : p) :
(f.restrict hf) x = f x, _⟩
theorem linear_map.subtype_comp_restrict {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {f : M →ₗ[R] M} {p : submodule R M} (hf : ∀ (x : M), x pf x p) :
theorem linear_map.restrict_eq_cod_restrict_dom_restrict {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {f : M →ₗ[R] M} {p : submodule R M} (hf : ∀ (x : M), x pf x p) :
theorem linear_map.restrict_eq_dom_restrict_cod_restrict {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {f : M →ₗ[R] M} {p : submodule R M} (hf : ∀ (x : M), f x p) :
@[protected, instance]
def linear_map.unique_of_left {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [subsingleton M] :
unique (M →ₛₗ[σ₁₂] M₂)
Equations
@[protected, instance]
def linear_map.unique_of_right {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [subsingleton M₂] :
unique (M →ₛₗ[σ₁₂] M₂)
Equations
def linear_map.eval_add_monoid_hom {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid 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 add_monoid_hom.

Equations
def linear_map.to_add_monoid_hom' {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} :
(M →ₛₗ[σ₁₂] M₂) →+ M →+ M₂

linear_map.to_add_monoid_hom promoted to an add_monoid_hom

Equations
theorem linear_map.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₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} (t : finset ι) (f : ι → (M →ₛₗ[σ₁₂] M₂)) (b : M) :
(∑ (d : ι) in t, f d) b = ∑ (d : ι) in t, (f d) b
def linear_map.smul_right {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₁ : Type u_11} [semiring R] [add_comm_monoid M] [add_comm_monoid M₁] [module R M] [module R M₁] [semiring S] [module R S] [module S M] [is_scalar_tower R S M] (f : M₁ →ₗ[R] S) (x : M) :
M₁ →ₗ[R] M

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

Equations
@[simp]
theorem linear_map.coe_smul_right {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₁ : Type u_11} [semiring R] [add_comm_monoid M] [add_comm_monoid M₁] [module R M] [module R M₁] [semiring S] [module R S] [module S M] [is_scalar_tower R S M] (f : M₁ →ₗ[R] S) (x : M) :
(f.smul_right x) = λ (c : M₁), f c x
theorem linear_map.smul_right_apply {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₁ : Type u_11} [semiring R] [add_comm_monoid M] [add_comm_monoid M₁] [module R M] [module R M₁] [semiring S] [module R S] [module S M] [is_scalar_tower R S M] (f : M₁ →ₗ[R] S) (x : M) (c : M₁) :
(f.smul_right x) c = f c x
@[protected, instance]
def linear_map.module.End.nontrivial {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] [nontrivial M] :
@[simp, norm_cast]
theorem linear_map.coe_fn_sum {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {ι : Type u_2} (t : finset ι) (f : ι → (M →ₛₗ[σ₁₂] M₂)) :
∑ (i : ι) in t, f i = ∑ (i : ι) in t, (f i)
@[simp]
theorem linear_map.pow_apply {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (f : M →ₗ[R] M) (n : ) (m : M) :
(f ^ n) m = f^[n] m
theorem linear_map.pow_map_zero_of_le {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {f : module.End R M} {m : M} {k l : } (hk : k l) (hm : (f ^ k) m = 0) :
(f ^ l) m = 0
theorem linear_map.commute_pow_left_of_commute {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {f : M →ₛₗ[σ₁₂] M₂} {g : module.End R M} {g₂ : module.End R₂ M₂} (h : linear_map.comp g₂ f = f.comp g) (k : ) :
linear_map.comp (g₂ ^ k) f = f.comp (g ^ k)
theorem linear_map.submodule_pow_eq_zero_of_pow_eq_zero {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {N : submodule R M} {g : module.End R N} {G : module.End R M} (h : linear_map.comp G N.subtype = N.subtype.comp g) {k : } (hG : G ^ k = 0) :
g ^ k = 0
theorem linear_map.coe_pow {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (f : M →ₗ[R] M) (n : ) :
(f ^ n) = (f^[n])
@[simp]
theorem linear_map.id_pow {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (n : ) :
theorem linear_map.iterate_succ {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {f' : M →ₗ[R] M} (n : ) :
f' ^ (n + 1) = (f' ^ n).comp f'
theorem linear_map.iterate_surjective {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {f' : M →ₗ[R] M} (h : function.surjective f') (n : ) :
theorem linear_map.iterate_injective {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {f' : M →ₗ[R] M} (h : function.injective f') (n : ) :
theorem linear_map.iterate_bijective {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {f' : M →ₗ[R] M} (h : function.bijective f') (n : ) :
theorem linear_map.injective_of_iterate_injective {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {f' : M →ₗ[R] M} {n : } (hn : n 0) (h : function.injective (f' ^ n)) :
theorem linear_map.surjective_of_iterate_surjective {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {f' : M →ₗ[R] M} {n : } (hn : n 0) (h : function.surjective (f' ^ n)) :
theorem linear_map.pi_apply_eq_sum_univ {R : Type u_1} {M : Type u_9} {ι : Type u_17} [semiring R] [add_comm_monoid M] [module R M] [fintype ι] (f : (ι → R) →ₗ[R] M) (x : ι → R) :
f x = ∑ (i : ι), x i f (λ (j : ι), ite (i = j) 1 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 linear_map.applyₗ'_apply_apply {R : Type u_1} (S : Type u_6) {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] [module S M₂] [smul_comm_class R S M₂] (v : M) (f : M →ₗ[R] M₂) :
def linear_map.applyₗ' {R : Type u_1} (S : Type u_6) {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] [module S M₂] [smul_comm_class 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 linear_map.applyₗ for a version where S = R.

Equations
@[simp]
theorem linear_map.ring_lmap_equiv_self_apply (R : Type u_1) (S : Type u_6) (M : Type u_9) [semiring R] [semiring S] [add_comm_monoid M] [module R M] [module S M] [smul_comm_class R S M] (f : R →ₗ[R] M) :
@[simp]
theorem linear_map.ring_lmap_equiv_self_symm_apply (R : Type u_1) (S : Type u_6) (M : Type u_9) [semiring R] [semiring S] [add_comm_monoid M] [module R M] [module S M] [smul_comm_class R S M] (x : M) :
def linear_map.ring_lmap_equiv_self (R : Type u_1) (S : Type u_6) (M : Type u_9) [semiring R] [semiring S] [add_comm_monoid M] [module R M] [module S M] [smul_comm_class 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
def linear_map.comp_right {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} {M₃ : Type u_13} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid 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
@[simp]
theorem linear_map.applyₗ_apply_apply {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] (v : M) (f : M →ₗ[R] M₂) :
def linear_map.applyₗ {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid 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 linear_map.applyₗ' for a version that works with two different semirings.

This is the linear_map version of add_monoid_hom.eval.

Equations
def linear_map.dom_restrict' {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] (p : submodule R M) :
(M →ₗ[R] M₂) →ₗ[R] p →ₗ[R] M₂

Alternative version of dom_restrict as a linear map.

Equations
@[simp]
theorem linear_map.dom_restrict'_apply {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] (f : M →ₗ[R] M₂) (p : submodule R M) (x : p) :
def linear_map.smul_rightₗ {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [comm_ring R] [add_comm_group M] [add_comm_group 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
@[simp]
theorem linear_map.smul_rightₗ_apply {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [comm_ring R] [add_comm_group M] [add_comm_group M₂] [module R M] [module R M₂] (f : M₂ →ₗ[R] R) (x : M) (c : M₂) :
@[simp]
theorem add_monoid_hom_lequiv_nat_apply {A : Type u_1} {B : Type u_2} (R : Type u_3) [semiring R] [add_comm_monoid A] [add_comm_monoid B] [module R B] (f : A →+ B) :
@[simp]
theorem add_monoid_hom_lequiv_nat_symm_apply {A : Type u_1} {B : Type u_2} (R : Type u_3) [semiring R] [add_comm_monoid A] [add_comm_monoid B] [module R B] (f : A →ₗ[] B) :
def add_monoid_hom_lequiv_nat {A : Type u_1} {B : Type u_2} (R : Type u_3) [semiring R] [add_comm_monoid A] [add_comm_monoid B] [module R B] :

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

Equations
@[simp]
theorem add_monoid_hom_lequiv_int_symm_apply {A : Type u_1} {B : Type u_2} (R : Type u_3) [semiring R] [add_comm_group A] [add_comm_group B] [module R B] (f : A →ₗ[] B) :
def add_monoid_hom_lequiv_int {A : Type u_1} {B : Type u_2} (R : Type u_3) [semiring R] [add_comm_group A] [add_comm_group B] [module R B] :

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

Equations
@[simp]
theorem add_monoid_hom_lequiv_int_apply {A : Type u_1} {B : Type u_2} (R : Type u_3) [semiring R] [add_comm_group A] [add_comm_group B] [module R B] (f : A →+ B) :

Properties of submodules #

def submodule.of_le {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {p p' : submodule R M} (h : p p') :

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

Equations
@[simp]
theorem submodule.coe_of_le {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {p p' : submodule R M} (h : p p') (x : p) :
theorem submodule.of_le_apply {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {p p' : submodule R M} (h : p p') (x : p) :
theorem submodule.of_le_injective {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {p p' : submodule R M} (h : p p') :
theorem submodule.subtype_comp_of_le {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (p q : submodule R M) (h : p q) :
@[simp]
theorem submodule.subsingleton_iff (R : Type u_1) {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] :
@[simp]
theorem submodule.nontrivial_iff (R : Type u_1) {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] :
@[protected, instance]
def submodule.unique {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] [subsingleton M] :
Equations
@[protected, instance]
def submodule.unique' {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] [subsingleton R] :
Equations
@[protected, instance]
def submodule.nontrivial {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] [nontrivial M] :
theorem submodule.mem_right_iff_eq_zero_of_disjoint {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {p p' : submodule R M} (h : disjoint p p') {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] [add_comm_monoid M] [module R M] {p p' : submodule R M} (h : disjoint p p') {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₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [ring_hom_surjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (p : submodule R M) :
submodule R₂ M₂

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

Equations
@[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₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [ring_hom_surjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (p : submodule R M) :
@[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₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [ring_hom_surjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂} {p : submodule R M} {x : M₂} :
x submodule.map f p ∃ (y : M), 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₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [ring_hom_surjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂} {p : submodule R M} {r : M} (h : r 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₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [ring_hom_surjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) {p : submodule R M} (r : p) :
@[simp]
theorem submodule.map_id {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (p : submodule R M) :
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₃] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [module R M] [module R₂ M₂] [module R₃ M₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] [ring_hom_surjective σ₁₂] [ring_hom_surjective σ₂₃] [ring_hom_surjective σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] M₃) (p : submodule R M) :
theorem submodule.map_mono {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [ring_hom_surjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂} {p p' : submodule R M} :
@[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₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} (p : submodule R M) [ring_hom_surjective σ₁₂] :
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₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} (p : submodule R M) [ring_hom_surjective σ₁₂] (f g : M →ₛₗ[σ₁₂] M₂) :
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₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [ring_hom_surjective σ₁₂] (N : submodule R M) :
(set.range (λ (ϕ : M →ₛₗ[σ₁₂] M₂), submodule.map ϕ N)).nonempty
noncomputable def submodule.equiv_map_of_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (i : function.injective f) (p : submodule R M) :

The pushforward of a submodule by an injective linear map is linearly equivalent to the original submodule.

Equations
@[simp]
theorem submodule.coe_equiv_map_of_injective_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (i : function.injective f) (p : submodule R M) (x : p) :
def submodule.comap {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} (f : M →ₛₗ[σ₁₂] M₂) (p : submodule R₂ M₂) :

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

Equations
@[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₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} (f : M →ₛₗ[σ₁₂] M₂) (p : submodule R₂ M₂) :
@[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₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {x : M} {f : M →ₛₗ[σ₁₂] M₂} {p : submodule R₂ M₂} :
theorem submodule.comap_id {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (p : submodule R M) :
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₃] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [module R M] [module R₂ M₂] [module R₃ M₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] M₃) (p : submodule R₃ M₃) :
theorem submodule.comap_mono {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {f : M →ₛₗ[σ₁₂] M₂} {q q' : submodule R₂ M₂} :
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₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [ring_hom_surjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂} {p : submodule R M} {q : submodule R₂ M₂} :
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₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [ring_hom_surjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) :
@[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₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [ring_hom_surjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) :
@[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₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} (p p' : submodule R M) [ring_hom_surjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) :
@[simp]
theorem submodule.map_supr {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [ring_hom_surjective σ₁₂] {ι : Sort u_2} (f : M →ₛₗ[σ₁₂] M₂) (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₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} (f : M →ₛₗ[σ₁₂] M₂) :
@[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₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} (q q' : submodule R₂ M₂) (f : M →ₛₗ[σ₁₂] M₂) :
@[simp]
theorem submodule.comap_infi {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [ring_hom_surjective σ₁₂] {ι : Sort u_2} (f : M →ₛₗ[σ₁₂] M₂) (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₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} (q : submodule R₂ M₂) :
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₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [ring_hom_surjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (q : submodule R₂ M₂) :
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₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [ring_hom_surjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (p : submodule R M) :
def submodule.gi_map_comap {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {f : M →ₛₗ[σ₁₂] M₂} (hf : function.surjective f) [ring_hom_surjective σ₁₂] :

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

Equations
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₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {f : M →ₛₗ[σ₁₂] M₂} (hf : function.surjective f) [ring_hom_surjective σ₁₂] (p : submodule R₂ M₂) :
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₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {f : M →ₛₗ[σ₁₂] M₂} (hf : function.surjective f) [ring_hom_surjective σ₁₂] :
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₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {f : M →ₛₗ[σ₁₂] M₂} (hf : function.surjective f) [ring_hom_surjective σ₁₂] :
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₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {f : M →ₛₗ[σ₁₂] M₂} (hf : function.surjective f) [ring_hom_surjective σ₁₂] (p q : submodule R₂ M₂) :
theorem submodule.map_supr_comap_of_sujective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} {ι : Type u_17} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {f : M →ₛₗ[σ₁₂] M₂} (hf : function.surjective f) [ring_hom_surjective σ₁₂] (S : ι → submodule R₂ M₂) :
submodule.map f (⨆ (i : ι), submodule.comap f (S i)) = supr 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₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {f : M →ₛₗ[σ₁₂] M₂} (hf : function.surjective f) [ring_hom_surjective σ₁₂] (p q : submodule R₂ M₂) :
theorem submodule.map_infi_comap_of_surjective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} {ι : Type u_17} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {f : M →ₛₗ[σ₁₂] M₂} (hf : function.surjective f) [ring_hom_surjective σ₁₂] (S : ι → submodule R₂ M₂) :
submodule.map f (⨅ (i : ι), submodule.comap f (S i)) = infi 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₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {f : M →ₛₗ[σ₁₂] M₂} (hf : function.surjective f) [ring_hom_surjective σ₁₂] (p q : submodule R₂ M₂) :
theorem submodule.comap_strict_mono_of_surjective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {f : M →ₛₗ[σ₁₂] M₂} (hf : function.surjective f) [ring_hom_surjective σ₁₂] :
def submodule.gci_map_comap {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [ring_hom_surjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂} (hf : function.injective f) :

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

Equations
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₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [ring_hom_surjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂} (hf : function.injective f) (p : submodule R M) :
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₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [ring_hom_surjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂} (hf : function.injective 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₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [ring_hom_surjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂} (hf : function.injective 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₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [ring_hom_surjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂} (hf : function.injective f) (p q : submodule R M) :
theorem submodule.comap_infi_map_of_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} {ι : Type u_17} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [ring_hom_surjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂} (hf : function.injective f) (S : ι → submodule R M) :
submodule.comap f (⨅ (i : ι), submodule.map f (S i)) = infi 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₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [ring_hom_surjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂} (hf : function.injective f) (p q : submodule R M) :
theorem submodule.comap_supr_map_of_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} {ι : Type u_17} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [ring_hom_surjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂} (hf : function.injective f) (S : ι → submodule R M) :
submodule.comap f (⨆ (i : ι), submodule.map f (S i)) = supr 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₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [ring_hom_surjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂} (hf : function.injective f) (p q : submodule R M) :
theorem submodule.map_strict_mono_of_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [ring_hom_surjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂} (hf : function.injective f) :
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₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [ring_hom_surjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂} {p : submodule R M} {p' : submodule R₂ M₂} :
theorem submodule.map_comap_subtype {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (p p' : submodule R M) :
theorem submodule.eq_zero_of_bot_submodule {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (b : ) :
b = 0
theorem linear_map.infi_invariant {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {σ : R →+* R} [ring_hom_surjective σ] {ι : Type u_2} (f : M →ₛₗ[σ] M) {p : ι → submodule R M} (hf : ∀ (i : ι) (v : M), v p if v p i) (v : M) (H : v infi p) :
f v infi p

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

def submodule.span (R : Type u_1) {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (s : set M) :

The span of a set s ⊆ M is the smallest submodule of M that contains s.

Equations
theorem submodule.mem_span {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {x : M} {s : set M} :
x submodule.span R s ∀ (p : submodule R M), s px p
theorem submodule.subset_span {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {s : set M} :
theorem submodule.span_le {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {s : set M} {p : submodule R M} :
theorem submodule.span_mono {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {s t : set M} (h : s t) :
theorem submodule.span_eq_of_le {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (p : submodule R M) {s : set M} (h₁ : s p) (h₂ : p submodule.span R s) :
theorem submodule.span_eq {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (p : submodule R M) :
@[simp]
theorem submodule.span_coe_eq_restrict_scalars {R : Type u_1} {S : Type u_6} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (p : submodule R M) [semiring S] [has_scalar S R] [module S M] [is_scalar_tower S R M] :

A version of submodule.span_eq for when the span is by a smaller ring.

theorem submodule.map_span {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [ring_hom_surjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (s : set M) :
theorem linear_map.map_span {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [ring_hom_surjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (s : set M) :

Alias of submodule.map_span.

theorem submodule.map_span_le {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [ring_hom_surjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (s : set M) (N : submodule R₂ M₂) :
submodule.map f (submodule.span R s) N ∀ (m : M), m sf m N
theorem linear_map.map_span_le {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [ring_hom_surjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (s : set M) (N : submodule R₂ M₂) :
submodule.map f (submodule.span R s) N ∀ (m : M), m sf m N

Alias of submodule.map_span_le.

@[simp]
theorem submodule.span_insert_zero {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {s : set M} :
theorem submodule.span_preimage_le {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} (f : M →ₛₗ[σ₁₂] M₂) (s : set M₂) :
theorem linear_map.span_preimage_le {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} (f : M →ₛₗ[σ₁₂] M₂) (s : set M₂) :

Alias of submodule.span_preimage_le.

theorem submodule.span_induction {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {x : M} {s : set M} {p : M → Prop} (h : x submodule.span R s) (Hs : ∀ (x : M), x sp x) (H0 : p 0) (H1 : ∀ (x y : M), p xp yp (x + y)) (H2 : ∀ (a : R) (x : M), p xp (a x)) :
p x

An induction principle for span membership. If p holds for 0 and all elements of s, and is preserved under addition and scalar multiplication, then p holds for all elements of the span of s.

theorem submodule.span_induction' {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {s : set M} {p : (submodule.span R s) → Prop} (Hs : ∀ (x : M) (h : x s), p x, _⟩) (H0 : p 0) (H1 : ∀ (x y : (submodule.span R s)), p xp yp (x + y)) (H2 : ∀ (a : R) (x : (submodule.span R s)), p xp (a x)) (x : (submodule.span R s)) :
p x

The difference with submodule.span_induction is that this acts on the subtype.

@[simp]
theorem submodule.span_span_coe_preimage {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {s : set M} :
@[simp]
@[protected]
def submodule.gi (R : Type u_1) (M : Type u_9) [semiring R] [add_comm_monoid M] [module R M] :

span forms a Galois insertion with the coercion from submodule to set.

Equations
@[simp]
theorem submodule.span_empty {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] :
@[simp]
theorem submodule.span_univ {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] :
theorem submodule.span_union {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (s t : set M) :
theorem submodule.span_Union {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {ι : Sort u_2} (s : ι → set M) :
submodule.span R (⋃ (i : ι), s i) = ⨆ (i : ι), submodule.span R (s i)
theorem submodule.span_attach_bUnion {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] [decidable_eq M] {α : Type u_2} (s : finset α) (f : s → finset M) :
theorem submodule.span_eq_supr_of_singleton_spans {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (s : set M) :
submodule.span R s = ⨆ (x : M) (H : x s), submodule.span R {x}
theorem submodule.span_smul_le {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (s : set M) (r : R) :
theorem submodule.subset_span_trans {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {U V W : set M} (hUV : U (submodule.span R V)) (hVW : V (submodule.span R W)) :
theorem submodule.span_smul_eq_of_is_unit {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (s : set M) (r : R) (hr : is_unit r) :

See submodule.span_smul_eq (in ring_theory.ideal.operations) for span R (r • s) = r • span R s that holds for arbitrary r in a comm_semiring.

@[simp]
theorem submodule.coe_supr_of_directed {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {ι : Sort u_2} [hι : nonempty ι] (S : ι → submodule R M) (H : directed has_le.le S) :
(supr S) = ⋃ (i : ι), (S i)
@[simp]
theorem submodule.mem_supr_of_directed {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {ι : Sort u_2} [nonempty ι] (S : ι → submodule R M) (H : directed has_le.le S) {x : M} :
x supr S ∃ (i : ι), x S i
theorem submodule.mem_Sup_of_directed {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {s : set (submodule R M)} {z : M} (hs : s.nonempty) (hdir : directed_on has_le.le s) :
z Sup s ∃ (y : submodule R M) (H : y s), z y
@[simp, norm_cast]
theorem submodule.coe_supr_of_chain {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (a : →o submodule R M) :
(⨆ (k : ), a k) = ⋃ (k : ), (a k)

We can regard coe_supr_of_chain as the statement that coe : (submodule R M) → set M is Scott continuous for the ω-complete partial order induced by the complete lattice structures.

@[simp]
theorem submodule.mem_supr_of_chain {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (a : →o submodule R M) (m : M) :
(m ⨆ (k : ), a k) ∃ (k : ), m a k
theorem submodule.mem_sup {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {p p' : submodule R M} {x : M} :
x p p' ∃ (y : M) (H : y p) (z : M) (H : z p'), y + z = x
theorem submodule.mem_sup' {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {p p' : submodule R M} {x : M} :
x p p' ∃ (y : p) (z : p'), y + z = x
theorem submodule.coe_sup {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {p p' : submodule R M} :
(p p') = p + p'
theorem submodule.mem_span_singleton_self {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (x : M) :
theorem submodule.nontrivial_span_singleton {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {x : M} (h : x 0) :
theorem submodule.mem_span_singleton {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {x y : M} :
x submodule.span R {y} ∃ (a : R), a y = x
theorem submodule.le_span_singleton_iff {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {s : submodule R M} {v₀ : M} :
s submodule.span R {v₀} ∀ (v : M), v s(∃ (r : R), r v₀ = v)
theorem submodule.span_singleton_eq_top_iff {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (x : M) :
submodule.span R {x} = ∀ (v : M), ∃ (r : R), r x = v
@[simp]
theorem submodule.span_zero_singleton {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] :
theorem submodule.span_singleton_eq_range {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (y : M) :
(submodule.span R {y}) = set.range (λ (_x : R), _x y)
theorem submodule.span_singleton_smul_le {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (r : R) (x : M) :
theorem submodule.span_singleton_smul_eq {K : Type u_1} {E : Type u_2} [division_ring K] [add_comm_group E] [module K E] {r : K} (x : E) (hr : r 0) :
theorem submodule.disjoint_span_singleton {K : Type u_1} {E : Type u_2} [division_ring K] [add_comm_group E] [module K E] {s : submodule K E} {x : E} :
disjoint s (submodule.span K {x}) x sx = 0
theorem submodule.disjoint_span_singleton' {K : Type u_1} {E : Type u_2} [division_ring K] [add_comm_group E] [module K E] {p : submodule K E} {x : E} (x0 : x 0) :
theorem submodule.mem_span_singleton_trans {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {x y z : M} (hxy : x submodule.span R {y}) (hyz : y submodule.span R {z}) :
theorem submodule.mem_span_insert {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {x : M} {s : set M} {y : M} :
x submodule.span R (insert y s) ∃ (a : R) (z : M) (H : z submodule.span R s), x = a y + z
theorem submodule.span_insert {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (x : M) (s : set M) :
theorem submodule.span_insert_eq_span {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {x : M} {s : set M} (h : x submodule.span R s) :
theorem submodule.span_span {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {s : set M} :
theorem submodule.span_le_restrict_scalars (R : Type u_1) (S : Type u_6) {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (s : set M) [semiring S] [has_scalar R S] [module S M] [is_scalar_tower R S M] :

If R is "smaller" ring than S then the span by R is smaller than the span by S.

@[simp]
theorem submodule.span_subset_span (R : Type u_1) (S : Type u_6) {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (s : set M) [semiring S] [has_scalar R S] [module S M] [is_scalar_tower R S M] :

A version of submodule.span_le_restrict_scalars with coercions.

theorem submodule.span_span_of_tower (R : Type u_1) (S : Type u_6) {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (s : set M) [semiring S] [has_scalar R S] [module S M] [is_scalar_tower R S M] :

Taking the span by a large ring of the span by the small ring is the same as taking the span by just the large ring.

theorem submodule.span_eq_bot {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {s : set M} :
submodule.span R s = ∀ (x : M), x sx = 0
@[simp]
theorem submodule.span_singleton_eq_bot {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {x : M} :
@[simp]
theorem submodule.span_zero {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] :
@[simp]
theorem submodule.span_image {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} {s : set M} [ring_hom_surjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) :
theorem submodule.apply_mem_span_image_of_mem_span {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [ring_hom_surjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) {x : M} {s : set M} (h : x submodule.span R s) :
f x submodule.span R₂ (f '' s)
theorem submodule.not_mem_span_of_apply_not_mem_span_image {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} [ring_hom_surjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) {x : M} {s : set M} (h : f x submodule.span R₂ (f '' s)) :

f is an explicit argument so we can apply this theorem and obtain h as a new goal.

theorem submodule.supr_eq_span {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {ι : Sort u_2} (p : ι → submodule R M) :
(⨆ (i : ι), p i) = submodule.span R (⋃ (i : ι), (p i))
theorem submodule.span_singleton_le_iff_mem {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (m : M) (p : submodule R M) :
@[protected, instance]
def submodule.is_compactly_generated {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] :
theorem submodule.lt_sup_iff_not_mem {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {I : submodule R M} {a : M} :
I < I submodule.span R {a} a I
theorem submodule.mem_supr {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {ι : Sort u_2} (p : ι → submodule R M) {m : M} :
(m ⨆ (i : ι), p i) ∀ (N : submodule R M), (∀ (i : ι), p i N)m N
theorem submodule.mem_span_finite_of_mem_span {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {S : set M} {x : M} (hx : x submodule.span R S) :
∃ (T : finset M), T S x submodule.span R T

For every element in the span of a set, there exists a finite subset of the set such that the element is contained in the span of the subset.

def submodule.prod {R : Type u_1} {M : Type u_9} {M' : Type u_10} [semiring R] [add_comm_monoid M] [add_comm_monoid M'] [module R M] [module R M'] (p : submodule R M) (q₁ : submodule R M') :
submodule R (M × M')

The product of two submodules is a submodule.

Equations
@[simp]
theorem submodule.prod_coe {R : Type u_1} {M : Type u_9} {M' : Type u_10} [semiring R] [add_comm_monoid M] [add_comm_monoid M'] [module R M] [module R M'] (p : submodule R M) (q₁ : submodule R M') :
(p.prod q₁) = p.prod q₁
@[simp]
theorem submodule.mem_prod {R : Type u_1} {M : Type u_9} {M' : Type u_10} [semiring R] [add_comm_monoid M] [add_comm_monoid M'] [module R M] [module R M'] {p : submodule R M} {q : submodule R M'} {x : M × M'} :
x p.prod q x.fst p x.snd q
theorem submodule.span_prod_le {R : Type u_1} {M : Type u_9} {M' : Type u_10} [semiring R] [add_comm_monoid M] [add_comm_monoid M'] [module R M] [module R M'] (s : set M) (t : set M') :
@[simp]
theorem submodule.prod_top {R : Type u_1} {M : Type u_9} {M' : Type u_10} [semiring R] [add_comm_monoid M] [add_comm_monoid M'] [module R M] [module R M'] :
@[simp]
theorem submodule.prod_bot {R : Type u_1} {M : Type u_9} {M' : Type u_10} [semiring R] [add_comm_monoid M] [add_comm_monoid M'] [module R M] [module R M'] :
theorem submodule.prod_mono {R : Type u_1} {M : Type u_9} {M' : Type u_10} [semiring R] [add_comm_monoid M] [add_comm_monoid M'] [module R M] [module R M'] {p p' : submodule R M} {q q' : submodule R M'} :
p p'q q'p.prod q p'.prod q'
@[simp]
theorem submodule.prod_inf_prod {R : Type u_1} {M : Type u_9} {M' : Type u_10} [semiring R] [add_comm_monoid M] [add_comm_monoid M'] [module R M] [module R M'] (p p' : submodule R M) (q₁ q₁' : submodule R M') :
p.prod q₁ p'.prod q₁' = (p p').prod (q₁ q₁')
@[simp]
theorem submodule.prod_sup_prod {R : Type u_1} {M : Type u_9} {M' : Type u_10} [semiring R] [add_comm_monoid M] [add_comm_monoid M'] [module R M] [module R M'] (p p' : submodule R M) (q₁ q₁' : submodule R M') :
p.prod q₁ p'.prod q₁' = (p p').prod (q₁ q₁')
@[simp]
theorem submodule.neg_coe {R : Type u_1} {M : Type u_9} [ring R] [add_comm_group M] [module R M] (p : submodule R M) :
@[protected, simp]
theorem submodule.map_neg {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [ring R] [add_comm_group M] [add_comm_group M₂] [module R M] [module R M₂] (p : submodule R M) (f : M →ₗ[R] M₂) :
@[simp]
theorem submodule.span_neg {R : Type u_1} {M : Type u_9} [ring R] [add_comm_group M] [module R M] (s : set M) :
theorem submodule.mem_span_insert' {R : Type u_1} {M : Type u_9} [ring R] [add_comm_group M] [module R M] {x y : M} {s : set M} :
x submodule.span R (insert y s) ∃ (a : R), x + a y submodule.span R s
theorem submodule.comap_smul {K : Type u_7} {V : Type u_18} {V₂ : Type u_19} [field K] [add_comm_group V] [module K V] [add_comm_group V₂] [module K V₂] (f : V →ₗ[K] V₂) (p : submodule K V₂) (a : K) (h : a 0) :
theorem submodule.map_smul {K : Type u_7} {V : Type u_18} {V₂ : Type u_19} [field K] [add_comm_group V] [module K V] [add_comm_group V₂] [module K V₂] (f : V →ₗ[K] V₂) (p : submodule K V) (a : K) (h : a 0) :
theorem submodule.comap_smul' {K : Type u_7} {V : Type u_18} {V₂ : Type u_19} [field K] [add_comm_group V] [module K V] [add_comm_group V₂] [module K V₂] (f : V →ₗ[K] V₂) (p : submodule K V₂) (a : K) :
submodule.comap (a f) p = ⨅ (h : a 0), submodule.comap f p
theorem submodule.map_smul' {K : Type u_7} {V : Type u_18} {V₂ : Type u_19} [field K] [add_comm_group V] [module K V] [add_comm_group V₂] [module K V₂] (f : V →ₗ[K] V₂) (p : submodule K V) (a : K) :
submodule.map (a f) p = ⨆ (h : a 0), submodule.map f p

Properties of linear maps #

theorem linear_map.eq_on_span {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] {σ₁₂ : R →+* R₂} [module R M] [module R₂ M₂] {s : set M} {f g : M →ₛₗ[σ₁₂] M₂} (H : set.eq_on f g s) ⦃x : M⦄ (h : x submodule.span R s) :
f x = g x

If two linear maps are equal on a set s, then they are equal on submodule.span s.

See also linear_map.eq_on_span' for a version using set.eq_on.

theorem linear_map.eq_on_span' {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] {σ₁₂ : R →+* R₂} [module R M] [module R₂ M₂] {s : set M} {f g : M →ₛₗ[σ₁₂] M₂} (H : set.eq_on f g s) :

If two linear maps are equal on a set s, then they are equal on submodule.span s.

This version uses set.eq_on, and the hidden argument will expand to h : x ∈ (span R s : set M). See linear_map.eq_on_span for a version that takes h : x ∈ span R s as an argument.

theorem linear_map.ext_on {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] {σ₁₂ : R →+* R₂} [module R M] [module R₂ M₂] {s : set M} {f g : M →ₛₗ[σ₁₂] M₂} (hv : submodule.span R s = ) (h : set.eq_on f g s) :
f = g

If s generates the whole module and linear maps f, g are equal on s, then they are equal.

theorem linear_map.ext_on_range {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} {ι : Type u_17} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] {σ₁₂ : R →+* R₂} [module R M] [module R₂ M₂] {v : ι → M} {f g : M →ₛₗ[σ₁₂] M₂} (hv : submodule.span R (set.range v) = ) (h : ∀ (i : ι), f (v i) = g (v i)) :
f = g

If the range of v : ι → M generates the whole module and linear maps f, g are equal at each v i, then they are equal.

@[simp]
theorem linear_map.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₂] [add_comm_monoid M] [add_comm_monoid M₂] {σ₁₂ : R →+* R₂} [module R M] [module R₂ M₂] {γ : Type u_20} [has_zero γ] (f : M →ₛₗ[σ₁₂] M₂) {t : ι →₀ γ} {g : ι → γ → M} :
f (t.sum g) = t.sum (λ (i : ι) (d : γ), f (g i d))
theorem linear_map.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₂] [add_comm_monoid M] [add_comm_monoid M₂] {σ₁₂ : R →+* R₂} [module R M] [module R₂ M₂] {γ : Type u_20} [has_zero γ] (t : ι →₀ γ) (g : ι → γ → (M →ₛₗ[σ₁₂] M₂)) :
(t.sum g) = t.sum (λ (i : ι) (d : γ), (g i d))
@[simp]
theorem linear_map.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₂] [add_comm_monoid M] [add_comm_monoid M₂] {σ₁₂ : R →+* R₂} [module R M] [module R₂ M₂] {γ : Type u_20} [has_zero γ] (t : ι →₀ γ) (g : ι → γ → (M →ₛₗ[σ₁₂] M₂)) (b : M) :
(t.sum g) b = t.sum (λ (i : ι) (d : γ), (g i d) b)
@[simp]
theorem linear_map.map_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₂] [add_comm_monoid M] [add_comm_monoid M₂] {σ₁₂ : R →+* R₂} [module R M] [module R₂ M₂] {γ : ι → Type u_20} [decidable_eq ι] [Π (i : ι), has_zero (γ i)] [Π (i : ι) (x : γ i), decidable (x 0)] (f : M →ₛₗ[σ₁₂] M₂) {t : Π₀ (i : ι), γ i} {g : Π (i : ι), γ i → M} :
f (t.sum g) = t.sum (λ (i : ι) (d : γ i), f (g i d))
theorem linear_map.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₂] [add_comm_monoid M] [add_comm_monoid M₂] {σ₁₂ : R →+* R₂} [module R M] [module R₂ M₂] {γ : ι → Type u_20} [decidable_eq ι] [Π (i : ι), has_zero (γ i)] [Π (i : ι) (x : γ i), decidable (x 0)] (t : Π₀ (i : ι), γ i) (g : Π (i : ι), γ i(M →ₛₗ[σ₁₂] M₂)) :
(t.sum g) = t.sum (λ (i : ι) (d : γ i), (g i d))
@[simp]
theorem linear_map.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₂] [add_comm_monoid M] [add_comm_monoid M₂] {σ₁₂ : R →+* R₂} [module R M] [module R₂ M₂] {γ : ι → Type u_20} [decidable_eq ι] [Π (i : ι), has_zero (γ i)] [Π (i : ι) (x : γ i), decidable (x 0)] (t : Π₀ (i : ι), γ i) (g : Π (i : ι), γ i(M →ₛₗ[σ₁₂] M₂)) (b : M) :
(t.sum g) b = t.sum (λ (i : ι) (d : γ i), (g i d) b)
@[simp]
theorem linear_map.map_dfinsupp_sum_add_hom {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} {ι : Type u_17} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] {σ₁₂ : R →+* R₂} [module R M] [module R₂ M₂] {γ : ι → Type u_20} [decidable_eq ι] [Π (i : ι), add_zero_class (γ i)] (f : M →ₛₗ[σ₁₂] M₂) {t : Π₀ (i : ι), γ i} {g : Π (i : ι), γ i →+ M} :
theorem linear_map.map_cod_restrict {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₂₁ : R₂ →+* R} [ring_hom_surjective σ₂₁] (p : submodule R M) (f : M₂ →ₛₗ[σ₂₁] M) (h : ∀ (c : M₂), f c p) (p' : submodule R₂ M₂) :
theorem linear_map.comap_cod_restrict {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {σ₂₁ : R₂ →+* R} (p : submodule R M) (f : M₂ →ₛₗ[σ₂₁] M) (hf : ∀ (c : M₂), f c p) (p' : submodule R p) :
def linear_map.range {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) :
submodule R₂ M₂

The range of a linear map f : M → M₂ is a submodule of M₂. See Note [range copy pattern].

Equations
theorem linear_map.range_coe {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) :
@[simp]
theorem linear_map.mem_range {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} {x : M₂} :
x f.range ∃ (y : M), f y = x
theorem linear_map.range_eq_map {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) :
theorem linear_map.mem_range_self {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) (x : M) :
@[simp]
theorem linear_map.range_id {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] :
theorem linear_map.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₃] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [module R M] [module R₂ M₂] [module R₃ M₃] {τ₁₂ : R →+* R₂} {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [ring_hom_comp_triple τ₁₂ τ₂₃ τ₁₃] [ring_hom_surjective τ₁₂] [ring_hom_surjective τ₂₃] [ring_hom_surjective τ₁₃] (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) :
theorem linear_map.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₃] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [module R M] [module R₂ M₂] [module R₃ M₃] {τ₁₂ : R →+* R₂} {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [ring_hom_comp_triple τ₁₂ τ₂₃ τ₁₃] [ring_hom_surjective τ₂₃] [ring_hom_surjective τ₁₃] (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) :
theorem linear_map.range_eq_top {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} :
theorem linear_map.range_le_iff_comap {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} {p : submodule R₂ M₂} :
theorem linear_map.map_le_range {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} {p : submodule R M} :
@[simp]
theorem linear_map.iterate_range_coe {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (f : M →ₗ[R] M) (n : ) :
def linear_map.iterate_range {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (f : M →ₗ[R] M) :

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

Equations
def linear_map.range_restrict {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) :
M →ₛₗ[τ₁₂] (f.range)

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

This is the bundled version of set.range_factorization.

Equations
@[protected, instance]
def linear_map.fintype_range {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} [fintype M] [decidable_eq M₂] [ring_hom_surjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) :

The range of a linear map is finite if the domain is finite. Note: this instance can form a diamond with subtype.fintype in the presence of fintype M₂.

Equations
@[simp]
theorem linear_map.to_span_singleton_apply (R : Type u_1) (M : Type u_9) [semiring R] [add_comm_monoid M] [module R M] (x : M) (b : R) :
def linear_map.to_span_singleton (R : Type u_1) (M : Type u_9) [semiring R] [add_comm_monoid M] [module R M] (x : M) :

Given an element x of a module M over R, the natural map from R to scalar multiples of x.

Equations
theorem linear_map.span_singleton_eq_range (R : Type u_1) (M : Type u_9) [semiring R] [add_comm_monoid M] [module R M] (x : M) :

The range of to_span_singleton x is the span of x.

theorem linear_map.to_span_singleton_one (R : Type u_1) (M : Type u_9) [semiring R] [add_comm_monoid M] [module R M] (x : M) :
def linear_map.ker {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] 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
@[simp]
theorem linear_map.mem_ker {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {f : M →ₛₗ[τ₁₂] M₂} {y : M} :
y f.ker f y = 0
@[simp]
theorem linear_map.ker_id {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] :
@[simp]
theorem linear_map.map_coe_ker {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) (x : (f.ker)) :
f x = 0
theorem linear_map.comp_ker_subtype {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) :
theorem linear_map.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₃] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [module R M] [module R₂ M₂] [module R₃ M₃] {τ₁₂ : R →+* R₂} {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [ring_hom_comp_triple τ₁₂ τ₂₃ τ₁₃] (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) :
theorem linear_map.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₃] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [module R M] [module R₂ M₂] [module R₃ M₃] {τ₁₂ : R →+* R₂} {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [ring_hom_comp_triple τ₁₂ τ₂₃ τ₁₃] (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) :
f.ker (g.comp f).ker
theorem linear_map.disjoint_ker {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {f : M →ₛₗ[τ₁₂] M₂} {p : submodule R M} :
disjoint p f.ker ∀ (x : M), x pf x = 0x = 0
theorem linear_map.ker_eq_bot' {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {f : M →ₛₗ[τ₁₂] M₂} :
f.ker = ∀ (m : M), f m = 0m = 0
theorem linear_map.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₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [ring_hom_inv_pair τ₁₂ τ₂₁] {f : M →ₛₗ[τ₁₂] M₂} {g : M₂ →ₛₗ[τ₂₁] M} (h : g.comp f = linear_map.id) :
theorem linear_map.le_ker_iff_map {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} {p : submodule R M} :
theorem linear_map.ker_cod_restrict {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {τ₂₁ : R₂ →+* R} (p : submodule R M) (f : M₂ →ₛₗ[τ₂₁] M) (hf : ∀ (c : M₂), f c p) :
theorem linear_map.range_cod_restrict {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {τ₂₁ : R₂ →+* R} [ring_hom_surjective τ₂₁] (p : submodule R M) (f : M₂ →ₛₗ[τ₂₁] M) (hf : ∀ (c : M₂), f c p) :
theorem linear_map.ker_restrict {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {p : submodule R M} {f : M →ₗ[R] M} (hf : ∀ (x : M), x pf x 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₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) (q : submodule R₂ M₂) :
theorem submodule.map_comap_eq_self {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} {q : submodule R₂ M₂} (h : q f.range) :
@[simp]
theorem linear_map.ker_zero {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} :
@[simp]
theorem linear_map.range_zero {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] :
theorem linear_map.ker_eq_top {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {f : M →ₛₗ[τ₁₂] M₂} :
f.ker = f = 0
theorem linear_map.range_le_bot_iff {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) :
f.range f = 0
theorem linear_map.range_eq_bot {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} :
f.range = f = 0
theorem linear_map.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₃] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [module R M] [module R₂ M₂] [module R₃ M₃] {τ₁₂ : R →+* R₂} {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [ring_hom_comp_triple τ₁₂ τ₂₃ τ₁₃] [ring_hom_surjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} {g : M₂ →ₛₗ[τ₂₃] M₃} :
f.range g.ker g.comp f = 0
theorem linear_map.comap_le_comap_iff {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} (hf : f.range = ) {p p' : submodule R₂ M₂} :
theorem linear_map.comap_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} (hf : f.range = ) :
theorem linear_map.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₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {f : M →ₛₗ[τ₁₂] M₂} (hf : function.injective f) :
@[simp]
theorem linear_map.iterate_ker_coe {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (f : M →ₗ[R] M) (n : ) :
(f.iterate_ker) n = (f ^ n).ker
def linear_map.iterate_ker {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (f : M →ₗ[R] M) :

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

Equations
theorem submodule.comap_map_eq {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_group M] [add_comm_group M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) (p : submodule R M) :
theorem submodule.comap_map_eq_self {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_group M] [add_comm_group M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} {p : submodule R M} (h : f.ker p) :
theorem linear_map.map_le_map_iff {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_group M] [add_comm_group M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) {p p' : submodule R M} :
theorem linear_map.map_le_map_iff' {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_group M] [add_comm_group M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} (hf : f.ker = ) {p p' : submodule R M} :
theorem linear_map.map_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_group M] [add_comm_group M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} (hf : f.ker = ) :
theorem linear_map.map_eq_top_iff {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_group M] [add_comm_group M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} (hf : f.range = ) {p : submodule R M} :
theorem linear_map.sub_mem_ker_iff {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [ring R] [ring R₂] [add_comm_group M] [add_comm_group M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {f : M →ₛₗ[τ₁₂] M₂} {x y : M} :
x - y f.ker f x = f y
theorem linear_map.disjoint_ker' {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [ring R] [ring R₂] [add_comm_group M] [add_comm_group M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {f : M →ₛₗ[τ₁₂] M₂} {p : submodule R M} :
disjoint p f.ker ∀ (x y : M), x py pf x = f yx = y
theorem linear_map.inj_of_disjoint_ker {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [ring R] [ring R₂] [add_comm_group M] [add_comm_group M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {f : M →ₛₗ[τ₁₂] M₂} {p : submodule R M} {s : set M} (h : s p) (hd : disjoint p f.ker) (x y : M) (H : x s) (H_1 : y s) :
f x = f yx = y
theorem linear_map.ker_eq_bot {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [ring R] [ring R₂] [add_comm_group M] [add_comm_group M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {f : M →ₛₗ[τ₁₂] M₂} :
theorem linear_map.ker_le_iff {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [ring R] [ring R₂] [add_comm_group M] [add_comm_group M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {f : M →ₛₗ[τ₁₂] M₂} [ring_hom_surjective τ₁₂] {p : submodule R M} :
f.ker p ∃ (y : M₂) (H : y f.range), f ⁻¹' {y} p
theorem linear_map.ker_smul {K : Type u_7} {V : Type u_18} {V₂ : Type u_19} [field K] [add_comm_group V] [module K V] [add_comm_group V₂] [module K V₂] (f : V →ₗ[K] V₂) (a : K) (h : a 0) :
(a f).ker = f.ker
theorem linear_map.ker_smul' {K : Type u_7} {V : Type u_18} {V₂ : Type u_19} [field K] [add_comm_group V] [module K V] [add_comm_group V₂] [module K V₂] (f : V →ₗ[K] V₂) (a : K) :
(a f).ker = ⨅ (h : a 0), f.ker
theorem linear_map.range_smul {K : Type u_7} {V : Type u_18} {V₂ : Type u_19} [field K] [add_comm_group V] [module K V] [add_comm_group V₂] [module K V₂] (f : V →ₗ[K] V₂) (a : K) (h : a 0) :
(a f).range = f.range
theorem linear_map.range_smul' {K : Type u_7} {V : Type u_18} {V₂ : Type u_19} [field K] [add_comm_group V] [module K V] [add_comm_group V₂] [module K V₂] (f : V →ₗ[K] V₂) (a : K) :
(a f).range = ⨆ (h : a 0), f.range
theorem linear_map.span_singleton_sup_ker_eq_top {K : Type u_7} {V : Type u_18} [field K] [add_comm_group V] [module K V] (f : V →ₗ[K] K) {x : V} (hx : f x 0) :
theorem is_linear_map.is_linear_map_add {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] :
is_linear_map R (λ (x : M × M), x.fst + x.snd)
theorem is_linear_map.is_linear_map_sub {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_group M] [module R M] :
is_linear_map R (λ (x : M × M), 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₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) :
@[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₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) :
@[simp]
theorem submodule.ker_subtype {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (p : submodule R M) :
@[simp]
theorem submodule.range_subtype {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (p : submodule R M) :
theorem submodule.map_subtype_le {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (p : submodule R M) (p' : submodule R p) :
@[simp]
theorem submodule.map_subtype_top {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (p : submodule R M) :

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] [add_comm_monoid M] [module R M] {p p' : submodule R M} :
@[simp]
theorem submodule.comap_subtype_self {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (p : submodule R M) :
@[simp]
theorem submodule.ker_of_le {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (p p' : submodule R M) (h : p p') :
theorem submodule.range_of_le {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (p q : submodule R M) (h : p q) :
theorem submodule.disjoint_iff_comap_eq_bot {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {p q : submodule R M} :
def submodule.map_subtype.rel_iso {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (p : submodule R M) :
submodule R p ≃o {p' // p' p}

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

Equations
def submodule.map_subtype.order_embedding {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (p : 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
@[simp]
theorem submodule.map_subtype_embedding_eq {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (p : submodule R M) (p' : submodule R p) :
theorem linear_map.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₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {f : M →ₛₗ[τ₁₂] M₂} (h : ∀ (u v : (f.ker) →ₗ[R] M), f.comp u = f.comp vu = v) :

A monomorphism is injective.

theorem linear_map.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₃] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [module R M] [module R₂ M₂] [module R₃ M₃] {τ₁₂ : R →+* R₂} {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [ring_hom_comp_triple τ₁₂ τ₂₃ τ₁₃] [ring_hom_surjective τ₁₂] [ring_hom_surjective τ₂₃] [ring_hom_surjective τ₁₃] {f : M →ₛₗ[τ₁₂] M₂} (g : M₂ →ₛₗ[τ₂₃] M₃) (hf : f.range = ) :
(g.comp f).range = g.range
theorem linear_map.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₃] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [module R M] [module R₂ M₂] [module R₃ M₃] {τ₁₂ : R →+* R₂} {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [ring_hom_comp_triple τ₁₂ τ₂₃ τ₁₃] (f : M →ₛₗ[τ₁₂] M₂) {g : M₂ →ₛₗ[τ₂₃] M₃} (hg : g.ker = ) :
(g.comp f).ker = f.ker
def linear_map.submodule_image {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {M' : Type u_2} [add_comm_monoid M'] [module R M'] {O : submodule R M} (ϕ : O →ₗ[R] M') (N : submodule R M) :

If O is a submodule of M, and Φ : O →ₗ M' is a linear map, then (ϕ : O →ₗ M').submodule_image N is ϕ(N) as a submodule of M'

Equations
@[simp]
theorem linear_map.mem_submodule_image {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {M' : Type u_2} [add_comm_monoid M'] [module R M'] {O : submodule R M} {ϕ : O →ₗ[R] M'} {N : submodule R M} {x : M'} :
x ϕ.submodule_image N ∃ (y : M) (yO : y O) (yN : y N), ϕ y, yO⟩ = x
theorem linear_map.mem_submodule_image_of_le {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {M' : Type u_2} [add_comm_monoid M'] [module R M'] {O : submodule R M} {ϕ : O →ₗ[R] M'} {N : submodule R M} (hNO : N O) {x : M'} :
x ϕ.submodule_image N ∃ (y : M) (yN : y N), ϕ y, _⟩ = x
theorem linear_map.submodule_image_apply_of_le {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {M' : Type u_2} [add_comm_group M'] [module R M'] {O : submodule R M} (ϕ : O →ₗ[R] M') (N : submodule R M) (hNO : N O) :
@[simp]
theorem linear_map.range_range_restrict {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] (f : M →ₗ[R] M₂) :

Linear equivalences #

@[protected, instance]
def linear_equiv.has_zero {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] [subsingleton M] [subsingleton M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] :
has_zero (M ≃ₛₗ[σ₁₂] M₂)

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

Equations
@[simp]
theorem linear_equiv.zero_symm {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] [subsingleton M] [subsingleton M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] :
0.symm = 0
@[simp]
theorem linear_equiv.coe_zero {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] [subsingleton M] [subsingleton M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] :
0 = 0
theorem linear_equiv.zero_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] [subsingleton M] [subsingleton M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] (x : M) :
0 x = 0
@[protected, instance]
def linear_equiv.unique {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] [subsingleton M] [subsingleton M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] :
unique (M ≃ₛₗ[σ₁₂] M₂)

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

Equations
theorem linear_equiv.map_eq_comap {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : ring_hom_inv_pair σ₁₂ σ₂₁} {re₂₁ : ring_hom_inv_pair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) {p : submodule R M} :
def linear_equiv.of_submodule {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : ring_hom_inv_pair σ₁₂ σ₂₁} {re₂₁ : ring_hom_inv_pair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) (p : submodule R M) :

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 linear_equiv.of_submodule' but with map on the right instead of comap on the left.

Equations
@[simp]
theorem linear_equiv.of_submodule_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : ring_hom_inv_pair σ₁₂ σ₂₁} {re₂₁ : ring_hom_inv_pair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) (p : submodule R M) (x : p) :
@[simp]
theorem linear_equiv.of_submodule_symm_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : ring_hom_inv_pair σ₁₂ σ₂₁} {re₂₁ : ring_hom_inv_pair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) (p : submodule R M) (x : (submodule.map e p)) :
@[simp]
theorem linear_equiv.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₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] [has_zero γ] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [ring_hom_inv_pair τ₁₂ τ₂₁] [ring_hom_inv_pair τ₂₁ τ₁₂] (f : M ≃ₛₗ[τ₁₂] M₂) {t : ι →₀ γ} {g : ι → γ → M} :
f (t.sum g) = t.sum (λ (i : ι) (d : γ), f (g i d))
@[simp]
theorem linear_equiv.map_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₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [ring_hom_inv_pair τ₁₂ τ₂₁] [ring_hom_inv_pair τ₂₁ τ₁₂] {γ : ι → Type u_20} [decidable_eq ι] [Π (i : ι), has_zero (γ i)] [Π (i : ι) (x : γ i), decidable (x 0)] (f : M ≃ₛₗ[τ₁₂] M₂) (t : Π₀ (i : ι), γ i) (g : Π (i : ι), γ i → M) :
f (t.sum g) = t.sum (λ (i : ι) (d : γ i), f (g i d))
@[simp]
theorem linear_equiv.map_dfinsupp_sum_add_hom {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} {ι : Type u_17} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [ring_hom_inv_pair τ₁₂ τ₂₁] [ring_hom_inv_pair τ₂₁ τ₁₂] {γ : ι → Type u_20} [decidable_eq ι] [Π (i : ι), add_zero_class (γ i)] (f : M ≃ₛₗ[τ₁₂] M₂) (t : Π₀ (i : ι), γ i) (g : Π (i : ι), γ i →+ M) :
@[protected]
def linear_equiv.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 tensor_product.curry.

Equations
@[simp]
theorem linear_equiv.coe_curry (R : Type u_1) (V : Type u_18) (V₂ : Type u_19) [semiring R] :
@[simp]
theorem linear_equiv.coe_curry_symm (R : Type u_1) (V : Type u_18) (V₂ : Type u_19) [semiring R] :
def linear_equiv.of_eq {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] {module_M : module R M} (p q : submodule R M) (h : p = q) :

Linear equivalence between two equal submodules.

Equations
@[simp]
theorem linear_equiv.coe_of_eq_apply {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] {module_M : module R M} {p q : submodule R M} (h : p = q) (x : p) :
@[simp]
theorem linear_equiv.of_eq_symm {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] {module_M : module R M} {p q : submodule R M} (h : p = q) :
def linear_equiv.of_submodules {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : ring_hom_inv_pair σ₁₂ σ₂₁} {re₂₁ : ring_hom_inv_pair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) (p : submodule R M) (q : submodule R₂ M₂) (h : submodule.map e p = q) :
p ≃ₛₗ[σ₁₂] q

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

Equations
@[simp]
theorem linear_equiv.of_submodules_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : ring_hom_inv_pair σ₁₂ σ₂₁} {re₂₁ : ring_hom_inv_pair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) {p : submodule R M} {q : submodule R₂ M₂} (h : submodule.map e p = q) (x : p) :
((e.of_submodules p q h) x) = e x
@[simp]
theorem linear_equiv.of_submodules_symm_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : ring_hom_inv_pair σ₁₂ σ₂₁} {re₂₁ : ring_hom_inv_pair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) {p : submodule R M} {q : submodule R₂ M₂} (h : submodule.map e p = q) (x : q) :
(((e.of_submodules p q h).symm) x) = (e.symm) x
def linear_equiv.of_submodule' {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : ring_hom_inv_pair σ₁₂ σ₂₁} {re₂₁ : ring_hom_inv_pair σ₂₁ σ₁₂} [module R M] [module R₂ M₂] (f : M ≃ₛₗ[σ₁₂] M₂) (U : submodule R₂ M₂) :

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

This is linear_equiv.of_submodule but with comap on the left instead of map on the right.

Equations
theorem linear_equiv.of_submodule'_to_linear_map {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : ring_hom_inv_pair σ₁₂ σ₂₁} {re₂₁ : ring_hom_inv_pair σ₂₁ σ₁₂} [module R M] [module R₂ M₂] (f : M ≃ₛₗ[σ₁₂] M₂) (U : submodule R₂ M₂) :
@[simp]
theorem linear_equiv.of_submodule'_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : ring_hom_inv_pair σ₁₂ σ₂₁} {re₂₁ : ring_hom_inv_pair σ₂₁ σ₁₂} [module R M] [module R₂ M₂] (f : M ≃ₛₗ[σ₁₂] M₂) (U : submodule R₂ M₂) (x : (submodule.comap f U)) :
@[simp]
theorem linear_equiv.of_submodule'_symm_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : ring_hom_inv_pair σ₁₂ σ₂₁} {re₂₁ : ring_hom_inv_pair σ₂₁ σ₁₂} [module R M] [module R₂ M₂] (f : M ≃ₛₗ[σ₁₂] M₂) (U : submodule R₂ M₂) (x : U) :
def linear_equiv.of_top {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) (h : p = ) :

The top submodule of M is linearly equivalent to M.

Equations
@[simp]
theorem linear_equiv.of_top_apply {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) {h : p = } (x : p) :
@[simp]
theorem linear_equiv.coe_of_top_symm_apply {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) {h : p = } (x : M) :
theorem linear_equiv.of_top_symm_apply {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) {h : p = } (x : M) :
((linear_equiv.of_top p h).symm) x = x, _⟩
def linear_equiv.of_linear {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : ring_hom_inv_pair σ₁₂ σ₂₁} {re₂₁ : ring_hom_inv_pair σ₂₁ σ₁₂} (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₁] M) (h₁ : f.comp g = linear_map.id) (h₂ : g.comp f = linear_map.id) :
M ≃ₛₗ[σ₁₂] M₂

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

Equations
@[simp]
theorem linear_equiv.of_linear_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : ring_hom_inv_pair σ₁₂ σ₂₁} {re₂₁ : ring_hom_inv_pair σ₂₁ σ₁₂} (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₁] M) {h₁ : f.comp g = linear_map.id} {h₂ : g.comp f = linear_map.id} (x : M) :
(linear_equiv.of_linear f g h₁ h₂) x = f x
@[simp]
theorem linear_equiv.of_linear_symm_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : ring_hom_inv_pair σ₁₂ σ₂₁} {re₂₁ : ring_hom_inv_pair σ₂₁ σ₁₂} (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₁] M) {h₁ : f.comp g = linear_map.id} {h₂ : g.comp f = linear_map.id} (x : M₂) :
((linear_equiv.of_linear f g h₁ h₂).symm) x = g x
@[protected, simp]
theorem linear_equiv.range {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : ring_hom_inv_pair σ₁₂ σ₂₁} {re₂₁ : ring_hom_inv_pair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) :
theorem linear_equiv.eq_bot_of_equiv {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : ring_hom_inv_pair σ₁₂ σ₂₁} {re₂₁ : ring_hom_inv_pair σ₂₁ σ₁₂} (p : submodule R M) [module R₂ M₂] (e : p ≃ₛₗ[σ₁₂] ) :
p =
@[protected, simp]
theorem linear_equiv.ker {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : ring_hom_inv_pair σ₁₂ σ₂₁} {re₂₁ : ring_hom_inv_pair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) :
@[simp]
theorem linear_equiv.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₃] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] {module_M : module R M} {module_M₂ : module R₂ M₂} {module_M₃ : module R₃ M₃} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] {re₁₂ : ring_hom_inv_pair σ₁₂ σ₂₁} {re₂₁ : ring_hom_inv_pair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) (h : M₂ →ₛₗ[σ₂₃] M₃) [ring_hom_surjective σ₁₂] [ring_hom_surjective σ₂₃] [ring_hom_surjective σ₁₃] :
@[simp]
theorem linear_equiv.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₃] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] {module_M : module R M} {module_M₂ : module R₂ M₂} {module_M₃ : module R₃ M₃} {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] {σ₃₂ : R₃ →+* R₂} {re₂₃ : ring_hom_inv_pair σ₂₃ σ₃₂} {re₃₂ : ring_hom_inv_pair σ₃₂ σ₂₃} (e'' : M₂ ≃ₛₗ[σ₂₃] M₃) (l : M →ₛₗ[σ₁₂] M₂) :
(e''.comp l).ker = l.ker
def linear_equiv.of_left_inverse {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {f : M →ₛₗ[σ₁₂] M₂} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {g : M₂ → M} (h : function.left_inverse g f) :
M ≃ₛₗ[σ₁₂] (f.range)

An 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 linear_equiv.of_injective, and a bidirectional version of linear_map.range_restrict.

Equations
@[simp]
theorem linear_equiv.of_left_inverse_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {f : M →ₛₗ[σ₁₂] M₂} {g : M₂ →ₛₗ[σ₂₁] M} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] (h : function.left_inverse g f) (x : M) :
@[simp]
theorem linear_equiv.of_left_inverse_symm_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {f : M →ₛₗ[σ₁₂] M₂} {g : M₂ →ₛₗ[σ₂₁] M} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] (h : function.left_inverse g f) (x : (f.range)) :
noncomputable def linear_equiv.of_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} (f : M →ₛₗ[σ₁₂] M₂) [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] (h : function.injective f) :
M ≃ₛₗ[σ₁₂] (f.range)

An injective linear map f : M →ₗ[R] M₂ defines a linear equivalence between M and f.range. See also linear_map.of_left_inverse.

Equations
@[simp]
theorem linear_equiv.of_injective_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} (f : M →ₛₗ[σ₁₂] M₂) [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {h : function.injective f} (x : M) :
noncomputable def linear_equiv.of_bijective {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} (f : M →ₛₗ[σ₁₂] M₂) [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] (hf₁ : function.injective f) (hf₂ : function.surjective f) :
M ≃ₛₗ[σ₁₂] M₂

A bijective linear map is a linear equivalence.

Equations
@[simp]
theorem linear_equiv.of_bijective_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_M₂ : module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} (f : M →ₛₗ[σ₁₂] M₂) [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {hf₁ : function.injective f} {hf₂ : function.surjective f} (x : M) :
(linear_equiv.of_bijective f hf₁ hf₂) x = f x
@[simp]
theorem linear_equiv.map_neg {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_group M] [add_comm_group M₂] {module_M : module R M} {module_M₂ : module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : ring_hom_inv_pair σ₁₂ σ₂₁} {re₂₁ : ring_hom_inv_pair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) (a : M) :
e (-a) = -e a
@[simp]
theorem linear_equiv.map_sub {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [semiring R] [semiring R₂] [add_comm_group M] [add_comm_group M₂] {module_M : module R M} {module_M₂ : module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : ring_hom_inv_pair σ₁₂ σ₂₁} {re₂₁ : ring_hom_inv_pair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) (a b : M) :
e (a - b) = e a - e b
def linear_equiv.neg (R : Type u_1) {M : Type u_9} [semiring R] [add_comm_group M] [module R M] :

x ↦ -x as a linear_equiv

Equations
@[simp]
theorem linear_equiv.coe_neg {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_group M] [module R M] :
theorem linear_equiv.neg_apply {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_group M] [module R M] (x : M) :
@[simp]
theorem linear_equiv.symm_neg {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_group M] [module R M] :
def linear_equiv.smul_of_unit {R : Type u_1} {M : Type u_9} [comm_semiring R] [add_comm_monoid M] [module R M] (a : units R) :

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

Equations
def linear_equiv.arrow_congr {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {M₂₁ : Type u_4} {M₂₂ : Type u_5} [comm_semiring R] [add_comm_monoid M₁] [add_comm_monoid M₂] [add_comm_monoid M₂₁] [add_comm_monoid 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
@[simp]
theorem linear_equiv.arrow_congr_apply {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {M₂₁ : Type u_4} {M₂₂ : Type u_5} [comm_semiring R] [add_comm_monoid M₁] [add_comm_monoid M₂] [add_comm_monoid M₂₁] [add_comm_monoid 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₂) :
((e₁.arrow_congr e₂) f) x = e₂ (f ((e₁.symm) x))
@[simp]
theorem linear_equiv.arrow_congr_symm_apply {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {M₂₁ : Type u_4} {M₂₂ : Type u_5} [comm_semiring R] [add_comm_monoid M₁] [add_comm_monoid M₂] [add_comm_monoid M₂₁] [add_comm_monoid 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₁) :
(((e₁.arrow_congr e₂).symm) f) x = (e₂.symm) (f (e₁ x))
theorem linear_equiv.arrow_congr_comp {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} {M₃ : Type u_13} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [module R M] [module R M₂] [module R M₃] {N : Type u_2} {N₂ : Type u_3} {N₃ : Type u_4} [add_comm_monoid N] [add_comm_monoid N₂] [add_comm_monoid 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₃) :
(e₁.arrow_congr e₃) (g.comp f) = ((e₂.arrow_congr e₃) g).comp ((e₁.arrow_congr e₂) f)
theorem linear_equiv.arrow_congr_trans {R : Type u_1} [comm_semiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} {N₃ : Type u_7} [add_comm_monoid M₁] [module R M₁] [add_comm_monoid M₂] [module R M₂] [add_comm_monoid M₃] [module R M₃] [add_comm_monoid N₁] [module R N₁] [add_comm_monoid N₂] [module R N₂] [add_comm_monoid N₃] [module R N₃] (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : N₁ ≃ₗ[R] N₂) (e₃ : M₂ ≃ₗ[R] M₃) (e₄ : N₂ ≃ₗ[R] N₃) :
(e₁.arrow_congr e₂).trans (e₃.arrow_congr e₄) = (e₁.trans e₃).arrow_congr (e₂.trans e₄)
def linear_equiv.congr_right {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} {M₃ : Type u_13} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid 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
def linear_equiv.conj {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] (e : M ≃ₗ[R] M₂) :

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

Equations
theorem linear_equiv.conj_apply {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] (e : M ≃ₗ[R] M₂) (f : module.End R M) :
(e.conj) f = (e.comp f).comp (e.symm)
theorem linear_equiv.symm_conj_apply {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] (e : M ≃ₗ[R] M₂) (f : module.End R M₂) :
(e.symm.conj) f = ((e.symm).comp f).comp e
theorem linear_equiv.conj_comp {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] (e : M ≃ₗ[R] M₂) (f g : module.End R M) :
theorem linear_equiv.conj_trans {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} {M₃ : Type u_13} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [module R M] [module R M₂] [module R M₃] (e₁ : M ≃ₗ[R] M₂) (e₂ : M₂ ≃ₗ[R] M₃) :
e₁.conj.trans e₂.conj = (e₁.trans e₂).conj
@[simp]
theorem linear_equiv.conj_id {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] (e : M ≃ₗ[R] M₂) :
def linear_equiv.smul_of_ne_zero (K : Type u_7) (M : Type u_9) [field K] [add_comm_group M] [module K M] (a : K) (ha : a 0) :

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

Equations
theorem linear_equiv.ker_to_span_singleton (K : Type u_7) (M : Type u_9) [field K] [add_comm_group M] [module K M] {x : M} (h : x 0) :
noncomputable def linear_equiv.to_span_nonzero_singleton (K : Type u_7) (M : Type u_9) [field K] [add_comm_group M] [module K M] (x : M) (h : x 0) :

Given a nonzero element x of a vector space M over a field K, the natural map from K to the span of x, with invertibility check to consider it as an isomorphism.

Equations
theorem linear_equiv.to_span_nonzero_singleton_one (K : Type u_7) (M : Type u_9) [field K] [add_comm_group M] [module K M] (x : M) (h : x 0) :
noncomputable def linear_equiv.coord (K : Type u_7) (M : Type u_9) [field K] [add_comm_group M] [module K M] (x : M) (h : x 0) :

Given a nonzero element x of a vector space M over a field K, the natural map from the span of x to K.

theorem linear_equiv.coord_self (K : Type u_7) (M : Type u_9) [field K] [add_comm_group M] [module K M] (x : M) (h : x 0) :
(linear_equiv.coord K M x h) x, _⟩ = 1
def submodule.equiv_subtype_map {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] (p : submodule R M) (q : submodule R p) :

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

Equations
@[simp]
theorem submodule.equiv_subtype_map_apply {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {p : submodule R M} {q : submodule R p} (x : q) :
@[simp]
theorem submodule.equiv_subtype_map_symm_apply {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {p : submodule R M} {q : submodule R p} (x : (submodule.map p.subtype q)) :
@[simp]
theorem submodule.comap_subtype_equiv_of_le_apply_coe {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {p q : submodule R M} (hpq : p q) (x : (submodule.comap q.subtype p)) :
@[simp]
theorem submodule.comap_subtype_equiv_of_le_symm_apply_coe_coe {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {p q : submodule R M} (hpq : p q) (x : p) :
def submodule.comap_subtype_equiv_of_le {R : Type u_1} {M : Type u_9} [semiring R] [add_comm_monoid M] [module R M] {p q : submodule R M} (hpq : p q) :

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

Equations
@[simp]
theorem submodule.mem_map_equiv {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [comm_semiring R] [comm_semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [ring_hom_inv_pair τ₁₂ τ₂₁] [ring_hom_inv_pair τ₂₁ τ₁₂] (p : submodule R M) {e : M ≃ₛₗ[τ₁₂] M₂} {x : M₂} :
theorem submodule.map_equiv_eq_comap_symm {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [comm_semiring R] [comm_semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [ring_hom_inv_pair τ₁₂ τ₂₁] [ring_hom_inv_pair τ₂₁ τ₁₂] (e : M ≃ₛₗ[τ₁₂] M₂) (K : submodule R M) :
theorem submodule.comap_equiv_eq_map_symm {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [comm_semiring R] [comm_semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [ring_hom_inv_pair τ₁₂ τ₂₁] [ring_hom_inv_pair τ₂₁ τ₁₂] (e : M ≃ₛₗ[τ₁₂] M₂) (K : submodule R₂ M₂) :
theorem submodule.comap_le_comap_smul {R : Type u_1} {N : Type u_15} {N₂ : Type u_16} [comm_semiring R] [add_comm_monoid N] [add_comm_monoid 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} [comm_semiring R] [comm_semiring R₂] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} (q : submodule R₂ M₂) (f₁ f₂ : M →ₛₗ[τ₁₂] M₂) :
def submodule.compatible_maps {R : Type u_1} {N : Type u_15} {N₂ : Type u_16} [comm_semiring R] [add_comm_monoid N] [add_comm_monoid 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
def equiv.to_linear_equiv {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M₂] [module R M₂] (e : M M₂) (h : is_linear_map R e) :
M ≃ₗ[R] M₂

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

Equations
def add_equiv.to_linear_equiv {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M₂] [module R M₂] (e : M ≃+ M₂) (h : ∀ (c : R) (x : M), e (c x) = c e x) :
M ≃ₗ[R] M₂

An additive equivalence whose underlying function preserves smul is a linear equivalence.

Equations
@[simp]
theorem add_equiv.coe_to_linear_equiv {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M₂] [module R M₂] (e : M ≃+ M₂) (h : ∀ (c : R) (x : M), e (c x) = c e x) :
@[simp]
theorem add_equiv.coe_to_linear_equiv_symm {R : Type u_1} {M : Type u_9} {M₂ : Type u_12} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M₂] [module R M₂] (e : M ≃+ M₂) (h : ∀ (c : R) (x : M), e (c x) = c e x) :
def linear_map.fun_left (R : Type u_1) (M : Type u_9) [semiring R] [add_comm_monoid 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
@[simp]
theorem linear_map.fun_left_apply (R : Type u_1) (M : Type u_9) [semiring R] [add_comm_monoid M] [module R M] {m : Type u_20} {n : Type u_21} (f : m → n) (g : n → M) (i : m) :
(linear_map.fun_left R M f) g i = g (f i)
@[simp]
theorem linear_map.fun_left_id (R : Type u_1) (M : Type u_9) [semiring R] [add_comm_monoid M] [module R M] {n : Type u_21} (g : n → M) :
theorem linear_map.fun_left_comp (R : Type u_1) (M : Type u_9) [semiring R] [add_comm_monoid M] [module R M] {m : Type u_20} {n : Type u_21} {p : Type u_22} (f₁ : n → p) (f₂ : m → n) :
theorem linear_map.fun_left_surjective_of_injective (R : Type u_1) (M : Type u_9) [semiring R] [add_comm_monoid M] [module R M] {m : Type u_20} {n : Type u_21} (f : m → n) (hf : function.injective f) :
theorem linear_map.fun_left_injective_of_surjective (R : Type u_1) (M : Type u_9) [semiring R] [add_comm_monoid M] [module R M] {m : Type u_20} {n : Type u_21} (f : m → n) (hf : function.surjective f) :
def linear_equiv.fun_congr_left (R : Type u_1) (M : Type u_9) [semiring R] [add_comm_monoid 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
@[simp]
theorem linear_equiv.fun_congr_left_apply (R : Type u_1) (M : Type u_9) [semiring R] [add_comm_monoid M] [module R M] {m : Type u_20} {n : Type u_21} (e : m n) (x : n → M) :
@[simp]
theorem linear_equiv.fun_congr_left_id (R : Type u_1) (M : Type u_9) [semiring R] [add_comm_monoid M] [module R M] {n : Type u_21} :
@[simp]
theorem linear_equiv.fun_congr_left_comp (R : Type u_1) (M : Type u_9) [semiring R] [add_comm_monoid M] [module R M] {m : Type u_20} {n : Type u_21} {p : Type u_22} (e₁ : m n) (e₂ : n p) :
@[simp]
theorem linear_equiv.fun_congr_left_symm (R : Type u_1) (M : Type u_9) [semiring R] [add_comm_monoid M] [module R M] {m : Type u_20} {n : Type u_21} (e : m n) :
def linear_map.general_linear_group (R : Type u_1) (M : Type u_9) [semiring R] [add_comm_monoid M] [module R M] :
Type u_9

The group of invertible linear maps from M to itself

Equations

An invertible linear map f determines an equivalence from M to itself.

Equations

An equivalence from M to itself determines an invertible linear map.

Equations

The general linear group on R and M is multiplicatively equivalent to the type of linear equivalences between M and itself.

Equations
@[protected, instance]
def submodule.is_modular_lattice {R : Type u_1} {M : Type u_9} [ring R] [add_comm_group M] [module R M] :