mathlib documentation

algebra.graded_monoid

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:

With the sigma_graded locale open, these respectively imbue:

the base type A 0 with:

and the ith grade A i with A 0-actions (•) defined as left-multiplication:

(nothing)
graded_monoid.grade_zero.has_smul (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_submonoids, add_subgroups, or submodules), this file provides the Prop typeclasses:

set_like.has_graded_one A (which provides the obvious graded_monoid.ghas_one A instance)
set_like.has_graded_mul A (which provides the obvious graded_monoid.ghas_mul A instance)
set_like.graded_monoid A (which provides the obvious graded_monoid.gmonoid A and graded_monoid.gcomm_monoid A instances)

which respectively provide the API lemmas

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 set_like.graded_ring or similar, as all the information it would contain is already supplied by graded_monoid when A is a collection of objects satisfying add_submonoid_class such as submodules. These constructions are explored in algebra.direct_sum.internal.

This file also defines:

set_like.is_homogeneous A (which says that a is homogeneous iff a ∈ A i for some i : ι)
set_like.homogeneous_submonoid A, which is, as the name suggests, the submonoid consisting of all the homogeneous elements.

tags #

graded monoid

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

Type (max u_1 u_2)

A type alias of sigma types for graded monoids.

Equations

graded_monoid A = sigma A

Instances for graded_monoid

@[protected, instance]

def graded_monoid.inhabited {ι : Type u_1} {A : ι → Type u_2} [inhabited ι] [inhabited (A inhabited.default)] :

inhabited (graded_monoid A)

Equations

graded_monoid.inhabited = sigma.inhabited

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

A i → graded_monoid A

Construct an element of a graded monoid.

Equations

graded_monoid.mk = sigma.mk

Typeclasses #

@[class]

structure graded_monoid.ghas_one {ι : Type u_1} (A : ι → Type u_2) [has_zero ι] :

Type u_2

one : A 0

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

Instances of this typeclass

Instances of other typeclasses for graded_monoid.ghas_one

graded_monoid.ghas_one.has_sizeof_inst

@[protected, instance]

def graded_monoid.ghas_one.to_has_one {ι : Type u_1} (A : ι → Type u_2) [has_zero ι] [graded_monoid.ghas_one A] :

has_one (graded_monoid A)

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

@[class]

structure graded_monoid.ghas_mul {ι : Type u_1} (A : ι → Type u_2) [has_add ι] :

