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:

• GradedMonoid.GOne A
• GradedMonoid.GMul A
• GradedMonoid.GMonoid A
• GradedMonoid.GCommMonoid A

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 ith grade A i with A 0-actions (•) defined as left-multiplication:

• (nothing)
• GradedMonoid.GradeZero.SMul (A 0)
• GradedMonoid.GradeZero.MulAction (A 0)
• (nothing)

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 AddSubmonoids, AddSubgroups, or Submodules), this file provides the Prop typeclasses:

• SetLike.GradedOne A (which provides the obvious GradedMonoid.GOne A instance)
• SetLike.GradedMul A (which provides the obvious GradedMonoid.GMul A instance)
• SetLike.GradedMonoid A (which provides the obvious GradedMonoid.GMonoid A and GradedMonoid.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 Submodules. These constructions are explored in Algebra.DirectSum.Internal.

This file also defines:

• SetLike.isHomogeneous A (which says that a is homogeneous iff a ∈ A i for some i : ι)
• SetLike.homogeneousSubmonoid A, which is, as the name suggests, the submonoid consisting of all the homogeneous elements.

Tags

graded monoid

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

A type alias of sigma types for graded monoids.

Equations

• GradedMonoid A = Sigma A

instance GradedMonoid.instInhabitedOfDefault {ι : Type u_1} {A : ι → Type u_2} [Inhabited ι] [Inhabited (A default)] : Inhabited (GradedMonoid A)

Equations

• GradedMonoid.instInhabitedOfDefault = inferInstanceAs (Inhabited (Sigma A))

def GradedMonoid.mk {ι : Type u_1} {A : ι → Type u_2} (i : ι) : A i → GradedMonoid A

Construct an element of a graded monoid.

Equations

• GradedMonoid.mk = Sigma.mk

Actions

instance GradedMonoid.instSMul {ι : Type u_1} {α : Type u_3} {A : ι → Type u_2} [(i : ι) → SMul α (A i)] : SMul α (GradedMonoid A)

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) }

@[simp]

theorem GradedMonoid.fst_smul {ι : Type u_1} {α : Type u_3} {A : ι → Type u_2} [(i : ι) → SMul α (A i)] (a : α) (x : GradedMonoid A) : (a • x).fst = x.fst

@[simp]

theorem GradedMonoid.snd_smul {ι : Type u_1} {α : Type u_3} {A : ι → Type u_2} [(i : ι) → SMul α (A i)] (a : α) (x : GradedMonoid A) : (a • x).snd = a • x.snd

theorem GradedMonoid.smul_mk {ι : Type u_1} {α : Type u_3} {A : ι → Type u_2} [(i : ι) → SMul α (A i)] {i : ι} (c : α) (a : A i) : c • GradedMonoid.mk i a = GradedMonoid.mk i (c • a)

instance GradedMonoid.instSMulCommClass {ι : Type u_1} {α : Type u_3} {β : Type u_4} {A : ι → Type u_2} [(i : ι) → SMul α (A i)] [(i : ι) → SMul β (A i)] [∀ (i : ι), SMulCommClass α β (A i)] : SMulCommClass α β (GradedMonoid A)

Equations

• ⋯ = ⋯

instance GradedMonoid.instIsScalarTower {ι : Type u_1} {α : Type u_3} {β : Type u_4} {A : ι → Type u_2} [SMul α β] [(i : ι) → SMul α (A i)] [(i : ι) → SMul β (A i)] [∀ (i : ι), IsScalarTower α β (A i)] : IsScalarTower α β (GradedMonoid A)

Equations

• ⋯ = ⋯

instance GradedMonoid.instMulAction {ι : Type u_1} {α : Type u_3} {A : ι → Type u_2} [Monoid α] [(i : ι) → MulAction α (A i)] : MulAction α (GradedMonoid A)

Equations

• GradedMonoid.instMulAction = MulAction.mk ⋯ ⋯

Typeclasses

class GradedMonoid.GOne {ι : Type u_1} (A : ι → Type u_2) [Zero ι] : Type u_2

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

• one : A 0

  The term one of grade 0

