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

With the SigmaGraded locale open, 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 unecessary 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∈ A i for some i : ι)
• SetLike.HomogeneouSubmonoid A, which is, as the name suggests, the submonoid consisting of all the homogeneous elements.

tags

graded monoid

ink

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

A type alias of sigma types for graded monoids.

Equations

• GradedMonoid A = Sigma A

ink

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

Equations

• GradedMonoid.instInhabitedGradedMonoid = { default := default }

ink

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

Typeclasses

ink

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

• The term one of grade 0

  one : A 0

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

ink

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

GOne implies One (GradedMonoid A)

Equations

• GradedMonoid.GOne.toOne A = { one := { fst := 0, snd := GradedMonoid.GOne.one } }

ink

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

• The homogeneous multiplication map mul

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

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

ink

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

GMul implies Mul (GradedMonoid A).

Equations

• GradedMonoid.GMul.toMul A = { mul := fun x y => { fst := x.fst + y.fst, snd := GradedMonoid.GMul.mul x.snd y.snd } }

ink

theorem GradedMonoid.mk_mul_mk {ι : Type u_1} (A : ι → Type u_2) [inst : Add ι] [inst : 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)

ink

def GradedMonoid.GMonoid.gnpowRec {ι : Type u_1} {A : ι → Type u_2} [inst : AddMonoid ι] [inst : GradedMonoid.GMul A] [inst : 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 (_ : A 0 = A (0 • x)) GradedMonoid.GOne.one
• GradedMonoid.GMonoid.gnpowRec (Nat.succ n) x = cast (_ : A (x + n • x) = A ((n + 1) • x)) (GradedMonoid.GMul.mul x (GradedMonoid.GMonoid.gnpowRec n x))

ink

@[simp]

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

ink

@[simp]

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

ink

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.

ink

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.

ink

class GradedMonoid.GMonoid {ι : Type u_1} (A : ι → Type u_2) [inst : AddMonoid ι] extends GradedMonoid.GMul , GradedMonoid.GOne : Type (maxu_1u_2)

• Muliplication by one on the left is the identity

  one_mul : ∀ (a : GradedMonoid A), 1 * a = a

• Muliplication by one on the right is the identity

  mul_one : ∀ (a : GradedMonoid A), a * 1 = a

• Multiplication is associative

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

• Optional field to allow definitional control of natural powers

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

• The zeroth power will yield 1

  gnpow_zero' : autoParam (∀ (a : GradedMonoid A), GradedMonoid.mk (0 • a.fst) (gnpow 0 a.fst a.snd) = 1) _auto✝

• Successor powers behave as expected

  gnpow_succ' : autoParam (∀ (n : ℕ) (a : GradedMonoid A), GradedMonoid.mk (Nat.succ n • a.fst) (gnpow (Nat.succ n) a.fst a.snd) = a * { fst := n • a.fst, snd := gnpow n a.fst a.snd }) _auto✝

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.

ink

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

GMonoid implies a Monoid (GradedMonoid A).

Equations

• One or more equations did not get rendered due to their size.

ink

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

ink

class GradedMonoid.GCommMonoid {ι : Type u_1} (A : ι → Type u_2) [inst : AddCommMonoid ι] extends GradedMonoid.GMonoid : Type (maxu_1u_2)

• Multiplication is commutative

  mul_comm : ∀ (a b : GradedMonoid A), a * b = b * a

A graded version of CommMonoid.

ink

instance GradedMonoid.GCommMonoid.toCommMonoid {ι : Type u_1} (A : ι → Type u_2) [inst : AddCommMonoid ι] [inst : 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 = let src := GradedMonoid.GMonoid.toMonoid A; CommMonoid.mk (_ : ∀ (a b : GradedMonoid A), a * b = b * a)

Instances for A 0

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

ink

instance GradedMonoid.GradeZero.one {ι : Type u_1} (A : ι → Type u_2) [inst : Zero ι] [inst : 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 }

ink

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

(•) : A 0 → A i → A i→ A i → 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 y => (_ : 0 + i = i) ▸ GradedMonoid.GMul.mul x y }

ink

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

(*) : A 0 → A 0 → 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 x x_1 => x • x_1 }

ink

@[simp]

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

ink

@[simp]

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

ink

