Documentation

Mathlib.Algebra.MonoidAlgebra.ToDirectSum

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 #

Theorems #

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

as well as preserving arithmetic operations.

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

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
@[simp]
theorem AddMonoidAlgebra.toDirectSum_single {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Semiring M] (i : ι) (m : M) :
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) :

Interpret a homogeneous DirectSum as an AddMonoidAlgebra.

Equations
@[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 = Finsupp.single i m
@[simp]
@[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) :

Lemmas about arithmetic operations #

@[simp]
theorem AddMonoidAlgebra.toDirectSum_zero {ι : Type u_1} {M : Type u_3} [Semiring M] :
@[simp]
theorem AddMonoidAlgebra.toDirectSum_add {ι : Type u_1} {M : Type u_3} [Semiring M] (f g : AddMonoidAlgebra M ι) :
@[simp]
theorem AddMonoidAlgebra.toDirectSum_natCast {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddMonoid ι] [Semiring M] (n : ) :
(↑n).toDirectSum = n
@[simp]
theorem AddMonoidAlgebra.toDirectSum_sub {ι : Type u_1} {M : Type u_3} [Ring M] (f g : AddMonoidAlgebra M ι) :
@[simp]
theorem AddMonoidAlgebra.toDirectSum_neg {ι : Type u_1} {M : Type u_3} [Ring M] (f : AddMonoidAlgebra M ι) :
@[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] :
@[simp]
@[simp]
theorem DirectSum.toAddMonoidAlgebra_zero {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Semiring M] [(m : M) → Decidable (m 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) :
@[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] :
@[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) :
@[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) :
@[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)] :
@[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) :

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
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
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
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 AddMonoidAlgebra.toDirectSum_pow {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddMonoid ι] [Semiring M] (f : AddMonoidAlgebra M ι) (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 : ) :