instance GradedMonoid.GOne.toOne {ι : Type u_1} (A : ι → Type u_2) [Zero ι] [GradedMonoid.GOne A] : One (GradedMonoid A)

GOne implies One (GradedMonoid A)

Equations

• GradedMonoid.GOne.toOne A = { one := ⟨0, GradedMonoid.GOne.one⟩ }

@[simp]

theorem GradedMonoid.fst_one {ι : Type u_1} (A : ι → Type u_2) [Zero ι] [GradedMonoid.GOne A] : Sigma.fst 1 = 0

@[simp]

theorem GradedMonoid.snd_one {ι : Type u_1} (A : ι → Type u_2) [Zero ι] [GradedMonoid.GOne A] : Sigma.snd 1 = GradedMonoid.GOne.one

class GradedMonoid.GMul {ι : Type u_1} (A : ι → Type u_2) [Add ι] : Type (max u_1 u_2)

A graded version of Mul. Multiplication combines grades additively, like AddMonoidAlgebra.

• mul : {i j : ι} → A i → A j → A (i + j)

  The homogeneous multiplication map mul

instance GradedMonoid.GMul.toMul {ι : Type u_1} (A : ι → Type u_2) [Add ι] [GradedMonoid.GMul A] : Mul (GradedMonoid A)

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⟩ }

@[simp]

theorem GradedMonoid.fst_mul {ι : Type u_1} (A : ι → Type u_2) [Add ι] [GradedMonoid.GMul A] (x : GradedMonoid A) (y : GradedMonoid A) : (x * y).fst = x.fst + y.fst

@[simp]

theorem GradedMonoid.snd_mul {ι : Type u_1} (A : ι → Type u_2) [Add ι] [GradedMonoid.GMul A] (x : GradedMonoid A) (y : GradedMonoid A) : (x * y).snd = GradedMonoid.GMul.mul x.snd y.snd

theorem GradedMonoid.mk_mul_mk {ι : Type u_1} (A : ι → Type u_2) [Add ι] [GradedMonoid.GMul A] {i : ι} {j : ι} (a : A i) (b : A j) : GradedMonoid.mk i a * GradedMonoid.mk j b = GradedMonoid.mk (i + j) (GradedMonoid.GMul.mul a b)

def GradedMonoid.GMonoid.gnpowRec {ι : Type u_1} {A : ι → Type u_2} [AddMonoid ι] [GradedMonoid.GMul A] [GradedMonoid.GOne A] (n : ℕ) {i : ι} : A i → A (n • i)

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)

@[simp]

theorem GradedMonoid.GMonoid.gnpowRec_zero {ι : Type u_1} {A : ι → Type u_2} [AddMonoid ι] [GradedMonoid.GMul A] [GradedMonoid.GOne A] (a : GradedMonoid A) : GradedMonoid.mk (0 • a.fst) (GradedMonoid.GMonoid.gnpowRec 0 a.snd) = 1

@[simp]

theorem GradedMonoid.GMonoid.gnpowRec_succ {ι : Type u_1} {A : ι → Type u_2} [AddMonoid ι] [GradedMonoid.GMul A] [GradedMonoid.GOne A] (n : ℕ) (a : GradedMonoid A) : GradedMonoid.mk (n.succ • a.fst) (GradedMonoid.GMonoid.gnpowRec n.succ a.snd) = ⟨n • a.fst, GradedMonoid.GMonoid.gnpowRec n a.snd⟩ * a

def GradedMonoid.tacticApply_gmonoid_gnpowRec_zero_tac : Lean.ParserDescr

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.

def GradedMonoid.tacticApply_gmonoid_gnpowRec_succ_tac : Lean.ParserDescr

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.

class GradedMonoid.GMonoid {ι : Type u_1} (A : ι → Type u_2) [AddMonoid ι] extends GradedMonoid.GMul , GradedMonoid.GOne : 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.

• 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

• mul_assoc : ∀ (a b c : GradedMonoid A), a * b * c = a * (b * c)

  Multiplication is associative

• gnpow : (n : ℕ) → {i : ι} → A i → A (n • i)

  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

