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:
graded_monoid.ghas_one A
graded_monoid.ghas_mul A
graded_monoid.gmonoid A
graded_monoid.gcomm_monoid A
With the sigma_graded
locale open, these respectively imbue:
has_one (graded_monoid A)
has_mul (graded_monoid A)
monoid (graded_monoid A)
comm_monoid (graded_monoid A)
the base type A 0
with:
graded_monoid.grade_zero.has_one
graded_monoid.grade_zero.has_mul
graded_monoid.grade_zero.monoid
graded_monoid.grade_zero.comm_monoid
and the i
th grade A i
with A 0
-actions (•
) defined as left-multiplication:
- (nothing)
graded_monoid.grade_zero.has_scalar (A 0)
graded_monoid.grade_zero.mul_action (A 0)
- (nothing)
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_submonoid
s, add_subgroup
s, or submodule
s), this file
provides the Prop
typeclasses:
set_like.has_graded_one A
(which provides the obviousgraded_monoid.ghas_one A
instance)set_like.has_graded_mul A
(which provides the obviousgraded_monoid.ghas_mul A
instance)set_like.graded_monoid A
(which provides the obviousgraded_monoid.gmonoid A
andgraded_monoid.gcomm_monoid A
instances)set_like.is_homogeneous A
(which says thata
is homogeneous iffa ∈ A i
for somei : ι
)
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
.
This file also contains the definition of set_like.homogeneous_submonoid A
, which is, as the name
suggests, the submonoid consisting of all the homogeneous elements.
tags #
graded monoid
A type alias of sigma types for graded monoids.
Equations
- graded_monoid A = sigma A
Equations
Construct an element of a graded monoid.
Equations
Typeclasses #
ghas_one
implies has_one (graded_monoid A)
Equations
- graded_monoid.ghas_one.to_has_one A = {one := ⟨0, graded_monoid.ghas_one.one _inst_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
.
ghas_mul
implies has_mul (graded_monoid A)
.
Equations
- graded_monoid.ghas_mul.to_has_mul A = {mul := λ (x y : graded_monoid A), ⟨x.fst + y.fst, graded_monoid.ghas_mul.mul x.snd y.snd⟩}
A default implementation of power on a graded monoid, like npow_rec
.
gmonoid.gnpow
should be used instead.
Equations
- mul : Π {i j : ι}, A i → A j → A (i + j)
- one : A 0
- one_mul : ∀ (a : graded_monoid A), 1 * a = a
- mul_one : ∀ (a : graded_monoid A), a * 1 = a
- mul_assoc : ∀ (a b c : graded_monoid A), (a * b) * c = a * b * c
- gnpow : Π (n : ℕ) {i : ι}, A i → A (n • i)
- gnpow_zero' : (∀ (a : graded_monoid A), graded_monoid.mk (0 • a.fst) (graded_monoid.gmonoid.gnpow 0 a.snd) = 1) . "apply_gnpow_rec_zero_tac"
- gnpow_succ' : (∀ (n : ℕ) (a : graded_monoid A), graded_monoid.mk (n.succ • a.fst) (graded_monoid.gmonoid.gnpow n.succ a.snd) = a * ⟨n • a.fst, graded_monoid.gmonoid.gnpow n a.snd⟩) . "apply_gnpow_rec_succ_tac"
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.
gmonoid
implies a monoid (graded_monoid A)
.
Equations
- graded_monoid.gmonoid.to_monoid A = {mul := has_mul.mul (graded_monoid.ghas_mul.to_has_mul A), mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := λ (n : ℕ) (a : graded_monoid A), graded_monoid.mk (n • a.fst) (graded_monoid.gmonoid.gnpow n a.snd), npow_zero' := _, npow_succ' := _}
- mul : Π {i j : ι}, A i → A j → A (i + j)
- one : A 0
- one_mul : ∀ (a : graded_monoid A), 1 * a = a
- mul_one : ∀ (a : graded_monoid A), a * 1 = a
- mul_assoc : ∀ (a b c : graded_monoid A), (a * b) * c = a * b * c
- gnpow : Π (n : ℕ) {i : ι}, A i → A (n • i)
- gnpow_zero' : (∀ (a : graded_monoid A), graded_monoid.mk (0 • a.fst) (graded_monoid.gcomm_monoid.gnpow 0 a.snd) = 1) . "apply_gnpow_rec_zero_tac"
- gnpow_succ' : (∀ (n : ℕ) (a : graded_monoid A), graded_monoid.mk (n.succ • a.fst) (graded_monoid.gcomm_monoid.gnpow n.succ a.snd) = a * ⟨n • a.fst, graded_monoid.gcomm_monoid.gnpow n a.snd⟩) . "apply_gnpow_rec_succ_tac"
- mul_comm : ∀ (a b : graded_monoid A), a * b = b * a
A graded version of comm_monoid
.
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
- graded_monoid.gcomm_monoid.to_comm_monoid A = {mul := monoid.mul (graded_monoid.gmonoid.to_monoid A), mul_assoc := _, one := monoid.one (graded_monoid.gmonoid.to_monoid A), one_mul := _, mul_one := _, npow := monoid.npow (graded_monoid.gmonoid.to_monoid A), npow_zero' := _, npow_succ' := _, mul_comm := _}
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.
1 : A 0
is the value provided in ghas_one.one
.
Equations
- graded_monoid.grade_zero.has_one A = {one := graded_monoid.ghas_one.one _inst_2}
(•) : 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
- graded_monoid.grade_zero.has_scalar A i = {smul := λ (x : A 0) (y : A i), eq.rec (graded_monoid.ghas_mul.mul x y) _}
(*) : 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
The monoid
structure derived from gmonoid A
.
Equations
The comm_monoid
structure derived from gcomm_monoid A
.
Equations
graded_monoid.mk 0
is a monoid_hom
, using the graded_monoid.grade_zero.monoid
structure.
Equations
- graded_monoid.mk_zero_monoid_hom A = {to_fun := graded_monoid.mk 0, map_one' := _, map_mul' := _}
Each grade A i
derives a A 0
-action structure from gmonoid A
.
Equations
- graded_monoid.grade_zero.mul_action A = let _inst : mul_action (A 0) (graded_monoid A) := mul_action.comp_hom (graded_monoid A) (graded_monoid.mk_zero_monoid_hom A) in function.injective.mul_action (graded_monoid.mk i) _ _
Dependent products of graded elements #
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.rec
s in list.dprod
.
Equations
- l.dprod_index fι = list.foldr (λ (i : α) (b : ι), fι i + b) 0 l
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
- l.dprod fι fA = l.foldr_rec_on (λ (i : α) (b : ι), fι i + b) 0 graded_monoid.ghas_one.one (λ (i : ι) (x : A i) (a : α) (ha : a ∈ l), graded_monoid.ghas_mul.mul (fA a) x)
A variant of graded_monoid.mk_list_dprod
for rewriting in the other direction.
Concrete instances #
Equations
- has_one.ghas_one ι = {one := 1}
Equations
- has_mul.ghas_mul ι = {mul := λ (i j : ι), has_mul.mul}
If all grades are the same type and themselves form a monoid, then there is a trivial grading structure.
Equations
- monoid.gmonoid ι = {mul := graded_monoid.ghas_mul.mul (has_mul.ghas_mul ι), one := graded_monoid.ghas_one.one (has_one.ghas_one ι), one_mul := _, mul_one := _, mul_assoc := _, gnpow := λ (n : ℕ) (i : ι) (a : R), a ^ n, gnpow_zero' := _, gnpow_succ' := _}
If all grades are the same type and themselves form a commutative monoid, then there is a trivial grading structure.
Equations
- comm_monoid.gcomm_monoid ι = {mul := graded_monoid.gmonoid.mul (monoid.gmonoid ι), one := graded_monoid.gmonoid.one (monoid.gmonoid ι), one_mul := _, mul_one := _, mul_assoc := _, gnpow := graded_monoid.gmonoid.gnpow (monoid.gmonoid ι), gnpow_zero' := _, gnpow_succ' := _, mul_comm := _}
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 #
- one_mem : 1 ∈ A 0
A version of graded_monoid.ghas_one
for internally graded objects.
Instances
Equations
- set_like.ghas_one A = {one := ⟨1, _⟩}
A version of graded_monoid.ghas_one
for internally graded objects.
Instances
A version of graded_monoid.gmonoid
for internally graded objects.
Build a gmonoid
instance for a collection of subobjects.
Equations
- set_like.gmonoid A = {mul := graded_monoid.ghas_mul.mul (set_like.ghas_mul A), one := graded_monoid.ghas_one.one (set_like.ghas_one A), one_mul := _, mul_one := _, mul_assoc := _, gnpow := λ (n : ℕ) (i : ι) (a : ↥(A i)), ⟨↑a ^ n, _⟩, gnpow_zero' := _, gnpow_succ' := _}
Build a gcomm_monoid
instance for a collection of subobjects.
Equations
- set_like.gcomm_monoid A = {mul := graded_monoid.gmonoid.mul (set_like.gmonoid A), one := graded_monoid.gmonoid.one (set_like.gmonoid A), one_mul := _, mul_one := _, mul_assoc := _, gnpow := graded_monoid.gmonoid.gnpow (set_like.gmonoid A), gnpow_zero' := _, gnpow_succ' := _, mul_comm := _}
Coercing a dependent product of subtypes is the same as taking the regular product of the coercions.
A version of list.coe_dprod_set_like
with subtype.mk
.
An element a : R
is said to be homogeneous if there is some i : ι
such that a ∈ A i
.
Equations
- set_like.is_homogeneous A a = ∃ (i : ι), a ∈ A i
When A
is a set_like.graded_monoid A
, then the homogeneous elements forms a submonoid.
Equations
- set_like.homogeneous_submonoid A = {carrier := {a : R | set_like.is_homogeneous A a}, one_mem' := _, mul_mem' := _}