Finsupps and sum/product types #
This file contains results about modules involving Finsupp and sum/product/sigma types.
Tags #
function with finite support, module, linear algebra
def
Finsupp.sumFinsuppLEquivProdFinsupp
{M : Type u_2}
(R : Type u_5)
[Semiring R]
[AddCommMonoid M]
[Module R M]
{α : Type u_7}
{β : Type u_8}
:
The linear equivalence between (α ⊕ β) →₀ M and (α →₀ M) × (β →₀ M).
This is the LinearEquiv version of Finsupp.sumFinsuppEquivProdFinsupp.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
Finsupp.sumFinsuppLEquivProdFinsupp_apply
{M : Type u_2}
(R : Type u_5)
[Semiring R]
[AddCommMonoid M]
[Module R M]
{α : Type u_7}
{β : Type u_8}
(a✝ : α ⊕ β →₀ M)
:
(Finsupp.sumFinsuppLEquivProdFinsupp R) a✝ = Finsupp.sumFinsuppAddEquivProdFinsupp.toFun a✝
@[simp]
theorem
Finsupp.sumFinsuppLEquivProdFinsupp_symm_apply
{M : Type u_2}
(R : Type u_5)
[Semiring R]
[AddCommMonoid M]
[Module R M]
{α : Type u_7}
{β : Type u_8}
(a✝ : (α →₀ M) × (β →₀ M))
:
(Finsupp.sumFinsuppLEquivProdFinsupp R).symm a✝ = Finsupp.sumFinsuppAddEquivProdFinsupp.invFun a✝
theorem
Finsupp.fst_sumFinsuppLEquivProdFinsupp
{M : Type u_2}
(R : Type u_5)
[Semiring R]
[AddCommMonoid M]
[Module R M]
{α : Type u_7}
{β : Type u_8}
(f : α ⊕ β →₀ M)
(x : α)
:
((Finsupp.sumFinsuppLEquivProdFinsupp R) f).1 x = f (Sum.inl x)
theorem
Finsupp.snd_sumFinsuppLEquivProdFinsupp
{M : Type u_2}
(R : Type u_5)
[Semiring R]
[AddCommMonoid M]
[Module R M]
{α : Type u_7}
{β : Type u_8}
(f : α ⊕ β →₀ M)
(y : β)
:
((Finsupp.sumFinsuppLEquivProdFinsupp R) f).2 y = f (Sum.inr y)
theorem
Finsupp.sumFinsuppLEquivProdFinsupp_symm_inl
{M : Type u_2}
(R : Type u_5)
[Semiring R]
[AddCommMonoid M]
[Module R M]
{α : Type u_7}
{β : Type u_8}
(fg : (α →₀ M) × (β →₀ M))
(x : α)
:
((Finsupp.sumFinsuppLEquivProdFinsupp R).symm fg) (Sum.inl x) = fg.1 x
theorem
Finsupp.sumFinsuppLEquivProdFinsupp_symm_inr
{M : Type u_2}
(R : Type u_5)
[Semiring R]
[AddCommMonoid M]
[Module R M]
{α : Type u_7}
{β : Type u_8}
(fg : (α →₀ M) × (β →₀ M))
(y : β)
:
((Finsupp.sumFinsuppLEquivProdFinsupp R).symm fg) (Sum.inr y) = fg.2 y
noncomputable def
Finsupp.sigmaFinsuppLEquivPiFinsupp
(R : Type u_5)
[Semiring R]
{η : Type u_7}
[Fintype η]
{M : Type u_9}
{ιs : η → Type u_10}
[AddCommMonoid M]
[Module R M]
:
On a Fintype η, Finsupp.split is a linear equivalence between
(Σ (j : η), ιs j) →₀ M and (j : η) → (ιs j →₀ M).
This is the LinearEquiv version of Finsupp.sigmaFinsuppAddEquivPiFinsupp.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
Finsupp.sigmaFinsuppLEquivPiFinsupp_apply
(R : Type u_5)
[Semiring R]
{η : Type u_7}
[Fintype η]
{M : Type u_9}
{ιs : η → Type u_10}
[AddCommMonoid M]
[Module R M]
(f : (j : η) × ιs j →₀ M)
(j : η)
(i : ιs j)
:
((Finsupp.sigmaFinsuppLEquivPiFinsupp R) f j) i = f ⟨j, i⟩
@[simp]
theorem
Finsupp.sigmaFinsuppLEquivPiFinsupp_symm_apply
(R : Type u_5)
[Semiring R]
{η : Type u_7}
[Fintype η]
{M : Type u_9}
{ιs : η → Type u_10}
[AddCommMonoid M]
[Module R M]
(f : (j : η) → ιs j →₀ M)
(ji : (j : η) × ιs j)
:
((Finsupp.sigmaFinsuppLEquivPiFinsupp R).symm f) ji = (f ji.fst) ji.snd