theorem GradedMonoid.GMonoid.one_mul {ι : Type u_1} {A : ι → Type u_2} : ∀ {inst : AddMonoid ι} [self : GradedMonoid.GMonoid A] (a : GradedMonoid A), 1 * a = a

Multiplication by one on the left is the identity

theorem GradedMonoid.GMonoid.mul_one {ι : Type u_1} {A : ι → Type u_2} : ∀ {inst : AddMonoid ι} [self : GradedMonoid.GMonoid A] (a : GradedMonoid A), a * 1 = a

Multiplication by one on the right is the identity

theorem GradedMonoid.GMonoid.mul_assoc {ι : Type u_1} {A : ι → Type u_2} : ∀ {inst : AddMonoid ι} [self : GradedMonoid.GMonoid A] (a b c : GradedMonoid A), a * b * c = a * (b * c)

Multiplication is associative

theorem GradedMonoid.GMonoid.gnpow_zero' {ι : Type u_1} {A : ι → Type u_2} : ∀ {inst : AddMonoid ι} [self : GradedMonoid.GMonoid A] (a : GradedMonoid A), GradedMonoid.mk (0 • a.fst) (GradedMonoid.GMonoid.gnpow 0 a.snd) = 1

The zeroth power will yield 1

theorem GradedMonoid.GMonoid.gnpow_succ' {ι : Type u_1} {A : ι → Type u_2} : ∀ {inst : AddMonoid ι} [self : GradedMonoid.GMonoid A] (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

instance GradedMonoid.GMonoid.toMonoid {ι : Type u_1} (A : ι → Type u_2) [AddMonoid ι] [GradedMonoid.GMonoid A] : Monoid (GradedMonoid A)

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)) ⋯ ⋯

@[simp]

theorem GradedMonoid.fst_pow {ι : Type u_1} (A : ι → Type u_2) [AddMonoid ι] [GradedMonoid.GMonoid A] (x : GradedMonoid A) (n : ℕ) : (x ^ n).fst = n • x.fst

@[simp]

theorem GradedMonoid.snd_pow {ι : Type u_1} (A : ι → Type u_2) [AddMonoid ι] [GradedMonoid.GMonoid A] (x : GradedMonoid A) (n : ℕ) : (x ^ n).snd = GradedMonoid.GMonoid.gnpow n x.snd

theorem GradedMonoid.mk_pow {ι : Type u_1} (A : ι → Type u_2) [AddMonoid ι] [GradedMonoid.GMonoid A] {i : ι} (a : A i) (n : ℕ) : GradedMonoid.mk i a ^ n = GradedMonoid.mk (n • i) (GradedMonoid.GMonoid.gnpow n a)

class GradedMonoid.GCommMonoid {ι : Type u_1} (A : ι → Type u_2) [AddCommMonoid ι] extends GradedMonoid.GMonoid , GradedMonoid.GMul , GradedMonoid.GOne : Type (max u_1 u_2)

A graded version of CommMonoid.

theorem GradedMonoid.GCommMonoid.mul_comm {ι : Type u_1} {A : ι → Type u_2} : ∀ {inst : AddCommMonoid ι} [self : GradedMonoid.GCommMonoid A] (a b : GradedMonoid A), a * b = b * a

Multiplication is commutative

instance GradedMonoid.GCommMonoid.toCommMonoid {ι : Type u_1} (A : ι → Type u_2) [AddCommMonoid ι] [GradedMonoid.GCommMonoid A] : CommMonoid (GradedMonoid A)

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

Equations

• GradedMonoid.GCommMonoid.toCommMonoid A = CommMonoid.mk ⋯

Instances for A 0

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

instance GradedMonoid.GradeZero.one {ι : Type u_1} (A : ι → Type u_2) [Zero ι] [GradedMonoid.GOne A] : One (A 0)

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

Equations

• GradedMonoid.GradeZero.one A = { one := GradedMonoid.GOne.one }

instance GradedMonoid.GradeZero.smul {ι : Type u_1} (A : ι → Type u_2) [AddZeroClass ι] [GradedMonoid.GMul A] (i : ι) : SMul (A 0) (A i)

