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} [Semiring M] (f : AddMonoidAlgebra M ι) : DirectSum ι fun (x : ι) => M

Interpret an AddMonoidAlgebra as a homogenous DirectSum.

Equations

• AddMonoidAlgebra.toDirectSum f = Finsupp.toDFinsupp f

@[simp]

theorem AddMonoidAlgebra.toDirectSum_single {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Semiring M] (i : ι) (m : M) : AddMonoidAlgebra.toDirectSum (Finsupp.single i m) = (DirectSum.of (fun (i : ι) => M) i) m

def DirectSum.toAddMonoidAlgebra {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Semiring M] [(m : M) → Decidable (m ≠ 0)] (f : DirectSum ι fun (x : ι) => M) : AddMonoidAlgebra M ι

Interpret a homogenous DirectSum as an AddMonoidAlgebra.

Equations

• DirectSum.toAddMonoidAlgebra f = DFinsupp.toFinsupp f

@[simp]

theorem DirectSum.toAddMonoidAlgebra_of {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Semiring M] [(m : M) → Decidable (m ≠ 0)] (i : ι) (m : M) : DirectSum.toAddMonoidAlgebra ((DirectSum.of (fun (x : ι) => M) i) m) = Finsupp.single i m

@[simp]

theorem AddMonoidAlgebra.toDirectSum_toAddMonoidAlgebra {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Semiring M] [(m : M) → Decidable (m ≠ 0)] (f : AddMonoidAlgebra M ι) : DirectSum.toAddMonoidAlgebra (AddMonoidAlgebra.toDirectSum f) = f

@[simp]

theorem DirectSum.toAddMonoidAlgebra_toDirectSum {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Semiring M] [(m : M) → Decidable (m ≠ 0)] (f : DirectSum ι fun (x : ι) => M) : AddMonoidAlgebra.toDirectSum (DirectSum.toAddMonoidAlgebra f) = f

Lemmas about arithmetic operations

@[simp]

theorem AddMonoidAlgebra.toDirectSum_zero {ι : Type u_1} {M : Type u_3} [Semiring M] : AddMonoidAlgebra.toDirectSum 0 = 0

@[simp]

theorem AddMonoidAlgebra.toDirectSum_add {ι : Type u_1} {M : Type u_3} [Semiring M] (f : AddMonoidAlgebra M ι) (g : AddMonoidAlgebra M ι) : AddMonoidAlgebra.toDirectSum (f + g) = AddMonoidAlgebra.toDirectSum f + AddMonoidAlgebra.toDirectSum g

@[simp]

theorem AddMonoidAlgebra.toDirectSum_mul {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddMonoid ι] [Semiring M] (f : AddMonoidAlgebra M ι) (g : AddMonoidAlgebra M ι) : AddMonoidAlgebra.toDirectSum (f * g) = AddMonoidAlgebra.toDirectSum f * AddMonoidAlgebra.toDirectSum g

@[simp]

theorem DirectSum.toAddMonoidAlgebra_zero {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Semiring M] [(m : M) → Decidable (m ≠ 0)] : DirectSum.toAddMonoidAlgebra 0 = 0

@[simp]

theorem DirectSum.toAddMonoidAlgebra_add {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Semiring M] [(m : M) → Decidable (m ≠ 0)] (f : DirectSum ι fun (x : ι) => M) (g : DirectSum ι fun (x : ι) => M) : DirectSum.toAddMonoidAlgebra (f + g) = DirectSum.toAddMonoidAlgebra f + DirectSum.toAddMonoidAlgebra g

@[simp]

theorem DirectSum.toAddMonoidAlgebra_mul {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddMonoid ι] [Semiring M] [(m : M) → Decidable (m ≠ 0)] (f : DirectSum ι fun (x : ι) => M) (g : DirectSum ι fun (x : ι) => M) : DirectSum.toAddMonoidAlgebra (f * g) = DirectSum.toAddMonoidAlgebra f * DirectSum.toAddMonoidAlgebra g

