mathlib documentation

algebra.graded_monoid

Additively-graded multiplicative structures #

This module provides a set of heterogeneous typeclasses for defining a multiplicative structure over the sigma type graded_monoid A such that (*) : A i → A j → A (i + j); that is to say, A forms an additively-graded monoid. The typeclasses are:

With the sigma_graded locale open, these respectively imbue:

the base type A 0 with:

and the ith grade A i with A 0-actions () defined as left-multiplication:

For now, these typeclasses are primarily used in the construction of direct_sum.ring and the rest of that file.

Internally graded monoids #

In addition to the above typeclasses, in the most frequent case when A is an indexed collection of set_like subobjects (such as add_submonoids, add_subgroups, or submodules), this file provides the Prop typeclasses:

Strictly this last class is unecessary as it has no fields not present in its parents, but it is included for convenience. Note that there is no need for graded_ring or similar, as all the information it would contain is already supplied by graded_monoid when A is a collection of additively-closed set_like objects such as submodules. These constructions are explored in algebra.direct_sum.internal.

tags #

graded monoid

def graded_monoid {ι : Type u_1} (A : ι → Type u_2) :
Type (max u_1 u_2)

A type alias of sigma types for graded monoids.

Equations
@[protected, instance]
def graded_monoid.inhabited {ι : Type u_1} {A : ι → Type u_2} [inhabited ι] [inhabited (A (default ι))] :
Equations
def graded_monoid.mk {ι : Type u_1} {A : ι → Type u_2} (i : ι) :
A igraded_monoid A

Construct an element of a graded monoid.

Equations

Typeclasses #

@[class]
structure graded_monoid.ghas_one {ι : Type u_1} (A : ι → Type u_2) [has_zero ι] :
Type u_2
  • one : A 0

A graded version of has_one, which must be of grade 0.

Instances
@[protected, instance]
def graded_monoid.ghas_one.to_has_one {ι : Type u_1} (A : ι → Type u_2) [has_zero ι] [graded_monoid.ghas_one A] :

ghas_one implies has_one (graded_monoid A)

Equations
@[class]
structure graded_monoid.ghas_mul {ι : Type u_1} (A : ι → Type u_2) [has_add ι] :
Type (max u_1 u_2)
  • mul : Π {i j : ι}, A iA jA (i + j)

A graded version of has_mul. Multiplication combines grades additively, like add_monoid_algebra.

Instances
@[protected, instance]
def graded_monoid.ghas_mul.to_has_mul {ι : Type u_1} (A : ι → Type u_2) [has_add ι] [graded_monoid.ghas_mul A] :

ghas_mul implies has_mul (graded_monoid A).

Equations
theorem graded_monoid.mk_mul_mk {ι : Type u_1} (A : ι → Type u_2) [has_add ι] [graded_monoid.ghas_mul A] {i j : ι} (a : A i) (b : A j) :
def graded_monoid.gmonoid.gnpow_rec {ι : Type u_1} {A : ι → Type u_2} [add_monoid ι] [graded_monoid.ghas_mul A] [graded_monoid.ghas_one A] (n : ) {i : ι} :
A iA (n i)

A default implementation of power on a graded monoid, like npow_rec. gmonoid.gnpow should be used instead.

Equations

Tactic used to autofill graded_monoid.gmonoid.gnpow_zero' when the default graded_monoid.gmonoid.gnpow_rec is used.

Tactic used to autofill graded_monoid.gmonoid.gnpow_succ' when the default graded_monoid.gmonoid.gnpow_rec is used.

@[instance]
def graded_monoid.gmonoid.to_ghas_mul {ι : Type u_1} (A : ι → Type u_2) [add_monoid ι] [self : graded_monoid.gmonoid A] :
@[instance]
def graded_monoid.gmonoid.to_ghas_one {ι : Type u_1} (A : ι → Type u_2) [add_monoid ι] [self : graded_monoid.gmonoid A] :
@[class]
structure graded_monoid.gmonoid {ι : Type u_1} (A : ι → Type u_2) [add_monoid ι] :
Type (max u_1 u_2)

A graded version of monoid.

Like monoid.npow, this has an optional gmonoid.gnpow field to allow definitional control of natural powers of a graded monoid.

Instances
@[protected, instance]
def graded_monoid.gmonoid.to_monoid {ι : Type u_1} (A : ι → Type u_2) [add_monoid ι] [graded_monoid.gmonoid A] :

gmonoid implies a monoid (graded_monoid A).

