Documentation

Mathlib.LinearAlgebra.Finsupp.SumProd

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

source
noncomputable def Finsupp.sumFinsuppLEquivProdFinsupp {M : Type u_2} (R : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_4} {β : Type u_5} :
(α ⊕ β →₀ M) ≃ₗ[R] (α →₀ M) × (β →₀ M)

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
    source
    @[simp]
    theorem Finsupp.sumFinsuppLEquivProdFinsupp_apply {M : Type u_2} (R : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_4} {β : Type u_5} (a✝ : α ⊕ β →₀ M) :
    (sumFinsuppLEquivProdFinsupp R) a✝ = sumFinsuppAddEquivProdFinsupp.toFun a✝
    source
    @[simp]
    theorem Finsupp.sumFinsuppLEquivProdFinsupp_symm_apply {M : Type u_2} (R : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_4} {β : Type u_5} (a✝ : (α →₀ M) × (β →₀ M)) :
    (sumFinsuppLEquivProdFinsupp R).symm a✝ = sumFinsuppAddEquivProdFinsupp.invFun a✝
    source
    theorem Finsupp.fst_sumFinsuppLEquivProdFinsupp {M : Type u_2} (R : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_4} {β : Type u_5} (f : α ⊕ β →₀ M) (x : α) :
    ((sumFinsuppLEquivProdFinsupp R) f).1 x = f (Sum.inl x)
    source
    theorem Finsupp.snd_sumFinsuppLEquivProdFinsupp {M : Type u_2} (R : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_4} {β : Type u_5} (f : α ⊕ β →₀ M) (y : β) :
    ((sumFinsuppLEquivProdFinsupp R) f).2 y = f (Sum.inr y)
    source
    theorem Finsupp.sumFinsuppLEquivProdFinsupp_symm_inl {M : Type u_2} (R : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_4} {β : Type u_5} (fg : (α →₀ M) × (β →₀ M)) (x : α) :
    ((sumFinsuppLEquivProdFinsupp R).symm fg) (Sum.inl x) = fg.1 x
    source
    theorem Finsupp.sumFinsuppLEquivProdFinsupp_symm_inr {M : Type u_2} (R : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_4} {β : Type u_5} (fg : (α →₀ M) × (β →₀ M)) (y : β) :
    ((sumFinsuppLEquivProdFinsupp R).symm fg) (Sum.inr y) = fg.2 y
    source
    noncomputable def Finsupp.sigmaFinsuppLEquivPiFinsupp (R : Type u_3) [Semiring R] {η : Type u_4} [Fintype η] {M : Type u_6} {ιs : η → Type u_7} [AddCommMonoid M] [Module R M] :
    ((j : η) × ιs j →₀ M) ≃ₗ[R] (j : η) → ιs j →₀ 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
      source
      @[simp]
      theorem Finsupp.sigmaFinsuppLEquivPiFinsupp_apply (R : Type u_3) [Semiring R] {η : Type u_4} [Fintype η] {M : Type u_6} {ιs : η → Type u_7} [AddCommMonoid M] [Module R M] (f : (j : η) × ιs j →₀ M) (j : η) (i : ιs j) :
      ((sigmaFinsuppLEquivPiFinsupp R) f j) i = f ⟨j, i⟩
      source
      @[simp]
      theorem Finsupp.sigmaFinsuppLEquivPiFinsupp_symm_apply (R : Type u_3) [Semiring R] {η : Type u_4} [Fintype η] {M : Type u_6} {ιs : η → Type u_7} [AddCommMonoid M] [Module R M] (f : (j : η) → ιs j →₀ M) (ji : (j : η) × ιs j) :
      ((sigmaFinsuppLEquivPiFinsupp R).symm f) ji = (f ji.fst) ji.snd