mathlib3 documentation

algebra.direct_sum.ring

Additively-graded multiplicative structures on `⨁ i, A i` #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This module provides a set of heterogeneous typeclasses for defining a multiplicative structure over ⨁ i, A i such that (*) : A i → A j → A (i + j); that is to say, A forms an additively-graded ring. The typeclasses are:

direct_sum.gnon_unital_non_assoc_semiring A
direct_sum.gsemiring A
direct_sum.gring A
direct_sum.gcomm_semiring A
direct_sum.gcomm_ring A

Respectively, these imbue the external direct sum ⨁ i, A i with:

direct_sum.non_unital_non_assoc_semiring, direct_sum.non_unital_non_assoc_ring
direct_sum.semiring
direct_sum.ring
direct_sum.comm_semiring
direct_sum.comm_ring

the base ring A 0 with:

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

direct_sum.grade_zero.has_smul (A 0), direct_sum.grade_zero.smul_with_zero (A 0)
direct_sum.grade_zero.module (A 0)
(nothing)
(nothing)
(nothing)

Note that in the presence of these instances, ⨁ i, A i itself inherits an A 0-action.

direct_sum.of_zero_ring_hom : A 0 →+* ⨁ i, A i provides direct_sum.of A 0 as a ring homomorphism.

direct_sum.to_semiring extends direct_sum.to_add_monoid to produce a ring_hom.

Direct sums of subobjects #

Additionally, this module provides helper functions to construct gsemiring and gcomm_semiring instances for:

A : ι → submonoid S: direct_sum.gsemiring.of_add_submonoids, direct_sum.gcomm_semiring.of_add_submonoids.
A : ι → subgroup S: direct_sum.gsemiring.of_add_subgroups, direct_sum.gcomm_semiring.of_add_subgroups.
A : ι → submodule S: direct_sum.gsemiring.of_submodules, direct_sum.gcomm_semiring.of_submodules.

If complete_lattice.independent (set.range A), these provide a gradation of ⨆ i, A i, and the mapping ⨁ i, A i →+ ⨆ i, A i can be obtained as direct_sum.to_monoid (λ i, add_submonoid.inclusion $ le_supr A i).

tags #

graded ring, filtered ring, direct sum, add_submonoid

Typeclasses #

@[instance]

