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.

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 : ι) :
⨁ (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) :

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

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

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

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