Mathlib.LinearAlgebra.Finsupp.SumProd

Finsupp.sumFinsuppLEquivProdFinsupp definition

{α β : Type*} : (α ⊕ β →₀ M) ≃ₗ[R] (α →₀ M) × (β →₀ M)

Full source

/-- The linear equivalence between `(α ⊕ β) →₀ M` and `(α →₀ M) × (β →₀ M)`.

This is the `LinearEquiv` version of `Finsupp.sumFinsuppEquivProdFinsupp`. -/
@[simps apply symm_apply]
def sumFinsuppLEquivProdFinsupp {α β : Type*} : (α ⊕ β →₀ M) ≃ₗ[R] (α →₀ M) × (β →₀ M) :=
  { sumFinsuppAddEquivProdFinsupp with
    map_smul' := by
      intros
      ext <;>
        simp only [AddEquiv.toFun_eq_coe, Prod.smul_fst, Prod.smul_snd, smul_apply,
          snd_sumFinsuppAddEquivProdFinsupp, fst_sumFinsuppAddEquivProdFinsupp,
          RingHom.id_apply] }

Linear equivalence between finitely supported functions on a sum type and pairs of finitely supported functions

Informal description

The linear equivalence between the space of finitely supported functions on a sum type $\alpha \oplus \beta$ and the product space of finitely supported functions on $\alpha$ and $\beta$. Specifically, it establishes a linear isomorphism between $(\alpha \oplus \beta) \to_0 M$ and $(\alpha \to_0 M) \times (\beta \to_0 M)$, where $M$ is a module over a semiring $R$. This equivalence extends the additive equivalence `sumFinsuppAddEquivProdFinsupp` by additionally preserving scalar multiplication. The forward direction splits a function $f \colon \alpha \oplus \beta \to_0 M$ into two functions: one obtained by restricting $f$ to $\alpha$ via the left inclusion $\operatorname{inl}$, and the other by restricting $f$ to $\beta$ via the right inclusion $\operatorname{inr}$. The inverse direction combines two functions $f_1 \colon \alpha \to_0 M$ and $f_2 \colon \beta \to_0 M$ into a single function on $\alpha \oplus \beta$ using the sum elimination function.

Finsupp.fst_sumFinsuppLEquivProdFinsupp theorem

{α β : Type*} (f : α ⊕ β →₀ M) (x : α) : (sumFinsuppLEquivProdFinsupp R f).1 x = f (Sum.inl x)

Full source

theorem fst_sumFinsuppLEquivProdFinsupp {α β : Type*} (f : α ⊕ βα ⊕ β →₀ M) (x : α) :
    (sumFinsuppLEquivProdFinsupp R f).1 x = f (Sum.inl x) :=
  rfl

First Component of Linear Equivalence for Finitely Supported Functions on Sum Type Evaluates to Left Inclusion

Informal description

For any types $\alpha$ and $\beta$, and any finitely supported function $f \colon \alpha \oplus \beta \to_{\text{f}} M$, the first component of the linear equivalence $\text{sumFinsuppLEquivProdFinsupp}_R(f)$ evaluated at $x \in \alpha$ is equal to $f$ evaluated at the left inclusion $\operatorname{inl}(x)$. That is, \[ (\text{sumFinsuppLEquivProdFinsupp}_R(f))_1(x) = f(\operatorname{inl}(x)). \]

Finsupp.snd_sumFinsuppLEquivProdFinsupp theorem

{α β : Type*} (f : α ⊕ β →₀ M) (y : β) : (sumFinsuppLEquivProdFinsupp R f).2 y = f (Sum.inr y)

Full source

theorem snd_sumFinsuppLEquivProdFinsupp {α β : Type*} (f : α ⊕ βα ⊕ β →₀ M) (y : β) :
    (sumFinsuppLEquivProdFinsupp R f).2 y = f (Sum.inr y) :=
  rfl

Second Component of Linear Equivalence for Finitely Supported Functions on Sum Type Evaluates to Right Inclusion

Informal description

For any types $\alpha$ and $\beta$, and any finitely supported function $f \colon \alpha \oplus \beta \to_{\text{f}} M$, the second component of the linear equivalence `sumFinsuppLEquivProdFinsupp` applied to $f$ evaluated at $y \in \beta$ is equal to $f$ evaluated at the right inclusion $\operatorname{inr}(y)$. That is, \[ (\text{sumFinsuppLEquivProdFinsupp}_R(f))_2(y) = f(\operatorname{inr}(y)). \]

Finsupp.sumFinsuppLEquivProdFinsupp_symm_inl theorem

 {α β : Type*} (fg : (α →₀ M) × (β →₀ M)) (x : α) : ((sumFinsuppLEquivProdFinsupp R).symm fg) (Sum.inl x) = fg.1 x

Full source

theorem sumFinsuppLEquivProdFinsupp_symm_inl {α β : Type*} (fg : (α →₀ M) × (β →₀ M)) (x : α) :
    ((sumFinsuppLEquivProdFinsupp R).symm fg) (Sum.inl x) = fg.1 x :=
  rfl

Inverse of Linear Equivalence for Finitely Supported Functions on Sum Type Evaluates Left Inclusion to First Component

Informal description

For any types $\alpha$ and $\beta$, and any pair of finitely supported functions $(f,g) \in (\alpha \to_{\text{f}} M) \times (\beta \to_{\text{f}} M)$, the inverse of the linear equivalence `sumFinsuppLEquivProdFinsupp` evaluated at the left inclusion $\operatorname{inl}(x)$ for $x \in \alpha$ is equal to $f(x)$. That is, \[ (\text{sumFinsuppLEquivProdFinsupp}_R)^{-1}(f,g)(\operatorname{inl}(x)) = f(x). \]

