mathlib documentation

linear_algebra.prod

Products of semimodules #

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₂] [semimodule R M] [semimodule 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₂] [semimodule R M] [semimodule 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₂] [semimodule R M] [semimodule R M₂] (x : M × M₂) :
(linear_map.fst R M M₂) x = x.fst
@[simp]
theorem linear_map.snd_apply {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (x : M × M₂) :
(linear_map.snd R M M₂) x = x.snd
def linear_map.prod {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) :
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₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) (x : M) :
(f.prod g) x = (f x, g x)
@[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₂] :
@[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₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] [semimodule S M₂] [semimodule 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₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] [semimodule S M₂] [semimodule 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₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] [semimodule S M₂] [semimodule 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₂] [semimodule R M] [semimodule 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₂] [semimodule R M] [semimodule R M₂] :
M₂ →ₗ[R] M × M₂

The right injection into a product is a linear map.

Equations
@[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_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₂] :
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₂] :
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₂] :
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₂] :
def linear_map.coprod {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) :
M × M₂ →ₗ[R] M₃

The coprod function λ x : M × M₂, f.1 x.1 + f.2 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₃] [semimodule R M] [semimodule R M₂] [semimodule 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₃] [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₂] :
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₄] [semimodule R M] [semimodule R M₂] [semimodule R M₃] [semimodule 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₂] [semimodule R M] [semimodule 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₂] [semimodule R M] [semimodule 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₄] [semimodule R M] [semimodule R M₂] [semimodule R M₃] [semimodule 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_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₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] [semimodule 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₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] [semimodule 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₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] [semimodule 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₃] [semimodule R M] [semimodule R M₂] [semimodule 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₃] [semimodule R M] [semimodule R M₂] [semimodule 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₄] [semimodule R M] [semimodule R M₂] [semimodule R M₃] [semimodule 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₄] [semimodule R M] [semimodule R M₂] [semimodule R M₃] [semimodule 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.range_coprod {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) :
theorem linear_map.is_compl_range_inl_inr {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :
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₂] :
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₂] :
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₂) :
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₃) :
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₂) :
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₂) :
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₂} :
@[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₃) :
(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₃] [semimodule R M] [semimodule R M₂] [semimodule 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] [semimodule R M] {M₂ : Type u_1} [add_comm_group M₂] [semimodule R M₂] {M₃ : Type u_2} [add_comm_group M₃] [semimodule 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] [semimodule R M] {M₂ : Type u_1} [add_comm_group M₂] [semimodule R M₂] {M₃ : Type u_2} [add_comm_group M₃] [semimodule 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] [semimodule 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₂] [semimodule R M] [semimodule 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₂] [semimodule R M] [semimodule 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₂] [semimodule R M] [semimodule 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₂] [semimodule R M] [semimodule 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₂] [semimodule R M] [semimodule 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₂] [semimodule R M] [semimodule 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₂] [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} [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} [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} [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} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule 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₂] [semimodule R M] [semimodule R M₂] :
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₄} (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₄] {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₄) :
(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₄] {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₃) :
(e₁.prod e₂) p = (e₁ p.fst, e₂ p.snd)
@[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₄) :
(e₁.prod e₂) = e₁.prod_map e₂
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₄] {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₄) :
(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₄] {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₃) :
(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₄] {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₄) :
((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₃] [semimodule R M] [semimodule R M₂] [semimodule 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.