Additively-graded multiplicative structures #
This module provides a set of heterogeneous typeclasses for defining a multiplicative structure
over the sigma type GradedMonoid A
such that (*) : A i → A j → A (i + j)
; that is to say, A
forms an additively-graded monoid. The typeclasses are:
These respectively imbue:
One (GradedMonoid A)
Mul (GradedMonoid A)
Monoid (GradedMonoid A)
CommMonoid (GradedMonoid A)
the base type A 0
with:
GradedMonoid.GradeZero.One
GradedMonoid.GradeZero.Mul
GradedMonoid.GradeZero.Monoid
GradedMonoid.GradeZero.CommMonoid
and the i
th grade A i
with A 0
-actions (•
) defined as left-multiplication:
For now, these typeclasses are primarily used in the construction of DirectSum.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 GradedMonoid.mk
and DirectSum.of
to be pulled outside a product, such as in GradedMonoid.mk_list_dProd
and
DirectSum.of_list_dProd
.
Internally graded monoids #
In addition to the above typeclasses, in the most frequent case when A
is an indexed collection of
SetLike
subobjects (such as AddSubmonoid
s, AddSubgroup
s, or Submodule
s), this file
provides the Prop
typeclasses:
SetLike.GradedOne A
(which provides the obviousGradedMonoid.GOne A
instance)SetLike.GradedMul A
(which provides the obviousGradedMonoid.GMul A
instance)SetLike.GradedMonoid A
(which provides the obviousGradedMonoid.GMonoid A
andGradedMonoid.GCommMonoid A
instances)
which respectively provide the API lemmas
SetLike.one_mem_graded
SetLike.mul_mem_graded
SetLike.pow_mem_graded
,SetLike.list_prod_map_mem_graded
Strictly this last class is unnecessary as it has no fields not present in its parents, but it is
included for convenience. Note that there is no need for SetLike.GradedRing
or similar, as all
the information it would contain is already supplied by GradedMonoid
when A
is a collection
of objects satisfying AddSubmonoidClass
such as Submodule
s. These constructions are explored
in Algebra.DirectSum.Internal
.
This file also defines:
SetLike.isHomogeneous A
(which says thata
is homogeneous iffa ∈ A i
for somei : ι
)SetLike.homogeneousSubmonoid A
, which is, as the name suggests, the submonoid consisting of all the homogeneous elements.
Tags #
graded monoid
Equations
- GradedMonoid.instInhabitedOfDefault = inferInstanceAs (Inhabited (Sigma A))
Actions #
If R
acts on each A i
, then it acts on GradedMonoid A
via the .2
projection.
Equations
- GradedMonoid.instSMul = { smul := fun (r : α) (g : GradedMonoid A) => GradedMonoid.mk g.fst (r • g.snd) }
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- GradedMonoid.instMulAction = MulAction.mk ⋯ ⋯
Typeclasses #
GOne
implies One (GradedMonoid A)
Equations
- GradedMonoid.GOne.toOne A = { one := ⟨0, GradedMonoid.GOne.one⟩ }
GMul
implies Mul (GradedMonoid A)
.
Equations
- GradedMonoid.GMul.toMul A = { mul := fun (x y : GradedMonoid A) => ⟨x.fst + y.fst, GradedMonoid.GMul.mul x.snd y.snd⟩ }
A default implementation of power on a graded monoid, like npowRec
.
GMonoid.gnpow
should be used instead.
Equations
- GradedMonoid.GMonoid.gnpowRec 0 x = cast ⋯ GradedMonoid.GOne.one
- GradedMonoid.GMonoid.gnpowRec n.succ x = cast ⋯ (GradedMonoid.GMul.mul (GradedMonoid.GMonoid.gnpowRec n x) x)
Instances For
A tactic to for use as an optional value for GMonoid.gnpow_zero'
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A tactic to for use as an optional value for GMonoid.gnpow_succ'
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
- mul : {i j : ι} → A i → A j → A (i + j)
- one : A 0
- one_mul : ∀ (a : GradedMonoid A), 1 * a = a
Multiplication by
one
on the left is the identity - mul_one : ∀ (a : GradedMonoid A), a * 1 = a
Multiplication by
one
on the right is the identity Multiplication is associative
Optional field to allow definitional control of natural powers
- gnpow_zero' : ∀ (a : GradedMonoid A), GradedMonoid.mk (0 • a.fst) (GradedMonoid.GMonoid.gnpow 0 a.snd) = 1
The zeroth power will yield 1
- gnpow_succ' : ∀ (n : ℕ) (a : GradedMonoid A), GradedMonoid.mk (n.succ • a.fst) (GradedMonoid.GMonoid.gnpow n.succ a.snd) = ⟨n • a.fst, GradedMonoid.GMonoid.gnpow n a.snd⟩ * a
Successor powers behave as expected
Instances
Multiplication by one
on the left is the identity
Multiplication by one
on the right is the identity
Multiplication is associative
The zeroth power will yield 1
Successor powers behave as expected
GMonoid
implies a Monoid (GradedMonoid A)
.
Equations
- GradedMonoid.GMonoid.toMonoid A = Monoid.mk ⋯ ⋯ (fun (n : ℕ) (a : GradedMonoid A) => GradedMonoid.mk (n • a.fst) (GradedMonoid.GMonoid.gnpow n a.snd)) ⋯ ⋯
A graded version of CommMonoid
.
- mul : {i j : ι} → A i → A j → A (i + j)
- one : A 0
- one_mul : ∀ (a : GradedMonoid A), 1 * a = a
- mul_one : ∀ (a : GradedMonoid A), a * 1 = a
- gnpow_zero' : ∀ (a : GradedMonoid A), GradedMonoid.mk (0 • a.fst) (GradedMonoid.GMonoid.gnpow 0 a.snd) = 1
- gnpow_succ' : ∀ (n : ℕ) (a : GradedMonoid A), GradedMonoid.mk (n.succ • a.fst) (GradedMonoid.GMonoid.gnpow n.succ a.snd) = ⟨n • a.fst, GradedMonoid.GMonoid.gnpow n a.snd⟩ * a
- mul_comm : ∀ (a b : GradedMonoid A), a * b = b * a
Multiplication is commutative
Instances
Multiplication is commutative
GCommMonoid
implies a CommMonoid (GradedMonoid 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 AddCommMonoid (A 0)
structure to various
types of multiplicative structure.
1 : A 0
is the value provided in GOne.one
.
Equations
- GradedMonoid.GradeZero.one A = { one := GradedMonoid.GOne.one }
(•) : A 0 → A i → A i
is the value provided in GradedMonoid.GMul.mul
, composed with
an Eq.rec
to turn A (0 + i)
into A i
.
Equations
- GradedMonoid.GradeZero.smul A i = { smul := fun (x : A 0) (y : A i) => ⋯ ▸ GradedMonoid.GMul.mul x y }
(*) : A 0 → A 0 → A 0
is the value provided in GradedMonoid.GMul.mul
, composed with
an Eq.rec
to turn A (0 + 0)
into A 0
.
Equations
- GradedMonoid.GradeZero.mul A = { mul := fun (x1 x2 : A 0) => x1 • x2 }
Equations
- GradedMonoid.instNatPowOfNat A = { pow := fun (x : A 0) (n : ℕ) => ⋯ ▸ GradedMonoid.GMonoid.gnpow n x }
The Monoid
structure derived from GMonoid A
.
Equations
The CommMonoid
structure derived from GCommMonoid A
.
Equations
GradedMonoid.mk 0
is a MonoidHom
, using the GradedMonoid.GradeZero.monoid
structure.
Equations
- GradedMonoid.mkZeroMonoidHom A = { toFun := GradedMonoid.mk 0, map_one' := ⋯, map_mul' := ⋯ }
Instances For
Each grade A i
derives an A 0
-action structure from GMonoid A
.
Equations
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.dProdIndex fι = List.foldr (fun (i : α) (b : ι) => fι i + b) 0 l
Instances For
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 = List.foldrRecOn l (fun (i : α) (b : ι) => fι i + b) 0 GradedMonoid.GOne.one fun (x : ι) (x_1 : A x) (a : α) (x_2 : a ∈ l) => GradedMonoid.GMul.mul (fA a) x_1
Instances For
A variant of GradedMonoid.mk_list_dProd
for rewriting in the other direction.
Concrete instances #
If all grades are the same type and themselves form a monoid, then there is a trivial grading structure.
Equations
- Monoid.gMonoid ι = GradedMonoid.GMonoid.mk ⋯ ⋯ ⋯ (fun (n : ℕ) (x : ι) (a : R) => a ^ n) ⋯ ⋯
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 #
One has grade zero
Equations
- SetLike.gOne A = { one := ⟨1, ⋯⟩ }
Equations
- SetLike.gMul A = { mul := fun {i j : ι} (a : ↥(A i)) (b : ↥(A j)) => ⟨↑a * ↑b, ⋯⟩ }
A version of GradedMonoid.GMonoid
for internally graded objects.
Instances
The submonoid A 0
of R
.
Equations
- SetLike.GradeZero.submonoid A = { carrier := ↑(A 0), mul_mem' := ⋯, one_mem' := ⋯ }
Instances For
The monoid A 0
inherited from R
in the presence of SetLike.GradedMonoid A
.
Equations
- SetLike.GradeZero.instMonoid = inferInstanceAs (Monoid ↥(SetLike.GradeZero.submonoid A))
The commutative monoid A 0
inherited from R
in the presence of SetLike.GradedMonoid A
.
Equations
- SetLike.GradeZero.instCommMonoid = inferInstanceAs (CommMonoid ↥(SetLike.GradeZero.submonoid A))
The linter message "error: SetLike.GradeZero.coe_one.{u_3, u_2, u_1} Left-hand side does not simplify, when using the simp lemma on itself." is wrong. The LHS does simplify.
The linter message "error: SetLike.GradeZero.coe_mul.{u_3, u_2, u_1} Left-hand side does not simplify, when using the simp lemma on itself." is wrong. The LHS does simplify.
The linter message "error: SetLike.GradeZero.coe_pow.{u_3, u_2, u_1} Left-hand side does not simplify, when using the simp lemma on itself." is wrong. The LHS does simplify.
Build a GMonoid
instance for a collection of subobjects.
Equations
- SetLike.gMonoid A = GradedMonoid.GMonoid.mk ⋯ ⋯ ⋯ (fun (n : ℕ) (x : ι) (a : ↥(A x)) => ⟨↑a ^ n, ⋯⟩) ⋯ ⋯
Build a GCommMonoid
instance for a collection of subobjects.
Equations
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
- SetLike.Homogeneous A a = ∃ (i : ι), a ∈ A i
Instances For
When A
is a SetLike.GradedMonoid A
, then the homogeneous elements forms a submonoid.
Equations
- SetLike.homogeneousSubmonoid A = { carrier := {a : R | SetLike.Homogeneous A a}, mul_mem' := ⋯, one_mem' := ⋯ }