Equations
theorem graded_monoid.mk_pow {ι : Type u_1} (A : ι → Type u_2) [add_monoid ι] [graded_monoid.gmonoid A] {i : ι} (a : A i) (n : ) :
@[instance]
def graded_monoid.gcomm_monoid.to_gmonoid {ι : Type u_1} (A : ι → Type u_2) [add_comm_monoid ι] [self : graded_monoid.gcomm_monoid A] :
@[class]
structure graded_monoid.gcomm_monoid {ι : Type u_1} (A : ι → Type u_2) [add_comm_monoid ι] :
Type (max u_1 u_2)

A graded version of comm_monoid.

Instances
@[protected, instance]

gcomm_monoid implies a comm_monoid (graded_monoid A), although this is only used as an instance locally to define notation in gmonoid and similar typeclasses.

Equations

Instances for A 0 #

The various g* instances are enough to promote the add_comm_monoid (A 0) structure to various types of multiplicative structure.

@[protected, nolint, instance]
def graded_monoid.grade_zero.has_one {ι : Type u_1} (A : ι → Type u_2) [has_zero ι] [graded_monoid.ghas_one A] :
has_one (A 0)

1 : A 0 is the value provided in ghas_one.one.

Equations
@[protected, instance]
def graded_monoid.grade_zero.has_scalar {ι : Type u_1} (A : ι → Type u_2) [add_monoid ι] [graded_monoid.ghas_mul A] (i : ι) :
has_scalar (A 0) (A i)

(•) : A 0 → A i → A i is the value provided in graded_monoid.ghas_mul.mul, composed with an eq.rec to turn A (0 + i) into A i.

Equations
@[protected, instance]
def graded_monoid.grade_zero.has_mul {ι : Type u_1} (A : ι → Type u_2) [add_monoid ι] [graded_monoid.ghas_mul A] :
has_mul (A 0)

(*) : A 0 → A 0 → A 0 is the value provided in graded_monoid.ghas_mul.mul, composed with an eq.rec to turn A (0 + 0) into A 0.

Equations
@[simp]
theorem graded_monoid.mk_zero_smul {ι : Type u_1} {A : ι → Type u_2} [add_monoid ι] [graded_monoid.ghas_mul A] {i : ι} (a : A 0) (b : A i) :
@[simp]
theorem graded_monoid.grade_zero.smul_eq_mul {ι : Type u_1} {A : ι → Type u_2} [add_monoid ι] [graded_monoid.ghas_mul A] (a b : A 0) :
a b = a * b
@[protected, instance]
def graded_monoid.grade_zero.monoid {ι : Type u_1} (A : ι → Type u_2) [add_monoid ι] [graded_monoid.gmonoid A] :
monoid (A 0)

The monoid structure derived from gmonoid A.

Equations
@[protected, instance]
def graded_monoid.grade_zero.comm_monoid {ι : Type u_1} (A : ι → Type u_2) [add_comm_monoid ι] [graded_monoid.gcomm_monoid A] :

The comm_monoid structure derived from gcomm_monoid A.

Equations
@[protected, instance]
def graded_monoid.grade_zero.mul_action {ι : Type u_1} (A : ι → Type u_2) [add_monoid ι] [graded_monoid.gmonoid A] {i : ι} :
mul_action (A 0) (A i)

Each grade A i derives a A 0-action structure from gmonoid A.

Equations

Concrete instances #

@[simp]
theorem has_one.ghas_one_one (ι : Type u_1) {R : Type u_2} [has_zero ι] [has_one R] :
@[protected, instance]
def has_one.ghas_one (ι : Type u_1) {R : Type u_2} [has_zero ι] [has_one R] :
graded_monoid.ghas_one (λ (i : ι), R)
Equations
@[simp]
theorem has_mul.ghas_mul_mul (ι : Type u_1) {R : Type u_2} [has_add ι] [has_mul R] (i j : ι) (ᾰ ᾰ_1 : R) :
graded_monoid.ghas_mul.mul ᾰ_1 = * ᾰ_1
@[protected, instance]
def has_mul.ghas_mul (ι : Type u_1) {R : Type u_2} [has_add ι] [has_mul R] :
graded_monoid.ghas_mul (λ (i : ι), R)
Equations
@[simp]
theorem monoid.gmonoid_gnpow (ι : Type u_1) {R : Type u_2} [add_monoid ι] [monoid R] (n : ) (i : ι) (a : R) :
@[protected, instance]
def monoid.gmonoid (ι : Type u_1) {R : Type u_2} [add_monoid ι] [monoid R] :
graded_monoid.gmonoid (λ (i : ι), R)

