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.lean.
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. linear_equiv M M₂, the type of linear equivalences betweenMandM₂, is a structure that extendslinear_mapandequiv.- 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.
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} :
decomposing x : ι → R as a sum along the canonical basis
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) :
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.inverse
{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₂)
(g : M₂ → M) :
function.left_inverse g ⇑f → function.right_inverse g ⇑f → (M₂ →ₗ[R] M)
If a function g is a left and right inverse of a linear map f, then g is linear itself.
@[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) :
@[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)
Equations
- _ = _
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₂] :
λ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}
@[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]
def
linear_map.monoid
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
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₃] :
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₃] :
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₄] :
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_group 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_group M]
[add_comm_group M₂]
[semimodule R M]
[semimodule R M₂]
(f : M →ₗ[R] M₂)
(x : M) :
@[instance]
def
linear_map.add_comm_group
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_group 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, 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_group M]
[add_comm_group M₂]
[semimodule R M]
[semimodule R M₂]
(a : M) :
is_add_group_hom (λ (f : M →ₗ[R] M₂), ⇑f a)
Equations
@[simp]
theorem
linear_map.sub_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_group M]
[add_comm_group M₂]
[semimodule R M]
[semimodule R M₂]
(f g : M →ₗ[R] M₂)
(x : M) :
@[instance]
def
linear_map.has_scalar
{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₂] :
has_scalar R (M →ₗ[R] M₂)
@[simp]
theorem
linear_map.smul_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₂]
(f : M →ₗ[R] M₂)
(a : R)
(x : M) :
@[instance]
def
linear_map.semimodule
{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₂] :
semimodule R (M →ₗ[R] M₂)
Equations
- linear_map.semimodule = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := {smul := has_scalar.smul linear_map.has_scalar}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
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₃] :
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₃.
theorem
linear_map.smul_comp
{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) :
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) :
@[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 := add_comm_group.add linear_map.add_comm_group, add_assoc := _, zero := add_comm_group.zero linear_map.add_comm_group, zero_add := _, add_zero := _, neg := add_comm_group.neg linear_map.add_comm_group, add_left_neg := _, add_comm := _, mul := has_mul.mul linear_map.has_mul, mul_assoc := _, one := 1, 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} :
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]
def
submodule.has_bot
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
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} :
@[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]
def
submodule.has_top
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
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) :
@[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]
def
submodule.has_Inf
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
@[instance]
def
submodule.has_inf
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
@[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), has_Inf.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)), has_Inf.Inf {t : submodule R M | ∀ (t' : submodule R M), t' ∈ tt → t' ≤ t}, Inf := has_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_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.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₂] :
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} :
r ∈ p → ⇑f r ∈ submodule.map f p
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₂] :
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
The span of a set s ⊆ M is the smallest submodule of M that contains s.
Equations
- submodule.span R s = has_Inf.Inf {p : submodule R M | s ⊆ ↑p}
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} :
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} :
s ⊆ ↑p → 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.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} :
x ∈ submodule.span R s → (∀ (x : M), x ∈ s → p x) → p 0 → (∀ (x y : M), p x → p y → p (x + y)) → (∀ (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) :
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 : ι) :
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} :
x ∈ s → x ∈ has_Sup.Sup S
@[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} :
s.nonempty → directed_on has_le.le s → (z ∈ has_Sup.Sup s ↔ ∃ (y : submodule R M) (H : y ∈ s), z ∈ y)
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.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.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.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.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 (has_insert.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} :
x ∈ submodule.span R s → submodule.span R (has_insert.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.linear_eq_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₂}
(H : ∀ (x : M), x ∈ s → ⇑f x = ⇑g x)
{x : M} :
x ∈ submodule.span R s → ⇑f x = ⇑g x
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.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₂] :
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₂) :
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 (has_insert.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] :
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] :
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.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), 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) :
p < ⊤ → nontrivial p.quotient
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₂⦄ :
(∀ (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) :
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) :
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
@[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₂] :
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.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] :
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₂] :
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.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.range ⊓ q
theorem
linear_map.map_comap_eq_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₂}
{q : submodule R M₂} :
q ≤ f.range → submodule.map f (submodule.comap f q) = q
@[simp]
theorem
linear_map.ker_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₂] :
@[simp]
theorem
linear_map.range_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₂] :
theorem
linear_map.ker_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_bot_iff
{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_ker_iff
{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.comap_le_comap_iff
{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₂}
(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}
{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.range = ⊤ → function.injective (submodule.comap f)
theorem
linear_map.map_coprod_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₃)
(p : submodule R M)
(q : submodule R M₂) :
submodule.map (f.coprod g) (p.prod q) = submodule.map f p ⊔ submodule.map g q
theorem
linear_map.comap_prod_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₃)
(p : submodule R M₂)
(q : submodule R M₃) :
submodule.comap (f.prod g) (p.prod q) = submodule.comap f p ⊓ submodule.comap g q
theorem
linear_map.prod_eq_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₂]
(p : submodule R M)
(q : submodule R M₂) :
p.prod q = submodule.comap (linear_map.fst R M M₂) p ⊓ submodule.comap (linear_map.snd R M M₂) q
theorem
linear_map.prod_eq_sup_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₂]
(p : submodule R M)
(q : submodule R M₂) :
p.prod q = submodule.map (linear_map.inl R M M₂) p ⊔ submodule.map (linear_map.inr R M M₂) q
theorem
linear_map.span_inl_union_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₂]
{s : set M}
{t : set M₂} :
submodule.span R (⇑(linear_map.inl R M M₂) '' s ∪ ⇑(linear_map.inr R M M₂) '' t) = (submodule.span R s).prod (submodule.span R t)
@[simp]
theorem
linear_map.ker_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₃) :
theorem
linear_map.range_prod_le
{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.ker_eq_bot_of_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₂]
{f : M →ₗ[R] M₂} :
function.injective ⇑f → f.ker = ⊥
theorem
linear_map.comap_map_eq
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_group M]
[add_comm_group M₂]
[semimodule R M]
[semimodule R M₂]
(f : M →ₗ[R] M₂)
(p : submodule R M) :
submodule.comap f (submodule.map f p) = p ⊔ f.ker
theorem
linear_map.comap_map_eq_self
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_group M]
[add_comm_group M₂]
[semimodule R M]
[semimodule R M₂]
{f : M →ₗ[R] M₂}
{p : submodule R M} :
f.ker ≤ p → submodule.comap f (submodule.map f p) = p
theorem
linear_map.map_le_map_iff
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_group M]
[add_comm_group M₂]
[semimodule R M]
[semimodule R M₂]
(f : M →ₗ[R] 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}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_group M]
[add_comm_group M₂]
[semimodule R M]
[semimodule R M₂]
{f : M →ₗ[R] 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}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_group M]
[add_comm_group M₂]
[semimodule R M]
[semimodule R M₂]
{f : M →ₗ[R] M₂} :
f.ker = ⊥ → function.injective (submodule.map f)
theorem
linear_map.map_eq_top_iff
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_group M]
[add_comm_group M₂]
[semimodule R M]
[semimodule R M₂]
{f : M →ₗ[R] M₂}
(hf : f.range = ⊤)
{p : submodule R M} :
theorem
linear_map.sub_mem_ker_iff
{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₂]
{f : M →ₗ[R] M₂}
{x y : M} :
theorem
linear_map.disjoint_ker'
{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₂]
{f : M →ₗ[R] M₂}
{p : submodule R M} :
theorem
linear_map.inj_of_disjoint_ker
{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₂]
{f : M →ₗ[R] M₂}
{p : submodule R M}
{s : set M}
(h : s ⊆ ↑p)
(hd : disjoint p f.ker)
(x y : M) :
theorem
linear_map.ker_eq_bot
{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₂]
{f : M →ₗ[R] M₂} :
theorem
linear_map.range_prod_eq
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[ring R]
[add_comm_group 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₃} :
If the union of the kernels ker f and ker g spans the domain, then the range of
prod f g is equal to the product of range f and range g.
theorem
linear_map.ker_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₂)
(a : K) :
theorem
linear_map.ker_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₂)
(a : K) :
theorem
linear_map.range_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₂)
(a : K) :
theorem
linear_map.range_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₂)
(a : K) :
theorem
submodule.sup_eq_range
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
(p q : submodule R M) :
theorem
is_linear_map.is_linear_map_add
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule 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]
[semimodule R M] :
is_linear_map R (λ (x : M × M), x.fst - x.snd)
@[simp]
theorem
submodule.map_top
{R : Type u}
{M : Type v}
{M₂ : Type w}
{T : semiring R}
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(f : M →ₗ[R] M₂) :
submodule.map f ⊤ = f.range
@[simp]
theorem
submodule.comap_bot
{R : Type u}
{M : Type v}
{M₂ : Type w}
{T : semiring R}
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(f : M →ₗ[R] M₂) :
submodule.comap f ⊥ = f.ker
@[simp]
theorem
submodule.ker_subtype
{R : Type u}
{M : Type v}
{T : semiring R}
[add_comm_monoid M]
[semimodule R M]
(p : submodule R M) :
@[simp]
theorem
submodule.range_subtype
{R : Type u}
{M : Type v}
{T : semiring R}
[add_comm_monoid M]
[semimodule R M]
(p : submodule R M) :
theorem
submodule.map_subtype_le
{R : Type u}
{M : Type v}
{T : semiring R}
[add_comm_monoid M]
[semimodule 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}
{M : Type v}
{T : semiring R}
[add_comm_monoid M]
[semimodule 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}
{M : Type v}
{T : semiring R}
[add_comm_monoid M]
[semimodule R M]
{p p' : submodule R M} :
@[simp]
theorem
submodule.comap_subtype_self
{R : Type u}
{M : Type v}
{T : semiring R}
[add_comm_monoid M]
[semimodule R M]
(p : submodule R M) :
submodule.comap p.subtype p = ⊤
@[simp]
theorem
submodule.ker_of_le
{R : Type u}
{M : Type v}
{T : semiring R}
[add_comm_monoid M]
[semimodule R M]
(p p' : submodule R M)
(h : p ≤ p') :
(submodule.of_le h).ker = ⊥
theorem
submodule.range_of_le
{R : Type u}
{M : Type v}
{T : semiring R}
[add_comm_monoid M]
[semimodule R M]
(p q : submodule R M)
(h : p ≤ q) :
(submodule.of_le h).range = submodule.comap q.subtype p
@[simp]
theorem
submodule.map_inl
{R : Type u}
{M : Type v}
{M₂ : Type w}
{T : semiring R}
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(p : submodule R M) :
submodule.map (linear_map.inl R M M₂) p = p.prod ⊥
@[simp]
theorem
submodule.map_inr
{R : Type u}
{M : Type v}
{M₂ : Type w}
{T : semiring R}
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(q : submodule R M₂) :
submodule.map (linear_map.inr R M M₂) q = ⊥.prod q
@[simp]
theorem
submodule.comap_fst
{R : Type u}
{M : Type v}
{M₂ : Type w}
{T : semiring R}
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(p : submodule R M) :
submodule.comap (linear_map.fst R M M₂) p = p.prod ⊤
@[simp]
theorem
submodule.comap_snd
{R : Type u}
{M : Type v}
{M₂ : Type w}
{T : semiring R}
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(q : submodule R M₂) :
submodule.comap (linear_map.snd R M M₂) q = ⊤.prod q
@[simp]
theorem
submodule.prod_comap_inl
{R : Type u}
{M : Type v}
{M₂ : Type w}
{T : semiring R}
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(p : submodule R M)
(q : submodule R M₂) :
submodule.comap (linear_map.inl R M M₂) (p.prod q) = p
@[simp]
theorem
submodule.prod_comap_inr
{R : Type u}
{M : Type v}
{M₂ : Type w}
{T : semiring R}
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(p : submodule R M)
(q : submodule R M₂) :
submodule.comap (linear_map.inr R M M₂) (p.prod q) = q
@[simp]
theorem
submodule.prod_map_fst
{R : Type u}
{M : Type v}
{M₂ : Type w}
{T : semiring R}
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(p : submodule R M)
(q : submodule R M₂) :
submodule.map (linear_map.fst R M M₂) (p.prod q) = p
@[simp]
theorem
submodule.prod_map_snd
{R : Type u}
{M : Type v}
{M₂ : Type w}
{T : semiring R}
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂]
(p : submodule R M)
(q : submodule R M₂) :
submodule.map (linear_map.snd R M M₂) (p.prod q) = q
@[simp]
theorem
submodule.ker_inl
{R : Type u}
{M : Type v}
{M₂ : Type w}
{T : semiring R}
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂] :
(linear_map.inl R M M₂).ker = ⊥
@[simp]
theorem
submodule.ker_inr
{R : Type u}
{M : Type v}
{M₂ : Type w}
{T : semiring R}
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂] :
(linear_map.inr R M M₂).ker = ⊥
@[simp]
theorem
submodule.range_fst
{R : Type u}
{M : Type v}
{M₂ : Type w}
{T : semiring R}
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂] :
(linear_map.fst R M M₂).range = ⊤
@[simp]
theorem
submodule.range_snd
{R : Type u}
{M : Type v}
{M₂ : Type w}
{T : semiring R}
[add_comm_monoid M]
[add_comm_monoid M₂]
[semimodule R M]
[semimodule R M₂] :
(linear_map.snd R M M₂).range = ⊤
theorem
submodule.disjoint_iff_comap_eq_bot
{R : Type u}
{M : Type v}
{T : ring R}
[add_comm_group M]
[semimodule R M]
{p q : submodule R M} :
def
submodule.map_subtype.rel_iso
{R : Type u}
{M : Type v}
{T : ring R}
[add_comm_group M]
[semimodule 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}
{M : Type v}
{T : ring R}
[add_comm_group M]
[semimodule 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}
{M : Type v}
{T : ring R}
[add_comm_group M]
[semimodule R M]
(p : submodule R M)
(p' : submodule R ↥p) :
⇑(submodule.map_subtype.order_embedding p) p' = submodule.map p.subtype p'
def
submodule.mkq
{R : Type u}
{M : Type v}
{T : ring R}
[add_comm_group M]
[semimodule R M]
(p : submodule R M) :
The map from a module M to the quotient of M by a submodule p as a linear map.
@[simp]
theorem
submodule.mkq_apply
{R : Type u}
{M : Type v}
{T : ring R}
[add_comm_group M]
[semimodule R M]
(p : submodule R M)
(x : M) :
⇑(p.mkq) x = submodule.quotient.mk x
def
submodule.liftq
{R : Type u}
{M : Type v}
{M₂ : Type w}
{T : ring R}
[add_comm_group M]
[add_comm_group M₂]
[semimodule R M]
[semimodule R M₂]
(p : submodule R M)
(f : M →ₗ[R] M₂) :
The map from the quotient of M by a submodule p to M₂ induced by a linear map f : M → M₂
vanishing on p, as a linear map.
@[simp]
theorem
submodule.liftq_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
{T : ring R}
[add_comm_group M]
[add_comm_group M₂]
[semimodule R M]
[semimodule R M₂]
(p : submodule R M)
(f : M →ₗ[R] M₂)
{h : p ≤ f.ker}
(x : M) :
⇑(p.liftq f h) (submodule.quotient.mk x) = ⇑f x
@[simp]
theorem
submodule.liftq_mkq
{R : Type u}
{M : Type v}
{M₂ : Type w}
{T : ring R}
[add_comm_group M]
[add_comm_group M₂]
[semimodule R M]
[semimodule R M₂]
(p : submodule R M)
(f : M →ₗ[R] M₂)
(h : p ≤ f.ker) :
@[simp]
theorem
submodule.range_mkq
{R : Type u}
{M : Type v}
{T : ring R}
[add_comm_group M]
[semimodule R M]
(p : submodule R M) :
@[simp]
theorem
submodule.ker_mkq
{R : Type u}
{M : Type v}
{T : ring R}
[add_comm_group M]
[semimodule R M]
(p : submodule R M) :
theorem
submodule.le_comap_mkq
{R : Type u}
{M : Type v}
{T : ring R}
[add_comm_group M]
[semimodule R M]
(p : submodule R M)
(p' : submodule R p.quotient) :
p ≤ submodule.comap p.mkq p'
@[simp]
theorem
submodule.mkq_map_self
{R : Type u}
{M : Type v}
{T : ring R}
[add_comm_group M]
[semimodule R M]
(p : submodule R M) :
submodule.map p.mkq p = ⊥
@[simp]
theorem
submodule.comap_map_mkq
{R : Type u}
{M : Type v}
{T : ring R}
[add_comm_group M]
[semimodule R M]
(p p' : submodule R M) :
submodule.comap p.mkq (submodule.map p.mkq p') = p ⊔ p'
@[simp]
theorem
submodule.map_mkq_eq_top
{R : Type u}
{M : Type v}
{T : ring R}
[add_comm_group M]
[semimodule R M]
(p p' : submodule R M) :
def
submodule.mapq
{R : Type u}
{M : Type v}
{M₂ : Type w}
{T : ring R}
[add_comm_group M]
[add_comm_group M₂]
[semimodule R M]
[semimodule R M₂]
(p : submodule R M)
(q : submodule R M₂)
(f : M →ₗ[R] M₂) :
The map from the quotient of M by submodule p to the quotient of M₂ by submodule q along
f : M → M₂ is linear.
@[simp]
theorem
submodule.mapq_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
{T : ring R}
[add_comm_group M]
[add_comm_group M₂]
[semimodule R M]
[semimodule R M₂]
(p : submodule R M)
(q : submodule R M₂)
(f : M →ₗ[R] M₂)
{h : p ≤ submodule.comap f q}
(x : M) :
⇑(p.mapq q f h) (submodule.quotient.mk x) = submodule.quotient.mk (⇑f x)
theorem
submodule.mapq_mkq
{R : Type u}
{M : Type v}
{M₂ : Type w}
{T : ring R}
[add_comm_group M]
[add_comm_group M₂]
[semimodule R M]
[semimodule R M₂]
(p : submodule R M)
(q : submodule R M₂)
(f : M →ₗ[R] M₂)
{h : p ≤ submodule.comap f q} :
theorem
submodule.comap_liftq
{R : Type u}
{M : Type v}
{M₂ : Type w}
{T : ring R}
[add_comm_group M]
[add_comm_group M₂]
[semimodule R M]
[semimodule R M₂]
(p : submodule R M)
(q : submodule R M₂)
(f : M →ₗ[R] M₂)
(h : p ≤ f.ker) :
submodule.comap (p.liftq f h) q = submodule.map p.mkq (submodule.comap f q)
theorem
submodule.map_liftq
{R : Type u}
{M : Type v}
{M₂ : Type w}
{T : ring R}
[add_comm_group M]
[add_comm_group M₂]
[semimodule R M]
[semimodule R M₂]
(p : submodule R M)
(f : M →ₗ[R] M₂)
(h : p ≤ f.ker)
(q : submodule R p.quotient) :
submodule.map (p.liftq f h) q = submodule.map f (submodule.comap p.mkq q)
theorem
submodule.ker_liftq
{R : Type u}
{M : Type v}
{M₂ : Type w}
{T : ring R}
[add_comm_group M]
[add_comm_group M₂]
[semimodule R M]
[semimodule R M₂]
(p : submodule R M)
(f : M →ₗ[R] M₂)
(h : p ≤ f.ker) :
theorem
submodule.range_liftq
{R : Type u}
{M : Type v}
{M₂ : Type w}
{T : ring R}
[add_comm_group M]
[add_comm_group M₂]
[semimodule R M]
[semimodule R M₂]
(p : submodule R M)
(f : M →ₗ[R] M₂)
(h : p ≤ f.ker) :
theorem
submodule.ker_liftq_eq_bot
{R : Type u}
{M : Type v}
{M₂ : Type w}
{T : ring R}
[add_comm_group M]
[add_comm_group M₂]
[semimodule R M]
[semimodule R M₂]
(p : submodule R M)
(f : M →ₗ[R] M₂)
(h : p ≤ f.ker) :
def
submodule.comap_mkq.rel_iso
{R : Type u}
{M : Type v}
{T : ring R}
[add_comm_group M]
[semimodule R M]
(p : submodule R M) :
The correspondence theorem for modules: there is an order isomorphism between submodules of the
quotient of M by p, and submodules of M larger than p.
Equations
- submodule.comap_mkq.rel_iso p = {to_equiv := {to_fun := λ (p' : submodule R p.quotient), ⟨submodule.comap p.mkq p', _⟩, inv_fun := λ (q : {p' // p ≤ p'}), submodule.map p.mkq ↑q, left_inv := _, right_inv := _}, map_rel_iff' := _}
def
submodule.comap_mkq.order_embedding
{R : Type u}
{M : Type v}
{T : ring R}
[add_comm_group M]
[semimodule R M]
(p : submodule R M) :
The ordering on submodules of the quotient of M by p embeds into the ordering on submodules
of M.
Equations
- submodule.comap_mkq.order_embedding p = (rel_iso.to_rel_embedding (submodule.comap_mkq.rel_iso p)).trans (subtype.rel_embedding has_le.le (λ (p' : submodule R M), p ≤ p'))
@[simp]
theorem
submodule.comap_mkq_embedding_eq
{R : Type u}
{M : Type v}
{T : ring R}
[add_comm_group M]
[semimodule R M]
(p : submodule R M)
(p' : submodule R p.quotient) :
⇑(submodule.comap_mkq.order_embedding p) p' = submodule.comap p.mkq p'
theorem
linear_map.range_mkq_comp
{R : Type u}
{M : Type v}
{M₂ : Type w}
[ring R]
[add_comm_group M]
[add_comm_group M₂]
[module R M]
[module R M₂]
(f : M →ₗ[R] M₂) :
@[simp]
theorem
linear_map.range_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₂) :
Linear equivalences
@[nolint]
def
linear_equiv.to_linear_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₂] :
@[nolint]
structure
linear_equiv
(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 (max v w)
- to_fun : M → M₂
- map_add' : ∀ (x y : M), c.to_fun (x + y) = c.to_fun x + c.to_fun y
- map_smul' : ∀ (c_1 : R) (x : M), c.to_fun (c_1 • x) = c_1 • c.to_fun x
- inv_fun : M₂ → M
- left_inv : function.left_inverse c.inv_fun c.to_fun
- right_inv : function.right_inverse c.inv_fun c.to_fun
A linear equivalence is an invertible linear map.
@[nolint]
def
linear_equiv.to_equiv
{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_equiv.has_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₂] :
Equations
- linear_equiv.has_coe = {coe := linear_equiv.to_linear_map _inst_7}
@[instance]
def
linear_equiv.has_coe_to_fun
{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₂] :
has_coe_to_fun (M ≃ₗ[R] M₂)
@[simp]
theorem
linear_equiv.mk_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₂]
{to_fun : M → M₂}
{inv_fun : M₂ → M}
{map_add : ∀ (x y : M), to_fun (x + y) = to_fun x + to_fun y}
{map_smul : ∀ (c : R) (x : M), to_fun (c • x) = c • to_fun x}
{left_inv : function.left_inverse inv_fun to_fun}
{right_inv : function.right_inverse inv_fun to_fun}
{a : M} :
theorem
linear_equiv.to_equiv_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₂] :
@[simp]
theorem
linear_equiv.coe_coe
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
{semimodule_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
(e : M ≃ₗ[R] M₂) :
@[simp]
theorem
linear_equiv.coe_to_equiv
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
{semimodule_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
(e : M ≃ₗ[R] M₂) :
@[simp]
theorem
linear_equiv.to_fun_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
{semimodule_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
(e : M ≃ₗ[R] M₂)
{m : M} :
@[ext]
theorem
linear_equiv.ext
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
{semimodule_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
{e e' : M ≃ₗ[R] M₂} :
theorem
linear_equiv.eq_of_linear_map_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 f' : M ≃ₗ[R] M₂} :
def
linear_equiv.refl
(R : Type u)
(M : Type v)
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
The identity map is a linear equivalence.
Equations
- linear_equiv.refl R M = {to_fun := linear_map.id.to_fun, map_add' := _, map_smul' := _, inv_fun := (equiv.refl M).inv_fun, left_inv := _, right_inv := _}
@[simp]
theorem
linear_equiv.refl_apply
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
(x : M) :
⇑(linear_equiv.refl R M) x = x
def
linear_equiv.symm
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
{semimodule_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂} :
Linear equivalences are symmetric.
@[simp]
theorem
linear_equiv.inv_fun_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
{semimodule_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
(e : M ≃ₗ[R] M₂)
{m : M₂} :
def
linear_equiv.trans
{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_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
{semimodule_M₃ : semimodule R M₃} :
Linear equivalences are transitive.
def
linear_equiv.to_add_equiv
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
{semimodule_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂} :
A linear equivalence is an additive equivalence.
@[simp]
theorem
linear_equiv.coe_to_add_equiv
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
{semimodule_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
(e : M ≃ₗ[R] M₂) :
⇑(e.to_add_equiv) = ⇑e
@[simp]
theorem
linear_equiv.trans_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_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
{semimodule_M₃ : semimodule R M₃}
(e₁ : M ≃ₗ[R] M₂)
(e₂ : M₂ ≃ₗ[R] M₃)
(c : M) :
@[simp]
theorem
linear_equiv.apply_symm_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
{semimodule_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
(e : M ≃ₗ[R] M₂)
(c : M₂) :
@[simp]
theorem
linear_equiv.symm_apply_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
{semimodule_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
(e : M ≃ₗ[R] M₂)
(b : M) :
@[simp]
theorem
linear_equiv.symm_trans_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_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
{semimodule_M₃ : semimodule R M₃}
(e₁ : M ≃ₗ[R] M₂)
(e₂ : M₂ ≃ₗ[R] M₃)
(c : M₃) :
@[simp]
theorem
linear_equiv.trans_refl
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
{semimodule_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
(e : M ≃ₗ[R] M₂) :
e.trans (linear_equiv.refl R M₂) = e
@[simp]
theorem
linear_equiv.refl_trans
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
{semimodule_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
(e : M ≃ₗ[R] M₂) :
(linear_equiv.refl R M).trans e = e
theorem
linear_equiv.symm_apply_eq
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
{semimodule_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
(e : M ≃ₗ[R] M₂)
{x : M₂}
{y : M} :
theorem
linear_equiv.eq_symm_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
{semimodule_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
(e : M ≃ₗ[R] M₂)
{x : M₂}
{y : M} :
@[simp]
theorem
linear_equiv.trans_symm
{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.trans f.symm = linear_equiv.refl R M
@[simp]
theorem
linear_equiv.symm_trans
{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.symm.trans f = linear_equiv.refl R M₂
@[simp]
theorem
linear_equiv.refl_to_linear_map
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
↑(linear_equiv.refl R M) = linear_map.id
@[simp]
theorem
linear_equiv.comp_coe
{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₂)
(f' : M₂ ≃ₗ[R] M₃) :
@[simp]
theorem
linear_equiv.map_add
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
{semimodule_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
(e : M ≃ₗ[R] M₂)
(a b : M) :
@[simp]
theorem
linear_equiv.map_zero
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
{semimodule_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
(e : M ≃ₗ[R] M₂) :
@[simp]
theorem
linear_equiv.map_smul
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
{semimodule_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
(e : M ≃ₗ[R] M₂)
(c : R)
(x : M) :
@[simp]
theorem
linear_equiv.map_eq_zero_iff
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
{semimodule_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
(e : M ≃ₗ[R] M₂)
{x : M} :
theorem
linear_equiv.map_ne_zero_iff
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
{semimodule_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
(e : M ≃ₗ[R] M₂)
{x : M} :
@[simp]
theorem
linear_equiv.symm_symm
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
{semimodule_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
(e : M ≃ₗ[R] M₂) :
theorem
linear_equiv.bijective
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
{semimodule_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
(e : M ≃ₗ[R] M₂) :
theorem
linear_equiv.injective
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
{semimodule_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
(e : M ≃ₗ[R] M₂) :
theorem
linear_equiv.surjective
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
{semimodule_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
(e : M ≃ₗ[R] M₂) :
theorem
linear_equiv.image_eq_preimage
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
{semimodule_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
(e : M ≃ₗ[R] M₂)
(s : set M) :
theorem
linear_equiv.map_eq_comap
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
{semimodule_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
(e : M ≃ₗ[R] M₂)
{p : submodule R M} :
submodule.map ↑e p = submodule.comap ↑(e.symm) p
def
linear_equiv.of_submodule
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
{semimodule_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
(e : M ≃ₗ[R] M₂)
(p : submodule R M) :
A linear equivalence of two modules restricts to a linear equivalence from any submodule of the domain onto the image of the submodule.
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}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
{semimodule_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
(e : M ≃ₗ[R] M₂)
(p : submodule R M)
(x : ↥p) :
@[simp]
theorem
linear_equiv.of_submodule_symm_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
{semimodule_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
(e : M ≃ₗ[R] M₂)
(p : submodule R M)
(x : ↥(submodule.map ↑e p)) :
def
linear_equiv.prod
{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_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
{semimodule_M₃ : semimodule R M₃}
{semimodule_M₄ : semimodule R M₄} :
Product of linear equivalences; the maps come from equiv.prod_congr.
theorem
linear_equiv.prod_symm
{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_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
{semimodule_M₃ : semimodule R M₃}
{semimodule_M₄ : semimodule R M₄}
(e₁ : M ≃ₗ[R] M₂)
(e₂ : M₃ ≃ₗ[R] M₄) :
@[simp]
theorem
linear_equiv.prod_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_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
{semimodule_M₃ : semimodule R M₃}
{semimodule_M₄ : semimodule R M₄}
(e₁ : M ≃ₗ[R] M₂)
(e₂ : M₃ ≃ₗ[R] M₄)
(p : M × M₃) :
@[simp]
theorem
linear_equiv.coe_prod
{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_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
{semimodule_M₃ : semimodule R M₃}
{semimodule_M₄ : semimodule R M₄}
(e₁ : M ≃ₗ[R] M₂)
(e₂ : M₃ ≃ₗ[R] M₄) :
Linear equivalence between a curried and uncurried function.
Differs from tensor_product.curry.
Equations
- linear_equiv.uncurry R V V₂ = {to_fun := (equiv.arrow_arrow_equiv_prod_arrow V V₂ R).to_fun, map_add' := _, map_smul' := _, inv_fun := (equiv.arrow_arrow_equiv_prod_arrow V V₂ R).inv_fun, left_inv := _, right_inv := _}
@[simp]
theorem
linear_equiv.coe_uncurry
(R : Type u)
(V : Type v')
(V₂ : Type w')
[semiring R] :
⇑(linear_equiv.uncurry R V V₂) = function.uncurry
@[simp]
theorem
linear_equiv.coe_uncurry_symm
(R : Type u)
(V : Type v')
(V₂ : Type w')
[semiring R] :
⇑((linear_equiv.uncurry R V V₂).symm) = function.curry
def
linear_equiv.of_eq
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
{semimodule_M : semimodule R M}
(p q : submodule R M) :
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}
{M : Type v}
[semiring R]
[add_comm_monoid M]
{semimodule_M : semimodule 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}
{M : Type v}
[semiring R]
[add_comm_monoid M]
{semimodule_M : semimodule 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}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
{semimodule_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
(e : M ≃ₗ[R] M₂)
(p : submodule R M)
(q : submodule R M₂) :
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}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
{semimodule_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
(e : M ≃ₗ[R] 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}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
{semimodule_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
(e : M ≃ₗ[R] M₂)
{p : submodule R M}
{q : submodule R M₂}
(h : submodule.map ↑e p = q)
(x : ↥q) :
def
linear_equiv.of_top
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
{semimodule_M : semimodule R M}
(p : submodule R M) :
The top submodule of M is linearly equivalent to M.
@[simp]
theorem
linear_equiv.of_top_apply
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
{semimodule_M : semimodule 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}
{M : Type v}
[semiring R]
[add_comm_monoid M]
{semimodule_M : semimodule 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}
{M : Type v}
[semiring R]
[add_comm_monoid M]
{semimodule_M : semimodule 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}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
{semimodule_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
(f : M →ₗ[R] M₂)
(g : M₂ →ₗ[R] M) :
f.comp g = linear_map.id → g.comp f = linear_map.id → (M ≃ₗ[R] M₂)
If a linear map has an inverse, it is a linear equivalence.
@[simp]
theorem
linear_equiv.of_linear_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
{semimodule_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
(f : M →ₗ[R] M₂)
(g : M₂ →ₗ[R] 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}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
{semimodule_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
(f : M →ₗ[R] M₂)
(g : M₂ →ₗ[R] 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
@[simp]
theorem
linear_equiv.range
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
{semimodule_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
(e : M ≃ₗ[R] M₂) :
theorem
linear_equiv.eq_bot_of_equiv
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
{semimodule_M : semimodule R M}
(p : submodule R M)
[semimodule R M₂] :
@[simp]
theorem
linear_equiv.ker
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
{semimodule_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
(e : M ≃ₗ[R] M₂) :
@[simp]
theorem
linear_equiv.map_neg
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_group M]
[add_comm_group M₂]
{semimodule_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
(e : M ≃ₗ[R] M₂)
(a : M) :
@[simp]
theorem
linear_equiv.map_sub
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_group M]
[add_comm_group M₂]
{semimodule_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
(e : M ≃ₗ[R] M₂)
(a b : M) :
def
linear_equiv.skew_prod
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
{M₄ : Type z}
[semiring R]
[add_comm_group M]
[add_comm_group M₂]
[add_comm_group M₃]
[add_comm_group M₄]
{semimodule_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
{semimodule_M₃ : semimodule R M₃}
{semimodule_M₄ : semimodule R M₄} :
Equivalence given by a block lower diagonal matrix. e₁ and e₂ are diagonal square blocks,
and f is a rectangular block below the diagonal.
Equations
- e₁.skew_prod e₂ f = {to_fun := ((↑e₁.comp (linear_map.fst R M M₃)).prod (↑e₂.comp (linear_map.snd R M M₃) + f.comp (linear_map.fst R M M₃))).to_fun, map_add' := _, map_smul' := _, inv_fun := λ (p : M₂ × M₄), (⇑(e₁.symm) p.fst, ⇑(e₂.symm) (p.snd - ⇑f (⇑(e₁.symm) p.fst))), left_inv := _, right_inv := _}
@[simp]
theorem
linear_equiv.skew_prod_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
{M₄ : Type z}
[semiring R]
[add_comm_group M]
[add_comm_group M₂]
[add_comm_group M₃]
[add_comm_group M₄]
{semimodule_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
{semimodule_M₃ : semimodule R M₃}
{semimodule_M₄ : semimodule R M₄}
(e₁ : M ≃ₗ[R] M₂)
(e₂ : M₃ ≃ₗ[R] M₄)
(f : M →ₗ[R] M₄)
(x : M × M₃) :
@[simp]
theorem
linear_equiv.skew_prod_symm_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
{M₄ : Type z}
[semiring R]
[add_comm_group M]
[add_comm_group M₂]
[add_comm_group M₃]
[add_comm_group M₄]
{semimodule_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
{semimodule_M₃ : semimodule R M₃}
{semimodule_M₄ : semimodule R M₄}
(e₁ : M ≃ₗ[R] M₂)
(e₂ : M₃ ≃ₗ[R] M₄)
(f : M →ₗ[R] M₄)
(x : M₂ × M₄) :
def
linear_equiv.of_injective
{R : Type u}
{M : Type v}
{M₂ : Type w}
[ring R]
[add_comm_group M]
[add_comm_group M₂]
{semimodule_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
(f : M →ₗ[R] M₂) :
An injective linear map f : M →ₗ[R] M₂ defines a linear equivalence
between M and f.range.
Equations
- linear_equiv.of_injective f h = {to_fun := ((equiv.set.range ⇑f _).trans (equiv.set.of_eq _)).to_fun, map_add' := _, map_smul' := _, inv_fun := ((equiv.set.range ⇑f _).trans (equiv.set.of_eq _)).inv_fun, left_inv := _, right_inv := _}
@[simp]
theorem
linear_equiv.of_injective_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
[ring R]
[add_comm_group M]
[add_comm_group M₂]
{semimodule_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
(f : M →ₗ[R] M₂)
{h : f.ker = ⊥}
(x : M) :
↑(⇑(linear_equiv.of_injective f h) x) = ⇑f x
def
linear_equiv.of_bijective
{R : Type u}
{M : Type v}
{M₂ : Type w}
[ring R]
[add_comm_group M]
[add_comm_group M₂]
{semimodule_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
(f : M →ₗ[R] M₂) :
A bijective linear map is a linear equivalence. Here, bijectivity is described by saying that
the kernel of f is {0} and the range is the universal set.
Equations
- linear_equiv.of_bijective f hf₁ hf₂ = (linear_equiv.of_injective f hf₁).trans (linear_equiv.of_top f.range hf₂)
@[simp]
theorem
linear_equiv.of_bijective_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
[ring R]
[add_comm_group M]
[add_comm_group M₂]
{semimodule_M : semimodule R M}
{semimodule_M₂ : semimodule R M₂}
(f : M →ₗ[R] M₂)
{hf₁ : f.ker = ⊥}
{hf₂ : f.range = ⊤}
(x : M) :
⇑(linear_equiv.of_bijective f hf₁ hf₂) x = ⇑f x
def
linear_equiv.smul_of_unit
{R : Type u}
{M : Type v}
[comm_ring R]
[add_comm_group M]
[semimodule R M] :
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_ring R]
[add_comm_group M₁]
[add_comm_group M₂]
[add_comm_group M₂₁]
[add_comm_group M₂₂]
[module R M₁]
[module R M₂]
[module R M₂₁]
[module 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_ring R]
[add_comm_group M₁]
[add_comm_group M₂]
[add_comm_group M₂₁]
[add_comm_group 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}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[comm_ring R]
[add_comm_group M]
[add_comm_group M₂]
[add_comm_group M₃]
[semimodule R M]
[semimodule R M₂]
[semimodule R M₃]
{N : Type u_1}
{N₂ : Type u_2}
{N₃ : Type u_3}
[add_comm_group N]
[add_comm_group N₂]
[add_comm_group 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}
[comm_ring R]
{M₁ : Type u_1}
{M₂ : Type u_2}
{M₃ : Type u_3}
{N₁ : Type u_4}
{N₂ : Type u_5}
{N₃ : Type u_6}
[add_comm_group M₁]
[module R M₁]
[add_comm_group M₂]
[module R M₂]
[add_comm_group M₃]
[module R M₃]
[add_comm_group N₁]
[module R N₁]
[add_comm_group N₂]
[module R N₂]
[add_comm_group 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}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[comm_ring R]
[add_comm_group M]
[add_comm_group M₂]
[add_comm_group M₃]
[semimodule R M]
[semimodule R M₂]
[semimodule 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}
{M : Type v}
{M₂ : Type w}
[comm_ring R]
[add_comm_group M]
[add_comm_group M₂]
[semimodule R M]
[semimodule R M₂] :
(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}
{M : Type v}
{M₂ : Type w}
[comm_ring R]
[add_comm_group M]
[add_comm_group M₂]
[semimodule R M]
[semimodule R M₂]
(e : M ≃ₗ[R] M₂)
(f : module.End R M) :
theorem
linear_equiv.symm_conj_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₂]
(e : M ≃ₗ[R] M₂)
(f : module.End R M₂) :
theorem
linear_equiv.conj_comp
{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₂]
(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}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[comm_ring R]
[add_comm_group M]
[add_comm_group M₂]
[add_comm_group M₃]
[semimodule R M]
[semimodule R M₂]
[semimodule R M₃]
(e₁ : M ≃ₗ[R] M₂)
(e₂ : M₂ ≃ₗ[R] M₃) :
@[simp]
theorem
linear_equiv.conj_id
{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₂]
(e : M ≃ₗ[R] M₂) :
def
linear_equiv.smul_of_ne_zero
(K : Type u')
(M : Type v)
[field K]
[add_comm_group M]
[module K M]
(a : K) :
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)
def
linear_equiv.to_span_nonzero_singleton
(K : Type u')
(M : Type v)
[field K]
[add_comm_group M]
[module K M]
(x : M) :
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')
(M : Type v)
[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, _⟩
def
linear_equiv.coord
(K : Type u')
(M : Type v)
[field K]
[add_comm_group M]
[module K M]
(x : M) :
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')
(M : Type v)
[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.comap_subtype_equiv_of_le
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{p q : submodule R M} :
If s ≤ t, then we can view s as a submodule of t by taking the comap
of t.subtype.
def
submodule.quot_equiv_of_eq_bot
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M) :
If p = ⊥, then M / p ≃ₗ[R] M.
Equations
- p.quot_equiv_of_eq_bot hp = linear_equiv.of_linear (p.liftq linear_map.id _) p.mkq _ _
@[simp]
theorem
submodule.quot_equiv_of_eq_bot_apply_mk
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M)
(hp : p = ⊥)
(x : M) :
⇑(p.quot_equiv_of_eq_bot hp) (submodule.quotient.mk x) = x
@[simp]
theorem
submodule.quot_equiv_of_eq_bot_symm_apply
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M)
(hp : p = ⊥)
(x : M) :
⇑((p.quot_equiv_of_eq_bot hp).symm) x = submodule.quotient.mk x
@[simp]
theorem
submodule.coe_quot_equiv_of_eq_bot_symm
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M)
(hp : p = ⊥) :
↑((p.quot_equiv_of_eq_bot hp).symm) = p.mkq
def
submodule.quot_equiv_of_eq
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[module R M]
(p q : submodule R M) :
Quotienting by equal submodules gives linearly equivalent quotients.
Equations
- p.quot_equiv_of_eq q h = {to_fun := (quotient.congr (equiv.refl M) _).to_fun, map_add' := _, map_smul' := _, inv_fun := (quotient.congr (equiv.refl M) _).inv_fun, left_inv := _, right_inv := _}
@[simp]
theorem
submodule.mem_map_equiv
{R : Type u}
{M : Type v}
{M₂ : Type w}
[comm_ring R]
[add_comm_group M]
[add_comm_group M₂]
[module R M]
[module R M₂]
(p : submodule R M)
{e : M ≃ₗ[R] M₂}
{x : M₂} :
theorem
submodule.comap_le_comap_smul
{R : Type u}
{M : Type v}
{M₂ : Type w}
[comm_ring R]
[add_comm_group M]
[add_comm_group M₂]
[module R M]
[module R M₂]
(q : submodule R M₂)
(f : M →ₗ[R] M₂)
(c : R) :
submodule.comap f q ≤ submodule.comap (c • f) q
theorem
submodule.inf_comap_le_comap_add
{R : Type u}
{M : Type v}
{M₂ : Type w}
[comm_ring R]
[add_comm_group M]
[add_comm_group M₂]
[module R M]
[module R M₂]
(q : submodule R M₂)
(f₁ f₂ : M →ₗ[R] M₂) :
submodule.comap f₁ q ⊓ submodule.comap f₂ q ≤ submodule.comap (f₁ + f₂) q
def
submodule.compatible_maps
{R : Type u}
{M : Type v}
{M₂ : Type w}
[comm_ring R]
[add_comm_group M]
[add_comm_group M₂]
[module R M]
[module R M₂] :
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
submodule.mapq_linear
{R : Type u}
{M : Type v}
{M₂ : Type w}
[comm_ring R]
[add_comm_group M]
[add_comm_group M₂]
[module R M]
[module R M₂]
(p : submodule R M)
(q : submodule R M₂) :
Given modules M, M₂ over a commutative ring, together with submodules p ⊆ M, q ⊆ M₂, the
natural map $\{f ∈ Hom(M, M₂) | f(p) ⊆ q \} \to Hom(M/p, M₂/q)$ is linear.
Equations
- p.mapq_linear q = {to_fun := λ (f : ↥(p.compatible_maps q)), p.mapq q f.val _, map_add' := _, map_smul' := _}
def
equiv.to_linear_equiv
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
[add_comm_monoid M₂]
[semimodule R M₂]
(e : M ≃ M₂) :
is_linear_map R ⇑e → (M ≃ₗ[R] M₂)
An equivalence whose underlying function is linear is a linear equivalence.
def
linear_map.quot_ker_equiv_range
{R : Type u}
{M : Type v}
{M₂ : Type w}
[ring R]
[add_comm_group M]
[add_comm_group M₂]
[module R M]
[module R M₂]
(f : M →ₗ[R] M₂) :
The first isomorphism law for modules. The quotient of M by the kernel of f is linearly
equivalent to the range of f.
Equations
- f.quot_ker_equiv_range = (linear_equiv.of_injective (f.ker.liftq f _) _).trans (linear_equiv.of_eq (f.ker.liftq f _).range f.range _)
@[simp]
theorem
linear_map.quot_ker_equiv_range_apply_mk
{R : Type u}
{M : Type v}
{M₂ : Type w}
[ring R]
[add_comm_group M]
[add_comm_group M₂]
[module R M]
[module R M₂]
(f : M →ₗ[R] M₂)
(x : M) :
↑(⇑(f.quot_ker_equiv_range) (submodule.quotient.mk x)) = ⇑f x
def
linear_map.quotient_inf_to_sup_quotient
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[module R M]
(p p' : submodule R M) :
(submodule.comap p.subtype (p ⊓ p')).quotient →ₗ[R] (submodule.comap (p ⊔ p').subtype p').quotient
Canonical linear map from the quotient p/(p ∩ p') to (p+p')/p', mapping x + (p ∩ p')
to x + p', where p and p' are submodules of an ambient module.
Equations
- linear_map.quotient_inf_to_sup_quotient p p' = (submodule.comap p.subtype (p ⊓ p')).liftq ((submodule.comap (p ⊔ p').subtype p').mkq.comp (submodule.of_le _)) _
def
linear_map.quotient_inf_equiv_sup_quotient
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[module R M]
(p p' : submodule R M) :
(submodule.comap p.subtype (p ⊓ p')).quotient ≃ₗ[R] (submodule.comap (p ⊔ p').subtype p').quotient
Second Isomorphism Law : the canonical map from p/(p ∩ p') to (p+p')/p' as a linear isomorphism.
Equations
@[simp]
theorem
linear_map.coe_quotient_inf_to_sup_quotient
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[module R M]
(p p' : submodule R M) :
@[simp]
theorem
linear_map.quotient_inf_equiv_sup_quotient_apply_mk
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[module R M]
(p p' : submodule R M)
(x : ↥p) :
theorem
linear_map.quotient_inf_equiv_sup_quotient_symm_apply_left
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[module R M]
(p p' : submodule R M)
(x : ↥(p ⊔ p'))
(hx : ↑x ∈ p) :
⇑((linear_map.quotient_inf_equiv_sup_quotient p p').symm) (submodule.quotient.mk x) = submodule.quotient.mk ⟨↑x, hx⟩
@[simp]
theorem
linear_map.quotient_inf_equiv_sup_quotient_symm_apply_eq_zero_iff
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[module R M]
{p p' : submodule R M}
{x : ↥(p ⊔ p')} :
⇑((linear_map.quotient_inf_equiv_sup_quotient p p').symm) (submodule.quotient.mk x) = 0 ↔ ↑x ∈ p'
theorem
linear_map.quotient_inf_equiv_sup_quotient_symm_apply_right
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[module R M]
(p p' : submodule R M)
{x : ↥(p ⊔ p')} :
↑x ∈ p' → ⇑((linear_map.quotient_inf_equiv_sup_quotient p p').symm) (submodule.quotient.mk x) = 0
theorem
linear_map.is_linear_map_prod_iso
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
{M₃ : Type u_4}
[comm_semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_group M₃]
[semimodule R M]
[semimodule R M₂]
[semimodule R M₃] :
def
linear_map.pi
{R : Type u}
{M₂ : Type w}
{ι : Type x}
[semiring R]
[add_comm_monoid M₂]
[semimodule R M₂]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), semimodule R (φ i)] :
pi construction for linear functions. From a family of linear functions it produces a linear
function into a family of modules.
@[simp]
theorem
linear_map.pi_apply
{R : Type u}
{M₂ : Type w}
{ι : Type x}
[semiring R]
[add_comm_monoid M₂]
[semimodule R M₂]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), semimodule R (φ i)]
(f : Π (i : ι), M₂ →ₗ[R] φ i)
(c : M₂)
(i : ι) :
⇑(linear_map.pi f) c i = ⇑(f i) c
theorem
linear_map.ker_pi
{R : Type u}
{M₂ : Type w}
{ι : Type x}
[semiring R]
[add_comm_monoid M₂]
[semimodule R M₂]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), semimodule R (φ i)]
(f : Π (i : ι), M₂ →ₗ[R] φ i) :
(linear_map.pi f).ker = ⨅ (i : ι), (f i).ker
theorem
linear_map.pi_eq_zero
{R : Type u}
{M₂ : Type w}
{ι : Type x}
[semiring R]
[add_comm_monoid M₂]
[semimodule R M₂]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), semimodule R (φ i)]
(f : Π (i : ι), M₂ →ₗ[R] φ i) :
linear_map.pi f = 0 ↔ ∀ (i : ι), f i = 0
theorem
linear_map.pi_zero
{R : Type u}
{M₂ : Type w}
{ι : Type x}
[semiring R]
[add_comm_monoid M₂]
[semimodule R M₂]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), semimodule R (φ i)] :
linear_map.pi (λ (i : ι), 0) = 0
theorem
linear_map.pi_comp
{R : Type u}
{M₂ : Type w}
{M₃ : Type y}
{ι : Type x}
[semiring R]
[add_comm_monoid M₂]
[semimodule R M₂]
[add_comm_monoid M₃]
[semimodule R M₃]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), semimodule R (φ i)]
(f : Π (i : ι), M₂ →ₗ[R] φ i)
(g : M₃ →ₗ[R] M₂) :
(linear_map.pi f).comp g = linear_map.pi (λ (i : ι), (f i).comp g)
def
linear_map.proj
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), semimodule R (φ i)]
(i : ι) :
The projections from a family of modules are linear maps.
@[simp]
theorem
linear_map.proj_apply
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), semimodule R (φ i)]
(i : ι)
(b : Π (i : ι), φ i) :
⇑(linear_map.proj i) b = b i
theorem
linear_map.proj_pi
{R : Type u}
{M₂ : Type w}
{ι : Type x}
[semiring R]
[add_comm_monoid M₂]
[semimodule R M₂]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), semimodule R (φ i)]
(f : Π (i : ι), M₂ →ₗ[R] φ i)
(i : ι) :
(linear_map.proj i).comp (linear_map.pi f) = f i
theorem
linear_map.infi_ker_proj
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), semimodule R (φ i)] :
(⨅ (i : ι), (linear_map.proj i).ker) = ⊥
def
linear_map.infi_ker_proj_equiv
(R : Type u)
{ι : Type x}
[semiring R]
(φ : ι → Type i)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), semimodule R (φ i)]
{I J : set ι}
[decidable_pred (λ (i : ι), i ∈ I)] :
If I and J are disjoint index sets, the product of the kernels of the Jth projections of
φ is linearly equivalent to the product over I.
Equations
- linear_map.infi_ker_proj_equiv R φ hd hu = linear_equiv.of_linear (linear_map.pi (λ (i : ↥I), (linear_map.proj ↑i).comp (⨅ (i : ι) (H : i ∈ J), (linear_map.proj i).ker).subtype)) (linear_map.cod_restrict (⨅ (i : ι) (H : i ∈ J), (linear_map.proj i).ker) (linear_map.pi (λ (i : ι), dite (i ∈ I) (λ (h : i ∈ I), linear_map.proj ⟨i, h⟩) (λ (h : i ∉ I), 0))) _) _ _
def
linear_map.diag
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), semimodule R (φ i)]
[decidable_eq ι]
(i j : ι) :
diag i j is the identity map if i = j. Otherwise it is the constant 0 map.
Equations
- linear_map.diag i j = function.update 0 i linear_map.id j
theorem
linear_map.update_apply
{R : Type u}
{M₂ : Type w}
{ι : Type x}
[semiring R]
[add_comm_monoid M₂]
[semimodule R M₂]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), semimodule R (φ i)]
[decidable_eq ι]
(f : Π (i : ι), M₂ →ₗ[R] φ i)
(c : M₂)
(i j : ι)
(b : M₂ →ₗ[R] φ i) :
⇑(function.update f i b j) c = function.update (λ (i : ι), ⇑(f i) c) i (⇑b c) j
def
linear_map.std_basis
(R : Type u)
{ι : Type x}
[semiring R]
(φ : ι → Type i)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), semimodule R (φ i)]
[decidable_eq ι]
(i : ι) :
The standard basis of the product of φ.
Equations
- linear_map.std_basis R φ i = linear_map.pi (linear_map.diag i)
theorem
linear_map.std_basis_apply
(R : Type u)
{ι : Type x}
[semiring R]
(φ : ι → Type i)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), semimodule R (φ i)]
[decidable_eq ι]
(i : ι)
(b : φ i) :
⇑(linear_map.std_basis R φ i) b = function.update 0 i b
@[simp]
theorem
linear_map.std_basis_same
(R : Type u)
{ι : Type x}
[semiring R]
(φ : ι → Type i)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), semimodule R (φ i)]
[decidable_eq ι]
(i : ι)
(b : φ i) :
⇑(linear_map.std_basis R φ i) b i = b
theorem
linear_map.std_basis_ne
(R : Type u)
{ι : Type x}
[semiring R]
(φ : ι → Type i)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), semimodule R (φ i)]
[decidable_eq ι]
(i j : ι)
(h : j ≠ i)
(b : φ i) :
⇑(linear_map.std_basis R φ i) b j = 0
theorem
linear_map.ker_std_basis
(R : Type u)
{ι : Type x}
[semiring R]
(φ : ι → Type i)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), semimodule R (φ i)]
[decidable_eq ι]
(i : ι) :
(linear_map.std_basis R φ i).ker = ⊥
theorem
linear_map.proj_comp_std_basis
(R : Type u)
{ι : Type x}
[semiring R]
(φ : ι → Type i)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), semimodule R (φ i)]
[decidable_eq ι]
(i j : ι) :
(linear_map.proj i).comp (linear_map.std_basis R φ j) = linear_map.diag j i
theorem
linear_map.proj_std_basis_same
(R : Type u)
{ι : Type x}
[semiring R]
(φ : ι → Type i)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), semimodule R (φ i)]
[decidable_eq ι]
(i : ι) :
(linear_map.proj i).comp (linear_map.std_basis R φ i) = linear_map.id
theorem
linear_map.proj_std_basis_ne
(R : Type u)
{ι : Type x}
[semiring R]
(φ : ι → Type i)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), semimodule R (φ i)]
[decidable_eq ι]
(i j : ι) :
i ≠ j → (linear_map.proj i).comp (linear_map.std_basis R φ j) = 0
theorem
linear_map.supr_range_std_basis_le_infi_ker_proj
(R : Type u)
{ι : Type x}
[semiring R]
(φ : ι → Type i)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), semimodule R (φ i)]
[decidable_eq ι]
(I J : set ι) :
disjoint I J → ((⨆ (i : ι) (H : i ∈ I), (linear_map.std_basis R φ i).range) ≤ ⨅ (i : ι) (H : i ∈ J), (linear_map.proj i).ker)
theorem
linear_map.infi_ker_proj_le_supr_range_std_basis
(R : Type u)
{ι : Type x}
[semiring R]
(φ : ι → Type i)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), semimodule R (φ i)]
[decidable_eq ι]
{I : finset ι}
{J : set ι} :
theorem
linear_map.supr_range_std_basis_eq_infi_ker_proj
(R : Type u)
{ι : Type x}
[semiring R]
(φ : ι → Type i)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), semimodule R (φ i)]
[decidable_eq ι]
{I J : set ι} :
theorem
linear_map.supr_range_std_basis
(R : Type u)
{ι : Type x}
[semiring R]
(φ : ι → Type i)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), semimodule R (φ i)]
[decidable_eq ι]
[fintype ι] :
(⨆ (i : ι), (linear_map.std_basis R φ i).range) = ⊤
theorem
linear_map.disjoint_std_basis_std_basis
(R : Type u)
{ι : Type x}
[semiring R]
(φ : ι → Type i)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), semimodule R (φ i)]
[decidable_eq ι]
(I J : set ι) :
disjoint I J → disjoint (⨆ (i : ι) (H : i ∈ I), (linear_map.std_basis R φ i).range) (⨆ (i : ι) (H : i ∈ J), (linear_map.std_basis R φ i).range)
theorem
linear_map.std_basis_eq_single
(R : Type u)
{ι : Type x}
[semiring R]
[decidable_eq ι]
{a : R} :
(λ (i : ι), ⇑(linear_map.std_basis R (λ (_x : ι), R) i) a) = λ (i : ι), ⇑(finsupp.single i a)
def
linear_map.fun_left
(R : Type u)
(M : Type v)
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{m : Type u_1}
{n : Type u_2} :
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)
(M : Type v)
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{m : Type u_1}
{n : Type u_2}
(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)
(M : Type v)
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{n : Type u_2}
(g : n → M) :
⇑(linear_map.fun_left R M id) g = g
theorem
linear_map.fun_left_comp
(R : Type u)
(M : Type v)
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{m : Type u_1}
{n : Type u_2}
{p : Type u_3}
(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₁)
def
linear_map.fun_congr_left
(R : Type u)
(M : Type v)
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{m : Type u_1}
{n : Type u_2} :
Given an R-module M and an equivalence m ≃ n between arbitrary types,
construct a linear equivalence (n → M) ≃ₗ[R] (m → M)
Equations
- linear_map.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_map.fun_congr_left_apply
(R : Type u)
(M : Type v)
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{m : Type u_1}
{n : Type u_2}
(e : m ≃ n)
(x : n → M) :
⇑(linear_map.fun_congr_left R M e) x = ⇑(linear_map.fun_left R M ⇑e) x
@[simp]
theorem
linear_map.fun_congr_left_id
(R : Type u)
(M : Type v)
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{n : Type u_2} :
linear_map.fun_congr_left R M (equiv.refl n) = linear_equiv.refl R (n → M)
@[simp]
theorem
linear_map.fun_congr_left_comp
(R : Type u)
(M : Type v)
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{m : Type u_1}
{n : Type u_2}
{p : Type u_3}
(e₁ : m ≃ n)
(e₂ : n ≃ p) :
linear_map.fun_congr_left R M (e₁.trans e₂) = (linear_map.fun_congr_left R M e₂).trans (linear_map.fun_congr_left R M e₁)
@[simp]
theorem
linear_map.fun_congr_left_symm
(R : Type u)
(M : Type v)
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{m : Type u_1}
{n : Type u_2}
(e : m ≃ n) :
(linear_map.fun_congr_left R M e).symm = linear_map.fun_congr_left R M e.symm
@[instance]
def
linear_map.automorphism_group
(R : Type u)
(M : Type v)
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
@[instance]
def
linear_map.automorphism_group.to_linear_map_is_monoid_hom
(R : Type u)
(M : Type v)
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
Equations
- _ = _
def
linear_map.general_linear_group
(R : Type u)
(M : Type v)
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
Type v
The group of invertible linear maps from M to itself
Equations
- linear_map.general_linear_group R M = units (M →ₗ[R] M)
@[instance]
def
linear_map.general_linear_group.has_coe_to_fun
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
def
linear_map.general_linear_group.to_linear_equiv
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
linear_map.general_linear_group R M → (M ≃ₗ[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}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
(M ≃ₗ[R] M) → linear_map.general_linear_group 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)
(M : Type v)
[semiring R]
[add_comm_monoid M]
[semimodule 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)
(M : Type v)
[semiring R]
[add_comm_monoid M]
[semimodule R M]
(f : linear_map.general_linear_group R M) :