def direct_sum.gnon_unital_non_assoc_semiring.to_ghas_mul {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [has_add ι] [Π (i : ι), add_comm_monoid (A i)] [self : direct_sum.gnon_unital_non_assoc_semiring A] :

graded_monoid.ghas_mul A

@[class]

structure direct_sum.gnon_unital_non_assoc_semiring {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [has_add ι] [Π (i : ι), add_comm_monoid (A i)] :

Type (max u_1 u_2)

mul : Π {i j : ι}, A i → A j → A (i + j)
mul_zero : ∀ {i j : ι} (a : A i), direct_sum.gnon_unital_non_assoc_semiring.mul a 0 = 0
zero_mul : ∀ {i j : ι} (b : A j), direct_sum.gnon_unital_non_assoc_semiring.mul 0 b = 0
mul_add : ∀ {i j : ι} (a : A i) (b c : A j), direct_sum.gnon_unital_non_assoc_semiring.mul a (b + c) = direct_sum.gnon_unital_non_assoc_semiring.mul a b + direct_sum.gnon_unital_non_assoc_semiring.mul a c
add_mul : ∀ {i j : ι} (a b : A i) (c : A j), direct_sum.gnon_unital_non_assoc_semiring.mul (a + b) c = direct_sum.gnon_unital_non_assoc_semiring.mul a c + direct_sum.gnon_unital_non_assoc_semiring.mul b c

A graded version of non_unital_non_assoc_semiring.

Instances of this typeclass

Instances of other typeclasses for direct_sum.gnon_unital_non_assoc_semiring

direct_sum.gnon_unital_non_assoc_semiring.has_sizeof_inst

@[class]

structure direct_sum.gsemiring {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [add_monoid ι] [Π (i : ι), add_comm_monoid (A i)] :

Type (max u_1 u_2)

mul : Π {i j : ι}, A i → A j → A (i + j)
mul_zero : ∀ {i j : ι} (a : A i), direct_sum.gsemiring.mul a 0 = 0
zero_mul : ∀ {i j : ι} (b : A j), direct_sum.gsemiring.mul 0 b = 0
mul_add : ∀ {i j : ι} (a : A i) (b c : A j), direct_sum.gsemiring.mul a (b + c) = direct_sum.gsemiring.mul a b + direct_sum.gsemiring.mul a c
add_mul : ∀ {i j : ι} (a b : A i) (c : A j), direct_sum.gsemiring.mul (a + b) c = direct_sum.gsemiring.mul a c + direct_sum.gsemiring.mul b c
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) (direct_sum.gsemiring.gnpow 0 a.snd) = 1) . "apply_gnpow_rec_zero_tac"
gnpow_succ' : (∀ (n : ℕ) (a : graded_monoid A), graded_monoid.mk (n.succ • a.fst) (direct_sum.gsemiring.gnpow n.succ a.snd) = a * ⟨n • a.fst, direct_sum.gsemiring.gnpow n a.snd⟩) . "apply_gnpow_rec_succ_tac"
nat_cast : ℕ → A 0
nat_cast_zero : direct_sum.gsemiring.nat_cast 0 = 0
nat_cast_succ : ∀ (n : ℕ), direct_sum.gsemiring.nat_cast (n + 1) = direct_sum.gsemiring.nat_cast n + graded_monoid.ghas_one.one

A graded version of semiring.

Instances of this typeclass

Instances of other typeclasses for direct_sum.gsemiring

direct_sum.gsemiring.has_sizeof_inst

@[instance]

def direct_sum.gsemiring.to_gnon_unital_non_assoc_semiring {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [add_monoid ι] [Π (i : ι), add_comm_monoid (A i)] [self : direct_sum.gsemiring A] :

direct_sum.gnon_unital_non_assoc_semiring A

@[instance]

def direct_sum.gsemiring.to_gmonoid {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [add_monoid ι] [Π (i : ι), add_comm_monoid (A i)] [self : direct_sum.gsemiring A] :

graded_monoid.gmonoid A

@[instance]

def direct_sum.gcomm_semiring.to_gsemiring {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [add_comm_monoid ι] [Π (i : ι), add_comm_monoid (A i)] [self : direct_sum.gcomm_semiring A] :

direct_sum.gsemiring A

@[instance]

def direct_sum.gcomm_semiring.to_gcomm_monoid {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [add_comm_monoid ι] [Π (i : ι), add_comm_monoid (A i)] [self : direct_sum.gcomm_semiring A] :

graded_monoid.gcomm_monoid A

@[class]

structure direct_sum.gcomm_semiring {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [add_comm_monoid ι] [Π (i : ι), add_comm_monoid (A i)] :

Type (max u_1 u_2)

mul : Π {i j : ι}, A i → A j → A (i + j)
mul_zero : ∀ {i j : ι} (a : A i), direct_sum.gcomm_semiring.mul a 0 = 0
zero_mul : ∀ {i j : ι} (b : A j), direct_sum.gcomm_semiring.mul 0 b = 0
mul_add : ∀ {i j : ι} (a : A i) (b c : A j), direct_sum.gcomm_semiring.mul a (b + c) = direct_sum.gcomm_semiring.mul a b + direct_sum.gcomm_semiring.mul a c
add_mul : ∀ {i j : ι} (a b : A i) (c : A j), direct_sum.gcomm_semiring.mul (a + b) c = direct_sum.gcomm_semiring.mul a c + direct_sum.gcomm_semiring.mul b c
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) (direct_sum.gcomm_semiring.gnpow 0 a.snd) = 1) . "apply_gnpow_rec_zero_tac"
gnpow_succ' : (∀ (n : ℕ) (a : graded_monoid A), graded_monoid.mk (n.succ • a.fst) (direct_sum.gcomm_semiring.gnpow n.succ a.snd) = a * ⟨n • a.fst, direct_sum.gcomm_semiring.gnpow n a.snd⟩) . "apply_gnpow_rec_succ_tac"
nat_cast : ℕ → A 0
nat_cast_zero : direct_sum.gcomm_semiring.nat_cast 0 = 0
nat_cast_succ : ∀ (n : ℕ), direct_sum.gcomm_semiring.nat_cast (n + 1) = direct_sum.gcomm_semiring.nat_cast n + graded_monoid.ghas_one.one
mul_comm : ∀ (a b : graded_monoid A), a * b = b * a

A graded version of comm_semiring.

Instances of this typeclass

Instances of other typeclasses for direct_sum.gcomm_semiring

direct_sum.gcomm_semiring.has_sizeof_inst

@[instance]

def direct_sum.gring.to_gsemiring {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [add_monoid ι] [Π (i : ι), add_comm_group (A i)] [self : direct_sum.gring A] :

direct_sum.gsemiring A

@[class]

structure direct_sum.gring {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [add_monoid ι] [Π (i : ι), add_comm_group (A i)] :

Type (max u_1 u_2)

mul : Π {i j : ι}, A i → A j → A (i + j)
mul_zero : ∀ {i j : ι} (a : A i), direct_sum.gring.mul a 0 = 0
zero_mul : ∀ {i j : ι} (b : A j), direct_sum.gring.mul 0 b = 0
mul_add : ∀ {i j : ι} (a : A i) (b c : A j), direct_sum.gring.mul a (b + c) = direct_sum.gring.mul a b + direct_sum.gring.mul a c
add_mul : ∀ {i j : ι} (a b : A i) (c : A j), direct_sum.gring.mul (a + b) c = direct_sum.gring.mul a c + direct_sum.gring.mul b c
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) (direct_sum.gring.gnpow 0 a.snd) = 1) . "apply_gnpow_rec_zero_tac"
gnpow_succ' : (∀ (n : ℕ) (a : graded_monoid A), graded_monoid.mk (n.succ • a.fst) (direct_sum.gring.gnpow n.succ a.snd) = a * ⟨n • a.fst, direct_sum.gring.gnpow n a.snd⟩) . "apply_gnpow_rec_succ_tac"
nat_cast : ℕ → A 0
nat_cast_zero : direct_sum.gring.nat_cast 0 = 0
nat_cast_succ : ∀ (n : ℕ), direct_sum.gring.nat_cast (n + 1) = direct_sum.gring.nat_cast n + graded_monoid.ghas_one.one
int_cast : ℤ → A 0
int_cast_of_nat : ∀ (n : ℕ), direct_sum.gring.int_cast ↑n = direct_sum.gring.nat_cast n
int_cast_neg_succ_of_nat : ∀ (n : ℕ), direct_sum.gring.int_cast (-↑(n + 1)) = -direct_sum.gring.nat_cast (n + 1)

A graded version of ring.

Instances of this typeclass

Instances of other typeclasses for direct_sum.gring

direct_sum.gring.has_sizeof_inst

@[instance]

def direct_sum.gcomm_ring.to_gring {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [add_comm_monoid ι] [Π (i : ι), add_comm_group (A i)] [self : direct_sum.gcomm_ring A] :

direct_sum.gring A

@[instance]

def direct_sum.gcomm_ring.to_gcomm_semiring {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [add_comm_monoid ι] [Π (i : ι), add_comm_group (A i)] [self : direct_sum.gcomm_ring A] :

direct_sum.gcomm_semiring A

@[class]

structure direct_sum.gcomm_ring {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [add_comm_monoid ι] [Π (i : ι), add_comm_group (A i)] :

Type (max u_1 u_2)

mul : Π {i j : ι}, A i → A j → A (i + j)
mul_zero : ∀ {i j : ι} (a : A i), direct_sum.gcomm_ring.mul a 0 = 0
zero_mul : ∀ {i j : ι} (b : A j), direct_sum.gcomm_ring.mul 0 b = 0
mul_add : ∀ {i j : ι} (a : A i) (b c : A j), direct_sum.gcomm_ring.mul a (b + c) = direct_sum.gcomm_ring.mul a b + direct_sum.gcomm_ring.mul a c
add_mul : ∀ {i j : ι} (a b : A i) (c : A j), direct_sum.gcomm_ring.mul (a + b) c = direct_sum.gcomm_ring.mul a c + direct_sum.gcomm_ring.mul b c
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) (direct_sum.gcomm_ring.gnpow 0 a.snd) = 1) . "apply_gnpow_rec_zero_tac"
gnpow_succ' : (∀ (n : ℕ) (a : graded_monoid A), graded_monoid.mk (n.succ • a.fst) (direct_sum.gcomm_ring.gnpow n.succ a.snd) = a * ⟨n • a.fst, direct_sum.gcomm_ring.gnpow n a.snd⟩) . "apply_gnpow_rec_succ_tac"
nat_cast : ℕ → A 0
nat_cast_zero : direct_sum.gcomm_ring.nat_cast 0 = 0
nat_cast_succ : ∀ (n : ℕ), direct_sum.gcomm_ring.nat_cast (n + 1) = direct_sum.gcomm_ring.nat_cast n + graded_monoid.ghas_one.one
int_cast : ℤ → A 0
int_cast_of_nat : ∀ (n : ℕ), direct_sum.gcomm_ring.int_cast ↑n = direct_sum.gcomm_ring.nat_cast n
int_cast_neg_succ_of_nat : ∀ (n : ℕ), direct_sum.gcomm_ring.int_cast (-↑(n + 1)) = -direct_sum.gcomm_ring.nat_cast (n + 1)
mul_comm : ∀ (a b : graded_monoid A), a * b = b * a

A graded version of comm_ring.

Instances of this typeclass

set_like.gcomm_ring

Instances of other typeclasses for direct_sum.gcomm_ring

direct_sum.gcomm_ring.has_sizeof_inst

theorem direct_sum.of_eq_of_graded_monoid_eq {ι : Type u_1} [decidable_eq ι] {A : ι → Type u_2} [Π (i : ι), add_comm_monoid (A i)] {i j : ι} {a : A i} {b : A j} (h : graded_monoid.mk i a = graded_monoid.mk j b) :

⇑(direct_sum.of A i) a = ⇑(direct_sum.of A j) b

Instances for `⨁ i, A i` #

@[protected, instance]

def direct_sum.has_one {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [has_zero ι] [graded_monoid.ghas_one A] [Π (i : ι), add_comm_monoid (A i)] :

has_one (direct_sum ι (λ (i : ι), A i))

Equations

direct_sum.has_one A = {one := ⇑(direct_sum.of (λ (i : ι), A i) 0) graded_monoid.ghas_one.one}

@[simp]

theorem direct_sum.gmul_hom_apply_apply {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [has_add ι] [Π (i : ι), add_comm_monoid (A i)] [direct_sum.gnon_unital_non_assoc_semiring A] {i j : ι} (a : A i) (b : A j) :

⇑(⇑(direct_sum.gmul_hom A) a) b = graded_monoid.ghas_mul.mul a b

def direct_sum.gmul_hom {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [has_add ι] [Π (i : ι), add_comm_monoid (A i)] [direct_sum.gnon_unital_non_assoc_semiring A] {i j : ι} :

A i →+ A j →+ A (i + j)

The piecewise multiplication from the has_mul instance, as a bundled homomorphism.

Equations

direct_sum.gmul_hom A = {to_fun := λ (a : A i), {to_fun := λ (b : A j), graded_monoid.ghas_mul.mul a b, map_zero' := _, map_add' := _}, map_zero' := _, map_add' := _}

def direct_sum.mul_hom {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [has_add ι] [Π (i : ι), add_comm_monoid (A i)] [direct_sum.gnon_unital_non_assoc_semiring A] :

direct_sum ι (λ (i : ι), A i) →+ direct_sum ι (λ (i : ι), A i) →+ direct_sum ι (λ (i : ι), A i)

The multiplication from the has_mul instance, as a bundled homomorphism.

Equations

direct_sum.mul_hom A = direct_sum.to_add_monoid (λ (i : ι), (direct_sum.to_add_monoid (λ (j : ι), ((⇑add_monoid_hom.comp_hom (direct_sum.of A (i + j))).comp (direct_sum.gmul_hom A)).flip)).flip)

@[protected, instance]

def direct_sum.non_unital_non_assoc_semiring {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [has_add ι] [Π (i : ι), add_comm_monoid (A i)] [direct_sum.gnon_unital_non_assoc_semiring A] :

non_unital_non_assoc_semiring (direct_sum ι (λ (i : ι), A i))

Equations

direct_sum.non_unital_non_assoc_semiring A = {add := has_add.add (add_zero_class.to_has_add (direct_sum ι (λ (i : ι), A i))), add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul (direct_sum.add_comm_monoid ι (λ (i : ι), A i)), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := λ (a b : direct_sum ι (λ (i : ι), A i)), ⇑(⇑(direct_sum.mul_hom A) a) b, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _}

theorem direct_sum.mul_hom_of_of {ι : Type u_1} [decidable_eq ι] {A : ι → Type u_2} [has_add ι] [Π (i : ι), add_comm_monoid (A i)] [direct_sum.gnon_unital_non_assoc_semiring A] {i j : ι} (a : A i) (b : A j) :

⇑(⇑(direct_sum.mul_hom A) (⇑(direct_sum.of (λ {i : ι}, A i) i) a)) (⇑(direct_sum.of (λ {j : ι}, A j) j) b) = ⇑(direct_sum.of (λ {i : ι}, A i) (i + j)) (graded_monoid.ghas_mul.mul a b)

theorem direct_sum.of_mul_of {ι : Type u_1} [decidable_eq ι] {A : ι → Type u_2} [has_add ι] [Π (i : ι), add_comm_monoid (A i)] [direct_sum.gnon_unital_non_assoc_semiring A] {i j : ι} (a : A i) (b : A j) :

⇑(direct_sum.of (λ {i : ι}, A i) i) a * ⇑(direct_sum.of (λ {j : ι}, A j) j) b = ⇑(direct_sum.of (λ {i : ι}, A i) (i + j)) (graded_monoid.ghas_mul.mul a b)

@[protected, instance]

def direct_sum.semiring {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [Π (i : ι), add_comm_monoid (A i)] [add_monoid ι] [direct_sum.gsemiring A] :

semiring (direct_sum ι (λ (i : ι), A i))

The semiring structure derived from gsemiring A.

Equations

direct_sum.semiring A = {add := has_add.add (distrib.to_has_add (direct_sum ι (λ (i : ι), A i))), add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := non_unital_non_assoc_semiring.nsmul (direct_sum.non_unital_non_assoc_semiring (λ (i : ι), A i)), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := has_mul.mul (distrib.to_has_mul (direct_sum ι (λ (i : ι), A i))), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := 1, one_mul := _, mul_one := _, nat_cast := λ (n : ℕ), ⇑(direct_sum.of (λ (i : ι), A i) 0) (direct_sum.gsemiring.nat_cast n), nat_cast_zero := _, nat_cast_succ := _, npow := monoid_with_zero.npow._default 1 has_mul.mul _ _, npow_zero' := _, npow_succ' := _}

theorem direct_sum.of_pow {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [Π (i : ι), add_comm_monoid (A i)] [add_monoid ι] [direct_sum.gsemiring A] {i : ι} (a : A i) (n : ℕ) :

⇑(direct_sum.of (λ {i : ι}, A i) i) a ^ n = ⇑(direct_sum.of (λ {i : ι}, A i) (n • i)) (graded_monoid.gmonoid.gnpow n a)

theorem direct_sum.of_list_dprod {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [Π (i : ι), add_comm_monoid (A i)] [add_monoid ι] [direct_sum.gsemiring A] {α : Type u_3} (l : list α) (fι : α → ι) (fA : Π (a : α), A (fι a)) :

⇑(direct_sum.of A (l.dprod_index fι)) (l.dprod fι fA) = (list.map (λ (a : α), ⇑(direct_sum.of A (fι a)) (fA a)) l).prod

theorem direct_sum.list_prod_of_fn_of_eq_dprod {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [Π (i : ι), add_comm_monoid (A i)] [add_monoid ι] [direct_sum.gsemiring A] (n : ℕ) (fι : fin n → ι) (fA : Π (a : fin n), A (fι a)) :

(list.of_fn (λ (a : fin n), ⇑(direct_sum.of A (fι a)) (fA a))).prod = ⇑(direct_sum.of A ((list.fin_range n).dprod_index fι)) ((list.fin_range n).dprod fι fA)

theorem direct_sum.mul_eq_dfinsupp_sum {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [Π (i : ι), add_comm_monoid (A i)] [add_monoid ι] [direct_sum.gsemiring A] [Π (i : ι) (x : A i), decidable (x ≠ 0)] (a a' : direct_sum ι (λ (i : ι), A i)) :

a * a' = dfinsupp.sum a (λ (i : ι) (ai : (λ (i : ι), A i) i), dfinsupp.sum a' (λ (j : ι) (aj : (λ (i : ι), A i) j), ⇑(direct_sum.of (λ (i : ι), A i) (i + j)) (graded_monoid.ghas_mul.mul ai aj)))

theorem direct_sum.mul_eq_sum_support_ghas_mul {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [Π (i : ι), add_comm_monoid (A i)] [add_monoid ι] [direct_sum.gsemiring A] [Π (i : ι) (x : A i), decidable (x ≠ 0)] (a a' : direct_sum ι (λ (i : ι), A i)) :

a * a' = (dfinsupp.support a ×ˢ dfinsupp.support a').sum (λ (ij : ι × ι), ⇑(direct_sum.of A (ij.fst + ij.snd)) (graded_monoid.ghas_mul.mul (⇑a ij.fst) (⇑a' ij.snd)))

A heavily unfolded version of the definition of multiplication

@[protected, instance]

def direct_sum.comm_semiring {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [Π (i : ι), add_comm_monoid (A i)] [add_comm_monoid ι] [direct_sum.gcomm_semiring A] :

comm_semiring (direct_sum ι (λ (i : ι), A i))

The comm_semiring structure derived from gcomm_semiring A.

Equations

direct_sum.comm_semiring A = {add := has_add.add (distrib.to_has_add (direct_sum ι (λ (i : ι), A i))), add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := semiring.nsmul (direct_sum.semiring (λ (i : ι), A i)), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := has_mul.mul (distrib.to_has_mul (direct_sum ι (λ (i : ι), A i))), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := 1, one_mul := _, mul_one := _, nat_cast := semiring.nat_cast (direct_sum.semiring (λ (i : ι), A i)), nat_cast_zero := _, nat_cast_succ := _, npow := semiring.npow (direct_sum.semiring (λ (i : ι), A i)), npow_zero' := _, npow_succ' := _, mul_comm := _}

@[protected, instance]

def direct_sum.non_assoc_ring {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [Π (i : ι), add_comm_group (A i)] [has_add ι] [direct_sum.gnon_unital_non_assoc_semiring A] :

non_unital_non_assoc_ring (direct_sum ι (λ (i : ι), A i))

The ring derived from gsemiring A.

Equations

direct_sum.non_assoc_ring A = {add := has_add.add (distrib.to_has_add (direct_sum ι (λ (i : ι), A i))), add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := non_unital_non_assoc_semiring.nsmul (direct_sum.non_unital_non_assoc_semiring (λ (i : ι), A i)), nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg (sub_neg_monoid.to_has_neg (direct_sum ι (λ (i : ι), A i))), sub := add_comm_group.sub (direct_sum.add_comm_group (λ (i : ι), A i)), sub_eq_add_neg := _, zsmul := add_comm_group.zsmul (direct_sum.add_comm_group (λ (i : ι), A i)), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := has_mul.mul (distrib.to_has_mul (direct_sum ι (λ (i : ι), A i))), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _}

@[protected, instance]

def direct_sum.ring {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [Π (i : ι), add_comm_group (A i)] [add_monoid ι] [direct_sum.gring A] :

ring (direct_sum ι (λ (i : ι), A i))

The ring derived from gsemiring A.

Equations

direct_sum.ring A = {add := has_add.add (distrib.to_has_add (direct_sum ι (λ (i : ι), A i))), add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := semiring.nsmul (direct_sum.semiring (λ (i : ι), A i)), nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg (sub_neg_monoid.to_has_neg (direct_sum ι (λ (i : ι), A i))), sub := add_comm_group.sub (direct_sum.add_comm_group (λ (i : ι), A i)), sub_eq_add_neg := _, zsmul := add_comm_group.zsmul (direct_sum.add_comm_group (λ (i : ι), A i)), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := λ (z : ℤ), ⇑(direct_sum.of (λ (i : ι), A i) 0) (direct_sum.gring.int_cast z), nat_cast := semiring.nat_cast (direct_sum.semiring (λ (i : ι), A i)), one := 1, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := has_mul.mul (distrib.to_has_mul (direct_sum ι (λ (i : ι), A i))), mul_assoc := _, one_mul := _, mul_one := _, npow := semiring.npow (direct_sum.semiring (λ (i : ι), A i)), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}

@[protected, instance]

def direct_sum.comm_ring {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [Π (i : ι), add_comm_group (A i)] [add_comm_monoid ι] [direct_sum.gcomm_ring A] :

comm_ring (direct_sum ι (λ (i : ι), A i))

The comm_ring derived from gcomm_semiring A.

Equations

direct_sum.comm_ring A = {add := has_add.add (distrib.to_has_add (direct_sum ι (λ (i : ι), A i))), add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := ring.nsmul (direct_sum.ring (λ (i : ι), A i)), nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg (sub_neg_monoid.to_has_neg (direct_sum ι (λ (i : ι), A i))), sub := ring.sub (direct_sum.ring (λ (i : ι), A i)), sub_eq_add_neg := _, zsmul := ring.zsmul (direct_sum.ring (λ (i : ι), A i)), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast (direct_sum.ring (λ (i : ι), A i)), nat_cast := ring.nat_cast (direct_sum.ring (λ (i : ι), A i)), one := 1, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := has_mul.mul (distrib.to_has_mul (direct_sum ι (λ (i : ι), A i))), mul_assoc := _, one_mul := _, mul_one := _, npow := ring.npow (direct_sum.ring (λ (i : ι), A i)), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, 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.

@[simp]

theorem direct_sum.of_zero_one {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [has_zero ι] [graded_monoid.ghas_one A] [Π (i : ι), add_comm_monoid (A i)] :

⇑(direct_sum.of A 0) 1 = 1

@[simp]

theorem direct_sum.of_zero_smul {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [add_zero_class ι] [Π (i : ι), add_comm_monoid (A i)] [direct_sum.gnon_unital_non_assoc_semiring A] {i : ι} (a : A 0) (b : A i) :

⇑(direct_sum.of A i) (a • b) = ⇑(direct_sum.of A 0) a * ⇑(direct_sum.of A i) b

@[simp]

theorem direct_sum.of_zero_mul {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [add_zero_class ι] [Π (i : ι), add_comm_monoid (A i)] [direct_sum.gnon_unital_non_assoc_semiring A] (a b : A 0) :

⇑(direct_sum.of A 0) (a * b) = ⇑(direct_sum.of A 0) a * ⇑(direct_sum.of A 0) b

@[protected, instance]

def direct_sum.grade_zero.non_unital_non_assoc_semiring {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [add_zero_class ι] [Π (i : ι), add_comm_monoid (A i)] [direct_sum.gnon_unital_non_assoc_semiring A] :

non_unital_non_assoc_semiring (A 0)

Equations

direct_sum.grade_zero.non_unital_non_assoc_semiring A = function.injective.non_unital_non_assoc_semiring ⇑(direct_sum.of A 0) _ _ _ _ _

@[protected, instance]

def direct_sum.grade_zero.smul_with_zero {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [add_zero_class ι] [Π (i : ι), add_comm_monoid (A i)] [direct_sum.gnon_unital_non_assoc_semiring A] (i : ι) :

smul_with_zero (A 0) (A i)

Equations

direct_sum.grade_zero.smul_with_zero A i = let _inst : smul_with_zero (A 0) (direct_sum ι (λ (i : ι), A i)) := smul_with_zero.comp_hom (direct_sum ι (λ (i : ι), A i)) (direct_sum.of A 0).to_zero_hom in function.injective.smul_with_zero (direct_sum.of A i).to_zero_hom _ _

@[simp]

theorem direct_sum.of_zero_pow {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [Π (i : ι), add_comm_monoid (A i)] [add_monoid ι] [direct_sum.gsemiring A] (a : A 0) (n : ℕ) :

⇑(direct_sum.of A 0) (a ^ n) = ⇑(direct_sum.of A 0) a ^ n

@[protected, instance]

def direct_sum.has_nat_cast {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [Π (i : ι), add_comm_monoid (A i)] [add_monoid ι] [direct_sum.gsemiring A] :

has_nat_cast (A 0)

Equations

direct_sum.has_nat_cast A = {nat_cast := direct_sum.gsemiring.nat_cast _inst_4}

@[simp]

theorem direct_sum.of_nat_cast {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [Π (i : ι), add_comm_monoid (A i)] [add_monoid ι] [direct_sum.gsemiring A] (n : ℕ) :

⇑(direct_sum.of A 0) ↑n = ↑n

@[protected, instance]

def direct_sum.grade_zero.semiring {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [Π (i : ι), add_comm_monoid (A i)] [add_monoid ι] [direct_sum.gsemiring A] :

The semiring structure derived from gsemiring A.

Equations

direct_sum.grade_zero.semiring A = function.injective.semiring ⇑(direct_sum.of A 0) _ _ _ _ _ _ _ _

def direct_sum.of_zero_ring_hom {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [Π (i : ι), add_comm_monoid (A i)] [add_monoid ι] [direct_sum.gsemiring A] :

A 0 →+* direct_sum ι (λ (i : ι), A i)

of A 0 is a ring_hom, using the direct_sum.grade_zero.semiring structure.

Equations

direct_sum.of_zero_ring_hom A = {to_fun := (direct_sum.of A 0).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

@[protected, instance]

def direct_sum.grade_zero.module {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [Π (i : ι), add_comm_monoid (A i)] [add_monoid ι] [direct_sum.gsemiring A] {i : ι} :

module (A 0) (A i)

Each grade A i derives a A 0-module structure from gsemiring A. Note that this results in an overall module (A 0) (⨁ i, A i) structure via direct_sum.module.

Equations

direct_sum.grade_zero.module A = let _inst : module (A 0) (direct_sum ι (λ (i : ι), A i)) := module.comp_hom (direct_sum ι (λ (i : ι), A i)) (direct_sum.of_zero_ring_hom A) in function.injective.module (A 0) (direct_sum.of A i) _ _

@[protected, instance]

def direct_sum.grade_zero.comm_semiring {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [Π (i : ι), add_comm_monoid (A i)] [add_comm_monoid ι] [direct_sum.gcomm_semiring A] :

comm_semiring (A 0)

The comm_semiring structure derived from gcomm_semiring A.

Equations

direct_sum.grade_zero.comm_semiring A = function.injective.comm_semiring ⇑(direct_sum.of A 0) _ _ _ _ _ _ _ _

@[protected, instance]

def direct_sum.grade_zero.non_unital_non_assoc_ring {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [Π (i : ι), add_comm_group (A i)] [add_zero_class ι] [direct_sum.gnon_unital_non_assoc_semiring A] :

non_unital_non_assoc_ring (A 0)

The non_unital_non_assoc_ring derived from gnon_unital_non_assoc_semiring A.

Equations

direct_sum.grade_zero.non_unital_non_assoc_ring A = function.injective.non_unital_non_assoc_ring ⇑(direct_sum.of A 0) _ _ _ _ _ _ _ _

@[protected, instance]

def direct_sum.has_int_cast {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [Π (i : ι), add_comm_group (A i)] [add_monoid ι] [direct_sum.gring A] :

has_int_cast (A 0)

Equations

direct_sum.has_int_cast A = {int_cast := direct_sum.gring.int_cast _inst_4}

@[simp]

theorem direct_sum.of_int_cast {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [Π (i : ι), add_comm_group (A i)] [add_monoid ι] [direct_sum.gring A] (n : ℤ) :

⇑(direct_sum.of A 0) ↑n = ↑n

@[protected, instance]

def direct_sum.grade_zero.ring {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [Π (i : ι), add_comm_group (A i)] [add_monoid ι] [direct_sum.gring A] :

ring (A 0)

The ring derived from gsemiring A.

Equations

direct_sum.grade_zero.ring A = function.injective.ring ⇑(direct_sum.of A 0) _ _ _ _ _ _ _ _ _ _ _ _

@[protected, instance]

def direct_sum.grade_zero.comm_ring {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [Π (i : ι), add_comm_group (A i)] [add_comm_monoid ι] [direct_sum.gcomm_ring A] :

comm_ring (A 0)

The comm_ring derived from gcomm_semiring A.

Equations

direct_sum.grade_zero.comm_ring A = function.injective.comm_ring ⇑(direct_sum.of A 0) _ _ _ _ _ _ _ _ _ _ _ _

@[ext]

theorem direct_sum.ring_hom_ext' {ι : Type u_1} [decidable_eq ι] {A : ι → Type u_2} {R : Type u_3} [Π (i : ι), add_comm_monoid (A i)] [add_monoid ι] [direct_sum.gsemiring A] [semiring R] ⦃F G : direct_sum ι (λ (i : ι), A i) →+* R⦄ (h : ∀ (i : ι), ↑F.comp (direct_sum.of A i) = ↑G.comp (direct_sum.of A i)) :

F = G

If two ring homomorphisms from ⨁ i, A i are equal on each of A i y, then they are equal.

See note [partially-applied ext lemmas].

theorem direct_sum.ring_hom_ext {ι : Type u_1} [decidable_eq ι] {A : ι → Type u_2} {R : Type u_3} [Π (i : ι), add_comm_monoid (A i)] [add_monoid ι] [direct_sum.gsemiring A] [semiring R] ⦃f g : direct_sum ι (λ (i : ι), A i) →+* R⦄ (h : ∀ (i : ι) (x : A i), ⇑f (⇑(direct_sum.of A i) x) = ⇑g (⇑(direct_sum.of A i) x)) :

f = g

Two ring_homs out of a direct sum are equal if they agree on the generators.

@[simp]

theorem direct_sum.to_semiring_apply {ι : Type u_1} [decidable_eq ι] {A : ι → Type u_2} {R : Type u_3} [Π (i : ι), add_comm_monoid (A i)] [add_monoid ι] [direct_sum.gsemiring A] [semiring R] (f : Π (i : ι), A i →+ R) (hone : ⇑(f 0) graded_monoid.ghas_one.one = 1) (hmul : ∀ {i j : ι} (ai : A i) (aj : A j), ⇑(f (i + j)) (graded_monoid.ghas_mul.mul ai aj) = ⇑(f i) ai * ⇑(f j) aj) (ᾰ : direct_sum ι (λ (i : ι), (λ (i : ι), A i) i)) :

⇑(direct_sum.to_semiring f hone hmul) ᾰ = ⇑(direct_sum.to_add_monoid f) ᾰ

def direct_sum.to_semiring {ι : Type u_1} [decidable_eq ι] {A : ι → Type u_2} {R : Type u_3} [Π (i : ι), add_comm_monoid (A i)] [add_monoid ι] [direct_sum.gsemiring A] [semiring R] (f : Π (i : ι), A i →+ R) (hone : ⇑(f 0) graded_monoid.ghas_one.one = 1) (hmul : ∀ {i j : ι} (ai : A i) (aj : A j), ⇑(f (i + j)) (graded_monoid.ghas_mul.mul ai aj) = ⇑(f i) ai * ⇑(f j) aj) :

direct_sum ι (λ (i : ι), A i) →+* R

A family of add_monoid_homs preserving direct_sum.ghas_one.one and direct_sum.ghas_mul.mul describes a ring_homs on ⨁ i, A i. This is a stronger version of direct_sum.to_monoid.

Of particular interest is the case when A i are bundled subojects, f is the family of coercions such as add_submonoid.subtype (A i), and the [gsemiring A] structure originates from direct_sum.gsemiring.of_add_submonoids, in which case the proofs about ghas_one and ghas_mul can be discharged by rfl.

Equations

direct_sum.to_semiring f hone hmul = {to_fun := ⇑(direct_sum.to_add_monoid f), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

@[simp]

theorem direct_sum.to_semiring_of {ι : Type u_1} [decidable_eq ι] {A : ι → Type u_2} {R : Type u_3} [Π (i : ι), add_comm_monoid (A i)] [add_monoid ι] [direct_sum.gsemiring A] [semiring R] (f : Π (i : ι), A i →+ R) (hone : ⇑(f 0) graded_monoid.ghas_one.one = 1) (hmul : ∀ {i j : ι} (ai : A i) (aj : A j), ⇑(f (i + j)) (graded_monoid.ghas_mul.mul ai aj) = ⇑(f i) ai * ⇑(f j) aj) (i : ι) (x : A i) :

⇑(direct_sum.to_semiring f hone hmul) (⇑(direct_sum.of (λ (i : ι), A i) i) x) = ⇑(f i) x

@[simp]

theorem direct_sum.to_semiring_coe_add_monoid_hom {ι : Type u_1} [decidable_eq ι] {A : ι → Type u_2} {R : Type u_3} [Π (i : ι), add_comm_monoid (A i)] [add_monoid ι] [direct_sum.gsemiring A] [semiring R] (f : Π (i : ι), A i →+ R) (hone : ⇑(f 0) graded_monoid.ghas_one.one = 1) (hmul : ∀ {i j : ι} (ai : A i) (aj : A j), ⇑(f (i + j)) (graded_monoid.ghas_mul.mul ai aj) = ⇑(f i) ai * ⇑(f j) aj) :

↑(direct_sum.to_semiring f hone hmul) = direct_sum.to_add_monoid f

@[simp]

theorem direct_sum.lift_ring_hom_apply {ι : Type u_1} [decidable_eq ι] {A : ι → Type u_2} {R : Type u_3} [Π (i : ι), add_comm_monoid (A i)] [add_monoid ι] [direct_sum.gsemiring A] [semiring R] (f : {f // ⇑f graded_monoid.ghas_one.one = 1 ∧ ∀ {i j : ι} (ai : A i) (aj : A j), ⇑f (graded_monoid.ghas_mul.mul ai aj) = ⇑f ai * ⇑f aj}) :

⇑direct_sum.lift_ring_hom f = direct_sum.to_semiring (λ (_x : ι), f.val) _ _

@[simp]

theorem direct_sum.lift_ring_hom_symm_apply_coe {ι : Type u_1} [decidable_eq ι] {A : ι → Type u_2} {R : Type u_3} [Π (i : ι), add_comm_monoid (A i)] [add_monoid ι] [direct_sum.gsemiring A] [semiring R] (F : direct_sum ι (λ (i : ι), A i) →+* R) (i : ι) :

↑(⇑(direct_sum.lift_ring_hom.symm) F) = ↑F.comp (direct_sum.of A i)

def direct_sum.lift_ring_hom {ι : Type u_1} [decidable_eq ι] {A : ι → Type u_2} {R : Type u_3} [Π (i : ι), add_comm_monoid (A i)] [add_monoid ι] [direct_sum.gsemiring A] [semiring R] :

{f // ⇑f graded_monoid.ghas_one.one = 1 ∧ ∀ {i j : ι} (ai : A i) (aj : A j), ⇑f (graded_monoid.ghas_mul.mul ai aj) = ⇑f ai * ⇑f aj} ≃ (direct_sum ι (λ (i : ι), A i) →+* R)

Families of add_monoid_homs preserving direct_sum.ghas_one.one and direct_sum.ghas_mul.mul are isomorphic to ring_homs on ⨁ i, A i. This is a stronger version of dfinsupp.lift_add_hom.

Equations

direct_sum.lift_ring_hom = {to_fun := λ (f : {f // ⇑f graded_monoid.ghas_one.one = 1 ∧ ∀ {i j : ι} (ai : A i) (aj : A j), ⇑f (graded_monoid.ghas_mul.mul ai aj) = ⇑f ai * ⇑f aj}), direct_sum.to_semiring (λ (_x : ι), f.val) _ _, inv_fun := λ (F : direct_sum ι (λ (i : ι), A i) →+* R), ⟨λ (i : ι), ↑F.comp (direct_sum.of A i), _⟩, left_inv := _, right_inv := _}

Concrete instances #

@[protected, instance]

def non_unital_non_assoc_semiring.direct_sum_gnon_unital_non_assoc_semiring (ι : Type u_1) [decidable_eq ι] {R : Type u_2} [add_monoid ι] [non_unital_non_assoc_semiring R] :

direct_sum.gnon_unital_non_assoc_semiring (λ (i : ι), R)

A direct sum of copies of a semiring inherits the multiplication structure.

Equations

non_unital_non_assoc_semiring.direct_sum_gnon_unital_non_assoc_semiring ι = {mul := graded_monoid.ghas_mul.mul (has_mul.ghas_mul ι), mul_zero := _, zero_mul := _, mul_add := _, add_mul := _}

@[protected, instance]

def semiring.direct_sum_gsemiring (ι : Type u_1) [decidable_eq ι] {R : Type u_2} [add_monoid ι] [semiring R] :

direct_sum.gsemiring (λ (i : ι), R)

A direct sum of copies of a semiring inherits the multiplication structure.

Equations

semiring.direct_sum_gsemiring ι = {mul := direct_sum.gnon_unital_non_assoc_semiring.mul (non_unital_non_assoc_semiring.direct_sum_gnon_unital_non_assoc_semiring ι), mul_zero := _, zero_mul := _, mul_add := _, add_mul := _, one := graded_monoid.gmonoid.one (monoid.gmonoid ι), one_mul := _, mul_one := _, mul_assoc := _, gnpow := graded_monoid.gmonoid.gnpow (monoid.gmonoid ι), gnpow_zero' := _, gnpow_succ' := _, nat_cast := λ (n : ℕ), ↑n, nat_cast_zero := _, nat_cast_succ := _}

@[protected, instance]

def comm_semiring.direct_sum_gcomm_semiring (ι : Type u_1) [decidable_eq ι] {R : Type u_2} [add_comm_monoid ι] [comm_semiring R] :

direct_sum.gcomm_semiring (λ (i : ι), R)

A direct sum of copies of a comm_semiring inherits the commutative multiplication structure.

Equations

comm_semiring.direct_sum_gcomm_semiring ι = {mul := graded_monoid.gcomm_monoid.mul (comm_monoid.gcomm_monoid ι), mul_zero := _, zero_mul := _, mul_add := _, add_mul := _, one := graded_monoid.gcomm_monoid.one (comm_monoid.gcomm_monoid ι), one_mul := _, mul_one := _, mul_assoc := _, gnpow := graded_monoid.gcomm_monoid.gnpow (comm_monoid.gcomm_monoid ι), gnpow_zero' := _, gnpow_succ' := _, nat_cast := direct_sum.gsemiring.nat_cast (semiring.direct_sum_gsemiring ι), nat_cast_zero := _, nat_cast_succ := _, mul_comm := _}