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 #
- products in the domain:
- products in the codomain:
- products in both domain and codomain:
linear_map.prod_maplinear_equiv.prod_maplinear_equiv.skew_prod
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₂] :
The first projection of a product is a linear map.
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₂] :
The second projection of a product is a linear map.
@[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₂] :
function.surjective ⇑(linear_map.fst R M 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₂] :
function.surjective ⇑(linear_map.snd R 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₂]
[add_comm_monoid M₃]
[module R M]
[module R M₂]
[module R M₃]
(f : M →ₗ[R] M₂)
(g : M →ₗ[R] M₃) :
The prod of two linear maps is a linear map.
@[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) :
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₂] :
(linear_map.fst R M M₂).prod (linear_map.snd R 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₂]
[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₃] :
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.
@[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₂] :
The left injection into a product is a linear map.
Equations
- linear_map.inl R M M₂ = linear_map.id.prod 0
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₂] :
The right injection into a product is a linear map.
Equations
- linear_map.inr R M M₂ = 0.prod linear_map.id
theorem
linear_map.range_inl
(R : Type u)
(M : Type v)
(M₂ : Type w)
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
linear_map.range (linear_map.inl R M M₂) = linear_map.ker (linear_map.snd R M 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₂] :
linear_map.ker (linear_map.snd R M M₂) = linear_map.range (linear_map.inl R M 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₂] :
linear_map.range (linear_map.inr R M M₂) = linear_map.ker (linear_map.fst R M 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₂] :
linear_map.ker (linear_map.fst R M M₂) = linear_map.range (linear_map.inr R M 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₂] :
⇑(linear_map.inr R M M₂) = prod.mk 0
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₂] :
linear_map.inl R M M₂ = linear_map.id.prod 0
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₂] :
linear_map.inr R M M₂ = 0.prod linear_map.id
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₂] :
function.injective ⇑(linear_map.inl R M 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₂] :
function.injective ⇑(linear_map.inr R 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₂]
[add_comm_monoid M₃]
[module R M]
[module R M₂]
[module R M₃]
(f : M →ₗ[R] M₃)
(g : M₂ →ₗ[R] M₃) :
The coprod function λ x : M × M₂, f x.1 + g x.2 is a linear map.
Equations
- f.coprod g = f.comp (linear_map.fst R M M₂) + g.comp (linear_map.snd R M M₂)
@[simp]
@[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₂] :
(linear_map.inl R M M₂).coprod (linear_map.inr R 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₃]
[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₃) :
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₂] :
linear_map.fst R M M₂ = linear_map.id.coprod 0
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₂] :
linear_map.snd R M M₂ = 0.coprod linear_map.id
@[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₃) :
@[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₂) :
submodule.map (f.coprod g) (S.prod S') = submodule.map f S ⊔ submodule.map g 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₂]
[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₃) :
⇑((linear_map.coprod_equiv S).symm) f = (f.comp (linear_map.inl R M M₂), f.comp (linear_map.inr R 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₂]
[add_comm_monoid M₃]
[module R M]
[module R M₂]
[module R M₃]
[module S M₃]
[smul_comm_class R S 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.
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₃.
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₄) :
prod.map of two linear maps.
Equations
- f.prod_map g = (f.comp (linear_map.fst R M M₂)).prod (g.comp (linear_map.snd R M M₂))
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₂) :
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₄) :
submodule.comap (f.prod_map g) (S.prod S') = (submodule.comap f S).prod (submodule.comap g 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₃]
[add_comm_monoid M₄]
[module R M]
[module R M₂]
[module R M₃]
[module R M₄]
(f : M →ₗ[R] M₂)
(g : M₃ →ₗ[R] M₄) :
linear_map.ker (f.prod_map g) = (linear_map.ker f).prod (linear_map.ker g)
@[simp]
theorem
linear_map.prod_map_id
{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_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₂] :
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₆) :
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₄) :
@[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₄] :
@[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₄) :
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₄] :
@[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₄)) :
@[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₂] :
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₂)) :
⇑(linear_map.prod_map_alg_hom R M M₂) ᾰ = (linear_map.prod_map_ring_hom R M M₂).to_fun ᾰ
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
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₃) :
linear_map.range (f.coprod g) = linear_map.range f ⊔ linear_map.range g
theorem
linear_map.is_compl_range_inl_inr
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
is_compl (linear_map.range (linear_map.inl R M M₂)) (linear_map.range (linear_map.inr R M M₂))
theorem
linear_map.sup_range_inl_inr
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
linear_map.range (linear_map.inl R M M₂) ⊔ linear_map.range (linear_map.inr R M 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₂] :
disjoint (linear_map.range (linear_map.inl R M M₂)) (linear_map.range (linear_map.inr R 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₂]
[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₂) :
submodule.map (f.coprod g) (p.prod q) = submodule.map f p ⊔ submodule.map g q
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₃) :
submodule.comap (f.prod g) (p.prod q) = submodule.comap f p ⊓ submodule.comap g q
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₂) :
p.prod q = submodule.comap (linear_map.fst R M M₂) p ⊓ submodule.comap (linear_map.snd R 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]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(p : submodule R M)
(q : submodule R M₂) :
p.prod q = submodule.map (linear_map.inl R M M₂) p ⊔ submodule.map (linear_map.inr R 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]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
{s : set M}
{t : set M₂} :
submodule.span R (⇑(linear_map.inl R M M₂) '' s ∪ ⇑(linear_map.inr R M M₂) '' t) = (submodule.span R s).prod (submodule.span R 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₂]
[add_comm_monoid M₃]
[module R M]
[module R M₂]
[module R M₃]
(f : M →ₗ[R] M₂)
(g : M →ₗ[R] M₃) :
linear_map.ker (f.prod g) = linear_map.ker f ⊓ linear_map.ker g
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₃) :
linear_map.range (f.prod g) ≤ (linear_map.range f).prod (linear_map.range g)
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₃) :
(linear_map.ker f).prod (linear_map.ker g) ≤ linear_map.ker (f.coprod g)
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)) :
linear_map.ker (f.coprod g) = (linear_map.ker f).prod (linear_map.ker 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) :
submodule.map (linear_map.inl R 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]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(q : submodule R M₂) :
submodule.map (linear_map.inr R 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]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(p : submodule R M) :
submodule.comap (linear_map.fst R M M₂) p = p.prod ⊤
@[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₂) :
submodule.comap (linear_map.snd R M M₂) q = ⊤.prod q
@[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₂) :
submodule.comap (linear_map.inl R 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]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(p : submodule R M)
(q : submodule R M₂) :
submodule.comap (linear_map.inr R 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]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(p : submodule R M)
(q : submodule R M₂) :
submodule.map (linear_map.fst R M M₂) (p.prod q) = p
@[simp]
theorem
submodule.prod_map_snd
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(p : submodule R M)
(q : submodule R M₂) :
submodule.map (linear_map.snd R M M₂) (p.prod q) = q
@[simp]
theorem
submodule.ker_inl
{R : Type u}
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
linear_map.ker (linear_map.inl R M 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₂] :
linear_map.ker (linear_map.inr R M 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₂] :
linear_map.range (linear_map.fst R M 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₂] :
linear_map.range (linear_map.snd R M 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₂] :
M as a submodule of M × N.
Equations
- submodule.fst R M M₂ = submodule.comap (linear_map.snd R M M₂) ⊥
@[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₂] :
↥(submodule.fst R M M₂) ≃ₗ[R] M
M as a submodule of M × N is isomorphic to M.
@[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₂)) :
⇑(submodule.fst_equiv R 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]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
submodule.map (linear_map.fst R M M₂) (submodule.fst R M 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₂] :
submodule.map (linear_map.snd R M M₂) (submodule.fst R M 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₂] :
N as a submodule of M × N.
Equations
- submodule.snd R M M₂ = submodule.comap (linear_map.fst R M M₂) ⊥
@[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₂)) :
⇑(submodule.snd_equiv R 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]
[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.
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₂] :
submodule.map (linear_map.fst R M M₂) (submodule.snd R M 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₂] :
submodule.map (linear_map.snd R M M₂) (submodule.snd R M 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
@[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) :
⇑(linear_equiv.prod_comm R M N) ᾰ = ᾰ.swap
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] :
Product of modules is commutative up to linear isomorphism.
@[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₄) :
Product of linear equivalences; the maps come from equiv.prod_congr.
Equations
- e₁.prod e₂ = {to_fun := (e₁.to_add_equiv.prod_congr e₂.to_add_equiv).to_fun, map_add' := _, map_smul' := _, inv_fun := (e₁.to_add_equiv.prod_congr e₂.to_add_equiv).inv_fun, left_inv := _, right_inv := _}
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₄) :
@[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₃) :
@[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₄) :
@[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₄) :
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
- e₁.skew_prod e₂ f = {to_fun := ((↑e₁.comp (linear_map.fst R M M₃)).prod (↑e₂.comp (linear_map.snd R M M₃) + f.comp (linear_map.fst R M M₃))).to_fun, map_add' := _, map_smul' := _, inv_fun := λ (p : M₂ × M₄), (⇑(e₁.symm) p.fst, ⇑(e₂.symm) (p.snd - ⇑f (⇑(e₁.symm) p.fst))), left_inv := _, right_inv := _}
@[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₃) :
@[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₄) :
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 = ⊤) :
linear_map.range (f.prod g) = (linear_map.range f).prod (linear_map.range 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) :
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.tunnel_aux Kφ = (Kφ.fst.subtype.comp (linear_equiv.symm Kφ.snd).to_linear_map).comp f
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) :
function.injective ⇑(f.tunnel_aux Kφ)
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) :
Auxiliary definition for tunnel.
Equations
- f.tunnel' i (n + 1) = ⟨submodule.map (f.tunnel_aux (f.tunnel' i n)) (submodule.fst R M N), (submodule.equiv_map_of_injective (f.tunnel_aux (f.tunnel' i n)) _ (submodule.fst R M N)).symm.trans (submodule.fst_equiv R M N)⟩
- f.tunnel' i 0 = ⟨⊤, linear_equiv.of_top ⊤ linear_map.tunnel'._main._proof_3⟩
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.
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 : ℕ) :
submodule R M
Give an injective map f : M × N →ₗ[R] M we can find a sequence of submodules
all isomorphic to N.
Equations
- f.tailing i n = submodule.map (f.tunnel_aux (f.tunnel' i n)) (submodule.snd R M N)
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 : ℕ) :
Each tailing f i n is a copy of N.
Equations
- f.tailing_linear_equiv i n = (submodule.equiv_map_of_injective (f.tunnel_aux (f.tunnel' i n)) _ (submodule.snd R M N)).symm.trans (submodule.snd_equiv R M N)
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 : ℕ) :
theorem
linear_map.tailing_sup_tunnel_succ_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 : ℕ) :
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
- f.tailings i = ⇑(partial_sups (f.tailing i))
@[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) :
@[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 : ℕ) :
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 : ℕ) :
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₂) :
Graph of a linear map.
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₄) :
g.graph = linear_map.ker ((-g).coprod linear_map.id)
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₂) :
f.graph = linear_map.range (linear_map.id.prod f)