(•) : 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 }

instance GradedMonoid.GradeZero.mul {ι : Type u_1} (A : ι → Type u_2) [AddZeroClass ι] [GradedMonoid.GMul A] : Mul (A 0)

(*) : 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 }

@[simp]

theorem GradedMonoid.mk_zero_smul {ι : Type u_1} {A : ι → Type u_2} [AddZeroClass ι] [GradedMonoid.GMul A] {i : ι} (a : A 0) (b : A i) : GradedMonoid.mk i (a • b) = GradedMonoid.mk 0 a * GradedMonoid.mk i b

theorem GradedMonoid.GradeZero.smul_eq_mul {ι : Type u_1} {A : ι → Type u_2} [AddZeroClass ι] [GradedMonoid.GMul A] (a : A 0) (b : A 0) : a • b = a * b

instance GradedMonoid.instNatPowOfNat {ι : Type u_1} (A : ι → Type u_2) [AddMonoid ι] [GradedMonoid.GMonoid A] : NatPow (A 0)

Equations

• GradedMonoid.instNatPowOfNat A = { pow := fun (x : A 0) (n : ℕ) => ⋯ ▸ GradedMonoid.GMonoid.gnpow n x }

@[simp]

theorem GradedMonoid.mk_zero_pow {ι : Type u_1} {A : ι → Type u_2} [AddMonoid ι] [GradedMonoid.GMonoid A] (a : A 0) (n : ℕ) : GradedMonoid.mk 0 (a ^ n) = GradedMonoid.mk 0 a ^ n

instance GradedMonoid.GradeZero.monoid {ι : Type u_1} (A : ι → Type u_2) [AddMonoid ι] [GradedMonoid.GMonoid A] : Monoid (A 0)

The Monoid structure derived from GMonoid A.

Equations

• GradedMonoid.GradeZero.monoid A = Function.Injective.monoid (GradedMonoid.mk 0) ⋯ ⋯ ⋯ ⋯

instance GradedMonoid.GradeZero.commMonoid {ι : Type u_1} (A : ι → Type u_2) [AddCommMonoid ι] [GradedMonoid.GCommMonoid A] : CommMonoid (A 0)

The CommMonoid structure derived from GCommMonoid A.

Equations

• GradedMonoid.GradeZero.commMonoid A = Function.Injective.commMonoid (GradedMonoid.mk 0) ⋯ ⋯ ⋯ ⋯

def GradedMonoid.mkZeroMonoidHom {ι : Type u_1} (A : ι → Type u_2) [AddMonoid ι] [GradedMonoid.GMonoid A] : A 0 →* GradedMonoid A

GradedMonoid.mk 0 is a MonoidHom, using the GradedMonoid.GradeZero.monoid structure.

Equations

• GradedMonoid.mkZeroMonoidHom A = { toFun := GradedMonoid.mk 0, map_one' := ⋯, map_mul' := ⋯ }

instance GradedMonoid.GradeZero.mulAction {ι : Type u_1} (A : ι → Type u_2) [AddMonoid ι] [GradedMonoid.GMonoid A] {i : ι} : MulAction (A 0) (A i)

Each grade A i derives an A 0-action structure from GMonoid A.

Equations

• GradedMonoid.GradeZero.mulAction A = Function.Injective.mulAction (GradedMonoid.mk i) ⋯ ⋯

Dependent products of graded elements

