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 DirectSum.instMul 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 AddMonoidAlgebra.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.

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.

@[simp]

theorem AddMonoidAlgebra.toDirectSum_single {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Semiring M] (i : ι) (m : M) : (single i m).toDirectSum = (DirectSum.of (fun (x : ι) => 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.

@[simp]

theorem DirectSum.toAddMonoidAlgebra_of {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Semiring M] [(m : M) → Decidable (m ≠ 0)] (i : ι) (m : M) : ((of (fun (x : ι) => M) i) m).toAddMonoidAlgebra = AddMonoidAlgebra.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] : 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_natCast {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddMonoid ι] [Semiring M] (n : ℕ) : (↑n).toDirectSum = ↑n

@[simp]

theorem AddMonoidAlgebra.toDirectSum_ofNat {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddMonoid ι] [Semiring M] (n : ℕ) [n.AtLeastTwo] : (OfNat.ofNat n).toDirectSum = OfNat.ofNat n

@[simp]

theorem AddMonoidAlgebra.toDirectSum_sub {ι : Type u_1} {M : Type u_3} [Ring M] (f g : AddMonoidAlgebra M ι) : (f - g).toDirectSum = f.toDirectSum - g.toDirectSum

@[simp]

theorem AddMonoidAlgebra.toDirectSum_neg {ι : Type u_1} {M : Type u_3} [Ring M] (f : AddMonoidAlgebra M ι) : (-f).toDirectSum = -f.toDirectSum

@[simp]

theorem AddMonoidAlgebra.toDirectSum_intCast {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddMonoid ι] [Ring M] (z : ℤ) : (↑z).toDirectSum = ↑z

@[simp]

theorem AddMonoidAlgebra.toDirectSum_one {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero ι] [Semiring M] : toDirectSum 1 = 1

@[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)] : 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_natCast {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddMonoid ι] [Semiring M] [(m : M) → Decidable (m ≠ 0)] (n : ℕ) : (↑n).toAddMonoidAlgebra = ↑n

@[simp]

theorem DirectSum.toAddMonoidAlgebra_ofNat {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddMonoid ι] [Semiring M] [(m : M) → Decidable (m ≠ 0)] (n : ℕ) [n.AtLeastTwo] : (OfNat.ofNat n).toAddMonoidAlgebra = OfNat.ofNat n

@[simp]

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

@[simp]

theorem DirectSum.toAddMonoidAlgebra_neg {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Ring M] [(m : M) → Decidable (m ≠ 0)] (f : DirectSum ι fun (x : ι) => M) : (-f).toAddMonoidAlgebra = -f.toAddMonoidAlgebra

@[simp]

theorem DirectSum.toAddMonoidAlgebra_intCast {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddMonoid ι] [Ring M] [(m : M) → Decidable (m ≠ 0)] (z : ℤ) : (↑z).toAddMonoidAlgebra = ↑z

@[simp]

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

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

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

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

@[simp]

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

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

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.

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

@[simp]

theorem AddMonoidAlgebra.toDirectSum_pow {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddMonoid ι] [Semiring M] (f : AddMonoidAlgebra M ι) (n : ℕ) : (f ^ n).toDirectSum = f.toDirectSum ^ n

@[simp]

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