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. If p and q are submodules of a module, p ≤ q
means that p ⊆ q.
Many of the relevant definitions, including module, submodule, and linear_map, are found in
src/algebra/module.
Main definitions
- Many constructors for linear maps, including
prodandcoprod submodule.span sis defined to be the smallest submodule containing the sets.- If
pis a submodule ofM,submodule.quotient pis the quotient ofMwith respect top: that is, elements ofMare identified if their difference is inp. This is itself a module. - 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.
Main statements
- The first and second isomorphism laws for modules are proved as
quot_ker_equiv_rangeandquotient_inf_equiv_sup_quotient.
Notations
- We continue to use the notation
M →ₗ[R] M₂for the type of linear maps fromMtoM₂over the ringR. - We introduce the notations
M ≃ₗ M₂andM ≃ₗ[R] M₂forlinear_equiv M M₂. In the first, the ringRis implicit. - 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 (prod, coprod, arithmetic operations like +) instead of defining a function and proving
it is linear.
Tags
linear algebra, vector space, module
theorem
finsupp.smul_sum
{α : Type u}
{β : Type v}
{R : Type w}
{M : Type y}
[has_zero β]
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{v : α →₀ β}
{c : R}
{h : α → β → M} :
Properties of linear maps
@[simp]
theorem
linear_map.comp_id
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(f : M →ₗ[R] M₂) :
f.comp linear_map.id = f
@[simp]
theorem
linear_map.id_comp
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(f : M →ₗ[R] M₂) :
linear_map.id.comp f = f
theorem
linear_map.comp_assoc
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
{M₄ : Type z}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[add_comm_monoid M₄]
[semimodule R M]
[semimodule R M₂]
[semimodule R M₃]
[semimodule R M₄]
(f : M →ₗ[R] M₂)
(g : M₂ →ₗ[R] M₃)
(h : M₃ →ₗ[R] M₄) :
def
linear_map.dom_restrict
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(f : M →ₗ[R] 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}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(f : M →ₗ[R] M₂)
(p : submodule R M)
(x : ↥p) :
⇑(f.dom_restrict p) x = ⇑f ↑x
def
linear_map.cod_restrict
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(p : submodule R M)
(f : M₂ →ₗ[R] 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}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(p : submodule R M)
(f : M₂ →ₗ[R] 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}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[semimodule R M]
[semimodule R M₂]
[semimodule R M₃]
(f : M →ₗ[R] M₂)
(p : submodule R M₂)
(h : ∀ (b : M), ⇑f b ∈ p)
(g : M₃ →ₗ[R] M) :
(linear_map.cod_restrict p f h).comp g = linear_map.cod_restrict p (f.comp g) _
@[simp]
theorem
linear_map.subtype_comp_cod_restrict
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(f : M →ₗ[R] 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}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule 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.subtype_comp_restrict
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{f : M →ₗ[R] M}
{p : submodule R M}
(hf : ∀ (x : M), x ∈ p → ⇑f x ∈ p) :
p.subtype.comp (f.restrict hf) = f.dom_restrict p
theorem
linear_map.restrict_eq_cod_restrict_dom_restrict
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule 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}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule 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
@[instance]
def
linear_map.has_zero
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂] :
The constant 0 map is linear.
@[instance]
def
linear_map.inhabited
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂] :
Equations
- linear_map.inhabited = {default := 0}
@[simp]
theorem
linear_map.zero_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(x : M) :
@[simp]
theorem
linear_map.default_def
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂] :
@[instance]
def
linear_map.unique_of_left
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
[subsingleton M] :
Equations
- linear_map.unique_of_left = {to_inhabited := {default := default (M →ₗ[R] M₂) linear_map.inhabited}, uniq := _}
@[instance]
def
linear_map.unique_of_right
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
[subsingleton M₂] :
@[instance]
def
linear_map.has_add
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂] :
The sum of two linear maps is linear.
@[simp]
theorem
linear_map.add_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(f g : M →ₗ[R] M₂)
(x : M) :
@[instance]
def
linear_map.add_comm_monoid
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂] :
add_comm_monoid (M →ₗ[R] M₂)
The type of linear maps is an additive monoid.
Equations
- linear_map.add_comm_monoid = {add := has_add.add linear_map.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, add_comm := _}
@[instance]
def
linear_map.linear_map_apply_is_add_monoid_hom
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(a : M) :
is_add_monoid_hom (λ (f : M →ₗ[R] M₂), ⇑f a)
theorem
linear_map.add_comp
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[semimodule R M]
[semimodule R M₂]
[semimodule R M₃]
(f : M →ₗ[R] M₂)
(g h : M₂ →ₗ[R] M₃) :
theorem
linear_map.comp_add
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[semimodule R M]
[semimodule R M₂]
[semimodule R M₃]
(f g : M →ₗ[R] M₂)
(h : M₂ →ₗ[R] M₃) :
theorem
linear_map.sum_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
{ι : Type x}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(t : finset ι)
(f : ι → (M →ₗ[R] M₂))
(b : M) :
def
linear_map.smul_right
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(f : M₂ →ₗ[R] R)
(x : M) :
λb, f b • x is a linear map.
@[simp]
theorem
linear_map.smul_right_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(f : M₂ →ₗ[R] R)
(x : M)
(c : M₂) :
⇑(f.smul_right x) c = ⇑f c • x
@[instance]
def
linear_map.has_one
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
Equations
- linear_map.has_one = {one := linear_map.id _inst_6}
@[instance]
def
linear_map.has_mul
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
Equations
- linear_map.has_mul = {mul := linear_map.comp _inst_6}
theorem
linear_map.mul_eq_comp
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
(f g : M →ₗ[R] M) :
@[simp]
theorem
linear_map.one_app
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
(x : M) :
@[simp]
theorem
linear_map.mul_app
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
(A B : M →ₗ[R] M)
(x : M) :
@[simp]
theorem
linear_map.comp_zero
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[semimodule R M]
[semimodule R M₂]
[semimodule R M₃]
(f : M →ₗ[R] M₂) :
@[simp]
theorem
linear_map.zero_comp
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[semimodule R M]
[semimodule R M₂]
[semimodule R M₃]
(f : M →ₗ[R] M₂) :
theorem
linear_map.coe_fn_sum
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
{ι : Type u_1}
(t : finset ι)
(f : ι → (M →ₗ[R] M₂)) :
@[instance]
Equations
- linear_map.monoid = {mul := has_mul.mul linear_map.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _}
theorem
linear_map.pi_apply_eq_sum_univ
{R : Type u}
{M : Type v}
{ι : Type x}
[semiring R]
[add_comm_monoid M]
[semimodule 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.
def
linear_map.fst
(R : Type u)
(M : Type v)
(M₂ : Type w)
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂] :
The first projection of a product is a linear map.
def
linear_map.snd
(R : Type u)
(M : Type v)
(M₂ : Type w)
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂] :
The second projection of a product is a linear map.
@[simp]
theorem
linear_map.fst_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(x : M × M₂) :
⇑(linear_map.fst R M M₂) x = x.fst
@[simp]
theorem
linear_map.snd_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(x : M × M₂) :
⇑(linear_map.snd R M M₂) x = x.snd
def
linear_map.prod
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[semimodule R M]
[semimodule R M₂]
[semimodule R M₃]
(f : M →ₗ[R] M₂)
(g : M →ₗ[R] M₃) :
The prod of two linear maps is a linear map.
@[simp]
theorem
linear_map.prod_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[semimodule R M]
[semimodule R M₂]
[semimodule R M₃]
(f : M →ₗ[R] M₂)
(g : M →ₗ[R] M₃)
(x : M) :
@[simp]
theorem
linear_map.fst_prod
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[semimodule R M]
[semimodule R M₂]
[semimodule R M₃]
(f : M →ₗ[R] M₂)
(g : M →ₗ[R] M₃) :
(linear_map.fst R M₂ M₃).comp (f.prod g) = f
@[simp]
theorem
linear_map.snd_prod
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[semimodule R M]
[semimodule R M₂]
[semimodule R M₃]
(f : M →ₗ[R] M₂)
(g : M →ₗ[R] M₃) :
(linear_map.snd R M₂ M₃).comp (f.prod g) = g
@[simp]
theorem
linear_map.pair_fst_snd
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂] :
(linear_map.fst R M M₂).prod (linear_map.snd R M M₂) = linear_map.id
def
linear_map.inl
(R : Type u)
(M : Type v)
(M₂ : Type w)
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂] :
The left injection into a product is a linear map.
Equations
- linear_map.inl R M M₂ = {to_fun := ⇑(add_monoid_hom.inl M M₂), map_add' := _, map_smul' := _}
def
linear_map.inr
(R : Type u)
(M : Type v)
(M₂ : Type w)
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂] :
The right injection into a product is a linear map.
Equations
- linear_map.inr R M M₂ = {to_fun := ⇑(add_monoid_hom.inr M M₂), map_add' := _, map_smul' := _}
@[simp]
theorem
linear_map.inl_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(x : M) :
⇑(linear_map.inl R M M₂) x = (x, 0)
@[simp]
theorem
linear_map.inr_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(x : M₂) :
⇑(linear_map.inr R M M₂) x = (0, x)
theorem
linear_map.inl_injective
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂] :
function.injective ⇑(linear_map.inl R M M₂)
theorem
linear_map.inr_injective
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂] :
function.injective ⇑(linear_map.inr R M M₂)
def
linear_map.coprod
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[semimodule R M]
[semimodule R M₂]
[semimodule R M₃]
(f : M →ₗ[R] M₃)
(g : M₂ →ₗ[R] M₃) :
The coprod function λ x : M × M₂, f x.1 + g x.2 is a linear map.
@[simp]
theorem
linear_map.coprod_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[semimodule R M]
[semimodule R M₂]
[semimodule R M₃]
(f : M →ₗ[R] M₃)
(g : M₂ →ₗ[R] M₃)
(x : M)
(y : M₂) :
@[simp]
theorem
linear_map.coprod_inl
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[semimodule R M]
[semimodule R M₂]
[semimodule R M₃]
(f : M →ₗ[R] M₃)
(g : M₂ →ₗ[R] M₃) :
(f.coprod g).comp (linear_map.inl R M M₂) = f
@[simp]
theorem
linear_map.coprod_inr
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[semimodule R M]
[semimodule R M₂]
[semimodule R M₃]
(f : M →ₗ[R] M₃)
(g : M₂ →ₗ[R] M₃) :
(f.coprod g).comp (linear_map.inr R M M₂) = g
@[simp]
theorem
linear_map.coprod_inl_inr
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂] :
(linear_map.inl R M M₂).coprod (linear_map.inr R M M₂) = linear_map.id
theorem
linear_map.fst_eq_coprod
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂] :
linear_map.fst R M M₂ = linear_map.id.coprod 0
theorem
linear_map.snd_eq_coprod
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂] :
linear_map.snd R M M₂ = 0.coprod linear_map.id
theorem
linear_map.inl_eq_prod
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂] :
linear_map.inl R M M₂ = linear_map.id.prod 0
theorem
linear_map.inr_eq_prod
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂] :
linear_map.inr R M M₂ = 0.prod linear_map.id
def
linear_map.prod_map
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
{M₄ : Type z}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[add_comm_monoid M₄]
[semimodule R M]
[semimodule R M₂]
[semimodule R M₃]
[semimodule R M₄]
(f : M →ₗ[R] M₃)
(g : M₂ →ₗ[R] M₄) :
prod.map of two linear maps.
Equations
- f.prod_map g = (f.comp (linear_map.fst R M M₂)).prod (g.comp (linear_map.snd R M M₂))
@[simp]
theorem
linear_map.prod_map_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
{M₄ : Type z}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[add_comm_monoid M₄]
[semimodule R M]
[semimodule R M₂]
[semimodule R M₃]
[semimodule R M₄]
(f : M →ₗ[R] M₃)
(g : M₂ →ₗ[R] M₄)
(x : M × M₂) :
@[instance]
def
linear_map.has_neg
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_group M₂]
[semimodule R M]
[semimodule R M₂] :
The negation of a linear map is linear.
@[simp]
theorem
linear_map.neg_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_group M₂]
[semimodule R M]
[semimodule R M₂]
(f : M →ₗ[R] M₂)
(x : M) :
@[simp]
theorem
linear_map.comp_neg
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[semiring R]
[add_comm_monoid M]
[add_comm_group M₂]
[add_comm_group M₃]
[semimodule R M]
[semimodule R M₂]
[semimodule R M₃]
(f : M →ₗ[R] M₂)
(g : M₂ →ₗ[R] M₃) :
@[instance]
def
linear_map.has_sub
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_group M₂]
[semimodule R M]
[semimodule R M₂] :
The negation of a linear map is linear.
@[simp]
theorem
linear_map.sub_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_group M₂]
[semimodule R M]
[semimodule R M₂]
(f g : M →ₗ[R] M₂)
(x : M) :
theorem
linear_map.sub_comp
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[semiring R]
[add_comm_monoid M]
[add_comm_group M₂]
[add_comm_group M₃]
[semimodule R M]
[semimodule R M₂]
[semimodule R M₃]
(f : M →ₗ[R] M₂)
(g h : M₂ →ₗ[R] M₃) :
theorem
linear_map.comp_sub
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[semiring R]
[add_comm_monoid M]
[add_comm_group M₂]
[add_comm_group M₃]
[semimodule R M]
[semimodule R M₂]
[semimodule R M₃]
(f g : M →ₗ[R] M₂)
(h : M₂ →ₗ[R] M₃) :
@[instance]
def
linear_map.add_comm_group
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_group M₂]
[semimodule R M]
[semimodule R M₂] :
add_comm_group (M →ₗ[R] M₂)
The type of linear maps is an additive group.
Equations
- linear_map.add_comm_group = {add := has_add.add linear_map.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, neg := has_neg.neg linear_map.has_neg, sub := has_sub.sub linear_map.has_sub, sub_eq_add_neg := _, add_left_neg := _, add_comm := _}
@[instance]
def
linear_map.linear_map_apply_is_add_group_hom
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_group M₂]
[semimodule R M]
[semimodule R M₂]
(a : M) :
is_add_group_hom (λ (f : M →ₗ[R] M₂), ⇑f a)
@[instance]
def
linear_map.has_scalar
{R : Type u}
{M : Type v}
{M₂ : Type w}
{S : Type u_1}
[semiring R]
[monoid S]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
[distrib_mul_action S M₂]
[smul_comm_class R S M₂] :
has_scalar S (M →ₗ[R] M₂)
@[simp]
theorem
linear_map.smul_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
{S : Type u_1}
[semiring R]
[monoid S]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
[distrib_mul_action S M₂]
[smul_comm_class R S M₂]
(f : M →ₗ[R] M₂)
(a : S)
(x : M) :
@[instance]
def
linear_map.distrib_mul_action
{R : Type u}
{M : Type v}
{M₂ : Type w}
{S : Type u_1}
[semiring R]
[monoid S]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
[distrib_mul_action S M₂]
[smul_comm_class R S M₂] :
distrib_mul_action S (M →ₗ[R] M₂)
Equations
- linear_map.distrib_mul_action = {to_mul_action := {to_has_scalar := linear_map.has_scalar _inst_10, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}
theorem
linear_map.smul_comp
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
{S : Type u_1}
[semiring R]
[monoid S]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[semimodule R M]
[semimodule R M₂]
[semimodule R M₃]
[distrib_mul_action S M₂]
[smul_comm_class R S M₂]
(a : S)
(g : M₃ →ₗ[R] M₂)
(f : M →ₗ[R] M₃) :
@[instance]
def
linear_map.semimodule
{R : Type u}
{M : Type v}
{M₂ : Type w}
{S : Type u_1}
[semiring R]
[semiring S]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
[semimodule S M₂]
[smul_comm_class R S M₂] :
semimodule S (M →ₗ[R] M₂)
Equations
- linear_map.semimodule = {to_distrib_mul_action := linear_map.distrib_mul_action _inst_11, add_smul := _, zero_smul := _}
def
linear_map.applyₗ'
{R : Type u}
{M : Type v}
{M₂ : Type w}
(S : Type u_1)
[semiring R]
[semiring S]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
[semimodule S M₂]
[smul_comm_class R S M₂]
(v : M) :
Applying a linear map at v : M, seen as S-linear map from M →ₗ[R] M₂ to M₂.
See applyₗ for a version where S = R
theorem
linear_map.comp_smul
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[comm_semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[semimodule R M]
[semimodule R M₂]
[semimodule R M₃]
(f : M →ₗ[R] M₂)
(g : M₂ →ₗ[R] M₃)
(a : R) :
def
linear_map.comp_right
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[comm_semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[semimodule R M]
[semimodule R M₂]
[semimodule 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₃.
def
linear_map.applyₗ
{R : Type u}
{M : Type v}
{M₂ : Type w}
[comm_semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(v : 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.
Equations
@[instance]
def
linear_map.endomorphism_semiring
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
Equations
- linear_map.endomorphism_semiring = {add := add_comm_monoid.add linear_map.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero linear_map.add_comm_monoid, zero_add := _, add_zero := _, add_comm := _, mul := has_mul.mul linear_map.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _}
theorem
linear_map.mul_apply
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
(f g : M →ₗ[R] M)
(x : M) :
@[instance]
def
linear_map.endomorphism_ring
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[semimodule R M] :
Equations
- linear_map.endomorphism_ring = {add := semiring.add linear_map.endomorphism_semiring, add_assoc := _, zero := semiring.zero linear_map.endomorphism_semiring, zero_add := _, add_zero := _, neg := add_comm_group.neg linear_map.add_comm_group, sub := add_comm_group.sub linear_map.add_comm_group, sub_eq_add_neg := _, add_left_neg := _, add_comm := _, mul := semiring.mul linear_map.endomorphism_semiring, mul_assoc := _, one := semiring.one linear_map.endomorphism_semiring, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _}
def
linear_map.smul_rightₗ
{R : Type u}
{M : Type v}
{M₂ : Type w}
[comm_ring R]
[add_comm_group M]
[add_comm_group M₂]
[semimodule R M]
[semimodule 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}
{M : Type v}
{M₂ : Type w}
[comm_ring R]
[add_comm_group M]
[add_comm_group M₂]
[semimodule R M]
[semimodule R M₂]
(f : M₂ →ₗ[R] R)
(x : M)
(c : M₂) :
Properties of submodules
@[instance]
def
submodule.partial_order
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
partial_order (submodule R M)
Equations
- submodule.partial_order = {le := λ (p p' : submodule R M), ∀ ⦃x : M⦄, x ∈ p → x ∈ p', lt := partial_order.lt (partial_order.lift coe submodule.coe_injective), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
theorem
submodule.le_def
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{p p' : submodule R M} :
theorem
submodule.le_def'
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{p p' : submodule R M} :
theorem
submodule.lt_def
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{p p' : submodule R M} :
theorem
submodule.not_le_iff_exists
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{p p' : submodule R M} :
theorem
submodule.exists_of_lt
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{p p' : submodule R M} :
theorem
submodule.lt_iff_le_and_exists
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{p p' : submodule R M} :
def
submodule.of_le
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule 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}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule 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}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{p p' : submodule R M}
(h : p ≤ p')
(x : ↥p) :
⇑(submodule.of_le h) x = ⟨↑x, _⟩
theorem
submodule.subtype_comp_of_le
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
(p q : submodule R M)
(h : p ≤ q) :
q.subtype.comp (submodule.of_le h) = p.subtype
@[instance]
The set {0} is the bottom element of the lattice of submodules.
@[instance]
def
submodule.inhabited'
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
Equations
@[simp]
theorem
submodule.bot_coe
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
@[simp]
theorem
submodule.mem_bot
(R : Type u)
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{x : M} :
theorem
submodule.nonzero_mem_of_bot_lt
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{I : submodule R M}
(bot_lt : ⊥ < I) :
@[instance]
def
submodule.order_bot
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
Equations
- submodule.order_bot = {bot := ⊥, le := partial_order.le submodule.partial_order, lt := partial_order.lt submodule.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _}
theorem
submodule.eq_bot_iff
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
(p : submodule R M) :
theorem
submodule.ne_bot_iff
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
(p : submodule R M) :
@[instance]
The universal set is the top element of the lattice of submodules.
@[simp]
theorem
submodule.top_coe
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
@[simp]
theorem
submodule.mem_top
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{x : M} :
theorem
submodule.eq_bot_of_zero_eq_one
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
(p : submodule R M)
(zero_eq_one : 0 = 1) :
@[instance]
def
submodule.order_top
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
Equations
- submodule.order_top = {top := ⊤, le := partial_order.le submodule.partial_order, lt := partial_order.lt submodule.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _}
@[instance]
@[instance]
@[instance]
def
submodule.complete_lattice
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
complete_lattice (submodule R M)
Equations
- submodule.complete_lattice = {sup := λ (a b : submodule R M), Inf {x : submodule R M | a ≤ x ∧ b ≤ x}, le := order_top.le submodule.order_top, lt := order_top.lt submodule.order_top, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := has_inf.inf submodule.has_inf, inf_le_left := _, inf_le_right := _, le_inf := _, top := order_top.top submodule.order_top, le_top := _, bot := order_bot.bot submodule.order_bot, bot_le := _, Sup := λ (tt : set (submodule R M)), Inf {t : submodule R M | ∀ (t' : submodule R M), t' ∈ tt → t' ≤ t}, Inf := Inf submodule.has_Inf, le_Sup := _, Sup_le := _, Inf_le := _, le_Inf := _}
@[instance]
def
submodule.add_comm_monoid_submodule
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
add_comm_monoid (submodule R M)
Equations
- submodule.add_comm_monoid_submodule = {add := has_sup.sup (semilattice_sup.to_has_sup (submodule R M)), add_assoc := _, zero := ⊥, zero_add := _, add_zero := _, add_comm := _}
@[simp]
theorem
submodule.add_eq_sup
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
(p q : submodule R M) :
@[simp]
theorem
submodule.zero_eq_bot
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
theorem
submodule.eq_top_iff'
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{p : submodule R M} :
theorem
submodule.bot_ne_top
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
[nontrivial M] :
@[simp]
theorem
submodule.inf_coe
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
(p p' : submodule R M) :
@[simp]
theorem
submodule.mem_inf
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{x : M}
{p p' : submodule R M} :
@[simp]
theorem
submodule.Inf_coe
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
(P : set (submodule R M)) :
@[simp]
theorem
submodule.infi_coe
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{ι : Sort u_1}
(p : ι → submodule R M) :
@[simp]
theorem
submodule.mem_Inf
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{S : set (submodule R M)}
{x : M} :
@[simp]
theorem
submodule.mem_infi
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{x : M}
{ι : Sort u_1}
(p : ι → submodule R M) :
theorem
submodule.disjoint_def
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{p p' : submodule R M} :
theorem
submodule.disjoint_def'
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{p p' : submodule R M} :
theorem
submodule.mem_right_iff_eq_zero_of_disjoint
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{p p' : submodule R M}
(h : disjoint p p')
{x : ↥p} :
theorem
submodule.mem_left_iff_eq_zero_of_disjoint
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{p p' : submodule R M}
(h : disjoint p p')
{x : ↥p'} :
def
submodule.map
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(f : M →ₗ[R] 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}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(f : M →ₗ[R] M₂)
(p : submodule R M) :
@[simp]
theorem
submodule.mem_map
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
{f : M →ₗ[R] M₂}
{p : submodule R M}
{x : M₂} :
theorem
submodule.mem_map_of_mem
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
{f : M →ₗ[R] M₂}
{p : submodule R M}
{r : M}
(h : r ∈ p) :
⇑f r ∈ submodule.map f p
@[simp]
theorem
submodule.map_id
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
(p : submodule R M) :
theorem
submodule.map_comp
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[semimodule R M]
[semimodule R M₂]
[semimodule R M₃]
(f : M →ₗ[R] M₂)
(g : M₂ →ₗ[R] 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}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
{f : M →ₗ[R] M₂}
{p p' : submodule R M} :
p ≤ p' → submodule.map f p ≤ submodule.map f p'
@[simp]
theorem
submodule.map_zero
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(p : submodule R M) :
submodule.map 0 p = ⊥
def
submodule.comap
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(f : M →ₗ[R] 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}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(f : M →ₗ[R] M₂)
(p : submodule R M₂) :
@[simp]
theorem
submodule.mem_comap
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
{x : M}
{f : M →ₗ[R] M₂}
{p : submodule R M₂} :
x ∈ submodule.comap f p ↔ ⇑f x ∈ p
theorem
submodule.comap_id
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
(p : submodule R M) :
theorem
submodule.comap_comp
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[semimodule R M]
[semimodule R M₂]
[semimodule R M₃]
(f : M →ₗ[R] M₂)
(g : M₂ →ₗ[R] 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}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
{f : M →ₗ[R] 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}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
{f : M →ₗ[R] 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}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(f : M →ₗ[R] M₂) :
@[simp]
theorem
submodule.map_bot
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(f : M →ₗ[R] M₂) :
submodule.map f ⊥ = ⊥
@[simp]
theorem
submodule.map_sup
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(p p' : submodule R M)
(f : M →ₗ[R] M₂) :
submodule.map f (p ⊔ p') = submodule.map f p ⊔ submodule.map f p'
@[simp]
theorem
submodule.map_supr
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
{ι : Sort u_1}
(f : M →ₗ[R] 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}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(f : M →ₗ[R] M₂) :
submodule.comap f ⊤ = ⊤
@[simp]
theorem
submodule.comap_inf
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(q q' : submodule R M₂)
(f : M →ₗ[R] M₂) :
submodule.comap f (q ⊓ q') = submodule.comap f q ⊓ submodule.comap f q'
@[simp]
theorem
submodule.comap_infi
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
{ι : Sort u_1}
(f : M →ₗ[R] 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}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(q : submodule R M₂) :
submodule.comap 0 q = ⊤
theorem
submodule.map_comap_le
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(f : M →ₗ[R] M₂)
(q : submodule R M₂) :
submodule.map f (submodule.comap f q) ≤ q
theorem
submodule.le_comap_map
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(f : M →ₗ[R] M₂)
(p : submodule R M) :
p ≤ submodule.comap f (submodule.map f p)
theorem
submodule.map_inf_eq_map_inf_comap
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
{f : M →ₗ[R] 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}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule 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}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
(b : ↥⊥) :
b = 0
def
submodule.span
(R : Type u)
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule 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}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{x : M}
{s : set M} :
theorem
submodule.subset_span
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{s : set M} :
s ⊆ ↑(submodule.span R s)
theorem
submodule.span_le
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{s : set M}
{p : submodule R M} :
submodule.span R s ≤ p ↔ s ⊆ ↑p
theorem
submodule.span_mono
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule 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}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
(p : submodule R M)
{s : set M}
(h₁ : s ⊆ ↑p)
(h₂ : p ≤ submodule.span R s) :
submodule.span R s = p
@[simp]
theorem
submodule.span_eq
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
(p : submodule R M) :
submodule.span R ↑p = p
theorem
submodule.map_span
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(f : M →ₗ[R] M₂)
(s : set M) :
submodule.map f (submodule.span R s) = submodule.span R (⇑f '' s)
theorem
submodule.span_preimage_le
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(f : M →ₗ[R] M₂)
(s : set M₂) :
submodule.span R (⇑f ⁻¹' s) ≤ submodule.comap f (submodule.span R s)
theorem
submodule.span_induction
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule 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.
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}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
submodule.span R ∅ = ⊥
@[simp]
theorem
submodule.span_univ
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
theorem
submodule.span_union
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule 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}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{ι : Sort u_1}
(s : ι → set M) :
submodule.span R (⋃ (i : ι), s i) = ⨆ (i : ι), submodule.span R (s i)
@[simp]
theorem
submodule.coe_supr_of_directed
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{ι : Sort u_1}
[hι : nonempty ι]
(S : ι → submodule R M)
(H : directed has_le.le S) :
theorem
submodule.mem_sup_left
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{S T : submodule R M}
{x : M} :
theorem
submodule.mem_sup_right
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{S T : submodule R M}
{x : M} :
theorem
submodule.mem_supr_of_mem
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{ι : Sort u_1}
{b : M}
{p : ι → submodule R M}
(i : ι)
(h : b ∈ p i) :
b ∈ ⨆ (i : ι), p i
theorem
submodule.mem_Sup_of_mem
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{S : set (submodule R M)}
{s : submodule R M}
(hs : s ∈ S)
{x : M} :
@[simp]
theorem
submodule.mem_supr_of_directed
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{ι : Sort u_1}
[nonempty ι]
(S : ι → submodule R M)
(H : directed has_le.le S)
{x : M} :
theorem
submodule.mem_Sup_of_directed
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{s : set (submodule R M)}
{z : M}
(hs : s.nonempty)
(hdir : directed_on has_le.le s) :
theorem
submodule.mem_sup
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{p p' : submodule R M}
{x : M} :
theorem
submodule.mem_sup'
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{p p' : submodule R M}
{x : M} :
theorem
submodule.mem_span_singleton_self
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
(x : M) :
x ∈ submodule.span R {x}
theorem
submodule.nontrivial_span_singleton
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{x : M}
(h : x ≠ 0) :
nontrivial ↥(submodule.span R {x})
theorem
submodule.mem_span_singleton
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{x y : M} :
x ∈ submodule.span R {y} ↔ ∃ (a : R), a • y = x
theorem
submodule.le_span_singleton_iff
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{s : submodule R M}
{v₀ : M} :
@[simp]
theorem
submodule.span_zero_singleton
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
submodule.span R {0} = ⊥
theorem
submodule.span_singleton_eq_range
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
(y : M) :
↑(submodule.span R {y}) = set.range (λ (_x : R), _x • y)
theorem
submodule.span_singleton_smul_le
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule 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_insert
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule 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_eq_span
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule 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}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{s : set M} :
submodule.span R ↑(submodule.span R s) = submodule.span R s
theorem
submodule.span_eq_bot
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{s : set M} :
@[simp]
theorem
submodule.span_singleton_eq_bot
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{x : M} :
submodule.span R {x} = ⊥ ↔ x = 0
@[simp]
theorem
submodule.span_zero
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
submodule.span R 0 = ⊥
@[simp]
theorem
submodule.span_image
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
{s : set M}
(f : M →ₗ[R] M₂) :
submodule.span R (⇑f '' s) = submodule.map f (submodule.span R s)
theorem
submodule.supr_eq_span
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{ι : Sort w}
(p : ι → submodule R M) :
(⨆ (i : ι), p i) = submodule.span R (⋃ (i : ι), ↑(p i))
theorem
submodule.span_singleton_le_iff_mem
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
(m : M)
(p : submodule R M) :
submodule.span R {m} ≤ p ↔ m ∈ p
theorem
submodule.lt_add_iff_not_mem
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{I : submodule R M}
{a : M} :
I < I + submodule.span R {a} ↔ a ∉ I
theorem
submodule.mem_supr
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{ι : Sort w}
(p : ι → submodule R M)
{m : M} :
def
submodule.prod
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule 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}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(p : submodule R M)
(q : submodule R M₂) :
@[simp]
theorem
submodule.mem_prod
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
{p : submodule R M}
{q : submodule R M₂}
{x : M × M₂} :
theorem
submodule.span_prod_le
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule 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}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂] :
@[simp]
theorem
submodule.prod_bot
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂] :
theorem
submodule.prod_mono
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
{p p' : submodule R M}
{q q' : submodule R M₂} :
@[simp]
theorem
submodule.prod_inf_prod
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(p p' : submodule R M)
(q q' : submodule R M₂) :
@[simp]
theorem
submodule.prod_sup_prod
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(p p' : submodule R M)
(q q' : submodule R M₂) :
@[simp]
theorem
submodule.neg_coe
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[semimodule R M]
(p : submodule R M) :
@[simp]
theorem
submodule.map_neg
{R : Type u}
{M : Type v}
{M₂ : Type w}
[ring R]
[add_comm_group M]
[add_comm_group M₂]
[semimodule R M]
[semimodule 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}
{M : Type v}
[ring R]
[add_comm_group M]
[semimodule R M]
(s : set M) :
submodule.span R (-s) = submodule.span R s
theorem
submodule.mem_span_insert'
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[semimodule R M]
{x y : M}
{s : set M} :
x ∈ submodule.span R (insert y s) ↔ ∃ (a : R), x + a • y ∈ submodule.span R s
def
submodule.quotient_rel
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[semimodule R M]
(p : submodule R M) :
setoid M
The equivalence relation associated to a submodule p, defined by x ≈ y iff y - x ∈ p.
def
submodule.quotient
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[semimodule R M]
(p : submodule R M) :
Type v
The quotient of a module M by a submodule p ⊆ M.
Equations
def
submodule.quotient.mk
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[semimodule R M]
{p : submodule R M} :
M → p.quotient
Map associating to an element of M the corresponding element of M/p,
when p is a submodule of M.
Equations
@[simp]
theorem
submodule.quotient.mk_eq_mk
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[semimodule R M]
{p : submodule R M}
(x : M) :
@[simp]
theorem
submodule.quotient.mk'_eq_mk
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[semimodule R M]
{p : submodule R M}
(x : M) :
@[simp]
theorem
submodule.quotient.quot_mk_eq_mk
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[semimodule R M]
{p : submodule R M}
(x : M) :
quot.mk setoid.r x = submodule.quotient.mk x
theorem
submodule.quotient.eq
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[semimodule R M]
(p : submodule R M)
{x y : M} :
submodule.quotient.mk x = submodule.quotient.mk y ↔ x - y ∈ p
@[instance]
def
submodule.quotient.has_zero
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[semimodule R M]
(p : submodule R M) :
Equations
@[instance]
def
submodule.quotient.inhabited
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[semimodule R M]
(p : submodule R M) :
Equations
- submodule.quotient.inhabited p = {default := 0}
@[simp]
theorem
submodule.quotient.mk_zero
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[semimodule R M]
(p : submodule R M) :
@[simp]
theorem
submodule.quotient.mk_eq_zero
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[semimodule R M]
(p : submodule R M)
{x : M} :
submodule.quotient.mk x = 0 ↔ x ∈ p
@[instance]
def
submodule.quotient.has_add
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[semimodule R M]
(p : submodule R M) :
Equations
- submodule.quotient.has_add p = {add := λ (a b : p.quotient), quotient.lift_on₂' a b (λ (a b : M), submodule.quotient.mk (a + b)) _}
@[simp]
theorem
submodule.quotient.mk_add
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[semimodule R M]
(p : submodule R M)
{x y : M} :
@[instance]
def
submodule.quotient.has_neg
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[semimodule R M]
(p : submodule R M) :
Equations
- submodule.quotient.has_neg p = {neg := λ (a : p.quotient), quotient.lift_on' a (λ (a : M), submodule.quotient.mk (-a)) _}
@[simp]
theorem
submodule.quotient.mk_neg
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[semimodule R M]
(p : submodule R M)
{x : M} :
@[instance]
def
submodule.quotient.has_sub
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[semimodule R M]
(p : submodule R M) :
Equations
- submodule.quotient.has_sub p = {sub := λ (a b : p.quotient), quotient.lift_on₂' a b (λ (a b : M), submodule.quotient.mk (a - b)) _}
@[simp]
theorem
submodule.quotient.mk_sub
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[semimodule R M]
(p : submodule R M)
{x y : M} :
@[instance]
def
submodule.quotient.add_comm_group
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[semimodule R M]
(p : submodule R M) :
Equations
- submodule.quotient.add_comm_group p = {add := has_add.add (submodule.quotient.has_add p), add_assoc := _, zero := 0, zero_add := _, add_zero := _, neg := has_neg.neg (submodule.quotient.has_neg p), sub := has_sub.sub (submodule.quotient.has_sub p), sub_eq_add_neg := _, add_left_neg := _, add_comm := _}
@[instance]
def
submodule.quotient.has_scalar
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[semimodule R M]
(p : submodule R M) :
has_scalar R p.quotient
Equations
- submodule.quotient.has_scalar p = {smul := λ (a : R) (x : p.quotient), quotient.lift_on' x (λ (x : M), submodule.quotient.mk (a • x)) _}
@[simp]
theorem
submodule.quotient.mk_smul
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[semimodule R M]
(p : submodule R M)
{r : R}
{x : M} :
submodule.quotient.mk (r • x) = r • submodule.quotient.mk x
@[instance]
def
submodule.quotient.semimodule
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[semimodule R M]
(p : submodule R M) :
semimodule R p.quotient
Equations
- submodule.quotient.semimodule p = semimodule.of_core {to_has_scalar := {smul := has_scalar.smul (submodule.quotient.has_scalar p)}, smul_add := _, add_smul := _, mul_smul := _, one_smul := _}
theorem
submodule.quotient.mk_surjective
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[semimodule R M]
(p : submodule R M) :
theorem
submodule.quotient.nontrivial_of_lt_top
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[semimodule R M]
(p : submodule R M)
(h : p < ⊤) :
theorem
submodule.quot_hom_ext
{R : Type u}
{M : Type v}
{M₂ : Type w}
[ring R]
[add_comm_group M]
[add_comm_group M₂]
[semimodule R M]
[semimodule R M₂]
(p : submodule R M)
⦃f g : p.quotient →ₗ[R] M₂⦄
(h : ∀ (x : M), ⇑f (submodule.quotient.mk x) = ⇑g (submodule.quotient.mk x)) :
f = g
theorem
submodule.comap_smul
{K : Type u'}
{V : Type v'}
{V₂ : Type w'}
[field K]
[add_comm_group V]
[vector_space K V]
[add_comm_group V₂]
[vector_space 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'}
{V : Type v'}
{V₂ : Type w'}
[field K]
[add_comm_group V]
[vector_space K V]
[add_comm_group V₂]
[vector_space 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'}
{V : Type v'}
{V₂ : Type w'}
[field K]
[add_comm_group V]
[vector_space K V]
[add_comm_group V₂]
[vector_space 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'}
{V : Type v'}
{V₂ : Type w'}
[field K]
[add_comm_group V]
[vector_space K V]
[add_comm_group V₂]
[vector_space 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}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
{s : set M}
{f g : M →ₗ[R] 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}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
{s : set M}
{f g : M →ₗ[R] 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}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
{s : set M}
{f g : M →ₗ[R] M₂}
(hv : submodule.span R s = ⊤)
(h : set.eq_on ⇑f ⇑g s) :
f = g
If s generates the whole semimodule and linear maps f, g are equal on s, then they are
equal.
theorem
linear_map.ext_on_range
{R : Type u}
{M : Type v}
{M₂ : Type w}
{ι : Type x}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
{v : ι → M}
{f g : M →ₗ[R] 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 semimodule and linear maps f, g are equal at
each v i, then they are equal.
@[simp]
theorem
linear_map.finsupp_sum
{R : Type u}
{M : Type v}
{M₂ : Type w}
{ι : Type x}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
{γ : Type u_1}
[has_zero γ]
(f : M →ₗ[R] M₂)
{t : ι →₀ γ}
{g : ι → γ → M} :
theorem
linear_map.map_cod_restrict
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(p : submodule R M)
(f : M₂ →ₗ[R] 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}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(p : submodule R M)
(f : M₂ →ₗ[R] 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}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(f : M →ₗ[R] M₂) :
submodule R M₂
The range of a linear map f : M → M₂ is a submodule of M₂.
Equations
- f.range = submodule.map f ⊤
theorem
linear_map.range_coe
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(f : M →ₗ[R] M₂) :
@[simp]
theorem
linear_map.mem_range
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
{f : M →ₗ[R] M₂}
{x : M₂} :
theorem
linear_map.mem_range_self
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(f : M →ₗ[R] M₂)
(x : M) :
@[simp]
theorem
linear_map.range_id
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
theorem
linear_map.range_comp
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[semimodule R M]
[semimodule R M₂]
[semimodule R M₃]
(f : M →ₗ[R] M₂)
(g : M₂ →ₗ[R] M₃) :
(g.comp f).range = submodule.map g f.range
theorem
linear_map.range_comp_le_range
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[semimodule R M]
[semimodule R M₂]
[semimodule R M₃]
(f : M →ₗ[R] M₂)
(g : M₂ →ₗ[R] M₃) :
theorem
linear_map.range_eq_top
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
{f : M →ₗ[R] M₂} :
theorem
linear_map.range_le_iff_comap
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
{f : M →ₗ[R] M₂}
{p : submodule R M₂} :
theorem
linear_map.map_le_range
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
{f : M →ₗ[R] M₂}
{p : submodule R M} :
submodule.map f p ≤ f.range
theorem
linear_map.range_coprod
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[semimodule R M]
[semimodule R M₂]
[semimodule R M₃]
(f : M →ₗ[R] M₃)
(g : M₂ →ₗ[R] M₃) :
theorem
linear_map.is_compl_range_inl_inr
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂] :
is_compl (linear_map.inl R M M₂).range (linear_map.inr R M M₂).range
theorem
linear_map.sup_range_inl_inr
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂] :
(linear_map.inl R M M₂).range ⊔ (linear_map.inr R M M₂).range = ⊤
def
linear_map.range_restrict
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(f : M →ₗ[R] M₂) :
Restrict the codomain of a linear map f to f.range.
Equations
- f.range_restrict = linear_map.cod_restrict f.range f _
def
linear_map.to_span_singleton
(R : Type u)
(M : Type v)
[semiring R]
[add_comm_monoid M]
[semimodule 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)
(M : Type v)
[semiring R]
[add_comm_monoid M]
[semimodule 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)
(M : Type v)
[semiring R]
[add_comm_monoid M]
[semimodule R M]
(x : M) :
⇑(linear_map.to_span_singleton R M x) 1 = x
def
linear_map.ker
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(f : M →ₗ[R] 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.mem_ker
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
{f : M →ₗ[R] M₂}
{y : M} :
@[simp]
theorem
linear_map.ker_id
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
@[simp]
theorem
linear_map.map_coe_ker
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(f : M →ₗ[R] M₂)
(x : ↥(f.ker)) :
theorem
linear_map.comp_ker_subtype
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(f : M →ₗ[R] M₂) :
theorem
linear_map.ker_comp
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[semimodule R M]
[semimodule R M₂]
[semimodule R M₃]
(f : M →ₗ[R] M₂)
(g : M₂ →ₗ[R] M₃) :
(g.comp f).ker = submodule.comap f g.ker
theorem
linear_map.ker_le_ker_comp
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[semimodule R M]
[semimodule R M₂]
[semimodule R M₃]
(f : M →ₗ[R] M₂)
(g : M₂ →ₗ[R] M₃) :
theorem
linear_map.disjoint_ker
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
{f : M →ₗ[R] M₂}
{p : submodule R M} :
theorem
linear_map.disjoint_inl_inr
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂] :
disjoint (linear_map.inl R M M₂).range (linear_map.inr R M M₂).range
theorem
linear_map.ker_eq_bot'
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
{f : M →ₗ[R] M₂} :
theorem
linear_map.le_ker_iff_map
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
{f : M →ₗ[R] M₂}
{p : submodule R M} :
theorem
linear_map.ker_cod_restrict
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(p : submodule R M)
(f : M₂ →ₗ[R] 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}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(p : submodule R M)
(f : M₂ →ₗ[R] M)
(hf : ∀ (c : M₂), ⇑f c ∈ p) :
(linear_map.cod_restrict p f hf).range = submodule.comap p.subtype f.range
theorem
linear_map.ker_restrict
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{p : submodule R M}
{f : M →ₗ[R] M}
(hf : ∀ (x : M), x ∈ p → ⇑f x ∈ p) :
(f.restrict hf).ker = (f.dom_restrict p).ker
theorem
linear_map.map_comap_eq
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(f : M →ₗ[R] M₂)
(q : submodule R M₂) :
submodule.map f (submodule.comap f q) = f.