mathlib documentation

linear_algebra.prod

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 #

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₂] :
M × M₂ →ₗ[R] M

The first projection of a product is a linear map.

Equations
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₂] :
M × M₂ →ₗ[R] M₂

The second projection of a product is a linear map.

Equations
@[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₂] :
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₂] :
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₃) :
M →ₗ[R] M₂ × M₃

The prod of two linear maps is a linear map.

Equations
@[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) :
(f.prod g) i = pi.prod f g i
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₂] :
@[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₃] :
((M →ₗ[R] M₂) × (M →ₗ[R] M₃)) ≃ₗ[S] M →ₗ[R] M₂ × 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.

Equations
@[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₂] :
M →ₗ[R] M × M₂

The left injection into a product is a linear map.

Equations
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₂] :
M₂ →ₗ[R] M × M₂

The right injection into a product is a linear map.

Equations
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₂] :
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₂] :
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₂] :
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₂] :
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₂] :
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₃) :
M × M₂ →ₗ[R] M₃

The coprod function λ x : M × M₂, f x.1 + g x.2 is a linear map.

Equations
@[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₃] [module R M] [module R M₂] [module R M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) (x : M × M₂) :
(f.coprod g) x = f x.fst + g x.snd
@[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₂] :
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₃) :
f.comp (g₁.coprod g₂) = (f.comp g₁).coprod (f.comp g₂)
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₂] :
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₂] :
@[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₃) :
(f.coprod g).comp (f'.prod g') = f.comp f' + g.comp g'
@[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₂) :
@[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₃) :
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₃] :
((M →ₗ[R] M₃) × (M₂ →ₗ[R] M₃)) ≃ₗ[S] M × M₂ →ₗ[R] 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.

Equations
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₃.

See note [partially-applied ext lemmas].

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₄) :
M × M₂ →ₗ[R] M₃ × M₄

prod.map of two linear maps.

Equations
@[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₂) :
(f.prod_map g) x = (f x.fst, g x.snd)
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₄) :
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₄) :
(f.prod_map g).ker = f.ker.prod g.ker
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₂] :
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₂] :
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₂] :
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₂) :
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₃) :
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₂) :
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₂) :
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₂} :
@[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₃) :
(f.prod g).ker = f.ker g.ker
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₃) :
f.ker.prod g.ker (f.coprod g).ker
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) :
(f.coprod g).ker = f.ker.prod g.ker
theorem submodule.sup_eq_range {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M] (p q : submodule R M) :
@[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) :
@[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₂) :
@[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) :
@[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₂) :
@[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₂) :
@[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₂) :
@[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₂] :
@[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₂] :
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₂] :
submodule R (M × M₂)

M as a submodule of M × N.

Equations
@[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₂] :

M as a submodule of M × N is isomorphic to M.

Equations
@[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₂)) :
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₂] :
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₂] :
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₂] :
submodule R (M × M₂)

N as a submodule of M × N.

Equations
@[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₂)) :
@[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.

Equations
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₂] :
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₂] :
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
theorem submodule.prod_eq_bot_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₂} :
p₁.prod p₂ = p₁ = p₂ =
theorem submodule.prod_eq_top_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₂} :
p₁.prod p₂ = p₁ = p₂ =
@[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) :
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] :
(M × N) ≃ₗ[R] N × M

Product of modules is commutative up to linear isomorphism.

Equations
@[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₄) :
(M × M₃) ≃ₗ[R] M₂ × M₄

Product of linear equivalences; the maps come from equiv.prod_congr.

Equations
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₄) :
(e₁.prod e₂).symm = e₁.symm.prod e₂.symm
@[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₃) :
(e₁.prod e₂) p = (e₁ p.fst, e₂ p.snd)
@[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₄) :
(e₁.prod e₂) = e₁.prod_map e₂
@[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₄) :
(M × M₃) ≃ₗ[R] M₂ × 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
@[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₃) :
(e₁.skew_prod e₂ f) x = (e₁ x.fst, e₂ x.snd + f x.fst)
@[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₄) :
((e₁.skew_prod e₂ f).symm) x = ((e₁.symm) x.fst, (e₂.symm) (x.snd - f ((e₁.symm) x.fst)))
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) :
M × N →ₗ[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
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) :
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) :
(Σ (K : submodule R M), K ≃ₗ[R] M)

Auxiliary definition for tunnel.

Equations
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) :

Give an injective map f : M × N →ₗ[R] M we can find a nested sequence of submodules all isomorphic to M.

Equations
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 : ) :

Give an injective map f : M × N →ₗ[R] M we can find a sequence of submodules all isomorphic to N.

Equations
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 : ) :
(f.tailing i n) ≃ₗ[R] N

Each tailing f i n is a copy of N.

Equations
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 : ) :
f.tailing i n (f.tunnel i) 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 : ) :
disjoint (f.tailing i n) ((f.tunnel i) (n + 1))
theorem linear_map.tailing_sup_tunnel_succ_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 : ) :
f.tailing i n (f.tunnel i) (n + 1) (f.tunnel i) 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) :
submodule R M

The supremum of all the copies of N found inside the tunnel.

Equations
@[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) :
f.tailings i 0 = f.tailing i 0
@[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 : ) :
f.tailings i (n + 1) = f.tailings i n f.tailing i (n + 1)
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 : ) :
disjoint (f.tailings i n) ((f.tunnel i) (n + 1))
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 : ) :
disjoint (f.tailings i n) (f.tailing i (n + 1))