Type (max u_1 u_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.

Instances of this typeclass

Instances of other typeclasses for graded_monoid.ghas_mul

graded_monoid.ghas_mul.has_sizeof_inst

@[protected, instance]

def graded_monoid.ghas_mul.to_has_mul {ι : Type u_1} (A : ι → Type u_2) [has_add ι] [graded_monoid.ghas_mul A] :

has_mul (graded_monoid A)

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

theorem graded_monoid.mk_mul_mk {ι : Type u_1} (A : ι → Type u_2) [has_add ι] [graded_monoid.ghas_mul A] {i j : ι} (a : A i) (b : A j) :

graded_monoid.mk i a * graded_monoid.mk j b = graded_monoid.mk (i + j) (graded_monoid.ghas_mul.mul a b)

def graded_monoid.gmonoid.gnpow_rec {ι : Type u_1} {A : ι → Type u_2} [add_monoid ι] [graded_monoid.ghas_mul A] [graded_monoid.ghas_one A] (n : ℕ) {i : ι} :

A i → A (n • i)

A default implementation of power on a graded monoid, like npow_rec. gmonoid.gnpow should be used instead.

Equations

graded_monoid.gmonoid.gnpow_rec (n + 1) a = cast _ (graded_monoid.ghas_mul.mul a (graded_monoid.gmonoid.gnpow_rec n a))
graded_monoid.gmonoid.gnpow_rec 0 a = cast _ graded_monoid.ghas_one.one

@[simp]

theorem graded_monoid.gmonoid.gnpow_rec_zero {ι : Type u_1} {A : ι → Type u_2} [add_monoid ι] [graded_monoid.ghas_mul A] [graded_monoid.ghas_one A] (a : graded_monoid A) :

graded_monoid.mk (0 • a.fst) (graded_monoid.gmonoid.gnpow_rec 0 a.snd) = 1

meta def graded_monoid.gmonoid.apply_gnpow_rec_zero_tac :

Tactic used to autofill graded_monoid.gmonoid.gnpow_zero' when the default graded_monoid.gmonoid.gnpow_rec is used.

@[simp]

theorem graded_monoid.gmonoid.gnpow_rec_succ {ι : Type u_1} {A : ι → Type u_2} [add_monoid ι] [graded_monoid.ghas_mul A] [graded_monoid.ghas_one A] (n : ℕ) (a : graded_monoid A) :

graded_monoid.mk (n.succ • a.fst) (graded_monoid.gmonoid.gnpow_rec n.succ a.snd) = a * ⟨n • a.fst, graded_monoid.gmonoid.gnpow_rec n a.snd⟩

meta def graded_monoid.gmonoid.apply_gnpow_rec_succ_tac :

Tactic used to autofill graded_monoid.gmonoid.gnpow_succ' when the default graded_monoid.gmonoid.gnpow_rec is used.

@[instance]

def graded_monoid.gmonoid.to_ghas_mul {ι : Type u_1} (A : ι → Type u_2) [add_monoid ι] [self : graded_monoid.gmonoid A] :

graded_monoid.ghas_mul A

@[instance]

def graded_monoid.gmonoid.to_ghas_one {ι : Type u_1} (A : ι → Type u_2) [add_monoid ι] [self : graded_monoid.gmonoid A] :

graded_monoid.ghas_one A

@[class]

structure graded_monoid.gmonoid {ι : Type u_1} (A : ι → Type u_2) [add_monoid ι] :

Type (max u_1 u_2)

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.

Instances of this typeclass

Instances of other typeclasses for graded_monoid.gmonoid

graded_monoid.gmonoid.has_sizeof_inst

@[protected, instance]

def graded_monoid.gmonoid.to_monoid {ι : Type u_1} (A : ι → Type u_2) [add_monoid ι] [graded_monoid.gmonoid A] :

monoid (graded_monoid A)

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

theorem graded_monoid.mk_pow {ι : Type u_1} (A : ι → Type u_2) [add_monoid ι] [graded_monoid.gmonoid A] {i : ι} (a : A i) (n : ℕ) :

graded_monoid.mk i a ^ n = graded_monoid.mk (n • i) (graded_monoid.gmonoid.gnpow n a)

@[instance]

def graded_monoid.gcomm_monoid.to_gmonoid {ι : Type u_1} (A : ι → Type u_2) [add_comm_monoid ι] [self : graded_monoid.gcomm_monoid A] :

graded_monoid.gmonoid A

@[class]

structure graded_monoid.gcomm_monoid {ι : Type u_1} (A : ι → Type u_2) [add_comm_monoid ι] :

Type (max u_1 u_2)

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.

Instances of this typeclass

Instances of other typeclasses for graded_monoid.gcomm_monoid

graded_monoid.gcomm_monoid.has_sizeof_inst

@[protected, instance]

def graded_monoid.gcomm_monoid.to_comm_monoid {ι : Type u_1} (A : ι → Type u_2) [add_comm_monoid ι] [graded_monoid.gcomm_monoid A] :

comm_monoid (graded_monoid A)

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.

@[protected, nolint, instance]

def graded_monoid.grade_zero.has_one {ι : Type u_1} (A : ι → Type u_2) [has_zero ι] [graded_monoid.ghas_one A] :

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}

@[protected, instance]

def graded_monoid.grade_zero.has_smul {ι : Type u_1} (A : ι → Type u_2) [add_zero_class ι] [graded_monoid.ghas_mul A] (i : ι) :

has_smul (A 0) (A i)

(•) : 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_smul A i = {smul := λ (x : A 0) (y : A i), eq.rec (graded_monoid.ghas_mul.mul x y) _}

@[protected, instance]

