mathlib documentation

algebra.monoid_algebra_to_direct_sum

Conversion between add_monoid_algebra and homogenous direct_sum #

This module provides conversions between add_monoid_algebra and direct_sum. The latter is essentially a dependent version of the former.

Note that since direct_sum.has_mul combines indices additively, there is no equivalent to monoid_algebra.

Main definitions #

Theorems #

The defining feature of these operations is that they map finsupp.single to direct_sum.of and vice versa:

as well as preserving arithmetic operations.

For the bundled equivalences, we provide lemmas that they reduce to add_monoid_algebra.to_direct_sum:

Implementation notes #

This file largely just copies the API of data/finsupp/to_dfinsupp, and reuses the proofs. Recall that add_monoid_algebra M ι is defeq to ι →₀ M and ⨁ i : ι, M is defeq to Π₀ i : ι, M.

Note that there is no add_monoid_algebra equivalent to finsupp.single, so many statements still involve this definition.

Basic definitions and lemmas #

source
def add_monoid_algebra.to_direct_sum {ι : Type u_1} {M : Type u_3} [semiring M] (f : add_monoid_algebra M ι) :
⨁ (i : ι), M

Interpret a add_monoid_algebra as a homogenous direct_sum.

Equations
source
@[simp]
theorem add_monoid_algebra.to_direct_sum_single {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [semiring M] (i : ι) (m : M) :
add_monoid_algebra.to_direct_sum (finsupp.single i m) = ⇑(direct_sum.of (λ (i : ι), M) i) m
source
def direct_sum.to_add_monoid_algebra {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [semiring M] [Π (m : M), decidable (m ≠ 0)] (f : ⨁ (i : ι), M) :
add_monoid_algebra M ι

Interpret a homogenous direct_sum as a add_monoid_algebra.

Equations
source
@[simp]
theorem direct_sum.to_add_monoid_algebra_of {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [semiring M] [Π (m : M), decidable (m ≠ 0)] (i : ι) (m : M) :
(⇑(direct_sum.of (λ (i : ι), M) i) m).to_add_monoid_algebra = finsupp.single i m
source
@[simp]
theorem add_monoid_algebra.to_direct_sum_to_add_monoid_algebra {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [semiring M] [Π (m : M), decidable (m ≠ 0)] (f : add_monoid_algebra M ι) :
f.to_direct_sum.to_add_monoid_algebra = f
source
@[simp]
theorem direct_sum.to_add_monoid_algebra_to_direct_sum {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [semiring M] [Π (m : M), decidable (m ≠ 0)] (f : ⨁ (i : ι), M) :
f.to_add_monoid_algebra.to_direct_sum = f

Lemmas about arithmetic operations #

source
@[simp]
theorem add_monoid_algebra.to_direct_sum_zero {ι : Type u_1} {M : Type u_3} [semiring M] :
0.to_direct_sum = 0
source
@[simp]
theorem add_monoid_algebra.to_direct_sum_add {ι : Type u_1} {M : Type u_3} [semiring M] (f g : add_monoid_algebra M ι) :
(f + g).to_direct_sum = f.to_direct_sum + g.to_direct_sum
source
@[simp]
theorem add_monoid_algebra.to_direct_sum_mul {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [add_monoid ι] [semiring M] (f g : add_monoid_algebra M ι) :
(f * g).to_direct_sum = (f.to_direct_sum) * g.to_direct_sum
source
@[simp]
theorem direct_sum.to_add_monoid_algebra_zero {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [semiring M] [Π (m : M), decidable (m ≠ 0)] :
0.to_add_monoid_algebra = 0
source
@[simp]
theorem direct_sum.to_add_monoid_algebra_add {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [semiring M] [Π (m : M), decidable (m ≠ 0)] (f g : ⨁ (i : ι), M) :
(f + g).to_add_monoid_algebra = f.to_add_monoid_algebra + g.to_add_monoid_algebra
source
@[simp]
theorem direct_sum.to_add_monoid_algebra_mul {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [add_monoid ι] [semiring M] [Π (m : M), decidable (m ≠ 0)] (f g : ⨁ (i : ι), M) :
(f * g).to_add_monoid_algebra = (f.to_add_monoid_algebra) * g.to_add_monoid_algebra

Bundled equivs #

source
@[simp]
theorem add_monoid_algebra_equiv_direct_sum_apply {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [semiring M] [Π (m : M), decidable (m ≠ 0)] :
⇑add_monoid_algebra_equiv_direct_sum = add_monoid_algebra.to_direct_sum
source
@[simp]
theorem add_monoid_algebra_equiv_direct_sum_symm_apply {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [semiring M] [Π (m : M), decidable (m ≠ 0)] :
⇑(add_monoid_algebra_equiv_direct_sum.symm) = direct_sum.to_add_monoid_algebra
source
def add_monoid_algebra_equiv_direct_sum {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [semiring M] [Π (m : M), decidable (m ≠ 0)] :
add_monoid_algebra M ι ≃ ⨁ (i : ι), M

add_monoid_algebra.to_direct_sum and direct_sum.to_add_monoid_algebra together form an equiv.

Equations
source
@[simp]
theorem add_monoid_algebra_add_equiv_direct_sum_apply {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [semiring M] [Π (m : M), decidable (m ≠ 0)] :
⇑add_monoid_algebra_add_equiv_direct_sum = add_monoid_algebra.to_direct_sum
source
@[simp]
theorem add_monoid_algebra_add_equiv_direct_sum_symm_apply {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [semiring M] [Π (m : M), decidable (m ≠ 0)] :
⇑(add_monoid_algebra_add_equiv_direct_sum.symm) = direct_sum.to_add_monoid_algebra
source
def add_monoid_algebra_add_equiv_direct_sum {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [semiring M] [Π (m : M), decidable (m ≠ 0)] :
add_monoid_algebra M ι ≃+ ⨁ (i : ι), M

The additive version of add_monoid_algebra.to_add_monoid_algebra. Note that this is noncomputable because add_monoid_algebra.has_add is noncomputable.

Equations
source
def add_monoid_algebra_ring_equiv_direct_sum {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [add_monoid ι] [semiring M] [Π (m : M), decidable (m ≠ 0)] :
add_monoid_algebra M ι ≃+* ⨁ (i : ι), M

add_monoid_algebra is equivalent to a homogenous direct sum. This is non-computable because add_monoid_algebra is noncomputable.

Equations