def List.dProdIndex {ι : Type u_1} {α : Type u_2} [AddMonoid ι] (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

• l.dProdIndex fι = List.foldr (fun (i : α) (b : ι) => fι i + b) 0 l

@[simp]

theorem List.dProdIndex_nil {ι : Type u_1} {α : Type u_2} [AddMonoid ι] (fι : α → ι) : [].dProdIndex fι = 0

@[simp]

theorem List.dProdIndex_cons {ι : Type u_1} {α : Type u_2} [AddMonoid ι] (a : α) (l : List α) (fι : α → ι) : (a :: l).dProdIndex fι = fι a + l.dProdIndex fι

theorem List.dProdIndex_eq_map_sum {ι : Type u_1} {α : Type u_2} [AddMonoid ι] (l : List α) (fι : α → ι) : l.dProdIndex fι = (List.map fι l).sum

def List.dProd {ι : Type u_1} {α : Type u_2} {A : ι → Type u_3} [AddMonoid ι] [GradedMonoid.GMonoid A] (l : List α) (fι : α → ι) (fA : (a : α) → A (fι a)) : A (l.dProdIndex 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

• 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

@[simp]

theorem List.dProd_nil {ι : Type u_1} {α : Type u_2} {A : ι → Type u_3} [AddMonoid ι] [GradedMonoid.GMonoid A] (fι : α → ι) (fA : (a : α) → A (fι a)) : [].dProd fι fA = GradedMonoid.GOne.one

@[simp]

theorem List.dProd_cons {ι : Type u_1} {α : Type u_2} {A : ι → Type u_3} [AddMonoid ι] [GradedMonoid.GMonoid A] (fι : α → ι) (fA : (a : α) → A (fι a)) (a : α) (l : List α) : (a :: l).dProd fι fA = GradedMonoid.GMul.mul (fA a) (l.dProd fι fA)

theorem GradedMonoid.mk_list_dProd {ι : Type u_1} {α : Type u_2} {A : ι → Type u_3} [AddMonoid ι] [GradedMonoid.GMonoid A] (l : List α) (fι : α → ι) (fA : (a : α) → A (fι a)) : GradedMonoid.mk (l.dProdIndex fι) (l.dProd fι fA) = (List.map (fun (a : α) => GradedMonoid.mk (fι a) (fA a)) l).prod

theorem GradedMonoid.list_prod_map_eq_dProd {ι : Type u_1} {α : Type u_2} {A : ι → Type u_3} [AddMonoid ι] [GradedMonoid.GMonoid A] (l : List α) (f : α → GradedMonoid A) : (List.map f l).prod = GradedMonoid.mk (l.dProdIndex fun (i : α) => (f i).fst) (l.dProd (fun (i : α) => (f i).fst) fun (i : α) => (f i).snd)

A variant of GradedMonoid.mk_list_dProd for rewriting in the other direction.

theorem GradedMonoid.list_prod_ofFn_eq_dProd {ι : Type u_1} {A : ι → Type u_3} [AddMonoid ι] [GradedMonoid.GMonoid A] {n : ℕ} (f : Fin n → GradedMonoid A) : (List.ofFn f).prod = GradedMonoid.mk ((List.finRange n).dProdIndex fun (i : Fin n) => (f i).fst) ((List.finRange n).dProd (fun (i : Fin n) => (f i).fst) fun (i : Fin n) => (f i).snd)

Concrete instances

instance One.gOne (ι : Type u_1) {R : Type u_2} [Zero ι] [One R] : GradedMonoid.GOne fun (x : ι) => R

Equations

• One.gOne ι = { one := 1 }

@[simp]

theorem One.gOne_one (ι : Type u_1) {R : Type u_2} [Zero ι] [One R] : GradedMonoid.GOne.one = 1

instance Mul.gMul (ι : Type u_1) {R : Type u_2} [Add ι] [Mul R] : GradedMonoid.GMul fun (x : ι) => R

Equations

• Mul.gMul ι = { mul := fun {i j : ι} (x y : R) => x * y }

@[simp]

theorem Mul.gMul_mul (ι : Type u_1) {R : Type u_2} [Add ι] [Mul R] : ∀ {i j : ι} (x y : R), GradedMonoid.GMul.mul x y = x * y

instance Monoid.gMonoid (ι : Type u_1) {R : Type u_2} [AddMonoid ι] [Monoid R] : GradedMonoid.GMonoid fun (x : ι) => R

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) ⋯ ⋯

@[simp]

theorem Monoid.gMonoid_gnpow (ι : Type u_1) {R : Type u_2} [AddMonoid ι] [Monoid R] (n : ℕ) : ∀ (x : ι) (a : R), GradedMonoid.GMonoid.gnpow n a = a ^ n

instance CommMonoid.gCommMonoid (ι : Type u_1) {R : Type u_2} [AddCommMonoid ι] [CommMonoid R] : GradedMonoid.GCommMonoid fun (x : ι) => R

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

Equations

• CommMonoid.gCommMonoid ι = GradedMonoid.GCommMonoid.mk ⋯

@[simp]

theorem List.dProd_monoid (ι : Type u_1) {R : Type u_2} {α : Type u_3} [AddMonoid ι] [Monoid R] (l : List α) (fι : α → ι) (fA : α → R) : l.dProd fι 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 SetLike.GradedOne {ι : Type u_1} {R : Type u_2} {S : Type u_3} [SetLike S R] [One R] [Zero ι] (A : ι → S) : Prop

A version of GradedMonoid.GOne for internally graded objects.

• one_mem : 1 ∈ A 0

  One has grade zero

theorem SetLike.GradedOne.one_mem {ι : Type u_1} {R : Type u_2} {S : Type u_3} : ∀ {inst : SetLike S R} {inst_1 : One R} {inst_2 : Zero ι} {A : ι → S} [self : SetLike.GradedOne A], 1 ∈ A 0

One has grade zero

theorem SetLike.one_mem_graded {ι : Type u_1} {R : Type u_2} {S : Type u_3} [SetLike S R] [One R] [Zero ι] (A : ι → S) [SetLike.GradedOne A] : 1 ∈ A 0

instance SetLike.gOne {ι : Type u_1} {R : Type u_2} {S : Type u_3} [SetLike S R] [One R] [Zero ι] (A : ι → S) [SetLike.GradedOne A] : GradedMonoid.GOne fun (i : ι) => ↥(A i)

Equations

• SetLike.gOne A = { one := ⟨1, ⋯⟩ }

@[simp]

theorem SetLike.coe_gOne {ι : Type u_1} {R : Type u_2} {S : Type u_3} [SetLike S R] [One R] [Zero ι] (A : ι → S) [SetLike.GradedOne A] : ↑GradedMonoid.GOne.one = 1

class SetLike.GradedMul {ι : Type u_1} {R : Type u_2} {S : Type u_3} [SetLike S R] [Mul R] [Add ι] (A : ι → S) : Prop

A version of GradedMonoid.ghas_one for internally graded objects.

• mul_mem : ∀ ⦃i j : ι⦄ {gi gj : R}, gi ∈ A i → gj ∈ A j → gi * gj ∈ A (i + j)

  Multiplication is homogeneous

theorem SetLike.GradedMul.mul_mem {ι : Type u_1} {R : Type u_2} {S : Type u_3} : ∀ {inst : SetLike S R} {inst_1 : Mul R} {inst_2 : Add ι} {A : ι → S} [self : SetLike.GradedMul A] ⦃i j : ι⦄ {gi gj : R}, gi ∈ A i → gj ∈ A j → gi * gj ∈ A (i + j)

Multiplication is homogeneous

theorem SetLike.mul_mem_graded {ι : Type u_1} {R : Type u_2} {S : Type u_3} [SetLike S R] [Mul R] [Add ι] {A : ι → S} [SetLike.GradedMul A] ⦃i : ι⦄ ⦃j : ι⦄ {gi : R} {gj : R} (hi : gi ∈ A i) (hj : gj ∈ A j) : gi * gj ∈ A (i + j)

instance SetLike.gMul {ι : Type u_1} {R : Type u_2} {S : Type u_3} [SetLike S R] [Mul R] [Add ι] (A : ι → S) [SetLike.GradedMul A] : GradedMonoid.GMul fun (i : ι) => ↥(A i)

Equations

• SetLike.gMul A = { mul := fun {i j : ι} (a : ↥(A i)) (b : ↥(A j)) => ⟨↑a * ↑b, ⋯⟩ }

@[simp]

theorem SetLike.coe_gMul {ι : Type u_1} {R : Type u_2} {S : Type u_3} [SetLike S R] [Mul R] [Add ι] (A : ι → S) [SetLike.GradedMul A] {i : ι} {j : ι} (x : ↥(A i)) (y : ↥(A j)) : ↑(GradedMonoid.GMul.mul x y) = ↑x * ↑y

class SetLike.GradedMonoid {ι : Type u_1} {R : Type u_2} {S : Type u_3} [SetLike S R] [Monoid R] [AddMonoid ι] (A : ι → S) extends SetLike.GradedOne , SetLike.GradedMul : Prop

A version of GradedMonoid.GMonoid for internally graded objects.

def SetLike.GradeZero.submonoid {ι : Type u_1} {R : Type u_2} {S : Type u_3} [SetLike S R] [Monoid R] [AddMonoid ι] (A : ι → S) [SetLike.GradedMonoid A] : Submonoid R

The submonoid A 0 of R.

Equations

• SetLike.GradeZero.submonoid A = { carrier := ↑(A 0), mul_mem' := ⋯, one_mem' := ⋯ }

@[simp]

theorem SetLike.GradeZero.submonoid_coe {ι : Type u_1} {R : Type u_2} {S : Type u_3} [SetLike S R] [Monoid R] [AddMonoid ι] (A : ι → S) [SetLike.GradedMonoid A] : ↑(SetLike.GradeZero.submonoid A) = ↑(A 0)

instance SetLike.GradeZero.instMonoid {ι : Type u_1} {R : Type u_2} {S : Type u_3} [SetLike S R] [Monoid R] [AddMonoid ι] {A : ι → S} [SetLike.GradedMonoid A] : Monoid ↥(A 0)

The monoid A 0 inherited from R in the presence of SetLike.GradedMonoid A.

Equations

• SetLike.GradeZero.instMonoid = inferInstanceAs (Monoid ↥(SetLike.GradeZero.submonoid A))

instance SetLike.GradeZero.instCommMonoid {ι : Type u_1} [AddMonoid ι] {R : Type u_4} {S : Type u_5} [SetLike S R] [CommMonoid R] {A : ι → S} [SetLike.GradedMonoid A] : CommMonoid ↥(A 0)

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))