def graded_monoid.grade_zero.has_mul {ι : Type u_1} (A : ι → Type u_2) [add_zero_class ι] [graded_monoid.ghas_mul A] :

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

graded_monoid.grade_zero.has_mul A = {mul := has_smul.smul (graded_monoid.grade_zero.has_smul A 0)}

@[simp]

theorem graded_monoid.mk_zero_smul {ι : Type u_1} {A : ι → Type u_2} [add_zero_class ι] [graded_monoid.ghas_mul A] {i : ι} (a : A 0) (b : A i) :

graded_monoid.mk i (a • b) = graded_monoid.mk 0 a * graded_monoid.mk i b

@[simp]

theorem graded_monoid.grade_zero.smul_eq_mul {ι : Type u_1} {A : ι → Type u_2} [add_zero_class ι] [graded_monoid.ghas_mul A] (a b : A 0) :

a • b = a * b

@[protected, instance]

def graded_monoid.nat.has_pow {ι : Type u_1} (A : ι → Type u_2) [add_monoid ι] [graded_monoid.gmonoid A] :

has_pow (A 0) ℕ

Equations

graded_monoid.nat.has_pow A = {pow := λ (x : A 0) (n : ℕ), eq.rec (graded_monoid.gmonoid.gnpow n x) _}

@[simp]

theorem graded_monoid.mk_zero_pow {ι : Type u_1} {A : ι → Type u_2} [add_monoid ι] [graded_monoid.gmonoid A] (a : A 0) (n : ℕ) :

graded_monoid.mk 0 (a ^ n) = graded_monoid.mk 0 a ^ n

@[protected, instance]

def graded_monoid.grade_zero.monoid {ι : Type u_1} (A : ι → Type u_2) [add_monoid ι] [graded_monoid.gmonoid A] :

monoid (A 0)

The monoid structure derived from gmonoid A.

Equations

graded_monoid.grade_zero.monoid A = function.injective.monoid (graded_monoid.mk 0) _ _ _ graded_monoid.mk_zero_pow

@[protected, instance]

def graded_monoid.grade_zero.comm_monoid {ι : Type u_1} (A : ι → Type u_2) [add_comm_monoid ι] [graded_monoid.gcomm_monoid A] :

comm_monoid (A 0)

The comm_monoid structure derived from gcomm_monoid A.

Equations

graded_monoid.grade_zero.comm_monoid A = function.injective.comm_monoid (graded_monoid.mk 0) _ _ _ _

def graded_monoid.mk_zero_monoid_hom {ι : Type u_1} (A : ι → Type u_2) [add_monoid ι] [graded_monoid.gmonoid A] :

A 0 →* graded_monoid A

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

@[protected, instance]

def graded_monoid.grade_zero.mul_action {ι : Type u_1} (A : ι → Type u_2) [add_monoid ι] [graded_monoid.gmonoid A] {i : ι} :

mul_action (A 0) (A i)

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 #

