AddMonoidAlgebra.gradeBy.isInternal
theorem AddMonoidAlgebra.gradeBy.isInternal :
∀ {M : Type u_1} {ι : Type u_2} {R : Type u_3} [inst : AddMonoid M] [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
[inst_3 : CommSemiring R] (f : M →+ ι), DirectSum.IsInternal (AddMonoidAlgebra.gradeBy R ⇑f)
The theorem `AddMonoidAlgebra.gradeBy.isInternal` declares that for any type `M`, index type `ι`, and ring `R`, given that `M` is an additive monoid, `ι` has decidable equality and is also an additive monoid, and `R` is a commutative semiring, if `f` is a function from `M` to `ι` that preserves addition (i.e., is a homomorphism), then `AddMonoidAlgebra.gradeBy R f`, which creates submodules of the `AddMonoidAlgebra R M` corresponding to each 'grade' given by `f`, describes an internally graded algebra. This means that these submodules add up - in the sense of the direct sum - to the entire algebra, without any overlaps.
More concisely: Given an additive monoid M, an index type ι with decidable equality that is also an additive monoid, and a commutative semiring R, if f : M -> ι is an additive homomorphism, then the submodules of AddMonoidAlgebra R f form an internally graded algebra, i.e., they sum up without overlaps to the entire algebra.
|
AddMonoidAlgebra.grade.isInternal
theorem AddMonoidAlgebra.grade.isInternal :
∀ {ι : Type u_2} {R : Type u_3} [inst : DecidableEq ι] [inst_1 : AddMonoid ι] [inst_2 : CommSemiring R],
DirectSum.IsInternal (AddMonoidAlgebra.grade R)
The theorem `AddMonoidAlgebra.grade.isInternal` asserts that for any type `ι`, a type `R`, given that `ι` has decidable equality, `ι` is an additive monoid, and `R` is a commutative semiring, the function `AddMonoidAlgebra.grade R` defines an internally graded algebra. In other words, the algebra defined by the `AddMonoidAlgebra.grade R` function is composed of direct sums of its submodules, each submodule corresponding to a grade.
More concisely: Given a decidely equalizable type `ι` that is an additive monoid and a commutative semiring `R`, the graded algebra `AddMonoidAlgebra.grade R` is internally graded by submodules.
|