# mathlibdocumentation

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 #

• add_monoid_algebra.to_direct_sum : add_monoid_algebra M ι → (⨁ i : ι, M)
• direct_sum.to_add_monoid_algebra : (⨁ i : ι, M) → add_monoid_algebra M ι
• Bundled equiv versions of the above:
• add_monoid_algebra_equiv_direct_sum : add_monoid_algebra M ι ≃ (⨁ i : ι, M)
• add_monoid_algebra_add_equiv_direct_sum : add_monoid_algebra M ι ≃+ (⨁ i : ι, M)
• add_monoid_algebra_ring_equiv_direct_sum R : add_monoid_algebra M ι ≃+* (⨁ i : ι, M)
• add_monoid_algebra_alg_equiv_direct_sum R : add_monoid_algebra A ι ≃ₐ[R] (⨁ i : ι, A)

## Theorems #

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

• add_monoid_algebra.to_direct_sum_single
• direct_sum.to_add_monoid_algebra_of

as well as preserving arithmetic operations.

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

• add_monoid_algebra_add_equiv_direct_sum_apply
• add_monoid_algebra_lequiv_direct_sum_apply
• add_monoid_algebra_add_equiv_direct_sum_symm_apply
• add_monoid_algebra_lequiv_direct_sum_symm_apply

## 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 : ι) :
⨁ (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) :
= (direct_sum.of (λ (i : ι), M) i) 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) :
((direct_sum.of (λ (i : ι), M) i) m).to_add_monoid_algebra =
@[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 : ι) :
@[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 : ι) :
@[simp]
theorem add_monoid_algebra.to_direct_sum_mul {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [add_monoid ι] [semiring M] (f g : ι) :
@[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 #

@[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)] :
@[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)] :
def add_monoid_algebra_equiv_direct_sum {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [semiring M] [Π (m : M), decidable (m 0)] :
⨁ (i : ι), M

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

Equations
@[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)] :
@[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)] :
noncomputable def add_monoid_algebra_add_equiv_direct_sum {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [semiring M] [Π (m : M), decidable (m 0)] :
≃+ ⨁ (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
@[simp]
theorem add_monoid_algebra_ring_equiv_direct_sum_apply {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [add_monoid ι] [semiring M] [Π (m : M), decidable (m 0)] :
noncomputable 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)] :
≃+* ⨁ (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
@[simp]
theorem add_monoid_algebra_ring_equiv_direct_sum_symm_apply {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [add_monoid ι] [semiring M] [Π (m : M), decidable (m 0)] :
@[simp]
theorem add_monoid_algebra_alg_equiv_direct_sum_apply {ι : Type u_1} {R : Type u_2} {A : Type u_4} [decidable_eq ι] [add_monoid ι] [semiring A] [ A] [Π (m : A), decidable (m 0)] :
noncomputable def add_monoid_algebra_alg_equiv_direct_sum {ι : Type u_1} {R : Type u_2} {A : Type u_4} [decidable_eq ι] [add_monoid ι] [semiring A] [ A] [Π (m : A), decidable (m 0)] :
≃ₐ[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
@[simp]
theorem add_monoid_algebra_alg_equiv_direct_sum_symm_apply {ι : Type u_1} {R : Type u_2} {A : Type u_4} [decidable_eq ι] [add_monoid ι] [semiring A] [ A] [Π (m : A), decidable (m 0)] :