def list.dprod_index {ι : Type u_1} {α : Type u_2} [add_monoid ι] (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.dprod_index fι = list.foldr (λ (i : α) (b : ι), fι i + b) 0 l

@[simp]

theorem list.dprod_index_nil {ι : Type u_1} {α : Type u_2} [add_monoid ι] (fι : α → ι) :

list.nil.dprod_index fι = 0

@[simp]

theorem list.dprod_index_cons {ι : Type u_1} {α : Type u_2} [add_monoid ι] (a : α) (l : list α) (fι : α → ι) :

(a :: l).dprod_index fι = fι a + l.dprod_index fι

theorem list.dprod_index_eq_map_sum {ι : Type u_1} {α : Type u_2} [add_monoid ι] (l : list α) (fι : α → ι) :

l.dprod_index fι = (list.map fι l).sum

def list.dprod {ι : Type u_1} {α : Type u_2} {A : ι → Type u_3} [add_monoid ι] [graded_monoid.gmonoid A] (l : list α) (fι : α → ι) (fA : Π (a : α), A (fι a)) :

A (l.dprod_index 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 = 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)

@[simp]

theorem list.dprod_nil {ι : Type u_1} {α : Type u_2} {A : ι → Type u_3} [add_monoid ι] [graded_monoid.gmonoid A] (fι : α → ι) (fA : Π (a : α), A (fι a)) :

list.nil.dprod fι fA = graded_monoid.ghas_one.one

@[simp]

theorem list.dprod_cons {ι : Type u_1} {α : Type u_2} {A : ι → Type u_3} [add_monoid ι] [graded_monoid.gmonoid A] (fι : α → ι) (fA : Π (a : α), A (fι a)) (a : α) (l : list α) :

(a :: l).dprod fι fA = graded_monoid.ghas_mul.mul (fA a) (l.dprod fι fA)

theorem graded_monoid.mk_list_dprod {ι : Type u_1} {α : Type u_2} {A : ι → Type u_3} [add_monoid ι] [graded_monoid.gmonoid A] (l : list α) (fι : α → ι) (fA : Π (a : α), A (fι a)) :

graded_monoid.mk (l.dprod_index fι) (l.dprod fι fA) = (list.map (λ (a : α), graded_monoid.mk (fι a) (fA a)) l).prod

theorem graded_monoid.list_prod_map_eq_dprod {ι : Type u_1} {α : Type u_2} {A : ι → Type u_3} [add_monoid ι] [graded_monoid.gmonoid A] (l : list α) (f : α → graded_monoid A) :

(list.map f l).prod = graded_monoid.mk (l.dprod_index (λ (i : α), (f i).fst)) (l.dprod (λ (i : α), (f i).fst) (λ (i : α), (f i).snd))

A variant of graded_monoid.mk_list_dprod for rewriting in the other direction.

theorem graded_monoid.list_prod_of_fn_eq_dprod {ι : Type u_1} {A : ι → Type u_3} [add_monoid ι] [graded_monoid.gmonoid A] {n : ℕ} (f : fin n → graded_monoid A) :

(list.of_fn f).prod = graded_monoid.mk ((list.fin_range n).dprod_index (λ (i : fin n), (f i).fst)) ((list.fin_range n).dprod (λ (i : fin n), (f i).fst) (λ (i : fin n), (f i).snd))

Concrete instances #

@[simp]

theorem has_one.ghas_one_one (ι : Type u_1) {R : Type u_2} [has_zero ι] [has_one R] :

graded_monoid.ghas_one.one = 1

@[protected, instance]

def has_one.ghas_one (ι : Type u_1) {R : Type u_2} [has_zero ι] [has_one R] :

graded_monoid.ghas_one (λ (i : ι), R)

Equations

has_one.ghas_one ι = {one := 1}

@[simp]

theorem has_mul.ghas_mul_mul (ι : Type u_1) {R : Type u_2} [has_add ι] [has_mul R] (i j : ι) (ᾰ ᾰ_1 : R) :

graded_monoid.ghas_mul.mul ᾰ ᾰ_1 = ᾰ * ᾰ_1

@[protected, instance]

def has_mul.ghas_mul (ι : Type u_1) {R : Type u_2} [has_add ι] [has_mul R] :

graded_monoid.ghas_mul (λ (i : ι), R)

Equations

has_mul.ghas_mul ι = {mul := λ (i j : ι), has_mul.mul}

@[simp]

theorem monoid.gmonoid_gnpow (ι : Type u_1) {R : Type u_2} [add_monoid ι] [monoid R] (n : ℕ) (i : ι) (a : R) :

graded_monoid.gmonoid.gnpow n a = a ^ n

@[protected, instance]

def monoid.gmonoid (ι : Type u_1) {R : Type u_2} [add_monoid ι] [monoid R] :

graded_monoid.gmonoid (λ (i : ι), R)

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

@[protected, instance]

def comm_monoid.gcomm_monoid (ι : Type u_1) {R : Type u_2} [add_comm_monoid ι] [comm_monoid R] :

graded_monoid.gcomm_monoid (λ (i : ι), R)

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 := _}

@[simp]

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

structure set_like.has_graded_one {ι : Type u_1} {R : Type u_2} {S : Type u_3} [set_like S R] [has_one R] [has_zero ι] (A : ι → S) :

