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 #

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
@[simp]
theorem add_monoid_algebra.to_direct_sum_single {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [semiring M] (i : ι) (m : M) :
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) :

Interpret a homogenous direct_sum as a add_monoid_algebra.

Equations
@[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) :
@[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 ι) :
@[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) :

Lemmas about arithmetic operations #

@[simp]
theorem add_monoid_algebra.to_direct_sum_zero {ι : Type u_1} {M : Type u_3} [semiring M] :
@[simp]
theorem add_monoid_algebra.to_direct_sum_add {ι : Type u_1} {M : Type u_3} [semiring M] (f g : add_monoid_algebra M ι) :
@[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 ι) :
@[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)] :
@[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) :
@[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) :

Bundled equivs #

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
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
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

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

Equations
def add_monoid_algebra_alg_equiv_direct_sum {ι : Type u_1} {R : Type u_2} {A : Type u_4} [decidable_eq ι] [add_monoid ι] [comm_semiring R] [semiring A] [algebra R A] [Π (m : A), decidable (m 0)] :
add_monoid_algebra A ι ≃ₐ[R] ⨁ (i : ι), A

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

Equations