# mathlibdocumentation

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 #

• products in the domain:
• `linear_map.fst`
• `linear_map.snd`
• `linear_map.coprod`
• `linear_map.prod_ext`
• products in the codomain:
• `linear_map.inl`
• `linear_map.inr`
• `linear_map.prod`
• products in both domain and codomain:
• `linear_map.prod_map`
• `linear_equiv.prod_map`
• `linear_equiv.skew_prod`
def linear_map.fst (R : Type u) (M : Type v) (M₂ : Type w) [semiring R] [add_comm_monoid M₂] [ M] [ 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₂] [ M] [ 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₂] [ M] [ M₂] (x : M × M₂) :
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₂] [ M] [ M₂] (x : M × M₂) :
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₂] [ M] [ M₂] :
theorem linear_map.snd_surjective {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ 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₃] [ M] [ M₂] [ 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₃] [ M] [ M₂] [ M₃] (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) (i : M) :
(f.prod g) i = 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₃] [ M] [ M₂] [ M₃] (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) :
(f.prod g) = g
@[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₃] [ M] [ M₂] [ M₃] (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) :
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₃] [ M] [ M₂] [ M₃] (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) :
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₂] [ M] [ M₂] :
M M₂).prod 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_3) [semiring R] [semiring S] [add_comm_monoid M₂] [add_comm_monoid M₃] [ M] [ M₂] [ M₃] [ M₂] [ M₃] [ M₂] [ M₃] (f : (M →ₗ[R] M₂) × (M →ₗ[R] M₃)) :
= f.fst.prod f.snd
def linear_map.prod_equiv {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} (S : Type u_3) [semiring R] [semiring S] [add_comm_monoid M₂] [add_comm_monoid M₃] [ M] [ M₂] [ M₃] [ M₂] [ M₃] [ M₂] [ 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_3) [semiring R] [semiring S] [add_comm_monoid M₂] [add_comm_monoid M₃] [ M] [ M₂] [ M₃] [ M₂] [ M₃] [ M₂] [ M₃] (f : M →ₗ[R] M₂ × M₃) :
.symm) f = M₂ M₃).comp f, M₂ M₃).comp f)
def linear_map.inl (R : Type u) (M : Type v) (M₂ : Type w) [semiring R] [add_comm_monoid M₂] [ M] [ M₂] :
M →ₗ[R] M × M₂

The left injection into a product is a linear map.

Equations
• M₂ =
def linear_map.inr (R : Type u) (M : Type v) (M₂ : Type w) [semiring R] [add_comm_monoid M₂] [ M] [ M₂] :
M₂ →ₗ[R] M × M₂

The right injection into a product is a linear map.

