Products of modules #
This file defines constructors for linear maps whose domains or codomains are products.
It contains theorems relating these to each other, as well as to submodule.prod, submodule.map,
submodule.comap, linear_map.range, and linear_map.ker.
Main definitions #
- products in the domain:
- products in the codomain:
- products in both domain and codomain:
linear_map.prod_maplinear_equiv.prod_maplinear_equiv.skew_prod
def
linear_map.fst
(R : Type u)
(M : Type v)
(M₂ : Type w)
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module 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₂]
[module R M]
[module 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₂]
[module R M]
[module 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₂]
[module R M]
[module R M₂]
(x : M × M₂) :
⇑(linear_map.snd R M M₂) x = x.snd
theorem
linear_map.fst_surjective
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
function.surjective ⇑(linear_map.fst R M M₂)
theorem
linear_map.snd_surjective
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
function.surjective ⇑(linear_map.snd R M M₂)
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₃]
[module R M]
[module R M₂]
[module R M₃]
(f : M →ₗ[R] M₂)
(g : M →ₗ[R] M₃) :
The prod of two linear maps is a linear map.
@[simp]
theorem
linear_map.prod_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[module R M]
[module R M₂]
[module R M₃]
(f : M →ₗ[R] M₂)
(g : M →ₗ[R] M₃)
(i : M) :
theorem
linear_map.coe_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₃]
[module R M]
[module R M₂]
[module R M₃]
(f : M →ₗ[R] M₂)
(g : M →ₗ[R] 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₃]
[module R M]
[module R M₂]
[module 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₃]
[module R M]
[module R M₂]
[module 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₂]
[module R M]
[module R M₂] :
(linear_map.fst R M M₂).prod (linear_map.snd R M M₂) = linear_map.id
@[simp]
theorem
linear_map.prod_equiv_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
(S : Type u_1)
[semiring R]
[semiring S]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[module R M]
[module R M₂]
[module R M₃]
[module S M₂]
[module S M₃]
[smul_comm_class R S M₂]
[smul_comm_class R S M₃]
(f : (M →ₗ[R] M₂) × (M →ₗ[R] M₃)) :
def
linear_map.prod_equiv
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
(S : Type u_1)
[semiring R]
[semiring S]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[module R M]
[module R M₂]
[module R M₃]
[module S M₂]
[module S M₃]
[smul_comm_class R S M₂]
[smul_comm_class R S M₃] :
Taking the product of two maps with the same domain is equivalent to taking the product of their codomains.
See note [bundled maps over different rings] for why separate R and S semirings are used.
@[simp]
theorem
linear_map.prod_equiv_symm_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
(S : Type u_1)
[semiring R]
[semiring S]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[module R M]
[module R M₂]
[module R M₃]
[module S M₂]
[module S M₃]
[smul_comm_class R S M₂]
[smul_comm_class R S M₃]
(f : M →ₗ[R] M₂ × M₃) :
⇑((linear_map.prod_equiv S).symm) f = ((linear_map.fst R M₂ M₃).comp f, (linear_map.snd R M₂ M₃).comp f)
def
linear_map.inl
(R : Type u)
(M : Type v)
(M₂ : Type w)
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
The left injection into a product is a linear map.
Equations
- linear_map.inl R M M₂ = linear_map.id.prod 0
def
linear_map.inr
(R : Type u)
(M : Type v)
(M₂ : Type w)
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
The right injection into a product is a linear map.
Equations
- linear_map.inr R M M₂ = 0.prod linear_map.id
theorem
linear_map.range_inl
(R : Type u)
(M : Type v)
(M₂ : Type w)
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
(linear_map.inl R M M₂).range = (linear_map.snd R M M₂).ker
theorem
linear_map.ker_snd
(R : Type u)
(M : Type v)
(M₂ : Type w)
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
(linear_map.snd R M M₂).ker = (linear_map.inl R M M₂).range
theorem
linear_map.range_inr
(R : Type u)
(M : Type v)
(M₂ : Type w)
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
(linear_map.inr R M M₂).range = (linear_map.fst R M M₂).ker
theorem
linear_map.ker_fst
(R : Type u)
(M : Type v)
(M₂ : Type w)
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
(linear_map.fst R M M₂).ker = (linear_map.inr R M M₂).range
@[simp]
theorem
linear_map.coe_inl
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
⇑(linear_map.inl R M M₂) = λ (x : M), (x, 0)
theorem
linear_map.inl_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(x : M) :
⇑(linear_map.inl R M M₂) x = (x, 0)
@[simp]
theorem
linear_map.coe_inr
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
⇑(linear_map.inr R M M₂) = prod.mk 0
theorem
linear_map.inr_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(x : M₂) :
⇑(linear_map.inr R M M₂) x = (0, x)
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₂]
[module R M]
[module 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₂]
[module R M]
[module R M₂] :
linear_map.inr R M M₂ = 0.prod linear_map.id
theorem
linear_map.inl_injective
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module 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₂]
[module R M]
[module 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₃]
[module R M]
[module R M₂]
[module R M₃]
(f : M →ₗ[R] M₃)
(g : M₂ →ₗ[R] M₃) :
The coprod function λ x : M × M₂, f x.1 + g x.2 is a linear map.
Equations
- f.coprod g = f.comp (linear_map.fst R M M₂) + g.comp (linear_map.snd R M M₂)
@[simp]
@[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₃]
[module R M]
[module R M₂]
[module 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₃]
[module R M]
[module R M₂]
[module 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₂]
[module R M]
[module R M₂] :
(linear_map.inl R M M₂).coprod (linear_map.inr R M M₂) = linear_map.id
theorem
linear_map.comp_coprod
{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₄]
[module R M]
[module R M₂]
[module R M₃]
[module R M₄]
(f : M₃ →ₗ[R] M₄)
(g₁ : M →ₗ[R] M₃)
(g₂ : M₂ →ₗ[R] M₃) :
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₂]
[module R M]
[module 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₂]
[module R M]
[module R M₂] :
linear_map.snd R M M₂ = 0.coprod linear_map.id
@[simp]
theorem
linear_map.coprod_comp_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₄]
[module R M]
[module R M₂]
[module R M₃]
[module R M₄]
(f : M₂ →ₗ[R] M₄)
(g : M₃ →ₗ[R] M₄)
(f' : M →ₗ[R] M₂)
(g' : M →ₗ[R] M₃) :
@[simp]
theorem
linear_map.coprod_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₃]
[module R M]
[module R M₂]
[module R M₃]
(f : M →ₗ[R] M₃)
(g : M₂ →ₗ[R] M₃)
(S : submodule R M)
(S' : submodule R M₂) :
submodule.map (f.coprod g) (S.prod S') = submodule.map f S ⊔ submodule.map g S'
@[simp]
theorem
linear_map.coprod_equiv_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
(S : Type u_1)
[semiring R]
[semiring S]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[module R M]
[module R M₂]
[module R M₃]
[module S M₃]
[smul_comm_class R S M₃]
(f : (M →ₗ[R] M₃) × (M₂ →ₗ[R] M₃)) :
@[simp]
theorem
linear_map.coprod_equiv_symm_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
(S : Type u_1)
[semiring R]
[semiring S]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[module R M]
[module R M₂]
[module R M₃]
[module S M₃]
[smul_comm_class R S M₃]
(f : M × M₂ →ₗ[R] M₃) :
⇑((linear_map.coprod_equiv S).symm) f = (f.comp (linear_map.inl R M M₂), f.comp (linear_map.inr R M M₂))
def
linear_map.coprod_equiv
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
(S : Type u_1)
[semiring R]
[semiring S]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[module R M]
[module R M₂]
[module R M₃]
[module S M₃]
[smul_comm_class R S M₃] :
Taking the product of two maps with the same codomain is equivalent to taking the product of their domains.
See note [bundled maps over different rings] for why separate R and S semirings are used.
theorem
linear_map.prod_ext_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₃]
[module R M]
[module R M₂]
[module R M₃]
{f g : M × M₂ →ₗ[R] M₃} :
f = g ↔ f.comp (linear_map.inl R M M₂) = g.comp (linear_map.inl R M M₂) ∧ f.comp (linear_map.inr R M M₂) = g.comp (linear_map.inr R M M₂)
@[ext]
theorem
linear_map.prod_ext
{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₃]
[module R M]
[module R M₂]
[module R M₃]
{f g : M × M₂ →ₗ[R] M₃}
(hl : f.comp (linear_map.inl R M M₂) = g.comp (linear_map.inl R M M₂))
(hr : f.comp (linear_map.inr R M M₂) = g.comp (linear_map.inr R M M₂)) :
f = g
Split equality of linear maps from a product into linear maps over each component, to allow ext
to apply lemmas specific to M →ₗ M₃ and M₂ →ₗ M₃.
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₄]
[module R M]
[module R M₂]
[module R M₃]
[module R M₄]
(f : M →ₗ[R] M₃)
(g : M₂ →ₗ[R] M₄) :
prod.map of two linear maps.
Equations
- f.prod_map g = (f.comp (linear_map.fst R M M₂)).prod (g.comp (linear_map.snd R M M₂))
@[simp]
theorem
linear_map.prod_map_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
{M₄ : Type z}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[add_comm_monoid M₄]
[module R M]
[module R M₂]
[module R M₃]
[module R M₄]
(f : M →ₗ[R] M₃)
(g : M₂ →ₗ[R] M₄)
(x : M × M₂) :
theorem
linear_map.prod_map_comap_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₄]
[module R M]
[module R M₂]
[module R M₃]
[module R M₄]
(f : M →ₗ[R] M₂)
(g : M₃ →ₗ[R] M₄)
(S : submodule R M₂)
(S' : submodule R M₄) :
submodule.comap (f.prod_map g) (S.prod S') = (submodule.comap f S).prod (submodule.comap g S')
theorem
linear_map.ker_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₄]
[module R M]
[module R M₂]
[module R M₃]
[module R M₄]
(f : M →ₗ[R] M₂)
(g : M₃ →ₗ[R] M₄) :
theorem
linear_map.inl_map_mul
{R : Type u}
[semiring R]
{A : Type u_2}
[non_unital_non_assoc_semiring A]
[module R A]
{B : Type u_3}
[non_unital_non_assoc_semiring B]
[module R B]
(a₁ a₂ : A) :
⇑(linear_map.inl R A B) (a₁ * a₂) = (⇑(linear_map.inl R A B) a₁) * ⇑(linear_map.inl R A B) a₂
theorem
linear_map.inr_map_mul
{R : Type u}
[semiring R]
{A : Type u_2}
[non_unital_non_assoc_semiring A]
[module R A]
{B : Type u_3}
[non_unital_non_assoc_semiring B]
[module R B]
(b₁ b₂ : B) :
⇑(linear_map.inr R A B) (b₁ * b₂) = (⇑(linear_map.inr R A B) b₁) * ⇑(linear_map.inr R A B) b₂
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₃]
[module R M]
[module R M₂]
[module R M₃]
(f : M →ₗ[R] M₃)
(g : M₂ →ₗ[R] M₃) :
theorem
linear_map.is_compl_range_inl_inr
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
is_compl (linear_map.inl R M M₂).range (linear_map.inr R M M₂).range
theorem
linear_map.sup_range_inl_inr
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
(linear_map.inl R M M₂).range ⊔ (linear_map.inr R M M₂).range = ⊤
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₂]
[module R M]
[module R M₂] :
disjoint (linear_map.inl R M M₂).range (linear_map.inr R M M₂).range
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₃]
[module R M]
[module R M₂]
[module 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₃]
[module R M]
[module R M₂]
[module 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₂]
[module R M]
[module 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₂]
[module R M]
[module 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₂]
[module R M]
[module 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₃]
[module R M]
[module R M₂]
[module 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₃]
[module R M]
[module R M₂]
[module R M₃]
(f : M →ₗ[R] M₂)
(g : M →ₗ[R] M₃) :
theorem
linear_map.ker_prod_ker_le_ker_coprod
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[module R M]
{M₂ : Type u_1}
[add_comm_group M₂]
[module R M₂]
{M₃ : Type u_2}
[add_comm_group M₃]
[module R M₃]
(f : M →ₗ[R] M₃)
(g : M₂ →ₗ[R] M₃) :
theorem
linear_map.ker_coprod_of_disjoint_range
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[module R M]
{M₂ : Type u_1}
[add_comm_group M₂]
[module R M₂]
{M₃ : Type u_2}
[add_comm_group M₃]
[module R M₃]
(f : M →ₗ[R] M₃)
(g : M₂ →ₗ[R] M₃)
(hd : disjoint f.range g.range) :
@[simp]
theorem
submodule.map_inl
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module 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}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module 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}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module 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}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module 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}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(p : submodule R M)
(q : submodule R M₂) :
submodule.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}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(p : submodule R M)
(q : submodule R M₂) :
submodule.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}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(p : submodule R M)
(q : submodule R M₂) :
submodule.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}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(p : submodule R M)
(q : submodule R M₂) :
submodule.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}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
(linear_map.inl R M M₂).ker = ⊥
@[simp]
theorem
submodule.ker_inr
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
(linear_map.inr R M M₂).ker = ⊥
@[simp]
theorem
submodule.range_fst
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
(linear_map.fst R M M₂).range = ⊤
@[simp]
theorem
submodule.range_snd
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
(linear_map.snd R M M₂).range = ⊤
def
submodule.fst
(R : Type u)
(M : Type v)
(M₂ : Type w)
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
M as a submodule of M × N.
Equations
- submodule.fst R M M₂ = submodule.comap (linear_map.snd R M M₂) ⊥
@[simp]
theorem
submodule.fst_equiv_symm_apply_coe
(R : Type u)
(M : Type v)
(M₂ : Type w)
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(m : M) :
↑(⇑((submodule.fst_equiv R M M₂).symm) m) = (m, 0)
def
submodule.fst_equiv
(R : Type u)
(M : Type v)
(M₂ : Type w)
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
↥(submodule.fst R M M₂) ≃ₗ[R] M
M as a submodule of M × N is isomorphic to M.
@[simp]
theorem
submodule.fst_equiv_apply
(R : Type u)
(M : Type v)
(M₂ : Type w)
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(x : ↥(submodule.fst R M M₂)) :
⇑(submodule.fst_equiv R M M₂) x = x.val.fst
theorem
submodule.fst_map_fst
(R : Type u)
(M : Type v)
(M₂ : Type w)
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
submodule.map (linear_map.fst R M M₂) (submodule.fst R M M₂) = ⊤
theorem
submodule.fst_map_snd
(R : Type u)
(M : Type v)
(M₂ : Type w)
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
submodule.map (linear_map.snd R M M₂) (submodule.fst R M M₂) = ⊥
def
submodule.snd
(R : Type u)
(M : Type v)
(M₂ : Type w)
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
N as a submodule of M × N.
Equations
- submodule.snd R M M₂ = submodule.comap (linear_map.fst R M M₂) ⊥
@[simp]
theorem
submodule.snd_equiv_apply
(R : Type u)
(M : Type v)
(M₂ : Type w)
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(x : ↥(submodule.snd R M M₂)) :
⇑(submodule.snd_equiv R M M₂) x = x.val.snd
@[simp]
theorem
submodule.snd_equiv_symm_apply_coe
(R : Type u)
(M : Type v)
(M₂ : Type w)
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(n : M₂) :
↑(⇑((submodule.snd_equiv R M M₂).symm) n) = (0, n)
def
submodule.snd_equiv
(R : Type u)
(M : Type v)
(M₂ : Type w)
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
↥(submodule.snd R M M₂) ≃ₗ[R] M₂
N as a submodule of M × N is isomorphic to N.
theorem
submodule.snd_map_fst
(R : Type u)
(M : Type v)
(M₂ : Type w)
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
submodule.map (linear_map.fst R M M₂) (submodule.snd R M M₂) = ⊥
theorem
submodule.snd_map_snd
(R : Type u)
(M : Type v)
(M₂ : Type w)
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
submodule.map (linear_map.snd R M M₂) (submodule.snd R M M₂) = ⊤
theorem
submodule.fst_sup_snd
(R : Type u)
(M : Type v)
(M₂ : Type w)
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
submodule.fst R M M₂ ⊔ submodule.snd R M M₂ = ⊤
theorem
submodule.fst_inf_snd
(R : Type u)
(M : Type v)
(M₂ : Type w)
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
submodule.fst R M M₂ ⊓ submodule.snd R M M₂ = ⊥
theorem
submodule.le_prod_iff
(R : Type u)
(M : Type v)
(M₂ : Type w)
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
{p₁ : submodule R M}
{p₂ : submodule R M₂}
{q : submodule R (M × M₂)} :
q ≤ p₁.prod p₂ ↔ submodule.map (linear_map.fst R M M₂) q ≤ p₁ ∧ submodule.map (linear_map.snd R M M₂) q ≤ p₂
theorem
submodule.prod_le_iff
(R : Type u)
(M : Type v)
(M₂ : Type w)
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
{p₁ : submodule R M}
{p₂ : submodule R M₂}
{q : submodule R (M × M₂)} :
p₁.prod p₂ ≤ q ↔ submodule.map (linear_map.inl R M M₂) p₁ ≤ q ∧ submodule.map (linear_map.inr R M M₂) p₂ ≤ q
@[simp]
theorem
linear_equiv.prod_comm_apply
(R : Type u_1)
(M : Type u_2)
(N : Type u_3)
[semiring R]
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N]
(ᾰ : M × N) :
⇑(linear_equiv.prod_comm R M N) ᾰ = ᾰ.swap
def
linear_equiv.prod_comm
(R : Type u_1)
(M : Type u_2)
(N : Type u_3)
[semiring R]
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N] :
Product of modules is commutative up to linear isomorphism.
@[protected]
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₄]
{module_M : module R M}
{module_M₂ : module R M₂}
{module_M₃ : module R M₃}
{module_M₄ : module R M₄}
(e₁ : M ≃ₗ[R] M₂)
(e₂ : M₃ ≃ₗ[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₄]
{module_M : module R M}
{module_M₂ : module R M₂}
{module_M₃ : module R M₃}
{module_M₄ : module 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₄]
{module_M : module R M}
{module_M₂ : module R M₂}
{module_M₃ : module R M₃}
{module_M₄ : module R M₄}
(e₁ : M ≃ₗ[R] M₂)
(e₂ : M₃ ≃ₗ[R] M₄)
(p : M × M₃) :
@[simp, norm_cast]
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₄]
{module_M : module R M}
{module_M₂ : module R M₂}
{module_M₃ : module R M₃}
{module_M₄ : module R M₄}
(e₁ : M ≃ₗ[R] M₂)
(e₂ : M₃ ≃ₗ[R] M₄) :
@[protected]
def
linear_equiv.skew_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_group M₄]
{module_M : module R M}
{module_M₂ : module R M₂}
{module_M₃ : module R M₃}
{module_M₄ : module R M₄}
(e₁ : M ≃ₗ[R] M₂)
(e₂ : M₃ ≃ₗ[R] M₄)
(f : M →ₗ[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_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[add_comm_group M₄]
{module_M : module R M}
{module_M₂ : module R M₂}
{module_M₃ : module R M₃}
{module_M₄ : module 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_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[add_comm_group M₄]
{module_M : module R M}
{module_M₂ : module R M₂}
{module_M₃ : module R M₃}
{module_M₄ : module R M₄}
(e₁ : M ≃ₗ[R] M₂)
(e₂ : M₃ ≃ₗ[R] M₄)
(f : M →ₗ[R] M₄)
(x : M₂ × 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₃]
[module R M]
[module R M₂]
[module R M₃]
{f : M →ₗ[R] M₂}
{g : M →ₗ[R] M₃}
(h : f.ker ⊔ g.ker = ⊤) :
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.
Tunnels and tailings #
Some preliminary work for establishing the strong rank condition for noetherian rings.
Given a morphism f : M × N →ₗ[R] M which is i : injective f,
we can find an infinite decreasing tunnel f i n of copies of M inside M,
and sitting beside these, an infinite sequence of copies of N.
We picturesquely name these as tailing f i n for each individual copy of N,
and tailings f i n for the supremum of the first n+1 copies:
they are the pieces left behind, sitting inside the tunnel.
By construction, each tailing f i (n+1) is disjoint from tailings f i n;
later, when we assume M is noetherian, this implies that N must be trivial,
and establishes the strong rank condition for any left-noetherian ring.
def
linear_map.tunnel_aux
{R : Type u}
{M : Type v}
[ring R]
{N : Type u_1}
[add_comm_group M]
[module R M]
[add_comm_group N]
[module R N]
(f : M × N →ₗ[R] M)
(Kφ : Σ (K : submodule R M), ↥K ≃ₗ[R] M) :
An auxiliary construction for tunnel.
The composition of f, followed by the isomorphism back to K,
followed by the inclusion of this submodule back into M.
Equations
- f.tunnel_aux Kφ = (Kφ.fst.subtype.comp (linear_equiv.symm Kφ.snd).to_linear_map).comp f
theorem
linear_map.tunnel_aux_injective
{R : Type u}
{M : Type v}
[ring R]
{N : Type u_1}
[add_comm_group M]
[module R M]
[add_comm_group N]
[module R N]
(f : M × N →ₗ[R] M)
(i : function.injective ⇑f)
(Kφ : Σ (K : submodule R M), ↥K ≃ₗ[R] M) :
function.injective ⇑(f.tunnel_aux Kφ)
noncomputable
def
linear_map.tunnel'
{R : Type u}
{M : Type v}
[ring R]
{N : Type u_1}
[add_comm_group M]
[module R M]
[add_comm_group N]
[module R N]
(f : M × N →ₗ[R] M)
(i : function.injective ⇑f) :
Auxiliary definition for tunnel.
Equations
- f.tunnel' i (n + 1) = ⟨submodule.map (f.tunnel_aux (f.tunnel' i n)) (submodule.fst R M N), (submodule.equiv_map_of_injective (f.tunnel_aux (f.tunnel' i n)) _ (submodule.fst R M N)).symm.trans (submodule.fst_equiv R M N)⟩
- f.tunnel' i 0 = ⟨⊤, linear_equiv.of_top ⊤ linear_map.tunnel'._main._proof_3⟩
noncomputable
def
linear_map.tunnel
{R : Type u}
{M : Type v}
[ring R]
{N : Type u_1}
[add_comm_group M]
[module R M]
[add_comm_group N]
[module R N]
(f : M × N →ₗ[R] M)
(i : function.injective ⇑f) :
ℕ →o order_dual (submodule R M)
Give an injective map f : M × N →ₗ[R] M we can find a nested sequence of submodules
all isomorphic to M.
noncomputable
def
linear_map.tailing
{R : Type u}
{M : Type v}
[ring R]
{N : Type u_1}
[add_comm_group M]
[module R M]
[add_comm_group N]
[module R N]
(f : M × N →ₗ[R] M)
(i : function.injective ⇑f)
(n : ℕ) :
submodule R M
Give an injective map f : M × N →ₗ[R] M we can find a sequence of submodules
all isomorphic to N.
Equations
- f.tailing i n = submodule.map (f.tunnel_aux (f.tunnel' i n)) (submodule.snd R M N)
noncomputable
def
linear_map.tailing_linear_equiv
{R : Type u}
{M : Type v}
[ring R]
{N : Type u_1}
[add_comm_group M]
[module R M]
[add_comm_group N]
[module R N]
(f : M × N →ₗ[R] M)
(i : function.injective ⇑f)
(n : ℕ) :
Each tailing f i n is a copy of N.
Equations
- f.tailing_linear_equiv i n = (submodule.equiv_map_of_injective (f.tunnel_aux (f.tunnel' i n)) _ (submodule.snd R M N)).symm.trans (submodule.snd_equiv R M N)
theorem
linear_map.tailing_le_tunnel
{R : Type u}
{M : Type v}
[ring R]
{N : Type u_1}
[add_comm_group M]
[module R M]
[add_comm_group N]
[module R N]
(f : M × N →ₗ[R] M)
(i : function.injective ⇑f)
(n : ℕ) :
theorem
linear_map.tailing_disjoint_tunnel_succ
{R : Type u}
{M : Type v}
[ring R]
{N : Type u_1}
[add_comm_group M]
[module R M]
[add_comm_group N]
[module R N]
(f : M × N →ₗ[R] M)
(i : function.injective ⇑f)
(n : ℕ) :
noncomputable
def
linear_map.tailings
{R : Type u}
{M : Type v}
[ring R]
{N : Type u_1}
[add_comm_group M]
[module R M]
[add_comm_group N]
[module R N]
(f : M × N →ₗ[R] M)
(i : function.injective ⇑f) :
The supremum of all the copies of N found inside the tunnel.
Equations
- f.tailings i = ⇑(partial_sups (f.tailing i))
@[simp]
theorem
linear_map.tailings_zero
{R : Type u}
{M : Type v}
[ring R]
{N : Type u_1}
[add_comm_group M]
[module R M]
[add_comm_group N]
[module R N]
(f : M × N →ₗ[R] M)
(i : function.injective ⇑f) :
@[simp]
theorem
linear_map.tailings_succ
{R : Type u}
{M : Type v}
[ring R]
{N : Type u_1}
[add_comm_group M]
[module R M]
[add_comm_group N]
[module R N]
(f : M × N →ₗ[R] M)
(i : function.injective ⇑f)
(n : ℕ) :
theorem
linear_map.tailings_disjoint_tunnel
{R : Type u}
{M : Type v}
[ring R]
{N : Type u_1}
[add_comm_group M]
[module R M]
[add_comm_group N]
[module R N]
(f : M × N →ₗ[R] M)
(i : function.injective ⇑f)
(n : ℕ) :
theorem
linear_map.tailings_disjoint_tailing
{R : Type u}
{M : Type v}
[ring R]
{N : Type u_1}
[add_comm_group M]
[module R M]
[add_comm_group N]
[module R N]
(f : M × N →ₗ[R] M)
(i : function.injective ⇑f)
(n : ℕ) :