Prop

one_mem : 1 ∈ A 0

A version of graded_monoid.ghas_one for internally graded objects.

Instances of this typeclass

set_like.graded_monoid.to_has_graded_one

theorem set_like.one_mem_graded {ι : Type u_1} {R : Type u_2} {S : Type u_3} [set_like S R] [has_one R] [has_zero ι] (A : ι → S) [set_like.has_graded_one A] :

1 ∈ A 0

@[protected, instance]

def set_like.ghas_one {ι : Type u_1} {R : Type u_2} {S : Type u_3} [set_like S R] [has_one R] [has_zero ι] (A : ι → S) [set_like.has_graded_one A] :

graded_monoid.ghas_one (λ (i : ι), ↥(A i))

Equations

set_like.ghas_one A = {one := ⟨1, _⟩}

@[simp]

theorem set_like.coe_ghas_one {ι : Type u_1} {R : Type u_2} {S : Type u_3} [set_like S R] [has_one R] [has_zero ι] (A : ι → S) [set_like.has_graded_one A] :

↑graded_monoid.ghas_one.one = 1

@[class]

structure set_like.has_graded_mul {ι : Type u_1} {R : Type u_2} {S : Type u_3} [set_like S R] [has_mul R] [has_add ι] (A : ι → S) :

Prop

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

A version of graded_monoid.ghas_one for internally graded objects.

Instances of this typeclass

set_like.graded_monoid.to_has_graded_mul

theorem set_like.mul_mem_graded {ι : Type u_1} {R : Type u_2} {S : Type u_3} [set_like S R] [has_mul R] [has_add ι] {A : ι → S} [set_like.has_graded_mul A] ⦃i j : ι⦄ {gi gj : R} (hi : gi ∈ A i) (hj : gj ∈ A j) :

gi * gj ∈ A (i + j)

@[protected, instance]

def set_like.ghas_mul {ι : Type u_1} {R : Type u_2} {S : Type u_3} [set_like S R] [has_mul R] [has_add ι] (A : ι → S) [set_like.has_graded_mul A] :

graded_monoid.ghas_mul (λ (i : ι), ↥(A i))

Equations

set_like.ghas_mul A = {mul := λ (i j : ι) (a : ↥(A i)) (b : ↥(A j)), ⟨↑a * ↑b, _⟩}

@[simp]

theorem set_like.coe_ghas_mul {ι : Type u_1} {R : Type u_2} {S : Type u_3} [set_like S R] [has_mul R] [has_add ι] (A : ι → S) [set_like.has_graded_mul A] {i j : ι} (x : ↥(A i)) (y : ↥(A j)) :

↑(graded_monoid.ghas_mul.mul x y) = ↑x * ↑y

@[instance]

def set_like.graded_monoid.to_has_graded_mul {ι : Type u_1} {R : Type u_2} {S : Type u_3} [set_like S R] [monoid R] [add_monoid ι] (A : ι → S) [self : set_like.graded_monoid A] :

set_like.has_graded_mul A

@[instance]

def set_like.graded_monoid.to_has_graded_one {ι : Type u_1} {R : Type u_2} {S : Type u_3} [set_like S R] [monoid R] [add_monoid ι] (A : ι → S) [self : set_like.graded_monoid A] :

set_like.has_graded_one A

@[class]

structure set_like.graded_monoid {ι : Type u_1} {R : Type u_2} {S : Type u_3} [set_like S R] [monoid R] [add_monoid ι] (A : ι → S) :

Prop

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

A version of graded_monoid.gmonoid for internally graded objects.

Instances of this typeclass

theorem set_like.pow_mem_graded {ι : Type u_1} {R : Type u_2} {S : Type u_3} [set_like S R] [monoid R] [add_monoid ι] {A : ι → S} [set_like.graded_monoid A] (n : ℕ) {r : R} {i : ι} (h : r ∈ A i) :

r ^ n ∈ A (n • i)