Equations
• M₂ =
theorem linear_map.range_inl (R : Type u) (M : Type v) (M₂ : Type w) [semiring R] [add_comm_monoid M₂] [ M] [ M₂] :
theorem linear_map.ker_snd (R : Type u) (M : Type v) (M₂ : Type w) [semiring R] [add_comm_monoid M₂] [ M] [ M₂] :
theorem linear_map.range_inr (R : Type u) (M : Type v) (M₂ : Type w) [semiring R] [add_comm_monoid M₂] [ M] [ M₂] :
theorem linear_map.ker_fst (R : Type u) (M : Type v) (M₂ : Type w) [semiring R] [add_comm_monoid M₂] [ M] [ M₂] :
@[simp]
theorem linear_map.coe_inl {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] :
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₂] [ M] [ M₂] (x : M) :
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₂] [ M] [ M₂] :
M M₂) =
theorem linear_map.inr_apply {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (x : M₂) :
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₂] [ M] [ M₂] :
M₂ =
theorem linear_map.inr_eq_prod {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] :
M₂ =
theorem linear_map.inl_injective {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] :
theorem linear_map.inr_injective {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ 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₃] [ M] [ M₂] [ 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₃] [ M] [ M₂] [ 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₃] [ M] [ M₂] [ M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) :
(f.coprod g).comp 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₃] [ M] [ M₂] [ M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) :
(f.coprod g).comp 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₂] [ M] [ M₂] :
M M₂).coprod 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₄] [ M] [ M₂] [ M₃] [ 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₂] [ M] [ M₂] :
M₂ =
theorem linear_map.snd_eq_coprod {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] :
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₄] [ M] [ M₂] [ M₃] [ 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₃] [ M] [ M₂] [ M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) (S : M) (S' : M₂) :
submodule.map (f.coprod g) (S.prod S') = S'
@[simp]
theorem linear_map.coprod_equiv_apply {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} (S : Type u_3) [semiring R] [semiring S] [add_comm_monoid M₂] [add_comm_monoid M₃] [ M] [ M₂] [ M₃] [ M₃] [ 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_3) [semiring R] [semiring S] [add_comm_monoid M₂] [add_comm_monoid M₃] [ M] [ M₂] [ M₃] [ M₃] [ M₃] (f : M × M₂ →ₗ[R] M₃) :
.symm) f = (f.comp M M₂), f.comp M M₂))
def linear_map.coprod_equiv {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} (S : Type u_3) [semiring R] [semiring S] [add_comm_monoid M₂] [add_comm_monoid M₃] [ M] [ M₂] [ M₃] [ M₃] [ 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₃] [ M] [ M₂] [ M₃] {f g : M × M₂ →ₗ[R] M₃} :
f = g f.comp M M₂) = g.comp M M₂) f.comp M M₂) = g.comp 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₃] [ M] [ M₂] [ M₃] {f g : M × M₂ →ₗ[R] M₃} (hl : f.comp M M₂) = g.comp M M₂)) (hr : f.comp M M₂) = g.comp 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₄] [ M] [ M₂] [ M₃] [ 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₄] [ M] [ M₂] [ M₃] [ 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₄] [ M] [ M₂] [ M₃] [ M₄] (f : M →ₗ[R] M₂) (g : M₃ →ₗ[R] M₄) (S : M₂) (S' : M₄) :
submodule.comap (f.prod_map g) (S.prod S') = S).prod 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₄] [ M] [ M₂] [ M₃] [ M₄] (f : M →ₗ[R] M₂) (g : M₃ →ₗ[R] M₄) :
@[simp]
theorem linear_map.prod_map_id {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] :
@[simp]
theorem linear_map.prod_map_one {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] :
1.prod_map 1 = 1
theorem linear_map.prod_map_comp {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} {M₅ : Type u_1} {M₆ : Type u_2} [semiring R] [add_comm_monoid M₂] [add_comm_monoid M₃] [add_comm_monoid M₄] [add_comm_monoid M₅] [add_comm_monoid M₆] [ M] [ M₂] [ M₃] [ M₄] [ M₅] [ M₆] (f₁₂ : M →ₗ[R] M₂) (f₂₃ : M₂ →ₗ[R] M₃) (g₁₂ : M₄ →ₗ[R] M₅) (g₂₃ : M₅ →ₗ[R] M₆) :
(f₂₃.prod_map g₂₃).comp (f₁₂.prod_map g₁₂) = (f₂₃.comp f₁₂).prod_map (g₂₃.comp g₁₂)
theorem linear_map.prod_map_mul {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (f₁₂ f₂₃ : M →ₗ[R] M) (g₁₂ g₂₃ : M₂ →ₗ[R] M₂) :
f₂₃.prod_map g₂₃ * f₁₂.prod_map g₁₂ = (f₂₃ * f₁₂).prod_map (g₂₃ * g₁₂)
theorem linear_map.prod_map_add {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₄] [ M] [ M₂] [ M₃] [ M₄] (f₁ f₂ : M →ₗ[R] M₃) (g₁ g₂ : M₂ →ₗ[R] M₄) :
(f₁ + f₂).prod_map (g₁ + g₂) = f₁.prod_map g₁ + f₂.prod_map g₂
@[simp]
theorem linear_map.prod_map_zero {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₄] [ M] [ M₂] [ M₃] [ M₄] :
0.prod_map 0 = 0
@[simp]
theorem linear_map.prod_map_smul {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} (S : Type u_3) [semiring R] [semiring S] [add_comm_monoid M₂] [add_comm_monoid M₃] [add_comm_monoid M₄] [ M] [ M₂] [ M₃] [ M₄] [ M₃] [ M₄] [ M₃] [ M₄] (s : S) (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₄) :
(s f).prod_map (s g) = s f.prod_map g
def linear_map.prod_map_linear (R : Type u) (M : Type v) (M₂ : Type w) (M₃ : Type y) (M₄ : Type z) (S : Type u_3) [semiring R] [semiring S] [add_comm_monoid M₂] [add_comm_monoid M₃] [add_comm_monoid M₄] [ M] [ M₂] [ M₃] [ M₄] [ M₃] [ M₄] [ M₃] [ M₄] :
(M →ₗ[R] M₃) × (M₂ →ₗ[R] M₄) →ₗ[S] M × M₂ →ₗ[R] M₃ × M₄

`linear_map.prod_map` as a `linear_map`

Equations
@[simp]
theorem linear_map.prod_map_linear_apply (R : Type u) (M : Type v) (M₂ : Type w) (M₃ : Type y) (M₄ : Type z) (S : Type u_3) [semiring R] [semiring S] [add_comm_monoid M₂] [add_comm_monoid M₃] [add_comm_monoid M₄] [ M] [ M₂] [ M₃] [ M₄] [ M₃] [ M₄] [ M₃] [ M₄] (f : (M →ₗ[R] M₃) × (M₂ →ₗ[R] M₄)) :
M₂ M₃ M₄ S) f = f.fst.prod_map f.snd
@[simp]
theorem linear_map.prod_map_ring_hom_apply (R : Type u) (M : Type v) (M₂ : Type w) [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (f : (M →ₗ[R] M) × (M₂ →ₗ[R] M₂)) :
M₂) f = f.fst.prod_map f.snd
def linear_map.prod_map_ring_hom (R : Type u) (M : Type v) (M₂ : Type w) [semiring R] [add_comm_monoid M₂] [ M] [ M₂] :
(M →ₗ[R] M) × (M₂ →ₗ[R] M₂) →+* M × M₂ →ₗ[R] M × M₂

`linear_map.prod_map` as a `ring_hom`

Equations
theorem linear_map.inl_map_mul {R : Type u} [semiring R] {A : Type u_4} [ A] {B : Type u_5} [ B] (a₁ a₂ : A) :
A B) (a₁ * a₂) = A B) a₁ * A B) a₂
theorem linear_map.inr_map_mul {R : Type u} [semiring R] {A : Type u_4} [ A] {B : Type u_5} [ B] (b₁ b₂ : B) :
A B) (b₁ * b₂) = A B) b₁ * A B) b₂
@[simp]
theorem linear_map.prod_map_alg_hom_apply (R : Type u) (M : Type v) (M₂ : Type w) [add_comm_monoid M₂] [ M] [ M₂] (ᾰ : (M →ₗ[R] M) × (M₂ →ₗ[R] M₂)) :
M₂) = M₂).to_fun
def linear_map.prod_map_alg_hom (R : Type u) (M : Type v) (M₂ : Type w) [add_comm_monoid M₂] [ M] [ M₂] :
M × M₂ →ₐ[R] (M × M₂)