instance GradedMonoid.instPowOfNatToOfNat0ToZeroNat {ι : Type u_1} (A : ι → Type u_2) [inst : AddMonoid ι] [inst : GradedMonoid.GMonoid A] : Pow (A 0) ℕ

Equations

• GradedMonoid.instPowOfNatToOfNat0ToZeroNat A = { pow := fun x n => (_ : n • 0 = 0) ▸ GradedMonoid.GMonoid.gnpow n x }

ink

@[simp]

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

ink

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

The Monoid structure derived from GMonoid A.

Equations

• One or more equations did not get rendered due to their size.

ink

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

The CommMonoid structure derived from GCommMonoid A.

Equations

• One or more equations did not get rendered due to their size.

ink

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

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

Equations

• One or more equations did not get rendered due to their size.

ink

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

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

Equations

• One or more equations did not get rendered due to their size.

Dependent products of graded elements

ink

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

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

• List.dProd l fι fA = List.foldrRecOn l (fun i b => fι i + b) 0 GradedMonoid.GOne.one fun x x_1 a x_2 => GradedMonoid.GMul.mul (fA a) x_1

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

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

ink

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

Concrete instances

ink

@[simp]

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

ink

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

Equations

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

ink

@[simp]

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

ink

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

Equations

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

ink

@[simp]

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

ink

instance Monoid.gMonoid (ι : Type u_1) {R : Type u_2} [inst : AddMonoid ι] [inst : 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

• One or more equations did not get rendered due to their size.

ink

instance CommMonoid.gCommMonoid (ι : Type u_1) {R : Type u_2} [inst : AddCommMonoid ι] [inst : 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 ι = let src := Monoid.gMonoid ι; GradedMonoid.GCommMonoid.mk (_ : ∀ (x x_1 : GradedMonoid fun x => R), x * x_1 = x_1 * x)

ink

@[simp]

theorem List.dProd_monoid (ι : Type u_2) {R : Type u_3} {α : Type u_1} [inst : AddMonoid ι] [inst : Monoid R] (l : List α) (fι : α → ι) (fA : α → R) : List.dProd l fι fA = List.prod (List.map fA l)

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

ink

class SetLike.GradedOne {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : SetLike S R] [inst : One R] [inst : Zero ι] (A : ι → S) : Prop

• One has grade zero

  one_mem : 1 ∈ A 0

A version of GradedMonoid.GOne for internally graded objects.

ink

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

ink

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

Equations

• SetLike.gOne A = { one := { val := 1, property := (_ : 1 ∈ A 0) } }

ink

@[simp]

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

ink

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

• Multiplication is homogeneous

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

A version of GradedMonoid.ghas_one for internally graded objects.

ink

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

ink

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

Equations

• SetLike.gMul A = { mul := fun {i j} a b => { val := ↑a * ↑b, property := (_ : ↑a * ↑b ∈ A (i + j)) } }

ink

@[simp]

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

ink

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

A version of GradedMonoid.GMonoid for internally graded objects.

ink

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

ink

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

ink

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

ink

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

Build a GMonoid instance for a collection of subobjects.

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

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

ink

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

Build a GCommMonoid instance for a collection of subobjects.

Equations

• SetLike.gCommMonoid A = let src := SetLike.gMonoid A; GradedMonoid.GCommMonoid.mk (_ : ∀ (x x_1 : GradedMonoid fun i => { x // x ∈ A i }), x * x_1 = x_1 * x)

ink

@[simp]

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

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

ink

theorem SetLike.list_dProd_eq {ι : Type u_1} {R : Type u_2} {α : Type u_4} {S : Type u_3} [inst : SetLike S R] [inst : Monoid R] [inst : AddMonoid ι] (A : ι → S) [inst : SetLike.GradedMonoid A] (fι : α → ι) (fA : (a : α) → { x // x ∈ A (fι a) }) (l : List α) : List.dProd l fι fA = { val := List.prod (List.map (fun a => ↑(fA a)) l), property := (_ : List.prod (List.map (fun a => ↑(fA a)) l) ∈ A (List.dProdIndex l fι)) }

A version of List.coe_dProd_set_like with Subtype.mk.

ink

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

Equations

• SetLike.Homogeneous A a = ∃ i, a ∈ A i

ink

@[simp]

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

ink

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

ink

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

ink

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

When A is a SetLike.GradedMonoid A, then the homogeneous elements forms a submonoid.

Equations

• One or more equations did not get rendered due to their size.