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:
- products in the codomain:
- products in both domain and codomain:
LinearMap.prodMapLinearEquiv.prodMapLinearEquiv.skewProd
def
LinearMap.fst
(R : Type u)
(M : Type v)
(M₂ : Type w)
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module 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' := ⋯ }
def
LinearMap.snd
(R : Type u)
(M : Type v)
(M₂ : Type w)
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module 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' := ⋯ }
@[simp]
theorem
LinearMap.fst_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[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}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[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}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
:
Function.Surjective ⇑(LinearMap.fst R M M₂)
theorem
LinearMap.snd_surjective
{R : Type u}
{M : Type v}
{M₂ : Type w}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
:
Function.Surjective ⇑(LinearMap.snd R M M₂)
def
LinearMap.prod
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid 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
LinearMap.prod_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[Module R M]
[Module R M₂]
[Module R M₃]
(f : M →ₗ[R] M₂)
(g : M →ₗ[R] M₃)
(i : M)
:
theorem
LinearMap.coe_prod
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[Module R M]
[Module R M₂]
[Module R M₃]
(f : M →ₗ[R] M₂)
(g : M →ₗ[R] M₃)
:
@[simp]
theorem
LinearMap.fst_prod
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[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}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[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}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[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}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[AddCommMonoid M₄]
[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)
def
LinearMap.prodEquiv
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
(S : Type u_3)
[Semiring R]
[Semiring S]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[Module R M]
[Module R M₂]
[Module R M₃]
[Module S M₂]
[Module S M₃]
[SMulCommClass R S M₂]
[SMulCommClass 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.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
LinearMap.prodEquiv_symm_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
(S : Type u_3)
[Semiring R]
[Semiring S]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid 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₃)
:
(LinearMap.prodEquiv S).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)
[Semiring R]
[Semiring S]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid 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.prodEquiv S) f = f.1.prod f.2
def
LinearMap.inl
(R : Type u)
(M : Type v)
(M₂ : Type w)
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
:
The left injection into a product is a linear map.
Equations
- LinearMap.inl R M M₂ = LinearMap.id.prod 0
def
LinearMap.inr
(R : Type u)
(M : Type v)
(M₂ : Type w)
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
:
The right injection into a product is a linear map.
Equations
- LinearMap.inr R M M₂ = LinearMap.prod 0 LinearMap.id
theorem
LinearMap.range_inl
(R : Type u)
(M : Type v)
(M₂ : Type w)
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
:
LinearMap.range (LinearMap.inl R M M₂) = LinearMap.ker (LinearMap.snd R M M₂)
theorem
LinearMap.ker_snd
(R : Type u)
(M : Type v)
(M₂ : Type w)
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
:
LinearMap.ker (LinearMap.snd R M M₂) = LinearMap.range (LinearMap.inl R M M₂)
theorem
LinearMap.range_inr
(R : Type u)
(M : Type v)
(M₂ : Type w)
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
:
LinearMap.range (LinearMap.inr R M M₂) = LinearMap.ker (LinearMap.fst R M M₂)
theorem
LinearMap.ker_fst
(R : Type u)
(M : Type v)
(M₂ : Type w)
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
:
LinearMap.ker (LinearMap.fst R M M₂) = LinearMap.range (LinearMap.inr R M M₂)
@[simp]
theorem
LinearMap.fst_comp_inl
(R : Type u)
(M : Type v)
(M₂ : Type w)
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[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)
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[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)
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[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)
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[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}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[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}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[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}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
:
⇑(LinearMap.inr R M M₂) = Prod.mk 0
theorem
LinearMap.inr_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[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}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[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}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[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}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
:
Function.Injective ⇑(LinearMap.inl R M M₂)
theorem
LinearMap.inr_injective
{R : Type u}
{M : Type v}
{M₂ : Type w}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
:
Function.Injective ⇑(LinearMap.inr R M M₂)
def
LinearMap.coprod
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid 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 ∘ₗ LinearMap.fst R M M₂ + g ∘ₗ LinearMap.snd R M M₂
@[simp]
theorem
LinearMap.coprod_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[Module R M]
[Module R M₂]
[Module R M₃]
(f : M →ₗ[R] M₃)
(g : M₂ →ₗ[R] M₃)
(x : M × M₂)
:
@[simp]
theorem
LinearMap.coprod_inl
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[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}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[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}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[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}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[Module R M]
[Module R M₂]
[Module R M₃]
(g : M₂ →ₗ[R] M₃)
:
LinearMap.coprod 0 g = g ∘ₗ LinearMap.snd R M M₂
theorem
LinearMap.coprod_zero_right
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[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}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[AddCommMonoid 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 ∘ₗ g₁.coprod g₂ = (f ∘ₗ g₁).coprod (f ∘ₗ g₂)
theorem
LinearMap.fst_eq_coprod
{R : Type u}
{M : Type v}
{M₂ : Type w}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[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}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[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}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[AddCommMonoid 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
LinearMap.coprod_map_prod
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid 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'
def
LinearMap.coprodEquiv
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
(S : Type u_3)
[Semiring R]
[Semiring S]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[Module R M]
[Module R M₂]
[Module R M₃]
[Module S M₃]
[SMulCommClass 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.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
LinearMap.coprodEquiv_symm_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
(S : Type u_3)
[Semiring R]
[Semiring S]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[Module R M]
[Module R M₂]
[Module R M₃]
[Module S M₃]
[SMulCommClass R S M₃]
(f : M × M₂ →ₗ[R] M₃)
:
(LinearMap.coprodEquiv S).symm f = (f ∘ₗ LinearMap.inl R M M₂, f ∘ₗ LinearMap.inr R M M₂)
@[simp]
theorem
LinearMap.coprodEquiv_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
(S : Type u_3)
[Semiring R]
[Semiring S]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[Module R M]
[Module R M₂]
[Module R M₃]
[Module S M₃]
[SMulCommClass R S M₃]
(f : (M →ₗ[R] M₃) × (M₂ →ₗ[R] M₃))
:
(LinearMap.coprodEquiv S) f = f.1.coprod f.2
theorem
LinearMap.prod_ext_iff
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[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}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[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}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[AddCommMonoid 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.prodMap g = (f ∘ₗ LinearMap.fst R M M₂).prod (g ∘ₗ LinearMap.snd R M M₂)
theorem
LinearMap.coe_prodMap
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
{M₄ : Type z}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[AddCommMonoid M₄]
[Module R M]
[Module R M₂]
[Module R M₃]
[Module R M₄]
(f : M →ₗ[R] M₃)
(g : M₂ →ₗ[R] M₄)
:
@[simp]
theorem
LinearMap.prodMap_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
{M₄ : Type z}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[AddCommMonoid 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.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}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[AddCommMonoid 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.prodMap g) (S.prod S') = (Submodule.comap f S).prod (Submodule.comap g S')
theorem
LinearMap.ker_prodMap
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
{M₄ : Type z}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[AddCommMonoid M₄]
[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) = (LinearMap.ker f).prod (LinearMap.ker g)
@[simp]
theorem
LinearMap.prodMap_id
{R : Type u}
{M : Type v}
{M₂ : Type w}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[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}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
:
LinearMap.prodMap 1 1 = 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}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[AddCommMonoid M₄]
[AddCommMonoid M₅]
[AddCommMonoid 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₂₃.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}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[AddCommMonoid 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₄)
:
@[simp]
theorem
LinearMap.prodMap_zero
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
{M₄ : Type z}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[AddCommMonoid M₄]
[Module R M]
[Module R M₂]
[Module R M₃]
[Module R M₄]
:
LinearMap.prodMap 0 0 = 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)
[Semiring R]
[Semiring S]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[AddCommMonoid M₄]
[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₄)
:
def
LinearMap.prodMapLinear
(R : Type u)
(M : Type v)
(M₂ : Type w)
(M₃ : Type y)
(M₄ : Type z)
(S : Type u_3)
[Semiring R]
[Semiring S]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[AddCommMonoid M₄]
[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₄]
:
@[simp]
theorem
LinearMap.prodMapLinear_apply
(R : Type u)
(M : Type v)
(M₂ : Type w)
(M₃ : Type y)
(M₄ : Type z)
(S : Type u_3)
[Semiring R]
[Semiring S]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[AddCommMonoid M₄]
[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.prodMapRingHom
(R : Type u)
(M : Type v)
(M₂ : Type w)
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
:
LinearMap.prodMap as a RingHom
@[simp]
theorem
LinearMap.prodMapRingHom_apply
(R : Type u)
(M : Type v)
(M₂ : Type w)
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
(f : (M →ₗ[R] M) × (M₂ →ₗ[R] M₂))
:
(LinearMap.prodMapRingHom R M M₂) f = f.1.prodMap f.2
theorem
LinearMap.inl_map_mul
{R : Type u}
[Semiring R]
{A : Type u_4}
[NonUnitalNonAssocSemiring A]
[Module R A]
{B : Type u_5}
[NonUnitalNonAssocSemiring B]
[Module R B]
(a₁ : A)
(a₂ : A)
:
(LinearMap.inl R A B) (a₁ * a₂) = (LinearMap.inl R A B) a₁ * (LinearMap.inl R A B) a₂
theorem
LinearMap.inr_map_mul
{R : Type u}
[Semiring R]
{A : Type u_4}
[NonUnitalNonAssocSemiring A]
[Module R A]
{B : Type u_5}
[NonUnitalNonAssocSemiring B]
[Module R B]
(b₁ : B)
(b₂ : B)
:
(LinearMap.inr R A B) (b₁ * b₂) = (LinearMap.inr R A B) b₁ * (LinearMap.inr R A B) b₂
def
LinearMap.prodMapAlgHom
(R : Type u)
(M : Type v)
(M₂ : Type w)
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
:
Module.End R M × Module.End R M₂ →ₐ[R] Module.End R (M × M₂)
LinearMap.prodMap as an AlgHom
Equations
- LinearMap.prodMapAlgHom R M M₂ = { toRingHom := LinearMap.prodMapRingHom R M M₂, commutes' := ⋯ }
@[simp]
theorem
LinearMap.prodMapAlgHom_apply_apply
(R : Type u)
(M : Type v)
(M₂ : Type w)
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
(f : (M →ₗ[R] M) × (M₂ →ₗ[R] M₂))
(i : M × M₂)
:
((LinearMap.prodMapAlgHom R M M₂) f) i = (f.1 i.1, f.2 i.2)
theorem
LinearMap.range_coprod
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[Module R M]
[Module R M₂]
[Module R M₃]
(f : M →ₗ[R] M₃)
(g : M₂ →ₗ[R] M₃)
:
LinearMap.range (f.coprod g) = LinearMap.range f ⊔ LinearMap.range g
theorem
LinearMap.isCompl_range_inl_inr
{R : Type u}
{M : Type v}
{M₂ : Type w}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
:
IsCompl (LinearMap.range (LinearMap.inl R M M₂)) (LinearMap.range (LinearMap.inr R M M₂))
theorem
LinearMap.sup_range_inl_inr
{R : Type u}
{M : Type v}
{M₂ : Type w}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
:
LinearMap.range (LinearMap.inl R M M₂) ⊔ LinearMap.range (LinearMap.inr R M M₂) = ⊤
theorem
LinearMap.disjoint_inl_inr
{R : Type u}
{M : Type v}
{M₂ : Type w}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
:
Disjoint (LinearMap.range (LinearMap.inl R M M₂)) (LinearMap.range (LinearMap.inr R M M₂))
theorem
LinearMap.map_coprod_prod
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid 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
LinearMap.comap_prod_prod
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid 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
LinearMap.prod_eq_inf_comap
{R : Type u}
{M : Type v}
{M₂ : Type w}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
(p : Submodule R M)
(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}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
(p : Submodule R M)
(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}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[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) = (Submodule.span R s).prod (Submodule.span R t)
@[simp]
theorem
LinearMap.ker_prod
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[Module R M]
[Module R M₂]
[Module R M₃]
(f : M →ₗ[R] M₂)
(g : M →ₗ[R] M₃)
:
LinearMap.ker (f.prod g) = LinearMap.ker f ⊓ LinearMap.ker g
theorem
LinearMap.range_prod_le
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[Module R M]
[Module R M₂]
[Module R M₃]
(f : M →ₗ[R] M₂)
(g : M →ₗ[R] M₃)
:
LinearMap.range (f.prod g) ≤ (LinearMap.range f).prod (LinearMap.range g)
theorem
LinearMap.ker_prod_ker_le_ker_coprod
{R : Type u}
{M : Type v}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{M₂ : Type u_3}
[AddCommGroup M₂]
[Module R M₂]
{M₃ : Type u_4}
[AddCommGroup M₃]
[Module R M₃]
(f : M →ₗ[R] M₃)
(g : M₂ →ₗ[R] M₃)
:
(LinearMap.ker f).prod (LinearMap.ker g) ≤ LinearMap.ker (f.coprod g)
theorem
LinearMap.ker_coprod_of_disjoint_range
{R : Type u}
{M : Type v}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{M₂ : Type u_3}
[AddCommGroup M₂]
[Module R M₂]
{M₃ : Type u_4}
[AddCommGroup M₃]
[Module R M₃]
(f : M →ₗ[R] M₃)
(g : M₂ →ₗ[R] M₃)
(hd : Disjoint (LinearMap.range f) (LinearMap.range g))
:
LinearMap.ker (f.coprod g) = (LinearMap.ker f).prod (LinearMap.ker g)
theorem
Submodule.sup_eq_range
{R : Type u}
{M : Type v}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(p : Submodule R M)
(q : Submodule R M)
:
p ⊔ q = LinearMap.range (p.subtype.coprod q.subtype)
@[simp]
theorem
Submodule.map_inl
{R : Type u}
{M : Type v}
{M₂ : Type w}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
(p : Submodule R M)
:
Submodule.map (LinearMap.inl R M M₂) p = p.prod ⊥
@[simp]
theorem
Submodule.map_inr
{R : Type u}
{M : Type v}
{M₂ : Type w}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[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}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
(p : Submodule R M)
:
Submodule.comap (LinearMap.fst R M M₂) p = p.prod ⊤
@[simp]
theorem
Submodule.comap_snd
{R : Type u}
{M : Type v}
{M₂ : Type w}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[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}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
(p : Submodule R M)
(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}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
(p : Submodule R M)
(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}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
(p : Submodule R M)
(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}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
(p : Submodule R M)
(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}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
:
LinearMap.ker (LinearMap.inl R M M₂) = ⊥
@[simp]
theorem
Submodule.ker_inr
{R : Type u}
{M : Type v}
{M₂ : Type w}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
:
LinearMap.ker (LinearMap.inr R M M₂) = ⊥
@[simp]
theorem
Submodule.range_fst
{R : Type u}
{M : Type v}
{M₂ : Type w}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
:
LinearMap.range (LinearMap.fst R M M₂) = ⊤
@[simp]
theorem
Submodule.range_snd
{R : Type u}
{M : Type v}
{M₂ : Type w}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
:
LinearMap.range (LinearMap.snd R M M₂) = ⊤
def
Submodule.fst
(R : Type u)
(M : Type v)
(M₂ : Type w)
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
:
M as a submodule of M × N.
Equations
- Submodule.fst R M M₂ = Submodule.comap (LinearMap.snd R M M₂) ⊥
def
Submodule.fstEquiv
(R : Type u)
(M : Type v)
(M₂ : Type w)
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid 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.
Equations
- Submodule.fstEquiv R M M₂ = { toFun := fun (x : ↥(Submodule.fst R M M₂)) => (↑x).1, map_add' := ⋯, map_smul' := ⋯, invFun := fun (m : M) => ⟨(m, 0), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
@[simp]
theorem
Submodule.fstEquiv_symm_apply_coe
(R : Type u)
(M : Type v)
(M₂ : Type w)
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
(m : M)
:
↑((Submodule.fstEquiv R M M₂).symm m) = (m, 0)
@[simp]
theorem
Submodule.fstEquiv_apply
(R : Type u)
(M : Type v)
(M₂ : Type w)
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
(x : ↥(Submodule.fst R M M₂))
:
(Submodule.fstEquiv R M M₂) x = (↑x).1
theorem
Submodule.fst_map_fst
(R : Type u)
(M : Type v)
(M₂ : Type w)
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
:
Submodule.map (LinearMap.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]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
:
Submodule.map (LinearMap.snd R M M₂) (Submodule.fst R M M₂) = ⊥
def
Submodule.snd
(R : Type u)
(M : Type v)
(M₂ : Type w)
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
:
N as a submodule of M × N.
Equations
- Submodule.snd R M M₂ = Submodule.comap (LinearMap.fst R M M₂) ⊥
def
Submodule.sndEquiv
(R : Type u)
(M : Type v)
(M₂ : Type w)
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid 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
- Submodule.sndEquiv R M M₂ = { toFun := fun (x : ↥(Submodule.snd R M M₂)) => (↑x).2, map_add' := ⋯, map_smul' := ⋯, invFun := fun (n : M₂) => ⟨(0, n), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
@[simp]
theorem
Submodule.sndEquiv_apply
(R : Type u)
(M : Type v)
(M₂ : Type w)
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
(x : ↥(Submodule.snd R M M₂))
:
(Submodule.sndEquiv R M M₂) x = (↑x).2
@[simp]
theorem
Submodule.sndEquiv_symm_apply_coe
(R : Type u)
(M : Type v)
(M₂ : Type w)
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
(n : M₂)
:
↑((Submodule.sndEquiv R M M₂).symm n) = (0, n)
theorem
Submodule.snd_map_fst
(R : Type u)
(M : Type v)
(M₂ : Type w)
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
:
Submodule.map (LinearMap.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]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
:
Submodule.map (LinearMap.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]
[AddCommMonoid M]
[AddCommMonoid 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]
[AddCommMonoid M]
[AddCommMonoid 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]
[AddCommMonoid M]
[AddCommMonoid 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 (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)
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid 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 (LinearMap.inl R M M₂) p₁ ≤ q ∧ Submodule.map (LinearMap.inr R M M₂) p₂ ≤ q
def
LinearEquiv.prodComm
(R : Type u_3)
(M : Type u_4)
(N : Type u_5)
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[Module R M]
[Module R N]
:
Product of modules is commutative up to linear isomorphism.
Equations
- LinearEquiv.prodComm R M N = { toFun := Prod.swap, map_add' := ⋯, map_smul' := ⋯, invFun := AddEquiv.prodComm.invFun, left_inv := ⋯, right_inv := ⋯ }
@[simp]
theorem
LinearEquiv.prodComm_apply
(R : Type u_3)
(M : Type u_4)
(N : Type u_5)
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[Module R M]
[Module R N]
:
∀ (a : M × N), (LinearEquiv.prodComm R M N) a = a.swap
theorem
LinearEquiv.fst_comp_prodComm
{R : Type u}
{M : Type v}
{M₂ : Type w}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
:
LinearMap.fst R M₂ M ∘ₗ ↑(LinearEquiv.prodComm R M M₂) = LinearMap.snd R M M₂
theorem
LinearEquiv.snd_comp_prodComm
{R : Type u}
{M : Type v}
{M₂ : Type w}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
:
LinearMap.snd R M₂ M ∘ₗ ↑(LinearEquiv.prodComm R M M₂) = LinearMap.fst R M M₂
def
LinearEquiv.prodAssoc
(R : Type u_3)
(M₁ : Type u_4)
(M₂ : Type u_5)
(M₃ : Type u_6)
[Semiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[Module R M₁]
[Module R M₂]
[Module R M₃]
:
Product of modules is associative up to linear isomorphism.
Equations
- LinearEquiv.prodAssoc R M₁ M₂ M₃ = { toFun := AddEquiv.prodAssoc.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := AddEquiv.prodAssoc.invFun, left_inv := ⋯, right_inv := ⋯ }
@[simp]
theorem
LinearEquiv.prodAssoc_apply
(R : Type u_3)
(M₁ : Type u_4)
(M₂ : Type u_5)
(M₃ : Type u_6)
[Semiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[Module R M₁]
[Module R M₂]
[Module R M₃]
:
∀ (a : (M₁ × M₂) × M₃), (LinearEquiv.prodAssoc R M₁ M₂ M₃) a = AddEquiv.prodAssoc.toFun a
theorem
LinearEquiv.fst_comp_prodAssoc
{R : Type u}
{M₂ : Type w}
{M₃ : Type y}
{M₁ : Type u_3}
[Semiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[Module R M₁]
[Module R M₂]
[Module R M₃]
:
LinearMap.fst R M₁ (M₂ × M₃) ∘ₗ ↑(LinearEquiv.prodAssoc R M₁ M₂ M₃) = LinearMap.fst R M₁ M₂ ∘ₗ LinearMap.fst R (M₁ × M₂) M₃
theorem
LinearEquiv.snd_comp_prodAssoc
{R : Type u}
{M₂ : Type w}
{M₃ : Type y}
{M₁ : Type u_3}
[Semiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[Module R M₁]
[Module R M₂]
[Module R M₃]
:
LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ ↑(LinearEquiv.prodAssoc R M₁ M₂ M₃) = (LinearMap.snd R M₁ M₂).prodMap LinearMap.id
def
LinearEquiv.prodProdProdComm
(R : Type u)
(M : Type v)
(M₂ : Type w)
(M₃ : Type y)
(M₄ : Type z)
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[AddCommMonoid M₄]
[Module R M]
[Module R M₂]
[Module R M₃]
[Module R 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.
@[simp]
theorem
LinearEquiv.prodProdProdComm_apply
(R : Type u)
(M : Type v)
(M₂ : Type w)
(M₃ : Type y)
(M₄ : Type z)
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[AddCommMonoid M₄]
[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)
@[simp]
theorem
LinearEquiv.prodProdProdComm_symm
(R : Type u)
(M : Type v)
(M₂ : Type w)
(M₃ : Type y)
(M₄ : Type z)
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[AddCommMonoid M₄]
[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)
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[AddCommMonoid M₄]
[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}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[AddCommMonoid 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.prodCongr.
Equations
- e₁.prod e₂ = { toFun := (e₁.toAddEquiv.prodCongr e₂.toAddEquiv).toFun, map_add' := ⋯, map_smul' := ⋯, invFun := (e₁.toAddEquiv.prodCongr e₂.toAddEquiv).invFun, left_inv := ⋯, right_inv := ⋯ }
theorem
LinearEquiv.prod_symm
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
{M₄ : Type z}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[AddCommMonoid 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
LinearEquiv.prod_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
{M₄ : Type z}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[AddCommMonoid 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.1, e₂ p.2)
@[simp]
theorem
LinearEquiv.coe_prod
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
{M₄ : Type z}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[AddCommMonoid 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₁).prodMap ↑e₂
def
LinearEquiv.skewProd
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
{M₄ : Type z}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[AddCommGroup 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
- One or more equations did not get rendered due to their size.
@[simp]
theorem
LinearEquiv.skewProd_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
{M₄ : Type z}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[AddCommGroup 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
LinearEquiv.skewProd_symm_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
{M₄ : Type z}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[AddCommGroup 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
LinearMap.range_prod_eq
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[Ring R]
[AddCommGroup M]
[AddCommGroup M₂]
[AddCommGroup M₃]
[Module R M]
[Module R M₂]
[Module R M₃]
{f : M →ₗ[R] M₂}
{g : M →ₗ[R] M₃}
(h : LinearMap.ker f ⊔ LinearMap.ker g = ⊤)
:
LinearMap.range (f.prod g) = (LinearMap.range f).prod (LinearMap.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 #
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}
[AddCommGroup M]
[Module R M]
[AddCommGroup 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.tunnelAux Kφ = (Kφ.fst.subtype ∘ₗ ↑Kφ.snd.symm) ∘ₗ f
@[deprecated]
theorem
LinearMap.tunnelAux_injective
{R : Type u}
{M : Type v}
[Ring R]
{N : Type u_3}
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
(f : M × N →ₗ[R] M)
(i : Function.Injective ⇑f)
(Kφ : (K : Submodule R M) × ↥K ≃ₗ[R] M)
:
Function.Injective ⇑(f.tunnelAux Kφ)
@[deprecated]
def
LinearMap.tunnel'
{R : Type u}
{M : Type v}
[Ring R]
{N : Type u_3}
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
(f : M × N →ₗ[R] M)
(i : Function.Injective ⇑f)
:
Auxiliary definition for tunnel.
Equations
- One or more equations did not get rendered due to their size.
- f.tunnel' i 0 = ⟨⊤, LinearEquiv.ofTop ⊤ ⋯⟩
@[deprecated]
def
LinearMap.tunnel
{R : Type u}
{M : Type v}
[Ring R]
{N : Type u_3}
[AddCommGroup M]
[Module R M]
[AddCommGroup 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.
@[deprecated]
def
LinearMap.tailing
{R : Type u}
{M : Type v}
[Ring R]
{N : Type u_3}
[AddCommGroup M]
[Module R M]
[AddCommGroup 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.tunnelAux (f.tunnel' i n)) (Submodule.snd R M N)
@[deprecated]
def
LinearMap.tailingLinearEquiv
{R : Type u}
{M : Type v}
[Ring R]
{N : Type u_3}
[AddCommGroup M]
[Module R M]
[AddCommGroup 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.tailingLinearEquiv i n = (Submodule.equivMapOfInjective (f.tunnelAux (f.tunnel' i n)) ⋯ (Submodule.snd R M N)).symm.trans (Submodule.sndEquiv R M N)
@[deprecated]
theorem
LinearMap.tailing_le_tunnel
{R : Type u}
{M : Type v}
[Ring R]
{N : Type u_3}
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
(f : M × N →ₗ[R] M)
(i : Function.Injective ⇑f)
(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}
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
(f : M × N →ₗ[R] M)
(i : Function.Injective ⇑f)
(n : ℕ)
:
@[deprecated]
theorem
LinearMap.tailing_sup_tunnel_succ_le_tunnel
{R : Type u}
{M : Type v}
[Ring R]
{N : Type u_3}
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
(f : M × N →ₗ[R] M)
(i : Function.Injective ⇑f)
(n : ℕ)
:
@[deprecated]
def
LinearMap.tailings
{R : Type u}
{M : Type v}
[Ring R]
{N : Type u_3}
[AddCommGroup M]
[Module R M]
[AddCommGroup 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 = ⇑(partialSups (f.tailing i))
@[simp, deprecated]
theorem
LinearMap.tailings_zero
{R : Type u}
{M : Type v}
[Ring R]
{N : Type u_3}
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
(f : M × N →ₗ[R] M)
(i : Function.Injective ⇑f)
:
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}
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
(f : M × N →ₗ[R] M)
(i : Function.Injective ⇑f)
(n : ℕ)
:
@[deprecated]
theorem
LinearMap.tailings_disjoint_tunnel
{R : Type u}
{M : Type v}
[Ring R]
{N : Type u_3}
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
(f : M × N →ₗ[R] M)
(i : Function.Injective ⇑f)
(n : ℕ)
:
@[deprecated]
theorem
LinearMap.tailings_disjoint_tailing
{R : Type u}
{M : Type v}
[Ring R]
{N : Type u_3}
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
(f : M × N →ₗ[R] M)
(i : Function.Injective ⇑f)
(n : ℕ)
:
def
LinearMap.graph
{R : Type u}
{M : Type v}
{M₂ : Type w}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
(f : M →ₗ[R] M₂)
:
Graph of a linear map.
theorem
LinearMap.graph_eq_ker_coprod
{R : Type u}
{M₃ : Type y}
{M₄ : Type z}
[Semiring R]
[AddCommGroup M₃]
[AddCommGroup M₄]
[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}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
(f : M →ₗ[R] M₂)
:
f.graph = LinearMap.range (LinearMap.id.prod f)