`linear_map.prod_map` as an `algebra_hom`

Equations
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₃] [ M] [ M₂] [ 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₂] [ M] [ M₂] :
theorem linear_map.sup_range_inl_inr {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] :
theorem linear_map.disjoint_inl_inr {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ 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₃] [ M] [ M₂] [ M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) (p : M) (q : 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₃] [ M] [ M₂] [ M₃] (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) (p : M₂) (q : M₃) :
theorem linear_map.prod_eq_inf_comap {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (p : M) (q : M₂) :
p.prod q = submodule.comap M M₂) p submodule.comap 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₂] [ M] [ M₂] (p : M) (q : M₂) :
p.prod q = submodule.map M M₂) p submodule.map 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₂] [ M] [ M₂] {s : set M} {t : set M₂} :
( M M₂) '' s M M₂) '' t) = s).prod 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₃] [ M] [ M₂] [ 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₃] [ M] [ M₂] [ 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] [ M] {M₂ : Type u_1} [add_comm_group M₂] [ M₂] {M₃ : Type u_2} [add_comm_group M₃] [ 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] [ M] {M₂ : Type u_1} [add_comm_group M₂] [ M₂] {M₃ : Type u_2} [add_comm_group M₃] [ M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) (hd : ) :
theorem submodule.sup_eq_range {R : Type u} {M : Type v} [semiring R] [ M] (p q : M) :
p q =
@[simp]
theorem submodule.map_inl {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (p : M) :
submodule.map 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₂] [ M] [ M₂] (q : M₂) :
submodule.map 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₂] [ M] [ M₂] (p : M) :
@[simp]
theorem submodule.comap_snd {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (q : M₂) :
@[simp]
theorem submodule.prod_comap_inl {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (p : M) (q : M₂) :
submodule.comap 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₂] [ M] [ M₂] (p : M) (q : M₂) :
submodule.comap 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₂] [ M] [ M₂] (p : M) (q : M₂) :
submodule.map 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₂] [ M] [ M₂] (p : M) (q : M₂) :
submodule.map 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₂] [ M] [ M₂] :
@[simp]
theorem submodule.ker_inr {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] :
@[simp]
theorem submodule.range_fst {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] :
@[simp]
theorem submodule.range_snd {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] :
def submodule.fst (R : Type u) (M : Type v) (M₂ : Type w) [semiring R] [add_comm_monoid M₂] [ M] [ M₂] :
(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₂] [ M] [ M₂] (m : M) :
( 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₂] [ M] [ M₂] :
M M₂) ≃ₗ[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₂] [ M] [ M₂] (x : M 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₂] [ M] [ M₂] :
submodule.map M M₂) M M₂) =
theorem submodule.fst_map_snd (R : Type u) (M : Type v) (M₂ : Type w) [semiring R] [add_comm_monoid M₂] [ M] [ M₂] :
submodule.map M M₂) M M₂) =
def submodule.snd (R : Type u) (M : Type v) (M₂ : Type w) [semiring R] [add_comm_monoid M₂] [ M] [ M₂] :
(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₂] [ M] [ M₂] (x : M 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₂] [ M] [ M₂] (n : M₂) :
( 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₂] [ M] [ M₂] :
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₂] [ M] [ M₂] :
submodule.map M M₂) M M₂) =
theorem submodule.snd_map_snd (R : Type u) (M : Type v) (M₂ : Type w) [semiring R] [add_comm_monoid M₂] [ M] [ M₂] :
submodule.map M M₂) M M₂) =
theorem submodule.fst_sup_snd (R : Type u) (M : Type v) (M₂ : Type w) [semiring R] [add_comm_monoid M₂] [ M] [ M₂] :
M₂ M₂ =
theorem submodule.fst_inf_snd (R : Type u) (M : Type v) (M₂ : Type w) [semiring R] [add_comm_monoid M₂] [ M] [ M₂] :
M₂ M₂ =
theorem submodule.le_prod_iff (R : Type u) (M : Type v) (M₂ : Type w) [semiring R] [add_comm_monoid M₂] [ M] [ M₂] {p₁ : M} {p₂ : M₂} {q : (M × M₂)} :
q p₁.prod p₂ submodule.map M M₂) q p₁ submodule.map M M₂) q p₂
theorem submodule.prod_le_iff (R : Type u) (M : Type v) (M₂ : Type w) [semiring R] [add_comm_monoid M₂] [ M] [ M₂] {p₁ : M} {p₂ : M₂} {q : (M × M₂)} :
p₁.prod p₂ q submodule.map M M₂) p₁ q submodule.map 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₂] [ M] [ M₂] {p₁ : M} {p₂ : 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₂] [ M] [ M₂] {p₁ : M} {p₂ : 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] [ M] [ N] (ᾰ : M × N) :
N) = ᾰ.swap
def linear_equiv.prod_comm (R : Type u_1) (M : Type u_2) (N : Type u_3) [semiring R] [ M] [ 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₄] {module_M : M} {module_M₂ : M₂} {module_M₃ : M₃} {module_M₄ : 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₄] {module_M : M} {module_M₂ : M₂} {module_M₃ : M₃} {module_M₄ : 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₄] {module_M : M} {module_M₂ : M₂} {module_M₃ : M₃} {module_M₄ : 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₄] {module_M : M} {module_M₂ : M₂} {module_M₃ : M₃} {module_M₄ : 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_group M₄] {module_M : M} {module_M₂ : M₂} {module_M₃ : M₃} {module_M₄ : 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_group M₄] {module_M : M} {module_M₂ : M₂} {module_M₃ : M₃} {module_M₄ : 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_group M₄] {module_M : M} {module_M₂ : M₂} {module_M₃ : M₃} {module_M₄ : 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₃] [ M] [ M₂] [ M₃] {f : M →ₗ[R] M₂} {g : M →ₗ[R] M₃} (h : = ) :

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_3} [ M] [ N] (f : M × N →ₗ[R] M) (Kφ : Σ (K : 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_3} [ M] [ N] (f : M × N →ₗ[R] M) (i : function.injective f) (Kφ : Σ (K : M), K ≃ₗ[R] M) :
noncomputable def linear_map.tunnel' {R : Type u} {M : Type v} [ring R] {N : Type u_3} [ M] [ N] (f : M × N →ₗ[R] M) (i : function.injective f) :
(Σ (K : 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_3} [ M] [ 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_3} [ M] [ N] (f : M × N →ₗ[R] M) (i : function.injective f) (n : ) :
M

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_3} [ M] [ 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_3} [ M] [ 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_3} [ M] [ N] (f : M × N →ₗ[R] M) (i : function.injective f) (n : ) :
theorem linear_map.tailing_sup_tunnel_succ_le_tunnel {R : Type u} {M : Type v} [ring R] {N : Type u_3} [ M] [ 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_3} [ M] [ N] (f : M × N →ₗ[R] M) (i : function.injective f) :
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_3} [ M] [ 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_3} [ M] [ 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_3} [ M] [ 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_3} [ M] [ N] (f : M × N →ₗ[R] M) (i : function.injective f) (n : ) :
disjoint (f.tailings i n) (f.tailing i (n + 1))
def linear_map.graph {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (f : M →ₗ[R] M₂) :
(M × M₂)

Graph of a linear map.

Equations
@[simp]
theorem linear_map.mem_graph_iff {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (f : M →ₗ[R] M₂) (x : M × M₂) :
x f.graph x.snd = f x.fst
theorem linear_map.graph_eq_ker_coprod {R : Type u} {M₃ : Type y} {M₄ : Type z} [semiring R] [add_comm_group M₃] [add_comm_group M₄] [ M₃] [ M₄] (g : M₃ →ₗ[R] M₄) :
g.graph =
theorem linear_map.graph_eq_range_prod {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (f : M →ₗ[R] M₂) :