@[simp]

theorem SetLike.GradeZero.coe_one {ι : Type u_1} {R : Type u_2} {S : Type u_3} [SetLike S R] [Monoid R] [AddMonoid ι] {A : ι → S} [SetLike.GradedMonoid A] : ↑1 = 1

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.

@[simp]

theorem SetLike.GradeZero.coe_mul {ι : Type u_1} {R : Type u_2} {S : Type u_3} [SetLike S R] [Monoid R] [AddMonoid ι] {A : ι → S} [SetLike.GradedMonoid A] (a : ↥(A 0)) (b : ↥(A 0)) : ↑(a * b) = ↑a * ↑b

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.

@[simp]

theorem SetLike.GradeZero.coe_pow {ι : Type u_1} {R : Type u_2} {S : Type u_3} [SetLike S R] [Monoid R] [AddMonoid ι] {A : ι → S} [SetLike.GradedMonoid A] (a : ↥(A 0)) (n : ℕ) : ↑(a ^ n) = ↑a ^ n

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.

theorem SetLike.pow_mem_graded {ι : Type u_1} {R : Type u_2} {S : Type u_3} [SetLike S R] [Monoid R] [AddMonoid ι] {A : ι → S} [SetLike.GradedMonoid A] (n : ℕ) {r : R} {i : ι} (h : r ∈ A i) : r ^ n ∈ A (n • i)

