# Documentation

Mathlib.Algebra.MonoidAlgebra.ToDirectSum

# Conversion between AddMonoidAlgebra and homogenous DirectSum#

This module provides conversions between AddMonoidAlgebra and DirectSum. 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 MonoidAlgebra.

## Main definitions #

• AddMonoidAlgebra.toDirectSum : AddMonoidAlgebra M ι → (⨁ i : ι, M)
• DirectSum.toAddMonoidAlgebra : (⨁ i : ι, M) → AddMonoidAlgebra M ι
• Bundled equiv versions of the above:
• addMonoidAlgebraEquivDirectSum : AddMonoidAlgebra M ι ≃ (⨁ i : ι, M)
• addMonoidAlgebraAddEquivDirectSum : AddMonoidAlgebra M ι ≃+ (⨁ i : ι, M)
• addMonoidAlgebraRingEquivDirectSum R : AddMonoidAlgebra M ι ≃+* (⨁ i : ι, M)
• addMonoidAlgebraAlgEquivDirectSum R : AddMonoidAlgebra A ι ≃ₐ[R] (⨁ i : ι, A)

## Theorems #

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

• AddMonoidAlgebra.toDirectSum_single
• DirectSum.toAddMonoidAlgebra_of

as well as preserving arithmetic operations.

For the bundled equivalences, we provide lemmas that they reduce to AddMonoidAlgebra.toDirectSum:

• addMonoidAlgebraAddEquivDirectSum_apply
• add_monoid_algebra_lequiv_direct_sum_apply
• addMonoidAlgebraAddEquivDirectSum_symm_apply
• add_monoid_algebra_lequiv_direct_sum_symm_apply

## Implementation notes #

This file largely just copies the API of Mathlib/Data/Finsupp/ToDFinsupp.lean, and reuses the proofs. Recall that AddMonoidAlgebra M ι is defeq to ι →₀ M and ⨁ i : ι, M is defeq to Π₀ i : ι, M.

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

### Basic definitions and lemmas #

def AddMonoidAlgebra.toDirectSum {ι : Type u_1} {M : Type u_3} [] (f : ) :
⨁ (x : ι), M

Interpret an AddMonoidAlgebra as a homogenous DirectSum.

Instances For
@[simp]
theorem AddMonoidAlgebra.toDirectSum_single {ι : Type u_1} {M : Type u_3} [] [] (i : ι) (m : M) :
(AddMonoidAlgebra.toDirectSum fun₀ | i => m) = ↑(DirectSum.of (fun i => M) i) m
def DirectSum.toAddMonoidAlgebra {ι : Type u_1} {M : Type u_3} [] [] [(m : M) → Decidable (m 0)] (f : ⨁ (x : ι), M) :

Interpret a homogenous DirectSum as an AddMonoidAlgebra.

Instances For
@[simp]
theorem DirectSum.toAddMonoidAlgebra_of {ι : Type u_1} {M : Type u_3} [] [] [(m : M) → Decidable (m 0)] (i : ι) (m : M) :
DirectSum.toAddMonoidAlgebra (↑(DirectSum.of (fun x => M) i) m) = fun₀ | i => m
@[simp]
theorem AddMonoidAlgebra.toDirectSum_toAddMonoidAlgebra {ι : Type u_1} {M : Type u_3} [] [] [(m : M) → Decidable (m 0)] (f : ) :
@[simp]
theorem DirectSum.toAddMonoidAlgebra_toDirectSum {ι : Type u_1} {M : Type u_3} [] [] [(m : M) → Decidable (m 0)] (f : ⨁ (x : ι), M) :

### Lemmas about arithmetic operations #

@[simp]
theorem AddMonoidAlgebra.toDirectSum_zero {ι : Type u_1} {M : Type u_3} [] :
@[simp]
theorem AddMonoidAlgebra.toDirectSum_add {ι : Type u_1} {M : Type u_3} [] (f : ) (g : ) :
@[simp]
theorem AddMonoidAlgebra.toDirectSum_mul {ι : Type u_1} {M : Type u_3} [] [] [] (f : ) (g : ) :
@[simp]
theorem DirectSum.toAddMonoidAlgebra_zero {ι : Type u_1} {M : Type u_3} [] [] [(m : M) → Decidable (m 0)] :
@[simp]
theorem DirectSum.toAddMonoidAlgebra_add {ι : Type u_1} {M : Type u_3} [] [] [(m : M) → Decidable (m 0)] (f : ⨁ (x : ι), M) (g : ⨁ (x : ι), M) :
@[simp]
theorem DirectSum.toAddMonoidAlgebra_mul {ι : Type u_1} {M : Type u_3} [] [] [] [(m : M) → Decidable (m 0)] (f : ⨁ (x : ι), M) (g : ⨁ (x : ι), M) :

### Bundled Equivs #

@[simp]
theorem addMonoidAlgebraEquivDirectSum_symm_apply {ι : Type u_1} {M : Type u_3} [] [] [(m : M) → Decidable (m 0)] :
@[simp]
theorem addMonoidAlgebraEquivDirectSum_apply {ι : Type u_1} {M : Type u_3} [] [] [(m : M) → Decidable (m 0)] :
def addMonoidAlgebraEquivDirectSum {ι : Type u_1} {M : Type u_3} [] [] [(m : M) → Decidable (m 0)] :
⨁ (x : ι), M

AddMonoidAlgebra.toDirectSum and DirectSum.toAddMonoidAlgebra together form an equiv.

Instances For
@[simp]
theorem addMonoidAlgebraAddEquivDirectSum_symm_apply {ι : Type u_1} {M : Type u_3} [] [] [(m : M) → Decidable (m 0)] :
@[simp]
theorem addMonoidAlgebraAddEquivDirectSum_apply {ι : Type u_1} {M : Type u_3} [] [] [(m : M) → Decidable (m 0)] :
def addMonoidAlgebraAddEquivDirectSum {ι : Type u_1} {M : Type u_3} [] [] [(m : M) → Decidable (m 0)] :
≃+ ⨁ (x : ι), M

The additive version of AddMonoidAlgebra.addMonoidAlgebraEquivDirectSum.

Instances For
@[simp]
theorem addMonoidAlgebraRingEquivDirectSum_symm_apply {ι : Type u_1} {M : Type u_3} [] [] [] [(m : M) → Decidable (m 0)] :
@[simp]
theorem addMonoidAlgebraRingEquivDirectSum_apply {ι : Type u_1} {M : Type u_3} [] [] [] [(m : M) → Decidable (m 0)] :
def addMonoidAlgebraRingEquivDirectSum {ι : Type u_1} {M : Type u_3} [] [] [] [(m : M) → Decidable (m 0)] :
≃+* ⨁ (x : ι), M

The ring version of AddMonoidAlgebra.addMonoidAlgebraEquivDirectSum.

Instances For
@[simp]
theorem addMonoidAlgebraAlgEquivDirectSum_symm_apply {ι : Type u_1} {R : Type u_2} {A : Type u_4} [] [] [] [] [Algebra R A] [(m : A) → Decidable (m 0)] :
The algebra version of AddMonoidAlgebra.addMonoidAlgebraEquivDirectSum.