mathlib3 documentation

algebra.graded_monoid

Additively-graded multiplicative structures #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

Dependent graded products #

This also introduces list.dprod, which takes the (possibly non-commutative) product of a list of graded elements of type A i. This definition primarily exist to allow graded_monoid.mk and direct_sum.of to be pulled outside a product, such as in graded_monoid.mk_list_dprod and direct_sum.of_list_dprod.

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:

which respectively provide the API lemmas

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 set_like.graded_ring or similar, as all the information it would contain is already supplied by graded_monoid when A is a collection of objects satisfying add_submonoid_class such as submodules. These constructions are explored in algebra.direct_sum.internal.

This file also defines:

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
Instances for graded_monoid
@[protected, instance]
Equations
def graded_monoid.mk {ι : Type u_1} {A : ι Type u_2} (i : ι) :

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 of this typeclass
Instances of other typeclasses for graded_monoid.ghas_one
  • graded_monoid.ghas_one.has_sizeof_inst
@[protected, instance]

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 i A j A (i + j)

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

Instances of this typeclass
Instances of other typeclasses for graded_monoid.ghas_mul
  • graded_monoid.ghas_mul.has_sizeof_inst
@[protected, instance]

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 i A (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]
@[instance]
@[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 of this typeclass
Instances of other typeclasses for graded_monoid.gmonoid
  • graded_monoid.gmonoid.has_sizeof_inst
@[protected, instance]

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 : ) :
@[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 of this typeclass
Instances of other typeclasses for graded_monoid.gcomm_monoid
  • graded_monoid.gcomm_monoid.has_sizeof_inst
@[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_smul {ι : Type u_1} (A : ι Type u_2) [add_zero_class ι] [graded_monoid.ghas_mul A] (i : ι) :
has_smul (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]

(*) : 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_zero_class ι] [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_zero_class ι] [graded_monoid.ghas_mul A] (a b : A 0) :
a b = a * b
@[protected, instance]
def graded_monoid.nat.has_pow {ι : Type u_1} (A : ι Type u_2) [add_monoid ι] [graded_monoid.gmonoid A] :
has_pow (A 0)
Equations
@[simp]
theorem graded_monoid.mk_zero_pow {ι : Type u_1} {A : ι Type u_2} [add_monoid ι] [graded_monoid.gmonoid A] (a : A 0) (n : ) :
@[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]

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

Dependent products of graded elements #

def list.dprod_index {ι : Type u_1} {α : Type u_2} [add_monoid ι] (l : list α) (fι : α ι) :
ι

The index used by list.dprod. Propositionally this is equal to (l.map fι).sum, but definitionally it needs to have a different form to avoid introducing eq.recs in list.dprod.

Equations
@[simp]
theorem list.dprod_index_nil {ι : Type u_1} {α : Type u_2} [add_monoid ι] (fι : α ι) :
@[simp]
theorem list.dprod_index_cons {ι : Type u_1} {α : Type u_2} [add_monoid ι] (a : α) (l : list α) (fι : α ι) :
(a :: l).dprod_index = fι a + l.dprod_index
theorem list.dprod_index_eq_map_sum {ι : Type u_1} {α : Type u_2} [add_monoid ι] (l : list α) (fι : α ι) :
l.dprod_index = (list.map l).sum
def list.dprod {ι : Type u_1} {α : Type u_2} {A : ι Type u_3} [add_monoid ι] [graded_monoid.gmonoid A] (l : list α) (fι : α ι) (fA : Π (a : α), A (fι a)) :
A (l.dprod_index fι)

A dependent product for graded monoids represented by the indexed family of types A i. This is a dependent version of (l.map fA).prod.

For a list l : list α, this computes the product of fA a over a, where each fA is of type A (fι a).

Equations
@[simp]
theorem list.dprod_nil {ι : Type u_1} {α : Type u_2} {A : ι Type u_3} [add_monoid ι] [graded_monoid.gmonoid A] (fι : α ι) (fA : Π (a : α), A (fι a)) :
@[simp]
theorem list.dprod_cons {ι : Type u_1} {α : Type u_2} {A : ι Type u_3} [add_monoid ι] [graded_monoid.gmonoid A] (fι : α ι) (fA : Π (a : α), A (fι a)) (a : α) (l : list α) :
(a :: l).dprod fA = graded_monoid.ghas_mul.mul (fA a) (l.dprod fA)
theorem graded_monoid.mk_list_dprod {ι : Type u_1} {α : Type u_2} {A : ι Type u_3} [add_monoid ι] [graded_monoid.gmonoid A] (l : list α) (fι : α ι) (fA : Π (a : α), A (fι a)) :
graded_monoid.mk (l.dprod_index fι) (l.dprod fA) = (list.map (λ (a : α), graded_monoid.mk (fι a) (fA a)) l).prod
theorem graded_monoid.list_prod_map_eq_dprod {ι : Type u_1} {α : Type u_2} {A : ι Type u_3} [add_monoid ι] [graded_monoid.gmonoid A] (l : list α) (f : α graded_monoid A) :
(list.map f l).prod = graded_monoid.mk (l.dprod_index (λ (i : α), (f i).fst)) (l.dprod (λ (i : α), (f i).fst) (λ (i : α), (f i).snd))

A variant of graded_monoid.mk_list_dprod for rewriting in the other direction.

theorem graded_monoid.list_prod_of_fn_eq_dprod {ι : Type u_1} {A : ι Type u_3} [add_monoid ι] [graded_monoid.gmonoid A] {n : } (f : fin n graded_monoid A) :
(list.of_fn f).prod = graded_monoid.mk ((list.fin_range n).dprod_index (λ (i : fin n), (f i).fst)) ((list.fin_range n).dprod (λ (i : fin n), (f i).fst) (λ (i : fin n), (f i).snd))

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
@[simp]
theorem list.dprod_monoid (ι : Type u_1) {R : Type u_2} {α : Type u_3} [add_monoid ι] [monoid R] (l : list α) (fι : α ι) (fA : α R) :
l.dprod fA = (list.map fA l).prod

When all the indexed types are the same, the dependent product is just the regular product.

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 of this typeclass
theorem set_like.one_mem_graded {ι : 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] :
1 A 0
@[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

A version of graded_monoid.ghas_one for internally graded objects.

Instances of this typeclass
theorem set_like.mul_mem_graded {ι : 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 : ι⦄ {gi gj : R} (hi : gi A i) (hj : gj A j) :
gi * gj A (i + j)
@[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 i gj A j gi * gj A (i + j)

A version of graded_monoid.gmonoid for internally graded objects.

Instances of this typeclass
theorem set_like.pow_mem_graded {ι : 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] (n : ) {r : R} {i : ι} (h : r A i) :
r ^ n A (n i)
theorem set_like.list_prod_map_mem_graded {ι : 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] {ι' : Type u_4} (l : list ι') (i : ι' ι) (r : ι' R) (h : (j : ι'), j l r j A (i j)) :
(list.map r l).prod A (list.map i l).sum
theorem set_like.list_prod_of_fn_mem_graded {ι : 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] {n : } (i : fin n ι) (r : fin n R) (h : (j : fin n), r j A (i j)) :
@[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_gnpow {ι : 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
@[simp]
theorem set_like.coe_list_dprod {ι : Type u_1} {R : Type u_2} {α : Type u_3} {S : Type u_4} [set_like S R] [monoid R] [add_monoid ι] (A : ι S) [set_like.graded_monoid A] (fι : α ι) (fA : Π (a : α), (A (fι a))) (l : list α) :
(l.dprod fA) = (list.map (λ (a : α), (fA a)) l).prod

Coercing a dependent product of subtypes is the same as taking the regular product of the coercions.

theorem set_like.list_dprod_eq {ι : Type u_1} {R : Type u_2} {α : Type u_3} {S : Type u_4} [set_like S R] [monoid R] [add_monoid ι] (A : ι S) [set_like.graded_monoid A] (fι : α ι) (fA : Π (a : α), (A (fι a))) (l : list α) :
l.dprod fA = (list.map (λ (a : α), (fA a)) l).prod, _⟩

A version of list.coe_dprod_set_like with subtype.mk.

def set_like.is_homogeneous {ι : Type u_1} {R : Type u_2} {S : Type u_3} [set_like S R] (A : ι S) (a : R) :
Prop

An element a : R is said to be homogeneous if there is some i : ι such that a ∈ A i.

Equations
@[simp]
theorem set_like.is_homogeneous_coe {ι : Type u_1} {R : Type u_2} {S : Type u_3} [set_like S R] {A : ι S} {i : ι} (x : (A i)) :
theorem set_like.is_homogeneous_one {ι : Type u_1} {R : Type u_2} {S : Type u_3} [set_like S R] [has_zero ι] [has_one R] (A : ι S) [set_like.has_graded_one A] :
theorem set_like.is_homogeneous.mul {ι : Type u_1} {R : Type u_2} {S : Type u_3} [set_like S R] [has_add ι] [has_mul R] {A : ι S} [set_like.has_graded_mul A] {a b : R} :
def set_like.homogeneous_submonoid {ι : Type u_1} {R : Type u_2} {S : Type u_3} [set_like S R] [add_monoid ι] [monoid R] (A : ι S) [set_like.graded_monoid A] :

When A is a set_like.graded_monoid A, then the homogeneous elements forms a submonoid.

Equations