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

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

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

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

Construct an element of a graded monoid.

Typeclasses

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

• one : A 0

  The term one of grade 0

A graded version of One, which must be 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)

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

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

  The homogeneous multiplication map mul

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

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

GMul implies Mul (GradedMonoid A).

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 (_ : 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))

@[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 (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 }

def GradedMonoid.tacticApply_gmonoid_gnpowRec_zero_tac : Lean.ParserDescr

A tactic to for use as an optional value for GMonoid.gnpow_zero'.

def GradedMonoid.tacticApply_gmonoid_gnpowRec_succ_tac : Lean.ParserDescr

A tactic to for use as an optional value for GMonoid.gnpow_succ'.

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

• 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 (Nat.succ n • a.fst) (GradedMonoid.GMonoid.gnpow (Nat.succ n) a.snd) = a * { fst := n • a.fst, snd := GradedMonoid.GMonoid.gnpow n a.snd }

  Successor powers behave as expected

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.

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

GMonoid implies a Monoid (GradedMonoid A).

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 : Type (max u_1 u_2)

• 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
• mul_assoc : ∀ (a b c : GradedMonoid A), a * b * c = a * (b * c)
• gnpow : (n : ℕ) → {i : ι} → A i → A (n • i)
• 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 (Nat.succ n • a.fst) (GradedMonoid.GMonoid.gnpow (Nat.succ n) a.snd) = a * { fst := n • a.fst, snd := GradedMonoid.GMonoid.gnpow n a.snd }
• mul_comm : ∀ (a b : GradedMonoid A), a * b = b * a

  Multiplication is commutative

A graded version of CommMonoid.

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.

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.

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.

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.

@[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

@[simp]

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.instPowOfNatToOfNat0ToZeroNat {ι : Type u_1} (A : ι → Type u_2) [AddMonoid ι] [GradedMonoid.GMonoid A] : Pow (A 0) ℕ

@[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.

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.

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.

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.

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.

@[simp]

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

@[simp]

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

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

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

@[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)) : List.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 α) : List.dProd (a :: l) fι fA = GradedMonoid.GMul.mul (fA a) (List.dProd l 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 (List.dProdIndex l fι) (List.dProd l fι fA) = List.prod (List.map (fun a => GradedMonoid.mk (fι a) (fA a)) l)

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

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

@[simp]

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

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

@[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 Mul.gMul (ι : Type u_1) {R : Type u_2} [Add ι] [Mul R] : GradedMonoid.GMul fun x => R

@[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 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.

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.

@[simp]

theorem List.dProd_monoid (ι : Type u_1) {R : Type u_2} {α : Type u_3} [AddMonoid ι] [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

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

• one_mem : 1 ∈ A 0

  One has grade zero

A version of GradedMonoid.GOne for internally graded objects.

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 => { x // x ∈ A i }

@[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

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

  Multiplication is homogeneous

A version of GradedMonoid.ghas_one for internally graded objects.

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 => { x // x ∈ A i }

@[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 : { x // x ∈ A i }) (y : { x // x ∈ 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.

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 : ι'), j ∈ l → r j ∈ A (i j)) : List.prod (List.map r l) ∈ A (List.sum (List.map i l))

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.prod (List.ofFn r) ∈ A (List.sum (List.ofFn i))

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 => { x // x ∈ A i }

Build a GMonoid instance for a collection of subobjects.

@[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 : { x // 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 => { x // x ∈ A i }

Build a GCommMonoid instance for a collection of subobjects.

@[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 : α) → { 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.

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 : α) → { 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.

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.

@[simp]

theorem SetLike.homogeneous_coe {ι : Type u_1} {R : Type u_2} {S : Type u_3} [SetLike S R] {A : ι → S} {i : ι} (x : { x // 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.