GradedMonoid.GMulAction.one_smul
theorem GradedMonoid.GMulAction.one_smul :
∀ {ιA : Type u_1} {ιM : Type u_3} {A : ιA → Type u_4} {M : ιM → Type u_5} [inst : AddMonoid ιA]
[inst_1 : VAdd ιA ιM] [inst_2 : GradedMonoid.GMonoid A] [self : GradedMonoid.GMulAction A M] (b : GradedMonoid M),
1 • b = b
This theorem states that for any graded monoid `M` denoted by `b`, under certain assumptions, the operation `1 • b` (where `1` represents the neutral element and `•` represents the multiplication operation) results in `b` itself. The assumptions include the existence of an addition operation on the type `ιA`, a vector addition operation from `ιA` to `ιM`, a graded monoid structure on `A`, and a graded monoid multiplication operation on `A` and `M`. This theorem captures the mathematical property that multiplying any element by the neutral element in a graded monoid gives the element itself.
More concisely: For any graded monoid `M`, if `A` is a graded monoid with a graded monoid multiplication and there are given additions and vector additions, then for all elements `b` in `M`, `1 • b = b`.
|
SetLike.GradedSMul.smul_mem
theorem SetLike.GradedSMul.smul_mem :
∀ {ιA : Type u_1} {ιB : Type u_2} {S : Type u_5} {R : Type u_6} {N : Type u_7} {M : Type u_8} [inst : SetLike S R]
[inst_1 : SetLike N M] [inst_2 : SMul R M] [inst_3 : VAdd ιA ιB] {A : ιA → S} {B : ιB → N}
[self : SetLike.GradedSMul A B] ⦃i : ιA⦄ ⦃j : ιB⦄ {ai : R} {bj : M}, ai ∈ A i → bj ∈ B j → ai • bj ∈ B (i +ᵥ j)
This theorem states that multiplication is homogeneous in the context of certain mathematical structures. Specifically, if we have two types `ιA` and `ιB`, as well as sets `S` and `R`, along with `N` and `M` that are like these sets. We also have the operations `SMul` of `R` and `M`, and `VAdd` of `ιA` and `ιB`. Given functions `A : ιA → S` and `B : ιB → N`, and assuming `A` and `B` satisfy certain properties of graded multiplication (expressed by the `SetLike.GradedSMul A B` instance), then for any `i : ιA`, `j : ιB`, `ai : R`, and `bj : M`, if `ai` is an element of `A i` and `bj` is an element of `B j`, `ai` multiplied by `bj` (notated as `ai • bj`) is an element of `B` at the point `i +ᵥ j`. This is a realization of the concept of "graded" or "homogeneous" structures in algebra, where multiplication carries over properties related to some kind of "grade" or "degree".
More concisely: Given sets `S`, `N`, types `ιA` and `ιB`, functions `A : ιA → S` and `B : ιB → N` satisfying `SetLike.GradedSMul A B`, for all `i : ιA`, `j : ιB`, `ai : R ∈ A i`, `bj : M ∈ B j`, we have `ai • bj ∈ B (i + j)`.
|
GradedMonoid.GMulAction.mul_smul
theorem GradedMonoid.GMulAction.mul_smul :
∀ {ιA : Type u_1} {ιM : Type u_3} {A : ιA → Type u_4} {M : ιM → Type u_5} [inst : AddMonoid ιA]
[inst_1 : VAdd ιA ιM] [inst_2 : GradedMonoid.GMonoid A] [self : GradedMonoid.GMulAction A M]
(a a' : GradedMonoid A) (b : GradedMonoid M), (a * a') • b = a • a' • b
This theorem is about the associativity of two operations, `•` and `*`, on graded monoids, which are a kind of monoid where the elements are indexed by an additional parameter.
Specifically, the theorem states that for any graded monoids `A` and `M`, indexed by types `ιA` and `ιM` respectively, where `A` forms a graded monoid and `A` acts on `M` (i.e., `A` is a `GMulAction` on `M`), for any three elements `a`, `a'`, and `b` of `A` and `M` respectively, the operation `a * a' • b` is the same as `a • a' • b`.
The operation `*` is the multiplication in the graded monoid `A`, and `•` is the action of `A` on `M`. The associativity this theorem asserts is a key property in the theory of actions of graded monoids.
The `AddMonoid ιA` and `VAdd ιA ιM` structures are additional assumptions about the indexing types, which are used to define the grading of the monoids. They mean respectively that `ιA` forms an additive monoid, and that `ιA` and `ιM` together form a "vector addition" structure, which is a kind of generalised addition operation.
More concisely: For any graded monoids `A` and `M` indexed by additive monoids, where `A` acts on `M`, the graded monoid multiplication `a * a'` and action `•` of `a` on `M` commute, i.e., `a • a' • b = a * a' • b` for all `a, a' in A` and `b in M`.
|