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 #
- Many constructors for (semi)linear maps
submodule.span sis defined to be the smallest submodule containing the sets.- The kernel
kerand rangerangeof a linear map are submodules of the domain and codomain respectively. - The general linear group is defined to be the group of invertible linear maps from
Mto itself.
See linear_algebra.quotient for quotients by submodules.
Main theorems #
See linear_algebra.isomorphisms for Noether's three isomorphism theorems for modules.
Notations #
- We continue to use the notations
M →ₛₗ[σ] M₂andM →ₗ[R] M₂for the type of semilinear (resp. linear) maps fromMtoM₂over the ring homomorphismσ(resp. over the ringR). - We introduce the notation
R ∙ vfor the span of a singleton,submodule.span R {v}. This is\., not the same as the scalar multiplication•/\bub.
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 #
- Parts of this file have not yet been generalized to semilinear maps
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} :
@[simp]
@[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)
(ᾰ : α) :
⇑(finsupp.linear_equiv_fun_on_fintype R M α) x ᾰ = ⇑x ᾰ
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] :
Given fintype α, linear_equiv_fun_on_fintype R is the natural R-linear equivalence between
α →₀ β and α → β.
Equations
- finsupp.linear_equiv_fun_on_fintype R M α = {to_fun := coe_fn finsupp.has_coe_to_fun, map_add' := _, map_smul' := _, inv_fun := finsupp.equiv_fun_on_fintype.inv_fun, left_inv := _, right_inv := _}
@[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) :
⇑(finsupp.linear_equiv_fun_on_fintype R M α) (finsupp.single x m) = pi.single x 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) :
⇑((finsupp.linear_equiv_fun_on_fintype R M α).symm) (pi.single x m) = finsupp.single x 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) :
⇑((finsupp.linear_equiv_fun_on_fintype R M α).symm) ⇑f = f
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₄) :
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) :
The restriction of a linear map f : M → M₂ to a submodule p ⊆ M gives a linear map
p → M₂.
Equations
- f.dom_restrict p = f.comp p.subtype
@[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) :
⇑(f.dom_restrict p) x = ⇑f ↑x
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) :
A linear map f : M₂ → M whose values lie in a submodule p ⊆ M can be restricted to a
linear map M₂ → p.
@[simp]
theorem
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) :
↑(⇑(linear_map.cod_restrict p f h) x) = ⇑f x
@[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) :
(linear_map.cod_restrict p g h).comp f = linear_map.cod_restrict p (g.comp f) _
@[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) :
p.subtype.comp (linear_map.cod_restrict p f h) = f
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 ∈ p → ⇑f x ∈ p) :
Restrict domain and codomain of an endomorphism.
Equations
- f.restrict hf = linear_map.cod_restrict p (f.dom_restrict 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 ∈ p → ⇑f x ∈ p) :
f.restrict hf = linear_map.cod_restrict p (f.dom_restrict 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) :
f.restrict _ = (linear_map.cod_restrict p f hf).dom_restrict 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] :
Equations
- linear_map.unique_of_left = {to_inhabited := {default := default (M →ₛₗ[σ₁₂] M₂) linear_map.inhabited}, uniq := _}
@[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₂] :
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) :
Evaluation of a σ₁₂-linear map at a fixed a, as an add_monoid_hom.
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₂} :
linear_map.to_add_monoid_hom promoted to an add_monoid_hom
Equations
- linear_map.to_add_monoid_hom' = {to_fun := linear_map.to_add_monoid_hom σ₁₂, map_zero' := _, map_add' := _}
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) :
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) :
When f is an R-linear map taking values in S, then λb, f b • x is an R-linear map.
@[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] :
nontrivial (module.End R 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₂)) :
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) :
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) :
@[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_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 : ℕ) :
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 : ℕ) :
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 : ℕ) :
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) :
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₂) :
⇑(⇑(linear_map.applyₗ' S) v) f = ⇑f v
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₂] :
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.
@[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) :
⇑(linear_map.ring_lmap_equiv_self R S M) f = ⇑f 1
@[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) :
⇑((linear_map.ring_lmap_equiv_self R S M).symm) x = 1.smul_right x
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] :
The equivalence between R-linear maps from R to M, and points of M itself.
This says that the forgetful functor from R-modules to types is representable, by R.
This as an S-linear equivalence, under the assumption that S acts on M commuting with R.
When R is commutative, we can take this to be the usual action with S = R.
Otherwise, S = ℕ shows that the equivalence is additive.
See note [bundled maps over different rings].
def
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₃) :
Composition by f : M₂ → M₃ is a linear map from the space of linear maps M → M₂
to the space of linear maps M₂ → M₃.
@[simp]
theorem
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₂) :
⇑(⇑linear_map.applyₗ v) f = ⇑f v
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₂] :
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.
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) :
Alternative version of dom_restrict as a linear map.
Equations
- linear_map.dom_restrict' p = {to_fun := λ (φ : M →ₗ[R] M₂), φ.dom_restrict p, map_add' := _, map_smul' := _}
@[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₂] :
The family of linear maps M₂ → M parameterised by f ∈ M₂ → R, x ∈ M, is linear in f, x.
@[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) :
⇑((add_monoid_hom_lequiv_nat R).symm) f = f.to_add_monoid_hom
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
- add_monoid_hom_lequiv_nat R = {to_fun := add_monoid_hom.to_nat_linear_map _inst_3, map_add' := _, map_smul' := _, inv_fun := linear_map.to_add_monoid_hom (ring_hom.id ℕ), left_inv := _, right_inv := _}
@[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) :
⇑((add_monoid_hom_lequiv_int R).symm) f = f.to_add_monoid_hom
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
- add_monoid_hom_lequiv_int R = {to_fun := add_monoid_hom.to_int_linear_map _inst_3, map_add' := _, map_smul' := _, inv_fun := linear_map.to_add_monoid_hom (ring_hom.id ℤ), left_inv := _, right_inv := _}
@[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
- submodule.of_le h = linear_map.cod_restrict p' p.subtype _
@[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) :
↑(⇑(submodule.of_le h) x) = ↑x
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) :
⇑(submodule.of_le h) x = ⟨↑x, _⟩
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) :
q.subtype.comp (submodule.of_le h) = p.subtype
@[simp]
theorem
submodule.subsingleton_iff
(R : Type u_1)
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M] :
subsingleton (submodule R M) ↔ subsingleton M
@[simp]
theorem
submodule.nontrivial_iff
(R : Type u_1)
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M] :
nontrivial (submodule R M) ↔ nontrivial 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
- submodule.unique = {to_inhabited := {default := ⊥}, uniq := _}
@[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] :
nontrivial (submodule R M)
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₂
@[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₂} :
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) :
⇑f r ∈ submodule.map f p
theorem
submodule.apply_coe_mem_map
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[semiring R]
[semiring R₂]
[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) :
⇑f ↑r ∈ submodule.map f 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) :
submodule.map (g.comp f) p = submodule.map g (submodule.map f p)
theorem
submodule.map_mono
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[semiring R]
[semiring R₂]
[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} :
p ≤ p' → submodule.map f p ≤ submodule.map f p'
@[simp]
theorem
submodule.map_zero
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[semiring R]
[semiring R₂]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
(p : submodule R M)
[ring_hom_surjective σ₁₂] :
submodule.map 0 p = ⊥
theorem
submodule.map_add_le
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[semiring R]
[semiring R₂]
[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₂) :
submodule.map (f + g) p ≤ submodule.map f p ⊔ submodule.map g p
theorem
submodule.range_map_nonempty
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[semiring R]
[semiring R₂]
[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) :
↥p ≃ₛₗ[σ₁₂] ↥(submodule.map f p)
The pushforward of a submodule by an injective linear map is linearly equivalent to the original submodule.
@[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₂) :
submodule R M
The pullback of a submodule p ⊆ M₂ along f : M → M₂
@[simp]
theorem
submodule.comap_coe
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[semiring R]
[semiring R₂]
[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₂} :
x ∈ submodule.comap f p ↔ ⇑f x ∈ p
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₃) :
submodule.comap (g.comp f) p = submodule.comap f (submodule.comap g p)
theorem
submodule.comap_mono
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[semiring R]
[semiring R₂]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{f : M →ₛₗ[σ₁₂] M₂}
{q q' : submodule R₂ M₂} :
q ≤ q' → submodule.comap f q ≤ submodule.comap f q'
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₂} :
submodule.map f p ≤ q ↔ p ≤ submodule.comap f q
theorem
submodule.gc_map_comap
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[semiring R]
[semiring R₂]
[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₂) :
submodule.map f ⊥ = ⊥
@[simp]
theorem
submodule.map_sup
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[semiring R]
[semiring R₂]
[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₂) :
submodule.map f (p ⊔ p') = submodule.map f p ⊔ submodule.map f p'
@[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₂) :
submodule.comap f ⊤ = ⊤
@[simp]
theorem
submodule.comap_inf
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[semiring R]
[semiring R₂]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
(q q' : submodule R₂ M₂)
(f : M →ₛₗ[σ₁₂] M₂) :
submodule.comap f (q ⊓ q') = submodule.comap f q ⊓ submodule.comap f q'
@[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₂) :
submodule.comap 0 q = ⊤
theorem
submodule.map_comap_le
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[semiring R]
[semiring R₂]
[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₂) :
submodule.map f (submodule.comap f q) ≤ q
theorem
submodule.le_comap_map
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[semiring R]
[semiring R₂]
[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.comap f (submodule.map f p)
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₂) :
submodule.map f (submodule.comap f p) = p
theorem
submodule.map_surjective_of_surjective
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[semiring R]
[semiring R₂]
[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₂) :
submodule.map f (submodule.comap f p ⊔ submodule.comap f q) = p ⊔ q
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₂) :
submodule.map f (submodule.comap f p ⊓ submodule.comap f q) = p ⊓ q
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₂) :
submodule.comap f p ≤ submodule.comap f q ↔ p ≤ q
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) :
submodule.comap f (submodule.map f p) = p
theorem
submodule.comap_surjective_of_injective
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[semiring R]
[semiring R₂]
[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) :
submodule.comap f (submodule.map f p ⊓ submodule.map f q) = p ⊓ q
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) :
submodule.comap f (submodule.map f p ⊔ submodule.map f q) = p ⊔ q
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) :
submodule.map f p ≤ submodule.map f q ↔ p ≤ q
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₂} :
submodule.map f p ⊓ p' = submodule.map f (p ⊓ submodule.comap f p')
theorem
submodule.map_comap_subtype
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M]
(p p' : submodule R M) :
submodule.map p.subtype (submodule.comap p.subtype p') = p ⊓ p'
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 i → ⇑f v ∈ p i)
(v : M)
(H : 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) :
submodule R M
The span of a set s ⊆ M is the smallest submodule of M that contains s.
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} :
theorem
submodule.subset_span
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M]
{s : set M} :
s ⊆ ↑(submodule.span R s)
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} :
submodule.span R s ≤ p ↔ s ⊆ ↑p
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) :
submodule.span R s ≤ submodule.span R 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) :
submodule.span R s = p
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) :
submodule.span R ↑p = p
@[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) :
submodule.map f (submodule.span R s) = submodule.span R₂ (⇑f '' s)
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) :
submodule.map f (submodule.span R s) = submodule.span R₂ (⇑f '' s)
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 ∈ s → ⇑f 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 ∈ s → ⇑f 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} :
submodule.span R (insert 0 s) = submodule.span R s
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₂) :
submodule.span R (⇑f ⁻¹' s) ≤ submodule.comap f (submodule.span R₂ s)
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₂) :
submodule.span R (⇑f ⁻¹' s) ≤ submodule.comap f (submodule.span R₂ s)
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 ∈ s → p x)
(H0 : p 0)
(H1 : ∀ (x y : M), p x → p y → p (x + y))
(H2 : ∀ (a : R) (x : M), p x → p (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 x → p y → p (x + y))
(H2 : ∀ (a : R) (x : ↥(submodule.span R s)), p x → p (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} :
submodule.span R (coe ⁻¹' s) = ⊤
theorem
submodule.span_nat_eq_add_submonoid_closure
{M : Type u_9}
[add_comm_monoid M]
(s : set M) :
@[simp]
theorem
submodule.span_nat_eq
{M : Type u_9}
[add_comm_monoid M]
(s : add_submonoid M) :
(submodule.span ℕ ↑s).to_add_submonoid = s
@[simp]
theorem
submodule.span_int_eq
{M : Type u_1}
[add_comm_group M]
(s : add_subgroup M) :
(submodule.span ℤ ↑s).to_add_subgroup = s
@[protected]
span forms a Galois insertion with the coercion from submodule to set.
Equations
- submodule.gi R M = {choice := λ (s : set M) (_x : ↑(submodule.span R s) ≤ s), submodule.span R s, gc := _, le_l_u := _, choice_eq := _}
@[simp]
theorem
submodule.span_empty
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M] :
submodule.span R ∅ = ⊥
@[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) :
submodule.span R (s ∪ t) = submodule.span R s ⊔ submodule.span R t
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) :
submodule.span R ↑(s.attach.bUnion f) = ⨆ (x : ↥s), submodule.span R ↑(f x)
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) :
submodule.span R (r • s) ≤ submodule.span R s
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)) :
U ⊆ ↑(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) :
submodule.span R (r • s) = submodule.span R s
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.
theorem
submodule.coe_scott_continuous
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M] :
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.
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) :
x ∈ submodule.span R {x}
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) :
nontrivial ↥(submodule.span R {x})
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} :
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) :
@[simp]
theorem
submodule.span_zero_singleton
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M] :
submodule.span R {0} = ⊥
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) :
submodule.span R {r • x} ≤ submodule.span R {x}
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) :
submodule.span K {r • x} = submodule.span K {x}
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 ∈ s → x = 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) :
disjoint p (submodule.span K {x}) ↔ x ∉ p
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}) :
x ∈ 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) :
submodule.span R (insert x s) = submodule.span R {x} ⊔ submodule.span R s
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) :
submodule.span R (insert x s) = 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} :
submodule.span R ↑(submodule.span R s) = submodule.span R s
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] :
submodule.span R s ≤ submodule.restrict_scalars R (submodule.span S s)
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] :
↑(submodule.span R s) ⊆ ↑(submodule.span S s)
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] :
submodule.span S ↑(submodule.span R s) = submodule.span S s
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} :
@[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} :
submodule.span R {x} = ⊥ ↔ x = 0
@[simp]
theorem
submodule.span_zero
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M] :
submodule.span R 0 = ⊥
@[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₂) :
submodule.span R₂ (⇑f '' s) = submodule.map f (submodule.span R s)
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)) :
x ∉ submodule.span R 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) :
submodule.span R {m} ≤ p ↔ m ∈ p
theorem
submodule.singleton_span_is_compact_element
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M]
(x : 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_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) :
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') :
The product of two submodules is a submodule.
@[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') :
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') :
submodule.span R (s.prod t) ≤ (submodule.span R s).prod (submodule.span R t)
@[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'} :
@[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₂) :
submodule.map (-f) p = submodule.map f p
@[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) :
submodule.span R (-s) = submodule.span R s
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) :
submodule.comap (a • f) p = submodule.comap f p
theorem
submodule.map_smul
{K : Type u_7}
{V : Type u_18}
{V₂ : Type u_19}
[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) :
submodule.map (a • f) p = submodule.map f p
theorem
submodule.comap_smul'
{K : Type u_7}
{V : Type u_18}
{V₂ : Type u_19}
[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) :
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) :
set.eq_on ⇑f ⇑g ↑(submodule.span R 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} :
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₂)) :
@[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) :
@[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} :
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₂)) :
@[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) :
@[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} :
⇑f (⇑(dfinsupp.sum_add_hom g) t) = ⇑(dfinsupp.sum_add_hom (λ (i : ι), f.to_add_monoid_hom.comp (g i))) t
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₂) :
submodule.map (linear_map.cod_restrict p f h) p' = submodule.comap p.subtype (submodule.map f p')
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) :
submodule.comap (linear_map.cod_restrict p f hf) p' = submodule.comap f (submodule.map p.subtype 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].
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₂} :
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₂) :
f.range = submodule.map f ⊤
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₃) :
(g.comp f).range = submodule.map g f.range
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} :
submodule.map f p ≤ f.range
@[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 : ℕ) :
⇑(f.iterate_range) n = (f ^ n).range
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) :
ℕ →o order_dual (submodule R M)
The decreasing sequence of submodules consisting of the ranges of the iterates of a linear map.
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₂) :
Restrict the codomain of a linear map f to f.range.
This is the bundled version of set.range_factorization.
Equations
- f.range_restrict = linear_map.cod_restrict f.range f _
@[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) :
⇑(linear_map.to_span_singleton R M x) b = b • x
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) :
submodule.span R {x} = (linear_map.to_span_singleton R M x).range
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) :
⇑(linear_map.to_span_singleton R M x) 1 = x
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₂) :
submodule R M
The kernel of a linear map f : M → M₂ is defined to be comap f ⊥. This is equivalent to the
set of x : M such that f x = 0. The kernel is a submodule of M.
Equations
- f.ker = submodule.comap f ⊥
@[simp]
theorem
linear_map.ker_id
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M] :
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₃) :
(g.comp f).ker = submodule.comap f g.ker
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₃) :
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} :
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) :
(linear_map.cod_restrict p f hf).ker = f.ker
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) :
(linear_map.cod_restrict p f hf).range = submodule.comap p.subtype f.range
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₂) :
submodule.map f (submodule.comap f q) = f.range ⊓ q
theorem
submodule.map_comap_eq_self
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_12}
[semiring R]
[semiring R₂]
[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) :
submodule.map f (submodule.comap f q) = q
@[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.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₂) :
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₂} :
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₃} :
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₂} :
submodule.comap f p ≤ submodule.comap f p' ↔ p ≤ p'
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.
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) :
submodule.comap f (submodule.map f p) = p ⊔ f.ker
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) :
submodule.comap f (submodule.map f p) = 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} :
submodule.map f p ≤ submodule.map f p' ↔ p ≤ p' ⊔ f.ker
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} :
submodule.map f p ≤ submodule.map f p' ↔ p ≤ p'
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.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} :
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) :
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} :
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) :
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) :
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) :
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) :
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) :
submodule.span K {x} ⊔ f.ker = ⊤
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₂) :
submodule.map f ⊤ = f.range
@[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₂) :
submodule.comap f ⊥ = f.ker
@[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) :
submodule.map p.subtype p' ≤ 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) :
submodule.map p.subtype ⊤ = p
Under the canonical linear map from a submodule p to the ambient space M, the image of the
maximal submodule of p is just p.
@[simp]
theorem
submodule.comap_subtype_eq_top
{R : Type u_1}
{M : Type u_9}
[semiring R]
[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) :
submodule.comap p.subtype p = ⊤
@[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') :
(submodule.of_le h).ker = ⊥
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) :
(submodule.of_le h).range = submodule.comap q.subtype p
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) :
If N ⊆ M then submodules of N are the same as submodules of M contained in N
Equations
- submodule.map_subtype.rel_iso p = {to_equiv := {to_fun := λ (p' : submodule R ↥p), ⟨submodule.map p.subtype p', _⟩, inv_fun := λ (q : {p' // p' ≤ p}), submodule.comap p.subtype ↑q, left_inv := _, right_inv := _}, map_rel_iff' := _}
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
- submodule.map_subtype.order_embedding p = (rel_iso.to_rel_embedding (submodule.map_subtype.rel_iso p)).trans (subtype.rel_embedding has_le.le (λ (p' : submodule R M), p' ≤ p))
@[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) :
⇑(submodule.map_subtype.order_embedding p) p' = submodule.map p.subtype 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 v → u = 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 = ⊤) :
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 = ⊥) :
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) :
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
- ϕ.submodule_image N = submodule.map ϕ (submodule.comap O.subtype N)
@[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'} :
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'} :
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) :
ϕ.submodule_image N = (ϕ.comp (submodule.of_le hNO)).range
@[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 σ₂₁ σ₁₂] :
Between two zero modules, the zero map is an equivalence.
@[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 σ₂₁ σ₁₂] :
@[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 σ₂₁ σ₁₂] :
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) :
@[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 σ₂₁ σ₁₂] :
Between two zero modules, the zero map is the only equivalence.
Equations
- linear_equiv.unique = {to_inhabited := {default := 0}, uniq := _}
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} :
submodule.map ↑e p = submodule.comap ↑(e.symm) p
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
- e.of_submodule p = {to_fun := (linear_map.cod_restrict (submodule.map ↑e p) (↑e.dom_restrict p) _).to_fun, map_add' := _, map_smul' := _, inv_fun := λ (y : ↥(submodule.map ↑e p)), ⟨⇑↑(e.symm) ↑y, _⟩, left_inv := _, right_inv := _}
@[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} :
@[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) :
@[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) :
⇑f (⇑(dfinsupp.sum_add_hom g) t) = ⇑(dfinsupp.sum_add_hom (λ (i : ι), f.to_add_equiv.to_add_monoid_hom.comp (g i))) t
@[protected]
Linear equivalence between a curried and uncurried function.
Differs from tensor_product.curry.
Equations
- linear_equiv.curry R V V₂ = {to_fun := (equiv.curry V V₂ R).to_fun, map_add' := _, map_smul' := _, inv_fun := (equiv.curry V V₂ R).inv_fun, left_inv := _, right_inv := _}
@[simp]
theorem
linear_equiv.coe_curry
(R : Type u_1)
(V : Type u_18)
(V₂ : Type u_19)
[semiring R] :
⇑(linear_equiv.curry R V V₂) = function.curry
@[simp]
theorem
linear_equiv.coe_curry_symm
(R : Type u_1)
(V : Type u_18)
(V₂ : Type u_19)
[semiring R] :
⇑((linear_equiv.curry R V V₂).symm) = function.uncurry
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
- linear_equiv.of_eq p q h = {to_fun := (equiv.set.of_eq _).to_fun, map_add' := _, map_smul' := _, inv_fun := (equiv.set.of_eq _).inv_fun, left_inv := _, right_inv := _}
@[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) :
↑(⇑(linear_equiv.of_eq p q h) x) = ↑x
@[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) :
(linear_equiv.of_eq p q h).symm = linear_equiv.of_eq q p _
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) :
A linear equivalence which maps a submodule of one module onto another, restricts to a linear equivalence of the two submodules.
Equations
- e.of_submodules p q h = (e.of_submodule p).trans (linear_equiv.of_eq (submodule.map ↑e p) q h)
@[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) :
@[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) :
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
- f.of_submodule' U = (f.symm.of_submodules U (submodule.comap ↑(f.symm.symm) U) _).symm
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.
@[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) :
⇑(linear_equiv.of_top p h) x = ↑x
@[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) :
↑(⇑((linear_equiv.of_top p h).symm) x) = x
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) :
If a linear map has an inverse, it is a linear equivalence.
@[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 ≃ₛₗ[σ₁₂] ↥⊥) :
@[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₂) :
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) :
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.
@[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) :
↑(⇑(linear_equiv.of_left_inverse h) x) = ⇑f x
@[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) :
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) :
↑(⇑(linear_equiv.of_injective f h) x) = ⇑f x
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) :
A bijective linear map is a linear equivalence.
Equations
- linear_equiv.of_bijective f hf₁ hf₂ = (linear_equiv.of_injective f hf₁).trans (linear_equiv.of_top f.range _)
@[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) :
@[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) :
@[simp]
theorem
linear_equiv.coe_neg
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_group M]
[module R M] :
⇑(linear_equiv.neg R) = -id
theorem
linear_equiv.neg_apply
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_group M]
[module R M]
(x : M) :
⇑(linear_equiv.neg R) x = -x
@[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
- linear_equiv.smul_of_unit a = linear_equiv.of_linear (↑a • 1) (↑a⁻¹ • 1) _ _
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₂₂) :
A linear isomorphism between the domains and codomains of two spaces of linear maps gives a linear isomorphism between the two function spaces.
@[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₂) :
@[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₁) :
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₃) :
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
- f.congr_right = (linear_equiv.refl R M).arrow_congr f
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₂) :
module.End R M ≃ₗ[R] module.End R M₂
If M and M₂ are linearly isomorphic then the two spaces of linear maps from M and M₂ to
themselves are linearly isomorphic.
Equations
- e.conj = e.arrow_congr e
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) :
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₂) :
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) :
⇑(e.conj) (linear_map.comp g f) = linear_map.comp (⇑(e.conj) g) (⇑(e.conj) f)
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₃) :
@[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
- linear_equiv.smul_of_ne_zero K M a ha = linear_equiv.smul_of_unit (units.mk0 a ha)
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) :
(linear_map.to_span_singleton K M x).ker = ⊥
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) :
K ≃ₗ[K] ↥(submodule.span K {x})
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
- linear_equiv.to_span_nonzero_singleton K M x h = (linear_equiv.of_injective (linear_map.to_span_singleton K M x) _).trans (linear_equiv.of_eq (linear_map.to_span_singleton K M x).range (submodule.span K {x}) _)
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) :
⇑(linear_equiv.to_span_nonzero_singleton K M x h) 1 = ⟨x, _⟩
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) :
↥(submodule.span K {x}) ≃ₗ[K] K
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
- p.equiv_subtype_map q = {to_fun := (linear_map.cod_restrict (submodule.map p.subtype q) (p.subtype.dom_restrict q) _).to_fun, map_add' := _, map_smul' := _, inv_fun := λ (ᾰ : ↥(submodule.map p.subtype q)), subtype.cases_on ᾰ (λ (x : M) (hx : x ∈ submodule.map p.subtype q), ⟨⟨x, _⟩, _⟩), left_inv := _, right_inv := _}
@[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) :
↑(⇑(p.equiv_subtype_map q) x) = ⇑(p.subtype.dom_restrict q) x
@[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)) :
↑(⇑(submodule.comap_subtype_equiv_of_le hpq) x) = ↑x
@[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.
@[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) :
submodule.map ↑e K = submodule.comap ↑(e.symm) K
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₂) :
submodule.comap ↑e K = submodule.map ↑(e.symm) K
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₂) :
submodule.comap f₁ q ⊓ submodule.comap f₂ q ≤ submodule.comap (f₁ + f₂) q
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₂) :
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₂).
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) :
An equivalence whose underlying function is linear is a linear equivalence.
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) :
An additive equivalence whose underlying function preserves smul is a linear equivalence.
@[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) :
⇑(e.to_linear_equiv h) = ⇑e
@[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) :
Given an R-module M and a function m → n between arbitrary types,
construct a linear map (n → M) →ₗ[R] (m → M)
@[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) :
⇑(linear_map.fun_left R M id) g = g
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) :
linear_map.fun_left R M (f₁ ∘ f₂) = (linear_map.fun_left R M f₂).comp (linear_map.fun_left R M f₁)
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) :
Given an R-module M and an equivalence m ≃ n between arbitrary types,
construct a linear equivalence (n → M) ≃ₗ[R] (m → M)
Equations
- linear_equiv.fun_congr_left R M e = linear_equiv.of_linear (linear_map.fun_left R M ⇑e) (linear_map.fun_left R M ⇑(e.symm)) _ _
@[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) :
⇑(linear_equiv.fun_congr_left R M e) x = ⇑(linear_map.fun_left R M ⇑e) x
@[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} :
linear_equiv.fun_congr_left R M (equiv.refl n) = linear_equiv.refl R (n → M)
@[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) :
linear_equiv.fun_congr_left R M (e₁.trans e₂) = (linear_equiv.fun_congr_left R M e₂).trans (linear_equiv.fun_congr_left R M e₁)
@[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) :
(linear_equiv.fun_congr_left R M e).symm = linear_equiv.fun_congr_left R M e.symm
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
- linear_map.general_linear_group R M = units (M →ₗ[R] M)
@[protected, instance]
def
linear_map.general_linear_group.has_coe_to_fun
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M] :
has_coe_to_fun (linear_map.general_linear_group R M) (λ (_x : linear_map.general_linear_group R M), M → M)
def
linear_map.general_linear_group.to_linear_equiv
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M]
(f : linear_map.general_linear_group R M) :
An invertible linear map f determines an equivalence from M to itself.
def
linear_map.general_linear_group.of_linear_equiv
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M]
(f : M ≃ₗ[R] M) :
An equivalence from M to itself determines an invertible linear map.
def
linear_map.general_linear_group.general_linear_equiv
(R : Type u_1)
(M : Type u_9)
[semiring R]
[add_comm_monoid M]
[module R M] :
linear_map.general_linear_group R M ≃* M ≃ₗ[R] M
The general linear group on R and M is multiplicatively equivalent to the type of linear
equivalences between M and itself.
Equations
- linear_map.general_linear_group.general_linear_equiv R M = {to_fun := linear_map.general_linear_group.to_linear_equiv _inst_3, inv_fun := linear_map.general_linear_group.of_linear_equiv _inst_3, left_inv := _, right_inv := _, map_mul' := _}
@[simp]
theorem
linear_map.general_linear_group.general_linear_equiv_to_linear_map
(R : Type u_1)
(M : Type u_9)
[semiring R]
[add_comm_monoid M]
[module R M]
(f : linear_map.general_linear_group R M) :
@[simp]
theorem
linear_map.general_linear_group.coe_fn_general_linear_equiv
(R : Type u_1)
(M : Type u_9)
[semiring R]
[add_comm_monoid M]
[module R M]
(f : linear_map.general_linear_group R M) :
@[protected, instance]
def
submodule.is_modular_lattice
{R : Type u_1}
{M : Type u_9}
[ring R]
[add_comm_group M]
[module R M] :
is_modular_lattice (submodule R M)