theorem set_like.list_prod_map_mem_graded {ι : Type u_1} {R : Type u_2} {S : Type u_3} [set_like S R] [monoid R] [add_monoid ι] {A : ι → S} [set_like.graded_monoid A] {ι' : Type u_4} (l : list ι') (i : ι' → ι) (r : ι' → R) (h : ∀ (j : ι'), j ∈ l → r j ∈ A (i j)) :

(list.map r l).prod ∈ A (list.map i l).sum

theorem set_like.list_prod_of_fn_mem_graded {ι : Type u_1} {R : Type u_2} {S : Type u_3} [set_like S R] [monoid R] [add_monoid ι] {A : ι → S} [set_like.graded_monoid A] {n : ℕ} (i : fin n → ι) (r : fin n → R) (h : ∀ (j : fin n), r j ∈ A (i j)) :

(list.of_fn r).prod ∈ A (list.of_fn i).sum

@[protected, instance]

def set_like.gmonoid {ι : Type u_1} {R : Type u_2} {S : Type u_3} [set_like S R] [monoid R] [add_monoid ι] (A : ι → S) [set_like.graded_monoid A] :

graded_monoid.gmonoid (λ (i : ι), ↥(A i))

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

@[simp]

theorem set_like.coe_gnpow {ι : Type u_1} {R : Type u_2} {S : Type u_3} [set_like S R] [monoid R] [add_monoid ι] (A : ι → S) [set_like.graded_monoid A] {i : ι} (x : ↥(A i)) (n : ℕ) :

↑(graded_monoid.gmonoid.gnpow n x) = ↑x ^ n

@[protected, instance]

def set_like.gcomm_monoid {ι : Type u_1} {R : Type u_2} {S : Type u_3} [set_like S R] [comm_monoid R] [add_comm_monoid ι] (A : ι → S) [set_like.graded_monoid A] :

graded_monoid.gcomm_monoid (λ (i : ι), ↥(A i))

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 := _}

@[simp]

theorem set_like.coe_list_dprod {ι : Type u_1} {R : Type u_2} {α : Type u_3} {S : Type u_4} [set_like S R] [monoid R] [add_monoid ι] (A : ι → S) [set_like.graded_monoid A] (fι : α → ι) (fA : Π (a : α), ↥(A (fι a))) (l : list α) :

↑(l.dprod fι fA) = (list.map (λ (a : α), ↑(fA a)) l).prod

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

theorem set_like.list_dprod_eq {ι : Type u_1} {R : Type u_2} {α : Type u_3} {S : Type u_4} [set_like S R] [monoid R] [add_monoid ι] (A : ι → S) [set_like.graded_monoid A] (fι : α → ι) (fA : Π (a : α), ↥(A (fι a))) (l : list α) :

l.dprod fι fA = ⟨(list.map (λ (a : α), ↑(fA a)) l).prod, _⟩

A version of list.coe_dprod_set_like with subtype.mk.

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

set_like.is_homogeneous A a = ∃ (i : ι), a ∈ A i

@[simp]

theorem set_like.is_homogeneous_coe {ι : Type u_1} {R : Type u_2} {S : Type u_3} [set_like S R] {A : ι → S} {i : ι} (x : ↥(A i)) :

set_like.is_homogeneous A ↑x

theorem set_like.is_homogeneous_one {ι : Type u_1} {R : Type u_2} {S : Type u_3} [set_like S R] [has_zero ι] [has_one R] (A : ι → S) [set_like.has_graded_one A] :

set_like.is_homogeneous A 1

theorem set_like.is_homogeneous.mul {ι : Type u_1} {R : Type u_2} {S : Type u_3} [set_like S R] [has_add ι] [has_mul R] {A : ι → S} [set_like.has_graded_mul A] {a b : R} :

set_like.is_homogeneous A a → set_like.is_homogeneous A b → set_like.is_homogeneous A (a * b)

def set_like.homogeneous_submonoid {ι : Type u_1} {R : Type u_2} {S : Type u_3} [set_like S R] [add_monoid ι] [monoid R] (A : ι → S) [set_like.graded_monoid A] :

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}, mul_mem' := _, one_mem' := _}