mathlib3 documentation

linear_algebra.prod

Products of modules #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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_3) [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_3) [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_3) [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₂] :
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₂] :
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₂] :
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₂] :
@[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_3) [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_3) [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_3) [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
theorem linear_map.coe_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₄) :
@[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₄) :
@[simp]
@[simp]
theorem linear_map.prod_map_one {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₂] :
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₅] [add_comm_monoid M₆] [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₂₃.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] [add_comm_monoid M₂] [module R M] [module R 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₃] [add_comm_monoid M₄] [module R M] [module R M₂] [module R M₃] [module R 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₃] [add_comm_monoid M₄] [module R M] [module R M₂] [module R M₃] [module R 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₃] [add_comm_monoid M₄] [module R 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₄] (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₃] [add_comm_monoid M₄] [module R 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 × 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₃] [add_comm_monoid M₄] [module R 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₄)) :
(linear_map.prod_map_linear 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] [add_comm_monoid M₂] [module R M] [module R M₂] (f : (M →ₗ[R] M) × (M₂ →ₗ[R] M₂)) :
def linear_map.prod_map_ring_hom (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₂ →ₗ[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} [non_unital_non_assoc_semiring A] [module R A] {B : Type u_5} [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_4} [non_unital_non_assoc_semiring A] [module R A] {B : Type u_5} [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₂
@[simp]
theorem linear_map.prod_map_alg_hom_apply (R : Type u) (M : Type v) (M₂ : Type w) [comm_semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] (ᾰ : (M →ₗ[R] M) × (M₂ →ₗ[R] M₂)) :
def linear_map.prod_map_alg_hom (R : Type u) (M : Type v) (M₂ : Type w) [comm_semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] :
module.End R M × module.End R M₂ →ₐ[R] module.End 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₂] [add_comm_monoid M₃] [module R M] [module R M₂] [module R M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[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₃) :
theorem linear_map.range_prod_le {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [module R M] [module R M₂] [module R M₃] (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) :
theorem linear_map.ker_prod_ker_le_ker_coprod {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M] {M₂ : Type u_1} [add_comm_group M₂] [module R M₂] {M₃ : Type u_2} [add_comm_group M₃] [module R M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) :
theorem linear_map.ker_coprod_of_disjoint_range {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M] {M₂ : Type u_1} [add_comm_group M₂] [module R M₂] {M₃ : Type u_2} [add_comm_group M₃] [module R M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) (hd : disjoint (linear_map.range f) (linear_map.range g)) :
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₂] :
@[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₂] :
@[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
@[simp]
theorem linear_equiv.prod_prod_prod_comm_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₄] (mnmn : (M × M₂) × M₃ × M₄) :
(linear_equiv.prod_prod_prod_comm R M M₂ M₃ M₄) mnmn = ((mnmn.fst.fst, mnmn.snd.fst), mnmn.fst.snd, mnmn.snd.snd)
def linear_equiv.prod_prod_prod_comm (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₄] :
((M × M₂) × M₃ × M₄) ≃ₗ[R] (M × M₃) × M₂ × M₄

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

Equations
@[simp]
theorem linear_equiv.prod_prod_prod_comm_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 R M] [module R M₂] [module R M₃] [module R M₄] :
@[simp]
theorem linear_equiv.prod_prod_prod_comm_to_add_equiv (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₄] :
@[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 : linear_map.ker f linear_map.ker g = ) :

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} [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_3} [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_3} [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_3} [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_3} [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_3} [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_3} [add_comm_group M] [module R M] [add_comm_group N] [module R N] (f : M × N →ₗ[R] M) (i : function.injective f) (n : ) :
theorem linear_map.tailing_disjoint_tunnel_succ {R : Type u} {M : Type v} [ring R] {N : Type u_3} [add_comm_group M] [module R M] [add_comm_group N] [module R N] (f : M × N →ₗ[R] M) (i : function.injective f) (n : ) :
noncomputable def linear_map.tailings {R : Type u} {M : Type v} [ring R] {N : Type u_3} [add_comm_group M] [module R M] [add_comm_group N] [module R N] (f : M × N →ₗ[R] M) (i : function.injective f) :

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

Equations
@[simp]
theorem linear_map.tailings_zero {R : Type u} {M : Type v} [ring R] {N : Type u_3} [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_3} [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_3} [add_comm_group M] [module R M] [add_comm_group N] [module R N] (f : M × N →ₗ[R] M) (i : function.injective f) (n : ) :
theorem linear_map.tailings_disjoint_tailing {R : Type u} {M : Type v} [ring R] {N : Type u_3} [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))
def linear_map.graph {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₂] (f : M →ₗ[R] M₂) :
submodule R (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] [add_comm_monoid M₂] [module R M] [module R 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₄] [module R M₃] [module R M₄] (g : M₃ →ₗ[R] M₄) :
theorem linear_map.graph_eq_range_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₂] (f : M →ₗ[R] M₂) :