# Documentation

## Mathlib.LinearAlgebra.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, LinearMap.range, and LinearMap.ker.

## Main definitions #

• products in the domain:
• LinearMap.fst
• LinearMap.snd
• LinearMap.coprod
• LinearMap.prod_ext
• products in the codomain:
• LinearMap.inl
• LinearMap.inr
• LinearMap.prod
• products in both domain and codomain:
• LinearMap.prodMap
• LinearEquiv.prodMap
• LinearEquiv.skewProd
def LinearMap.fst (R : Type u) (M : Type v) (M₂ : Type w) [] [] [] [Module R M] [Module R M₂] :
M × M₂ →ₗ[R] M

The first projection of a product is a linear map.

Equations
• LinearMap.fst R M M₂ = { toFun := Prod.fst, map_add' := , map_smul' := }
Instances For
def LinearMap.snd (R : Type u) (M : Type v) (M₂ : Type w) [] [] [] [Module R M] [Module R M₂] :
M × M₂ →ₗ[R] M₂

The second projection of a product is a linear map.

Equations
• LinearMap.snd R M M₂ = { toFun := Prod.snd, map_add' := , map_smul' := }
Instances For
@[simp]
theorem LinearMap.fst_apply {R : Type u} {M : Type v} {M₂ : Type w} [] [] [] [Module R M] [Module R M₂] (x : M × M₂) :
(LinearMap.fst R M M₂) x = x.1
@[simp]
theorem LinearMap.snd_apply {R : Type u} {M : Type v} {M₂ : Type w} [] [] [] [Module R M] [Module R M₂] (x : M × M₂) :
(LinearMap.snd R M M₂) x = x.2
theorem LinearMap.fst_surjective {R : Type u} {M : Type v} {M₂ : Type w} [] [] [] [Module R M] [Module R M₂] :
theorem LinearMap.snd_surjective {R : Type u} {M : Type v} {M₂ : Type w} [] [] [] [Module R M] [Module R M₂] :
@[simp]
theorem LinearMap.prod_apply {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [] [] [] [] [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
def LinearMap.prod {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [] [] [] [] [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
• f.prod g = { toFun := Pi.prod f g, map_add' := , map_smul' := }
Instances For
theorem LinearMap.coe_prod {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [] [] [] [] [Module R M] [Module R M₂] [Module R M₃] (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) :
(f.prod g) = Pi.prod f g
@[simp]
theorem LinearMap.fst_prod {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [] [] [] [] [Module R M] [Module R M₂] [Module R M₃] (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) :
LinearMap.fst R M₂ M₃ ∘ₗ f.prod g = f
@[simp]
theorem LinearMap.snd_prod {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [] [] [] [] [Module R M] [Module R M₂] [Module R M₃] (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) :
LinearMap.snd R M₂ M₃ ∘ₗ f.prod g = g
@[simp]
theorem LinearMap.pair_fst_snd {R : Type u} {M : Type v} {M₂ : Type w} [] [] [] [Module R M] [Module R M₂] :
(LinearMap.fst R M M₂).prod (LinearMap.snd R M M₂) = LinearMap.id
theorem LinearMap.prod_comp {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [] [] [] [] [] [Module R M] [Module R M₂] [Module R M₃] [Module R M₄] (f : M₂ →ₗ[R] M₃) (g : M₂ →ₗ[R] M₄) (h : M →ₗ[R] M₂) :
f.prod g ∘ₗ h = (f ∘ₗ h).prod (g ∘ₗ h)
@[simp]
theorem LinearMap.prodEquiv_symm_apply {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} (S : Type u_3) [] [] [] [] [] [Module R M] [Module R M₂] [Module R M₃] [Module S M₂] [Module S M₃] [SMulCommClass R S M₂] [SMulCommClass R S M₃] (f : M →ₗ[R] M₂ × M₃) :
.symm f = (LinearMap.fst R M₂ M₃ ∘ₗ f, LinearMap.snd R M₂ M₃ ∘ₗ f)
@[simp]
theorem LinearMap.prodEquiv_apply {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} (S : Type u_3) [] [] [] [] [] [Module R M] [Module R M₂] [Module R M₃] [Module S M₂] [Module S M₃] [SMulCommClass R S M₂] [SMulCommClass R S M₃] (f : (M →ₗ[R] M₂) × (M →ₗ[R] M₃)) :
f = f.1.prod f.2
def LinearMap.prodEquiv {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} (S : Type u_3) [] [] [] [] [] [Module R M] [Module R M₂] [Module R M₃] [Module S M₂] [Module S M₃] [SMulCommClass R S M₂] [SMulCommClass 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
• One or more equations did not get rendered due to their size.
Instances For
def LinearMap.inl (R : Type u) (M : Type v) (M₂ : Type w) [] [] [] [Module R M] [Module R M₂] :
M →ₗ[R] M × M₂

The left injection into a product is a linear map.

Equations
Instances For
def LinearMap.inr (R : Type u) (M : Type v) (M₂ : Type w) [] [] [] [Module R M] [Module R M₂] :
M₂ →ₗ[R] M × M₂

The right injection into a product is a linear map.

Equations
Instances For
theorem LinearMap.range_inl (R : Type u) (M : Type v) (M₂ : Type w) [] [] [] [Module R M] [Module R M₂] :
theorem LinearMap.ker_snd (R : Type u) (M : Type v) (M₂ : Type w) [] [] [] [Module R M] [Module R M₂] :
theorem LinearMap.range_inr (R : Type u) (M : Type v) (M₂ : Type w) [] [] [] [Module R M] [Module R M₂] :
theorem LinearMap.ker_fst (R : Type u) (M : Type v) (M₂ : Type w) [] [] [] [Module R M] [Module R M₂] :
@[simp]
theorem LinearMap.fst_comp_inl (R : Type u) (M : Type v) (M₂ : Type w) [] [] [] [Module R M] [Module R M₂] :
LinearMap.fst R M M₂ ∘ₗ LinearMap.inl R M M₂ = LinearMap.id
@[simp]
theorem LinearMap.snd_comp_inl (R : Type u) (M : Type v) (M₂ : Type w) [] [] [] [Module R M] [Module R M₂] :
LinearMap.snd R M M₂ ∘ₗ LinearMap.inl R M M₂ = 0
@[simp]
theorem LinearMap.fst_comp_inr (R : Type u) (M : Type v) (M₂ : Type w) [] [] [] [Module R M] [Module R M₂] :
LinearMap.fst R M M₂ ∘ₗ LinearMap.inr R M M₂ = 0
@[simp]
theorem LinearMap.snd_comp_inr (R : Type u) (M : Type v) (M₂ : Type w) [] [] [] [Module R M] [Module R M₂] :
LinearMap.snd R M M₂ ∘ₗ LinearMap.inr R M M₂ = LinearMap.id
@[simp]
theorem LinearMap.coe_inl {R : Type u} {M : Type v} {M₂ : Type w} [] [] [] [Module R M] [Module R M₂] :
(LinearMap.inl R M M₂) = fun (x : M) => (x, 0)
theorem LinearMap.inl_apply {R : Type u} {M : Type v} {M₂ : Type w} [] [] [] [Module R M] [Module R M₂] (x : M) :
(LinearMap.inl R M M₂) x = (x, 0)
@[simp]
theorem LinearMap.coe_inr {R : Type u} {M : Type v} {M₂ : Type w} [] [] [] [Module R M] [Module R M₂] :
(LinearMap.inr R M M₂) =
theorem LinearMap.inr_apply {R : Type u} {M : Type v} {M₂ : Type w} [] [] [] [Module R M] [Module R M₂] (x : M₂) :
(LinearMap.inr R M M₂) x = (0, x)
theorem LinearMap.inl_eq_prod {R : Type u} {M : Type v} {M₂ : Type w} [] [] [] [Module R M] [Module R M₂] :
LinearMap.inl R M M₂ = LinearMap.id.prod 0
theorem LinearMap.inr_eq_prod {R : Type u} {M : Type v} {M₂ : Type w} [] [] [] [Module R M] [Module R M₂] :
LinearMap.inr R M M₂ = LinearMap.prod 0 LinearMap.id
theorem LinearMap.inl_injective {R : Type u} {M : Type v} {M₂ : Type w} [] [] [] [Module R M] [Module R M₂] :
theorem LinearMap.inr_injective {R : Type u} {M : Type v} {M₂ : Type w} [] [] [] [Module R M] [Module R M₂] :
def LinearMap.coprod {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [] [] [] [] [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
Instances For
@[simp]
theorem LinearMap.coprod_apply {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [] [] [] [] [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.1 + g x.2
@[simp]
theorem LinearMap.coprod_inl {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [] [] [] [] [Module R M] [Module R M₂] [Module R M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) :
f.coprod g ∘ₗ LinearMap.inl R M M₂ = f
@[simp]
theorem LinearMap.coprod_inr {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [] [] [] [] [Module R M] [Module R M₂] [Module R M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) :
f.coprod g ∘ₗ LinearMap.inr R M M₂ = g
@[simp]
theorem LinearMap.coprod_inl_inr {R : Type u} {M : Type v} {M₂ : Type w} [] [] [] [Module R M] [Module R M₂] :
(LinearMap.inl R M M₂).coprod (LinearMap.inr R M M₂) = LinearMap.id
theorem LinearMap.coprod_zero_left {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [] [] [] [] [Module R M] [Module R M₂] [Module R M₃] (g : M₂ →ₗ[R] M₃) :
= g ∘ₗ LinearMap.snd R M M₂
theorem LinearMap.coprod_zero_right {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [] [] [] [] [Module R M] [Module R M₂] [Module R M₃] (f : M →ₗ[R] M₃) :
f.coprod 0 = f ∘ₗ LinearMap.fst R M M₂
theorem LinearMap.comp_coprod {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [] [] [] [] [] [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 ∘ₗ g₁.coprod g₂ = (f ∘ₗ g₁).coprod (f ∘ₗ g₂)
theorem LinearMap.fst_eq_coprod {R : Type u} {M : Type v} {M₂ : Type w} [] [] [] [Module R M] [Module R M₂] :
LinearMap.fst R M M₂ = LinearMap.id.coprod 0
theorem LinearMap.snd_eq_coprod {R : Type u} {M : Type v} {M₂ : Type w} [] [] [] [Module R M] [Module R M₂] :
LinearMap.snd R M M₂ = LinearMap.coprod 0 LinearMap.id
@[simp]
theorem LinearMap.coprod_comp_prod {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [] [] [] [] [] [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 ∘ₗ f'.prod g' = f ∘ₗ f' + g ∘ₗ g'
@[simp]
theorem LinearMap.coprod_map_prod {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [] [] [] [] [Module R M] [Module R M₂] [Module R M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) (S : ) (S' : Submodule R M₂) :
Submodule.map (f.coprod g) (S.prod S') =
@[simp]
theorem LinearMap.coprodEquiv_apply {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} (S : Type u_3) [] [] [] [] [] [Module R M] [Module R M₂] [Module R M₃] [Module S M₃] [SMulCommClass R S M₃] (f : (M →ₗ[R] M₃) × (M₂ →ₗ[R] M₃)) :
= f.1.coprod f.2
@[simp]
theorem LinearMap.coprodEquiv_symm_apply {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} (S : Type u_3) [] [] [] [] [] [Module R M] [Module R M₂] [Module R M₃] [Module S M₃] [SMulCommClass R S M₃] (f : M × M₂ →ₗ[R] M₃) :
.symm f = (f ∘ₗ LinearMap.inl R M M₂, f ∘ₗ LinearMap.inr R M M₂)
def LinearMap.coprodEquiv {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} (S : Type u_3) [] [] [] [] [] [Module R M] [Module R M₂] [Module R M₃] [Module S M₃] [SMulCommClass 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
• One or more equations did not get rendered due to their size.
Instances For
theorem LinearMap.prod_ext_iff {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [] [] [] [] [Module R M] [Module R M₂] [Module R M₃] {f : M × M₂ →ₗ[R] M₃} {g : M × M₂ →ₗ[R] M₃} :
f = g f ∘ₗ LinearMap.inl R M M₂ = g ∘ₗ LinearMap.inl R M M₂ f ∘ₗ LinearMap.inr R M M₂ = g ∘ₗ LinearMap.inr R M M₂
theorem LinearMap.prod_ext {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [] [] [] [] [Module R M] [Module R M₂] [Module R M₃] {f : M × M₂ →ₗ[R] M₃} {g : M × M₂ →ₗ[R] M₃} (hl : f ∘ₗ LinearMap.inl R M M₂ = g ∘ₗ LinearMap.inl R M M₂) (hr : f ∘ₗ LinearMap.inr R M M₂ = g ∘ₗ LinearMap.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 LinearMap.prodMap {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [] [] [] [] [] [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
Instances For
theorem LinearMap.coe_prodMap {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [] [] [] [] [] [Module R M] [Module R M₂] [Module R M₃] [Module R M₄] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₄) :
(f.prodMap g) = Prod.map f g
@[simp]
theorem LinearMap.prodMap_apply {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [] [] [] [] [] [Module R M] [Module R M₂] [Module R M₃] [Module R M₄] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₄) (x : M × M₂) :
(f.prodMap g) x = (f x.1, g x.2)
theorem LinearMap.prodMap_comap_prod {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [] [] [] [] [] [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.prodMap g) (S.prod S') = ().prod ()
theorem LinearMap.ker_prodMap {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [] [] [] [] [] [Module R M] [Module R M₂] [Module R M₃] [Module R M₄] (f : M →ₗ[R] M₂) (g : M₃ →ₗ[R] M₄) :
LinearMap.ker (f.prodMap g) = ().prod ()
@[simp]
theorem LinearMap.prodMap_id {R : Type u} {M : Type v} {M₂ : Type w} [] [] [] [Module R M] [Module R M₂] :
LinearMap.id.prodMap LinearMap.id = LinearMap.id
@[simp]
theorem LinearMap.prodMap_one {R : Type u} {M : Type v} {M₂ : Type w} [] [] [] [Module R M] [Module R M₂] :
= 1
theorem LinearMap.prodMap_comp {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} {M₅ : Type u_1} {M₆ : Type u_2} [] [] [] [] [] [] [] [Module R M] [Module R M₂] [Module R M₃] [Module R M₄] [Module R M₅] [Module R M₆] (f₁₂ : M →ₗ[R] M₂) (f₂₃ : M₂ →ₗ[R] M₃) (g₁₂ : M₄ →ₗ[R] M₅) (g₂₃ : M₅ →ₗ[R] M₆) :
f₂₃.prodMap g₂₃ ∘ₗ f₁₂.prodMap g₁₂ = (f₂₃ ∘ₗ f₁₂).prodMap (g₂₃ ∘ₗ g₁₂)
theorem LinearMap.prodMap_mul {R : Type u} {M : Type v} {M₂ : Type w} [] [] [] [Module R M] [Module R M₂] (f₁₂ : M →ₗ[R] M) (f₂₃ : M →ₗ[R] M) (g₁₂ : M₂ →ₗ[R] M₂) (g₂₃ : M₂ →ₗ[R] M₂) :
f₂₃.prodMap g₂₃ * f₁₂.prodMap g₁₂ = (f₂₃ * f₁₂).prodMap (g₂₃ * g₁₂)
theorem LinearMap.prodMap_add {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [] [] [] [] [] [Module R M] [Module R M₂] [Module R M₃] [Module R M₄] (f₁ : M →ₗ[R] M₃) (f₂ : M →ₗ[R] M₃) (g₁ : M₂ →ₗ[R] M₄) (g₂ : M₂ →ₗ[R] M₄) :
(f₁ + f₂).prodMap (g₁ + g₂) = f₁.prodMap g₁ + f₂.prodMap g₂
@[simp]
theorem LinearMap.prodMap_zero {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [] [] [] [] [] [Module R M] [Module R M₂] [Module R M₃] [Module R M₄] :
= 0
@[simp]
theorem LinearMap.prodMap_smul {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} (S : Type u_3) [] [] [] [] [] [] [Module R M] [Module R M₂] [Module R M₃] [Module R M₄] [Module S M₃] [Module S M₄] [SMulCommClass R S M₃] [SMulCommClass R S M₄] (s : S) (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₄) :
(s f).prodMap (s g) = s f.prodMap g
@[simp]
theorem LinearMap.prodMapLinear_apply (R : Type u) (M : Type v) (M₂ : Type w) (M₃ : Type y) (M₄ : Type z) (S : Type u_3) [] [] [] [] [] [] [Module R M] [Module R M₂] [Module R M₃] [Module R M₄] [Module S M₃] [Module S M₄] [SMulCommClass R S M₃] [SMulCommClass R S M₄] (f : (M →ₗ[R] M₃) × (M₂ →ₗ[R] M₄)) :
(LinearMap.prodMapLinear R M M₂ M₃ M₄ S) f = f.1.prodMap f.2
def LinearMap.prodMapLinear (R : Type u) (M : Type v) (M₂ : Type w) (M₃ : Type y) (M₄ : Type z) (S : Type u_3) [] [] [] [] [] [] [Module R M] [Module R M₂] [Module R M₃] [Module R M₄] [Module S M₃] [Module S M₄] [SMulCommClass R S M₃] [SMulCommClass R S M₄] :
(M →ₗ[R] M₃) × (M₂ →ₗ[R] M₄) →ₗ[S] M × M₂ →ₗ[R] M₃ × M₄

LinearMap.prodMap as a LinearMap

Equations
Instances For
@[simp]
theorem LinearMap.prodMapRingHom_apply (R : Type u) (M : Type v) (M₂ : Type w) [] [] [] [Module R M] [Module R M₂] (f : (M →ₗ[R] M) × (M₂ →ₗ[R] M₂)) :
() f = f.1.prodMap f.2
def LinearMap.prodMapRingHom (R : Type u) (M : Type v) (M₂ : Type w) [] [] [] [Module R M] [Module R M₂] :
(M →ₗ[R] M) × (M₂ →ₗ[R] M₂) →+* M × M₂ →ₗ[R] M × M₂

LinearMap.prodMap as a RingHom

Equations
• = { toFun := fun (f : (M →ₗ[R] M) × (M₂ →ₗ[R] M₂)) => f.1.prodMap f.2, map_one' := , map_mul' := , map_zero' := , map_add' := }
Instances For
theorem LinearMap.inl_map_mul {R : Type u} [] {A : Type u_4} [Module R A] {B : Type u_5} [Module R B] (a₁ : A) (a₂ : A) :
() (a₁ * a₂) = () a₁ * () a₂
theorem LinearMap.inr_map_mul {R : Type u} [] {A : Type u_4} [Module R A] {B : Type u_5} [Module R B] (b₁ : B) (b₂ : B) :
() (b₁ * b₂) = () b₁ * () b₂
@[simp]
theorem LinearMap.prodMapAlgHom_apply_apply (R : Type u) (M : Type v) (M₂ : Type w) [] [] [] [Module R M] [Module R M₂] (f : (M →ₗ[R] M) × (M₂ →ₗ[R] M₂)) (i : M × M₂) :
(() f) i = (f.1 i.1, f.2 i.2)
def LinearMap.prodMapAlgHom (R : Type u) (M : Type v) (M₂ : Type w) [] [] [] [Module R M] [Module R M₂] :
× Module.End R M₂ →ₐ[R] Module.End R (M × M₂)

LinearMap.prodMap as an AlgHom

Equations
• = let __src := ; { toRingHom := __src, commutes' := }
Instances For
theorem LinearMap.range_coprod {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [] [] [] [] [Module R M] [Module R M₂] [Module R M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) :
LinearMap.range (f.coprod g) =
theorem LinearMap.isCompl_range_inl_inr {R : Type u} {M : Type v} {M₂ : Type w} [] [] [] [Module R M] [Module R M₂] :
theorem LinearMap.sup_range_inl_inr {R : Type u} {M : Type v} {M₂ : Type w} [] [] [] [Module R M] [Module R M₂] :
theorem LinearMap.disjoint_inl_inr {R : Type u} {M : Type v} {M₂ : Type w} [] [] [] [Module R M] [Module R M₂] :
theorem LinearMap.map_coprod_prod {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [] [] [] [] [Module R M] [Module R M₂] [Module R M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) (p : ) (q : Submodule R M₂) :
Submodule.map (f.coprod g) (p.prod q) =
theorem LinearMap.comap_prod_prod {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [] [] [] [] [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) =
theorem LinearMap.prod_eq_inf_comap {R : Type u} {M : Type v} {M₂ : Type w} [] [] [] [Module R M] [Module R M₂] (p : ) (q : Submodule R M₂) :
p.prod q = Submodule.comap (LinearMap.fst R M M₂) p Submodule.comap (LinearMap.snd R M M₂) q
theorem LinearMap.prod_eq_sup_map {R : Type u} {M : Type v} {M₂ : Type w} [] [] [] [Module R M] [Module R M₂] (p : ) (q : Submodule R M₂) :
p.prod q = Submodule.map (LinearMap.inl R M M₂) p Submodule.map (LinearMap.inr R M M₂) q
theorem LinearMap.span_inl_union_inr {R : Type u} {M : Type v} {M₂ : Type w} [] [] [] [Module R M] [Module R M₂] {s : Set M} {t : Set M₂} :
Submodule.span R ((LinearMap.inl R M M₂) '' s (LinearMap.inr R M M₂) '' t) = ().prod ()
@[simp]
theorem LinearMap.ker_prod {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [] [] [] [] [Module R M] [Module R M₂] [Module R M₃] (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) :
LinearMap.ker (f.prod g) =
theorem LinearMap.range_prod_le {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [] [] [] [] [Module R M] [Module R M₂] [Module R M₃] (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) :
LinearMap.range (f.prod g) ().prod ()
theorem LinearMap.ker_prod_ker_le_ker_coprod {R : Type u} {M : Type v} [] [] [Module R M] {M₂ : Type u_3} [] [Module R M₂] {M₃ : Type u_4} [] [Module R M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) :
().prod () LinearMap.ker (f.coprod g)
theorem LinearMap.ker_coprod_of_disjoint_range {R : Type u} {M : Type v} [] [] [Module R M] {M₂ : Type u_3} [] [Module R M₂] {M₃ : Type u_4} [] [Module R M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) (hd : ) :
LinearMap.ker (f.coprod g) = ().prod ()
theorem Submodule.sup_eq_range {R : Type u} {M : Type v} [] [] [Module R M] (p : ) (q : ) :
p q = LinearMap.range (p.subtype.coprod q.subtype)
@[simp]
theorem Submodule.map_inl {R : Type u} {M : Type v} {M₂ : Type w} [] [] [] [Module R M] [Module R M₂] (p : ) :
Submodule.map (LinearMap.inl R M M₂) p = p.prod
@[simp]
theorem Submodule.map_inr {R : Type u} {M : Type v} {M₂ : Type w} [] [] [] [Module R M] [Module R M₂] (q : Submodule R M₂) :
Submodule.map (LinearMap.inr R M M₂) q = .prod q
@[simp]
theorem Submodule.comap_fst {R : Type u} {M : Type v} {M₂ : Type w} [] [] [] [Module R M] [Module R M₂] (p : ) :
Submodule.comap (LinearMap.fst R M M₂) p = p.prod
@[simp]
theorem Submodule.comap_snd {R : Type u} {M : Type v} {M₂ : Type w} [] [] [] [Module R M] [Module R M₂] (q : Submodule R M₂) :
Submodule.comap (LinearMap.snd R M M₂) q = .prod q
@[simp]
theorem Submodule.prod_comap_inl {R : Type u} {M : Type v} {M₂ : Type w} [] [] [] [Module R M] [Module R M₂] (p : ) (q : Submodule R M₂) :
Submodule.comap (LinearMap.inl R M M₂) (p.prod q) = p
@[simp]
theorem Submodule.prod_comap_inr {R : Type u} {M : Type v} {M₂ : Type w} [] [] [] [Module R M] [Module R M₂] (p : ) (q : Submodule R M₂) :
Submodule.comap (LinearMap.inr R M M₂) (p.prod q) = q
@[simp]
theorem Submodule.prod_map_fst {R : Type u} {M : Type v} {M₂ : Type w} [] [] [] [Module R M] [Module R M₂] (p : ) (q : Submodule R M₂) :
Submodule.map (LinearMap.fst R M M₂) (p.prod q) = p
@[simp]
theorem Submodule.prod_map_snd {R : Type u} {M : Type v} {M₂ : Type w} [] [] [] [Module R M] [Module R M₂] (p : ) (q : Submodule R M₂) :
Submodule.map (LinearMap.snd R M M₂) (p.prod q) = q
@[simp]
theorem Submodule.ker_inl {R : Type u} {M : Type v} {M₂ : Type w} [] [] [] [Module R M] [Module R M₂] :
@[simp]
theorem Submodule.ker_inr {R : Type u} {M : Type v} {M₂ : Type w} [] [] [] [Module R M] [Module R M₂] :
@[simp]
theorem Submodule.range_fst {R : Type u} {M : Type v} {M₂ : Type w} [] [] [] [Module R M] [Module R M₂] :
@[simp]
theorem Submodule.range_snd {R : Type u} {M : Type v} {M₂ : Type w} [] [] [] [Module R M] [Module R M₂] :
def Submodule.fst (R : Type u) (M : Type v) (M₂ : Type w) [] [] [] [Module R M] [Module R M₂] :
Submodule R (M × M₂)

M as a submodule of M × N.

Equations
Instances For
@[simp]
theorem Submodule.fstEquiv_apply (R : Type u) (M : Type v) (M₂ : Type w) [] [] [] [Module R M] [Module R M₂] (x : (Submodule.fst R M M₂)) :
() x = (x).1
@[simp]
theorem Submodule.fstEquiv_symm_apply_coe (R : Type u) (M : Type v) (M₂ : Type w) [] [] [] [Module R M] [Module R M₂] (m : M) :
(().symm m) = (m, 0)
def Submodule.fstEquiv (R : Type u) (M : Type v) (M₂ : Type w) [] [] [] [Module R M] [Module R M₂] :
(Submodule.fst R M M₂) ≃ₗ[R] M

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

Equations
• = { toFun := fun (x : (Submodule.fst R M M₂)) => (x).1, map_add' := , map_smul' := , invFun := fun (m : M) => (m, 0), , left_inv := , right_inv := }
Instances For
theorem Submodule.fst_map_fst (R : Type u) (M : Type v) (M₂ : Type w) [] [] [] [Module R M] [Module R M₂] :
theorem Submodule.fst_map_snd (R : Type u) (M : Type v) (M₂ : Type w) [] [] [] [Module R M] [Module R M₂] :
def Submodule.snd (R : Type u) (M : Type v) (M₂ : Type w) [] [] [] [Module R M] [Module R M₂] :
Submodule R (M × M₂)

N as a submodule of M × N.

Equations
Instances For
@[simp]
theorem Submodule.sndEquiv_apply (R : Type u) (M : Type v) (M₂ : Type w) [] [] [] [Module R M] [Module R M₂] (x : (Submodule.snd R M M₂)) :
() x = (x).2
@[simp]
theorem Submodule.sndEquiv_symm_apply_coe (R : Type u) (M : Type v) (M₂ : Type w) [] [] [] [Module R M] [Module R M₂] (n : M₂) :
(().symm n) = (0, n)
def Submodule.sndEquiv (R : Type u) (M : Type v) (M₂ : Type w) [] [] [] [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
• = { toFun := fun (x : (Submodule.snd R M M₂)) => (x).2, map_add' := , map_smul' := , invFun := fun (n : M₂) => (0, n), , left_inv := , right_inv := }
Instances For
theorem Submodule.snd_map_fst (R : Type u) (M : Type v) (M₂ : Type w) [] [] [] [Module R M] [Module R M₂] :
theorem Submodule.snd_map_snd (R : Type u) (M : Type v) (M₂ : Type w) [] [] [] [Module R M] [Module R M₂] :
theorem Submodule.fst_sup_snd (R : Type u) (M : Type v) (M₂ : Type w) [] [] [] [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) [] [] [] [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) [] [] [] [Module R M] [Module R M₂] {p₁ : } {p₂ : Submodule R M₂} {q : Submodule R (M × M₂)} :
q p₁.prod p₂ Submodule.map (LinearMap.fst R M M₂) q p₁ Submodule.map (LinearMap.snd R M M₂) q p₂
theorem Submodule.prod_le_iff (R : Type u) (M : Type v) (M₂ : Type w) [] [] [] [Module R M] [Module R M₂] {p₁ : } {p₂ : Submodule R M₂} {q : Submodule R (M × M₂)} :
p₁.prod p₂ q Submodule.map (LinearMap.inl R M M₂) p₁ q Submodule.map (LinearMap.inr R M M₂) p₂ q
theorem Submodule.prod_eq_bot_iff (R : Type u) (M : Type v) (M₂ : Type w) [] [] [] [Module R M] [Module R M₂] {p₁ : } {p₂ : Submodule R M₂} :
p₁.prod p₂ = p₁ = p₂ =
theorem Submodule.prod_eq_top_iff (R : Type u) (M : Type v) (M₂ : Type w) [] [] [] [Module R M] [Module R M₂] {p₁ : } {p₂ : Submodule R M₂} :
p₁.prod p₂ = p₁ = p₂ =
@[simp]
theorem LinearEquiv.prodComm_apply (R : Type u_3) (M : Type u_4) (N : Type u_5) [] [] [] [Module R M] [Module R N] :
∀ (a : M × N), () a = a.swap
def LinearEquiv.prodComm (R : Type u_3) (M : Type u_4) (N : Type u_5) [] [] [] [Module R M] [Module R N] :
(M × N) ≃ₗ[R] N × M

Product of modules is commutative up to linear isomorphism.

Equations
• = let __src := AddEquiv.prodComm; { toFun := Prod.swap, map_add' := , map_smul' := , invFun := __src.invFun, left_inv := , right_inv := }
Instances For
theorem LinearEquiv.fst_comp_prodComm {R : Type u} {M : Type v} {M₂ : Type w} [] [] [] [Module R M] [Module R M₂] :
LinearMap.fst R M₂ M ∘ₗ () = LinearMap.snd R M M₂
theorem LinearEquiv.snd_comp_prodComm {R : Type u} {M : Type v} {M₂ : Type w} [] [] [] [Module R M] [Module R M₂] :
LinearMap.snd R M₂ M ∘ₗ () = LinearMap.fst R M M₂
@[simp]
theorem LinearEquiv.prodProdProdComm_apply (R : Type u) (M : Type v) (M₂ : Type w) (M₃ : Type y) (M₄ : Type z) [] [] [] [] [] [Module R M] [Module R M₂] [Module R M₃] [Module R M₄] (mnmn : (M × M₂) × M₃ × M₄) :
(LinearEquiv.prodProdProdComm R M M₂ M₃ M₄) mnmn = ((mnmn.1.1, mnmn.2.1), mnmn.1.2, mnmn.2.2)
def LinearEquiv.prodProdProdComm (R : Type u) (M : Type v) (M₂ : Type w) (M₃ : Type y) (M₄ : Type z) [] [] [] [] [] [Module R M] [Module R M₂] [Module R M₃] [Module R M₄] :
((M × M₂) × M₃ × M₄) ≃ₗ[R] (M × M₃) × M₂ × M₄

Four-way commutativity of prod. The name matches mul_mul_mul_comm.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem LinearEquiv.prodProdProdComm_symm (R : Type u) (M : Type v) (M₂ : Type w) (M₃ : Type y) (M₄ : Type z) [] [] [] [] [] [Module R M] [Module R M₂] [Module R M₃] [Module R M₄] :
(LinearEquiv.prodProdProdComm R M M₂ M₃ M₄).symm = LinearEquiv.prodProdProdComm R M M₃ M₂ M₄
@[simp]
theorem LinearEquiv.prodProdProdComm_toAddEquiv (R : Type u) (M : Type v) (M₂ : Type w) (M₃ : Type y) (M₄ : Type z) [] [] [] [] [] [Module R M] [Module R M₂] [Module R M₃] [Module R M₄] :
(LinearEquiv.prodProdProdComm R M M₂ M₃ M₄) = AddEquiv.prodProdProdComm M M₂ M₃ M₄
def LinearEquiv.prod {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [] [] [] [] [] {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.prodCongr.

Equations
• e₁.prod e₂ = let __src := e₁.toAddEquiv.prodCongr e₂.toAddEquiv; { toFun := __src.toFun, map_add' := , map_smul' := , invFun := __src.invFun, left_inv := , right_inv := }
Instances For
theorem LinearEquiv.prod_symm {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [] [] [] [] [] {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 LinearEquiv.prod_apply {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [] [] [] [] [] {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.1, e₂ p.2)
@[simp]
theorem LinearEquiv.coe_prod {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [] [] [] [] [] {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₁).prodMap e₂
def LinearEquiv.skewProd {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [] [] [] [] [] {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
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem LinearEquiv.skewProd_apply {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [] [] [] [] [] {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₁.skewProd e₂ f) x = (e₁ x.1, e₂ x.2 + f x.1)
@[simp]
theorem LinearEquiv.skewProd_symm_apply {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [] [] [] [] [] {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₁.skewProd e₂ f).symm x = (e₁.symm x.1, e₂.symm (x.2 - f (e₁.symm x.1)))
theorem LinearMap.range_prod_eq {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [Ring R] [] [] [] [Module R M] [Module R M₂] [Module R M₃] {f : M →ₗ[R] M₂} {g : M →ₗ[R] M₃} (h : ) :
LinearMap.range (f.prod g) = ().prod ()

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 #

NOTE: The proof of strong rank condition for noetherian rings is changed. LinearMap.tunnel and LinearMap.tailing are not used in mathlib anymore. These are marked as deprecated with no replacements. If you use them in external projects, please consider using other arguments instead.

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.

@[deprecated]
def LinearMap.tunnelAux {R : Type u} {M : Type v} [Ring R] {N : Type u_3} [] [Module R M] [] [Module R N] (f : M × N →ₗ[R] M) (Kφ : (K : ) × 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
• f.tunnelAux = (.fst.subtype ∘ₗ .snd.symm) ∘ₗ f
Instances For
@[deprecated]
theorem LinearMap.tunnelAux_injective {R : Type u} {M : Type v} [Ring R] {N : Type u_3} [] [Module R M] [] [Module R N] (f : M × N →ₗ[R] M) (i : ) (Kφ : (K : ) × K ≃ₗ[R] M) :
Function.Injective (f.tunnelAux )
@[deprecated]
def LinearMap.tunnel' {R : Type u} {M : Type v} [Ring R] {N : Type u_3} [] [Module R M] [] [Module R N] (f : M × N →ₗ[R] M) (i : ) :
(K : ) × K ≃ₗ[R] M

Auxiliary definition for tunnel.

Equations
• One or more equations did not get rendered due to their size.
• f.tunnel' i 0 = , ⟩
Instances For
@[deprecated]
def LinearMap.tunnel {R : Type u} {M : Type v} [Ring R] {N : Type u_3} [] [Module R M] [] [Module R N] (f : M × N →ₗ[R] M) (i : ) :

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

Equations
• f.tunnel i = { toFun := fun (n : ) => OrderDual.toDual (f.tunnel' i n).fst, monotone' := }
Instances For
@[deprecated]
def LinearMap.tailing {R : Type u} {M : Type v} [Ring R] {N : Type u_3} [] [Module R M] [] [Module R N] (f : M × N →ₗ[R] M) (i : ) (n : ) :

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

Equations
Instances For
@[deprecated]
def LinearMap.tailingLinearEquiv {R : Type u} {M : Type v} [Ring R] {N : Type u_3} [] [Module R M] [] [Module R N] (f : M × N →ₗ[R] M) (i : ) (n : ) :
(f.tailing i n) ≃ₗ[R] N

Each tailing f i n is a copy of N.

Equations
Instances For
@[deprecated]
theorem LinearMap.tailing_le_tunnel {R : Type u} {M : Type v} [Ring R] {N : Type u_3} [] [Module R M] [] [Module R N] (f : M × N →ₗ[R] M) (i : ) (n : ) :
f.tailing i n OrderDual.ofDual ((f.tunnel i) n)
@[deprecated]
theorem LinearMap.tailing_disjoint_tunnel_succ {R : Type u} {M : Type v} [Ring R] {N : Type u_3} [] [Module R M] [] [Module R N] (f : M × N →ₗ[R] M) (i : ) (n : ) :
Disjoint (f.tailing i n) (OrderDual.ofDual ((f.tunnel i) (n + 1)))
@[deprecated]
theorem LinearMap.tailing_sup_tunnel_succ_le_tunnel {R : Type u} {M : Type v} [Ring R] {N : Type u_3} [] [Module R M] [] [Module R N] (f : M × N →ₗ[R] M) (i : ) (n : ) :
f.tailing i n OrderDual.ofDual ((f.tunnel i) (n + 1)) OrderDual.ofDual ((f.tunnel i) n)
@[deprecated]
def LinearMap.tailings {R : Type u} {M : Type v} [Ring R] {N : Type u_3} [] [Module R M] [] [Module R N] (f : M × N →ₗ[R] M) (i : ) :

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

Equations
Instances For
@[simp, deprecated]
theorem LinearMap.tailings_zero {R : Type u} {M : Type v} [Ring R] {N : Type u_3} [] [Module R M] [] [Module R N] (f : M × N →ₗ[R] M) (i : ) :
f.tailings i 0 = f.tailing i 0
@[simp, deprecated]
theorem LinearMap.tailings_succ {R : Type u} {M : Type v} [Ring R] {N : Type u_3} [] [Module R M] [] [Module R N] (f : M × N →ₗ[R] M) (i : ) (n : ) :
f.tailings i (n + 1) = f.tailings i n f.tailing i (n + 1)
@[deprecated]
theorem LinearMap.tailings_disjoint_tunnel {R : Type u} {M : Type v} [Ring R] {N : Type u_3} [] [Module R M] [] [Module R N] (f : M × N →ₗ[R] M) (i : ) (n : ) :
Disjoint (f.tailings i n) (OrderDual.ofDual ((f.tunnel i) (n + 1)))
@[deprecated]
theorem LinearMap.tailings_disjoint_tailing {R : Type u} {M : Type v} [Ring R] {N : Type u_3} [] [Module R M] [] [Module R N] (f : M × N →ₗ[R] M) (i : ) (n : ) :
Disjoint (f.tailings i n) (f.tailing i (n + 1))
def LinearMap.graph {R : Type u} {M : Type v} {M₂ : Type w} [] [] [] [Module R M] [Module R M₂] (f : M →ₗ[R] M₂) :
Submodule R (M × M₂)

Graph of a linear map.

Equations
• f.graph = { carrier := {p : M × M₂ | p.2 = f p.1}, add_mem' := , zero_mem' := , smul_mem' := }
Instances For
@[simp]
theorem LinearMap.mem_graph_iff {R : Type u} {M : Type v} {M₂ : Type w} [] [] [] [Module R M] [Module R M₂] (f : M →ₗ[R] M₂) (x : M × M₂) :
x f.graph x.2 = f x.1
theorem LinearMap.graph_eq_ker_coprod {R : Type u} {M₃ : Type y} {M₄ : Type z} [] [] [] [Module R M₃] [Module R M₄] (g : M₃ →ₗ[R] M₄) :
g.graph = LinearMap.ker ((-g).coprod LinearMap.id)
theorem LinearMap.graph_eq_range_prod {R : Type u} {M : Type v} {M₂ : Type w} [] [] [] [Module R M] [Module R M₂] (f : M →ₗ[R] M₂) :
f.graph = LinearMap.range (LinearMap.id.prod f)