Finsupp.sumFinsuppLEquivProdFinsupp_symm_inr theorem

 {α β : Type*} (fg : (α →₀ M) × (β →₀ M)) (y : β) : ((sumFinsuppLEquivProdFinsupp R).symm fg) (Sum.inr y) = fg.2 y

Full source

theorem sumFinsuppLEquivProdFinsupp_symm_inr {α β : Type*} (fg : (α →₀ M) × (β →₀ M)) (y : β) :
    ((sumFinsuppLEquivProdFinsupp R).symm fg) (Sum.inr y) = fg.2 y :=
  rfl

Inverse of Linear Equivalence for Finitely Supported Functions Evaluates Right Inclusion as Second Component

Informal description

For any types $\alpha$ and $\beta$, and any pair of finitely supported functions $(f,g) \in (\alpha \to_{\text{f}} M) \times (\beta \to_{\text{f}} M)$, the inverse of the linear equivalence `sumFinsuppLEquivProdFinsupp` evaluated at the right inclusion $\operatorname{inr}(y)$ for $y \in \beta$ equals $g(y)$. That is, \[ (\text{sumFinsuppLEquivProdFinsupp}_R)^{-1}(f,g)(\operatorname{inr}(y)) = g(y). \]

Finsupp.sigmaFinsuppLEquivPiFinsupp definition

 {M : Type*} {ιs : η → Type*} [AddCommMonoid M] [Module R M] : ((Σ j, ιs j) →₀ M) ≃ₗ[R] (j : _) → (ιs j →₀ M)

Full source

/-- 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`. -/
noncomputable def sigmaFinsuppLEquivPiFinsupp {M : Type*} {ιs : η → Type*} [AddCommMonoid M]
    [Module R M] : ((Σ j, ιs j) →₀ M) ≃ₗ[R] (j : _) → (ιs j →₀ M) :=
  { sigmaFinsuppAddEquivPiFinsupp with
    map_smul' := fun c f => by
      ext
      simp }

Linear equivalence between finitely supported functions on a sigma type and product of finitely supported functions

Informal description

Given a finite type $\eta$, a family of types $\iota_j$ indexed by $j \in \eta$, an additive commutative monoid $M$, and a module structure over a semiring $R$ on $M$, the linear equivalence `Finsupp.sigmaFinsuppLEquivPiFinsupp` establishes a bijection between finitely supported functions from the sigma type $\Sigma (j : \eta), \iota_j$ to $M$ and the product type $\Pi j, (\iota_j \to_{\text{f}} M)$ of finitely supported functions from each $\iota_j$ to $M$. This equivalence preserves both addition and scalar multiplication, meaning that the sum of two finitely supported functions on the sigma type corresponds to the pointwise sum of their images under the equivalence, and scalar multiplication is similarly preserved.

Finsupp.sigmaFinsuppLEquivPiFinsupp_apply theorem

 {M : Type*} {ιs : η → Type*} [AddCommMonoid M] [Module R M] (f : (Σ j, ιs j) →₀ M) (j i) :
  sigmaFinsuppLEquivPiFinsupp R f j i = f ⟨j, i⟩

Full source

@[simp]
theorem sigmaFinsuppLEquivPiFinsupp_apply {M : Type*} {ιs : η → Type*} [AddCommMonoid M]
    [Module R M] (f : (Σ j, ιs j) →₀ M) (j i) : sigmaFinsuppLEquivPiFinsupp R f j i = f ⟨j, i⟩ :=
  rfl

Evaluation of the Linear Equivalence between Sigma and Pi Finitely Supported Functions

Informal description

Let $R$ be a semiring, $M$ an additive commutative monoid with a module structure over $R$, and $\eta$ a finite type. Given a family of types $\iota_j$ indexed by $j \in \eta$ and a finitely supported function $f : (\Sigma j, \iota_j) \to_{\text{f}} M$, the linear equivalence `sigmaFinsuppLEquivPiFinsupp` satisfies \[ (\text{sigmaFinsuppLEquivPiFinsupp}\, R\, f)\, j\, i = f \langle j, i \rangle \] for all $j \in \eta$ and $i \in \iota_j$.

Finsupp.sigmaFinsuppLEquivPiFinsupp_symm_apply theorem

 {M : Type*} {ιs : η → Type*} [AddCommMonoid M] [Module R M] (f : (j : _) → (ιs j →₀ M)) (ji) :
  (Finsupp.sigmaFinsuppLEquivPiFinsupp R).symm f ji = f ji.1 ji.2

Full source

@[simp]
theorem sigmaFinsuppLEquivPiFinsupp_symm_apply {M : Type*} {ιs : η → Type*} [AddCommMonoid M]
    [Module R M] (f : (j : _) → (ιs j →₀ M)) (ji) :
    (Finsupp.sigmaFinsuppLEquivPiFinsupp R).symm f ji = f ji.1 ji.2 :=
  rfl

Inverse of Linear Equivalence Between Sigma and Product Finsupps

Informal description

Let $\eta$ be a finite type, $\iota_j$ a family of types indexed by $j \in \eta$, $M$ an additive commutative monoid with a module structure over a semiring $R$, and $f$ a family of finitely supported functions $f_j : \iota_j \to_{\text{f}} M$ for each $j \in \eta$. The inverse of the linear equivalence `Finsupp.sigmaFinsuppLEquivPiFinsupp` maps $f$ to a finitely supported function on the sigma type $\Sigma (j : \eta), \iota_j$ such that for any $(j, i) \in \Sigma (j : \eta), \iota_j$, the value at $(j, i)$ is given by $f_j(i)$.

Tags