Conversion between AddMonoidAlgebra and homogeneous 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 homogeneous DirectSum.

Equations

• f.toDirectSum = 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 homogeneous DirectSum as an AddMonoidAlgebra.

Equations

• f.toAddMonoidAlgebra = 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.of (fun (x : ι) => M) i) m).toAddMonoidAlgebra = 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 ι) : f.toDirectSum.toAddMonoidAlgebra = 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) : f.toAddMonoidAlgebra.toDirectSum = 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 g : AddMonoidAlgebra M ι) : (f + g).toDirectSum = f.toDirectSum + g.toDirectSum

@[simp]

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

@[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 g : DirectSum ι fun (x : ι) => M) : (f + g).toAddMonoidAlgebra = f.toAddMonoidAlgebra + g.toAddMonoidAlgebra

@[simp]

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

Bundled Equivs

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

• addMonoidAlgebraEquivDirectSum = { toFun := AddMonoidAlgebra.toDirectSum, invFun := DirectSum.toAddMonoidAlgebra, left_inv := ⋯, right_inv := ⋯ }

@[simp]

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

@[simp]

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

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

• addMonoidAlgebraAddEquivDirectSum = { toFun := AddMonoidAlgebra.toDirectSum, invFun := DirectSum.toAddMonoidAlgebra, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

@[simp]

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

@[simp]

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

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

• addMonoidAlgebraRingEquivDirectSum = { toFun := AddMonoidAlgebra.toDirectSum, invFun := DirectSum.toAddMonoidAlgebra, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }

@[simp]

theorem addMonoidAlgebraRingEquivDirectSum_symm_apply {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddMonoid ι] [Semiring M] [(m : M) → Decidable (m ≠ 0)] : ⇑addMonoidAlgebraRingEquivDirectSum.symm = 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 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.

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

@[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)] : ⇑addMonoidAlgebraAlgEquivDirectSum.symm = DirectSum.toAddMonoidAlgebra