If all grades are the same type and themselves form a monoid, then there is a trivial grading structure.

Equations
@[protected, instance]
def comm_monoid.gcomm_monoid (ι : Type u_1) {R : Type u_2} [add_comm_monoid ι] [comm_monoid R] :

If all grades are the same type and themselves form a commutative monoid, then there is a trivial grading structure.

Equations

Shorthands for creating instance of the above typeclasses for collections of subobjects #

@[class]
structure set_like.has_graded_one {ι : Type u_1} {R : Type u_2} {S : Type u_3} [set_like S R] [has_one R] [has_zero ι] (A : ι → S) :
Prop
  • one_mem : 1 A 0

A version of graded_monoid.ghas_one for internally graded objects.

Instances
@[protected, instance]
def set_like.ghas_one {ι : Type u_1} {R : Type u_2} {S : Type u_3} [set_like S R] [has_one R] [has_zero ι] (A : ι → S) [set_like.has_graded_one A] :
graded_monoid.ghas_one (λ (i : ι), (A i))
Equations
@[simp]
theorem set_like.coe_ghas_one {ι : Type u_1} {R : Type u_2} {S : Type u_3} [set_like S R] [has_one R] [has_zero ι] (A : ι → S) [set_like.has_graded_one A] :
@[class]
structure set_like.has_graded_mul {ι : Type u_1} {R : Type u_2} {S : Type u_3} [set_like S R] [has_mul R] [has_add ι] (A : ι → S) :
Prop
  • mul_mem : ∀ ⦃i j : ι⦄ {gi gj : R}, gi A igj A jgi * gj A (i + j)

A version of graded_monoid.ghas_one for internally graded objects.

Instances
@[protected, instance]
def set_like.ghas_mul {ι : Type u_1} {R : Type u_2} {S : Type u_3} [set_like S R] [has_mul R] [has_add ι] (A : ι → S) [set_like.has_graded_mul A] :
graded_monoid.ghas_mul (λ (i : ι), (A i))
Equations
@[simp]
theorem set_like.coe_ghas_mul {ι : Type u_1} {R : Type u_2} {S : Type u_3} [set_like S R] [has_mul R] [has_add ι] (A : ι → S) [set_like.has_graded_mul A] {i j : ι} (x : (A i)) (y : (A j)) :
@[instance]
def set_like.graded_monoid.to_has_graded_mul {ι : Type u_1} {R : Type u_2} {S : Type u_3} [set_like S R] [monoid R] [add_monoid ι] (A : ι → S) [self : set_like.graded_monoid A] :
@[instance]
def set_like.graded_monoid.to_has_graded_one {ι : Type u_1} {R : Type u_2} {S : Type u_3} [set_like S R] [monoid R] [add_monoid ι] (A : ι → S) [self : set_like.graded_monoid A] :
@[class]
structure set_like.graded_monoid {ι : Type u_1} {R : Type u_2} {S : Type u_3} [set_like S R] [monoid R] [add_monoid ι] (A : ι → S) :
Prop
  • one_mem : 1 A 0
  • mul_mem : ∀ ⦃i j : ι⦄ {gi gj : R}, gi A igj A jgi * gj A (i + j)

A version of graded_monoid.gmonoid for internally graded objects.

Instances
@[protected, instance]
def set_like.gmonoid {ι : Type u_1} {R : Type u_2} {S : Type u_3} [set_like S R] [monoid R] [add_monoid ι] (A : ι → S) [set_like.graded_monoid A] :
graded_monoid.gmonoid (λ (i : ι), (A i))

Build a gmonoid instance for a collection of subobjects.

Equations
@[simp]
theorem set_like.coe_gpow {ι : Type u_1} {R : Type u_2} {S : Type u_3} [set_like S R] [monoid R] [add_monoid ι] (A : ι → S) [set_like.graded_monoid A] {i : ι} (x : (A i)) (n : ) :
@[protected, instance]
def set_like.gcomm_monoid {ι : Type u_1} {R : Type u_2} {S : Type u_3} [set_like S R] [comm_monoid R] [add_comm_monoid ι] (A : ι → S) [set_like.graded_monoid A] :
graded_monoid.gcomm_monoid (λ (i : ι), (A i))

Build a gcomm_monoid instance for a collection of subobjects.

Equations