theorem SetLike.list_prod_map_mem_graded {ι : Type u_1} {R : Type u_2} {S : Type u_3} [SetLike S R] [Monoid R] [AddMonoid ι] {A : ι → S} [SetLike.GradedMonoid A] {ι' : Type u_4} (l : List ι') (i : ι' → ι) (r : ι' → R) (h : ∀ j ∈ l, r j ∈ A (i j)) : (List.map r l).prod ∈ A (List.map i l).sum

theorem SetLike.list_prod_ofFn_mem_graded {ι : Type u_1} {R : Type u_2} {S : Type u_3} [SetLike S R] [Monoid R] [AddMonoid ι] {A : ι → S} [SetLike.GradedMonoid A] {n : ℕ} (i : Fin n → ι) (r : Fin n → R) (h : ∀ (j : Fin n), r j ∈ A (i j)) : (List.ofFn r).prod ∈ A (List.ofFn i).sum

instance SetLike.gMonoid {ι : Type u_1} {R : Type u_2} {S : Type u_3} [SetLike S R] [Monoid R] [AddMonoid ι] (A : ι → S) [SetLike.GradedMonoid A] : GradedMonoid.GMonoid fun (i : ι) => ↥(A i)

Build a GMonoid instance for a collection of subobjects.

Equations