Bundled Equivs

@[simp]

theorem addMonoidAlgebraEquivDirectSum_symm_apply {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Semiring M] [(m : M) → Decidable (m ≠ 0)] : ⇑addMonoidAlgebraEquivDirectSum.symm = DirectSum.toAddMonoidAlgebra

@[simp]

theorem addMonoidAlgebraEquivDirectSum_apply {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Semiring M] [(m : M) → Decidable (m ≠ 0)] : ⇑addMonoidAlgebraEquivDirectSum = AddMonoidAlgebra.toDirectSum

def addMonoidAlgebraEquivDirectSum {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Semiring M] [(m : M) → Decidable (m ≠ 0)] : AddMonoidAlgebra M ι ≃ DirectSum ι fun (x : ι) => M

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem addMonoidAlgebraAddEquivDirectSum_symm_apply {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Semiring M] [(m : M) → Decidable (m ≠ 0)] : ⇑(AddEquiv.symm addMonoidAlgebraAddEquivDirectSum) = DirectSum.toAddMonoidAlgebra

@[simp]

theorem addMonoidAlgebraAddEquivDirectSum_apply {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Semiring M] [(m : M) → Decidable (m ≠ 0)] : ⇑addMonoidAlgebraAddEquivDirectSum = AddMonoidAlgebra.toDirectSum

def addMonoidAlgebraAddEquivDirectSum {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Semiring M] [(m : M) → Decidable (m ≠ 0)] : AddMonoidAlgebra M ι ≃+ DirectSum ι fun (x : ι) => M

The additive version of AddMonoidAlgebra.addMonoidAlgebraEquivDirectSum.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem addMonoidAlgebraRingEquivDirectSum_symm_apply {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddMonoid ι] [Semiring M] [(m : M) → Decidable (m ≠ 0)] : ⇑(RingEquiv.symm addMonoidAlgebraRingEquivDirectSum) = DirectSum.toAddMonoidAlgebra

@[simp]

theorem addMonoidAlgebraRingEquivDirectSum_apply {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddMonoid ι] [Semiring M] [(m : M) → Decidable (m ≠ 0)] : ⇑addMonoidAlgebraRingEquivDirectSum = AddMonoidAlgebra.toDirectSum

def addMonoidAlgebraRingEquivDirectSum {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddMonoid ι] [Semiring M] [(m : M) → Decidable (m ≠ 0)] : AddMonoidAlgebra M ι ≃+* DirectSum ι fun (x : ι) => M

The ring version of AddMonoidAlgebra.addMonoidAlgebraEquivDirectSum.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem addMonoidAlgebraAlgEquivDirectSum_symm_apply {ι : Type u_1} {R : Type u_2} {A : Type u_4} [DecidableEq ι] [AddMonoid ι] [CommSemiring R] [Semiring A] [Algebra R A] [(m : A) → Decidable (m ≠ 0)] : ⇑(AlgEquiv.symm addMonoidAlgebraAlgEquivDirectSum) = DirectSum.toAddMonoidAlgebra

@[simp]

theorem addMonoidAlgebraAlgEquivDirectSum_apply {ι : Type u_1} {R : Type u_2} {A : Type u_4} [DecidableEq ι] [AddMonoid ι] [CommSemiring R] [Semiring A] [Algebra R A] [(m : A) → Decidable (m ≠ 0)] : ⇑addMonoidAlgebraAlgEquivDirectSum = AddMonoidAlgebra.toDirectSum

def addMonoidAlgebraAlgEquivDirectSum {ι : Type u_1} {R : Type u_2} {A : Type u_4} [DecidableEq ι] [AddMonoid ι] [CommSemiring R] [Semiring A] [Algebra R A] [(m : A) → Decidable (m ≠ 0)] : AddMonoidAlgebra A ι ≃ₐ[R] DirectSum ι fun (x : ι) => A

The algebra version of AddMonoidAlgebra.addMonoidAlgebraEquivDirectSum.

Equations

• One or more equations did not get rendered due to their size.