• SetLike.gMonoid A = GradedMonoid.GMonoid.mk ⋯ ⋯ ⋯ (fun (n : ℕ) (x : ι) (a : ↥(A x)) => ⟨↑a ^ n, ⋯⟩) ⋯ ⋯

@[simp]

theorem SetLike.coe_gnpow {ι : Type u_1} {R : Type u_2} {S : Type u_3} [SetLike S R] [Monoid R] [AddMonoid ι] (A : ι → S) [SetLike.GradedMonoid A] {i : ι} (x : ↥(A i)) (n : ℕ) : ↑(GradedMonoid.GMonoid.gnpow n x) = ↑x ^ n

instance SetLike.gCommMonoid {ι : Type u_1} {R : Type u_2} {S : Type u_3} [SetLike S R] [CommMonoid R] [AddCommMonoid ι] (A : ι → S) [SetLike.GradedMonoid A] : GradedMonoid.GCommMonoid fun (i : ι) => ↥(A i)

Build a GCommMonoid instance for a collection of subobjects.

Equations

• SetLike.gCommMonoid A = GradedMonoid.GCommMonoid.mk ⋯

@[simp]

theorem SetLike.coe_list_dProd {ι : Type u_1} {R : Type u_2} {α : Type u_3} {S : Type u_4} [SetLike S R] [Monoid R] [AddMonoid ι] (A : ι → S) [SetLike.GradedMonoid A] (fι : α → ι) (fA : (a : α) → ↥(A (fι a))) (l : List α) : ↑(l.dProd fι fA) = (List.map (fun (a : α) => ↑(fA a)) l).prod

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

theorem SetLike.list_dProd_eq {ι : Type u_1} {R : Type u_2} {α : Type u_3} {S : Type u_4} [SetLike S R] [Monoid R] [AddMonoid ι] (A : ι → S) [SetLike.GradedMonoid A] (fι : α → ι) (fA : (a : α) → ↥(A (fι a))) (l : List α) : l.dProd fι fA = ⟨(List.map (fun (a : α) => ↑(fA a)) l).prod, ⋯⟩

A version of List.coe_dProd_set_like with Subtype.mk.

def SetLike.Homogeneous {ι : Type u_1} {R : Type u_2} {S : Type u_3} [SetLike 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

• SetLike.Homogeneous A a = ∃ (i : ι), a ∈ A i

@[simp]

theorem SetLike.homogeneous_coe {ι : Type u_1} {R : Type u_2} {S : Type u_3} [SetLike S R] {A : ι → S} {i : ι} (x : ↥(A i)) : SetLike.Homogeneous A ↑x

theorem SetLike.homogeneous_one {ι : Type u_1} {R : Type u_2} {S : Type u_3} [SetLike S R] [Zero ι] [One R] (A : ι → S) [SetLike.GradedOne A] : SetLike.Homogeneous A 1

theorem SetLike.homogeneous_mul {ι : Type u_1} {R : Type u_2} {S : Type u_3} [SetLike S R] [Add ι] [Mul R] {A : ι → S} [SetLike.GradedMul A] {a : R} {b : R} : SetLike.Homogeneous A a → SetLike.Homogeneous A b → SetLike.Homogeneous A (a * b)

def SetLike.homogeneousSubmonoid {ι : Type u_1} {R : Type u_2} {S : Type u_3} [SetLike S R] [AddMonoid ι] [Monoid R] (A : ι → S) [SetLike.GradedMonoid A] : Submonoid R

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' := ⋯ }