mathlib documentation

algebra.direct_sum_graded

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

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:

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

the base ring A 0 with:

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

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 sums of subobjects #

Additionally, this module provides helper functions to construct gmonoid and gcomm_monoid instances for:

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 #

@[class]
structure direct_sum.ghas_one {ι : Type u_1} [decidable_eq ι] (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
@[class]
structure direct_sum.ghas_mul {ι : 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)

A graded version of has_mul that also subsumes distrib and mul_zero_class by requiring the multiplication be an add_monoid_hom. Multiplication combines grades additively, like add_monoid_algebra.

Instances
def direct_sum.ghas_one.to_sigma_has_one {ι : Type u_1} [decidable_eq ι] {A : ι → Type u_2} [has_zero ι] [direct_sum.ghas_one A] :
has_one (Σ (i : ι), A i)

direct_sum.ghas_one implies a has_one (Σ i, A i), although this is only used as an instance locally to define notation in direct_sum.gmonoid.

Equations
def direct_sum.ghas_mul.to_sigma_has_mul {ι : Type u_1} [decidable_eq ι] {A : ι → Type u_2} [has_add ι] [Π (i : ι), add_comm_monoid (A i)] [direct_sum.ghas_mul A] :
has_mul (Σ (i : ι), A i)

direct_sum.ghas_mul implies a has_mul (Σ i, A i), although this is only used as an instance locally to define notation in direct_sum.gmonoid.

Equations
@[class]
structure direct_sum.gmonoid {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [add_monoid ι] [Π (i : ι), add_comm_monoid (A i)] :
Type (max u_1 u_2)
  • to_ghas_mul : direct_sum.ghas_mul A
  • to_ghas_one : direct_sum.ghas_one A
  • one_mul : ∀ (a : Σ (i : ι), A i), 1 * a = a
  • mul_one : ∀ (a : Σ (i : ι), A i), a * 1 = a
  • mul_assoc : ∀ (a b c_1 : Σ (i : ι), A i), (a * b) * c_1 = a * b * c_1

A graded version of monoid.

Instances
@[class]
structure direct_sum.gcomm_monoid {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [add_comm_monoid ι] [Π (i : ι), add_comm_monoid (A i)] :
Type (max u_1 u_2)

A graded version of comm_monoid.

Instances

Shorthands for creating the above typeclasses #

From add_submonoids #

@[simp]
theorem direct_sum.ghas_one.of_add_submonoids_one {ι : Type u_1} [decidable_eq ι] {R : Type u_2} [semiring R] [has_zero ι] (carriers : ι → add_submonoid R) (one_mem : 1 carriers 0) :
def direct_sum.ghas_one.of_add_submonoids {ι : Type u_1} [decidable_eq ι] {R : Type u_2} [semiring R] [has_zero ι] (carriers : ι → add_submonoid R) (one_mem : 1 carriers 0) :
direct_sum.ghas_one (λ (i : ι), (carriers i))

Build a ghas_one instance for a collection of add_submonoids.

Equations
def direct_sum.ghas_mul.of_add_submonoids {ι : Type u_1} [decidable_eq ι] {R : Type u_2} [semiring R] [has_add ι] (carriers : ι → add_submonoid R) (mul_mem : ∀ ⦃i j : ι⦄ (gi : (carriers i)) (gj : (carriers j)), (gi) * gj carriers (i + j)) :
direct_sum.ghas_mul (λ (i : ι), (carriers i))

Build a ghas_mul instance for a collection of add_submonoids.

Equations
@[simp]
theorem direct_sum.ghas_mul.of_add_submonoids_mul {ι : Type u_1} [decidable_eq ι] {R : Type u_2} [semiring R] [has_add ι] (carriers : ι → add_submonoid R) (mul_mem : ∀ ⦃i j : ι⦄ (gi : (carriers i)) (gj : (carriers j)), (gi) * gj carriers (i + j)) (i j : ι) :
direct_sum.ghas_mul.mul = {to_fun := λ (a : (carriers i)), {to_fun := λ (b : (carriers j)), (a) * b, _⟩, map_zero' := _, map_add' := _}, map_zero' := _, map_add' := _}
def direct_sum.gmonoid.of_add_submonoids {ι : Type u_1} [decidable_eq ι] {R : Type u_2} [semiring R] [add_monoid ι] (carriers : ι → add_submonoid R) (one_mem : 1 carriers 0) (mul_mem : ∀ ⦃i j : ι⦄ (gi : (carriers i)) (gj : (carriers j)), (gi) * gj carriers (i + j)) :
direct_sum.gmonoid (λ (i : ι), (carriers i))

Build a gmonoid instance for a collection of add_submonoids.

Equations
@[simp]
theorem direct_sum.gmonoid.of_add_submonoids_to_ghas_mul {ι : Type u_1} [decidable_eq ι] {R : Type u_2} [semiring R] [add_monoid ι] (carriers : ι → add_submonoid R) (one_mem : 1 carriers 0) (mul_mem : ∀ ⦃i j : ι⦄ (gi : (carriers i)) (gj : (carriers j)), (gi) * gj carriers (i + j)) :
@[simp]
theorem direct_sum.gmonoid.of_add_submonoids_to_ghas_one {ι : Type u_1} [decidable_eq ι] {R : Type u_2} [semiring R] [add_monoid ι] (carriers : ι → add_submonoid R) (one_mem : 1 carriers 0) (mul_mem : ∀ ⦃i j : ι⦄ (gi : (carriers i)) (gj : (carriers j)), (gi) * gj carriers (i + j)) :
@[simp]
theorem direct_sum.gcomm_monoid.of_add_submonoids_to_gmonoid {ι : Type u_1} [decidable_eq ι] {R : Type u_2} [comm_semiring R] [add_comm_monoid ι] (carriers : ι → add_submonoid R) (one_mem : 1 carriers 0) (mul_mem : ∀ ⦃i j : ι⦄ (gi : (carriers i)) (gj : (carriers j)), (gi) * gj carriers (i + j)) :
def direct_sum.gcomm_monoid.of_add_submonoids {ι : Type u_1} [decidable_eq ι] {R : Type u_2} [comm_semiring R] [add_comm_monoid ι] (carriers : ι → add_submonoid R) (one_mem : 1 carriers 0) (mul_mem : ∀ ⦃i j : ι⦄ (gi : (carriers i)) (gj : (carriers j)), (gi) * gj carriers (i + j)) :
direct_sum.gcomm_monoid (λ (i : ι), (carriers i))

Build a gcomm_monoid instance for a collection of add_submonoids.

Equations

From add_subgroups #

@[simp]
theorem direct_sum.ghas_one.of_add_subgroups_one {ι : Type u_1} [decidable_eq ι] {R : Type u_2} [ring R] [has_zero ι] (carriers : ι → add_subgroup R) (one_mem : 1 carriers 0) :
def direct_sum.ghas_one.of_add_subgroups {ι : Type u_1} [decidable_eq ι] {R : Type u_2} [ring R] [has_zero ι] (carriers : ι → add_subgroup R) (one_mem : 1 carriers 0) :
direct_sum.ghas_one (λ (i : ι), (carriers i))

Build a ghas_one instance for a collection of add_subgroups.

Equations
def direct_sum.ghas_mul.of_add_subgroups {ι : Type u_1} [decidable_eq ι] {R : Type u_2} [ring R] [has_add ι] (carriers : ι → add_subgroup R) (mul_mem : ∀ ⦃i j : ι⦄ (gi : (carriers i)) (gj : (carriers j)), (gi) * gj carriers (i + j)) :
direct_sum.ghas_mul (λ (i : ι), (carriers i))

Build a ghas_mul instance for a collection of add_subgroups.

Equations
@[simp]
theorem direct_sum.ghas_mul.of_add_subgroups_mul {ι : Type u_1} [decidable_eq ι] {R : Type u_2} [ring R] [has_add ι] (carriers : ι → add_subgroup R) (mul_mem : ∀ ⦃i j : ι⦄ (gi : (carriers i)) (gj : (carriers j)), (gi) * gj carriers (i + j)) (i j : ι) :
direct_sum.ghas_mul.mul = {to_fun := λ (a : ((carriers i).to_add_submonoid)), {to_fun := λ (b : ((carriers j).to_add_submonoid)), (a) * b, _⟩, map_zero' := _, map_add' := _}, map_zero' := _, map_add' := _}
@[simp]
theorem direct_sum.gmonoid.of_add_subgroups_to_ghas_mul {ι : Type u_1} [decidable_eq ι] {R : Type u_2} [ring R] [add_monoid ι] (carriers : ι → add_subgroup R) (one_mem : 1 carriers 0) (mul_mem : ∀ ⦃i j : ι⦄ (gi : (carriers i)) (gj : (carriers j)), (gi) * gj carriers (i + j)) :
def direct_sum.gmonoid.of_add_subgroups {ι : Type u_1} [decidable_eq ι] {R : Type u_2} [ring R] [add_monoid ι] (carriers : ι → add_subgroup R) (one_mem : 1 carriers 0) (mul_mem : ∀ ⦃i j : ι⦄ (gi : (carriers i)) (gj : (carriers j)), (gi) * gj carriers (i + j)) :
direct_sum.gmonoid (λ (i : ι), (carriers i))

Build a gmonoid instance for a collection of add_subgroups.

Equations
@[simp]
theorem direct_sum.gmonoid.of_add_subgroups_to_ghas_one {ι : Type u_1} [decidable_eq ι] {R : Type u_2} [ring R] [add_monoid ι] (carriers : ι → add_subgroup R) (one_mem : 1 carriers 0) (mul_mem : ∀ ⦃i j : ι⦄ (gi : (carriers i)) (gj : (carriers j)), (gi) * gj carriers (i + j)) :
@[simp]
theorem direct_sum.gcomm_monoid.of_add_subgroups_to_gmonoid {ι : Type u_1} [decidable_eq ι] {R : Type u_2} [comm_ring R] [add_comm_monoid ι] (carriers : ι → add_subgroup R) (one_mem : 1 carriers 0) (mul_mem : ∀ ⦃i j : ι⦄ (gi : (carriers i)) (gj : (carriers j)), (gi) * gj carriers (i + j)) :
def direct_sum.gcomm_monoid.of_add_subgroups {ι : Type u_1} [decidable_eq ι] {R : Type u_2} [comm_ring R] [add_comm_monoid ι] (carriers : ι → add_subgroup R) (one_mem : 1 carriers 0) (mul_mem : ∀ ⦃i j : ι⦄ (gi : (carriers i)) (gj : (carriers j)), (gi) * gj carriers (i + j)) :
direct_sum.gcomm_monoid (λ (i : ι), (carriers i))

Build a gcomm_monoid instance for a collection of add_subgroups.

Equations

From submoduless #

def direct_sum.ghas_one.of_submodules {ι : Type u_1} [decidable_eq ι] {R : Type u_2} {A : Type u_3} [comm_semiring R] [semiring A] [algebra R A] [has_zero ι] (carriers : ι → submodule R A) (one_mem : 1 carriers 0) :
direct_sum.ghas_one (λ (i : ι), (carriers i))

Build a ghas_one instance for a collection of submodules.

Equations
@[simp]
theorem direct_sum.ghas_one.of_submodules_one {ι : Type u_1} [decidable_eq ι] {R : Type u_2} {A : Type u_3} [comm_semiring R] [semiring A] [algebra R A] [has_zero ι] (carriers : ι → submodule R A) (one_mem : 1 carriers 0) :
def direct_sum.ghas_mul.of_submodules {ι : Type u_1} [decidable_eq ι] {R : Type u_2} {A : Type u_3} [comm_semiring R] [semiring A] [algebra R A] [has_add ι] (carriers : ι → submodule R A) (mul_mem : ∀ ⦃i j : ι⦄ (gi : (carriers i)) (gj : (carriers j)), (gi) * gj carriers (i + j)) :
direct_sum.ghas_mul (λ (i : ι), (carriers i))

Build a ghas_mul instance for a collection of submodules.

Equations
@[simp]
theorem direct_sum.ghas_mul.of_submodules_mul {ι : Type u_1} [decidable_eq ι] {R : Type u_2} {A : Type u_3} [comm_semiring R] [semiring A] [algebra R A] [has_add ι] (carriers : ι → submodule R A) (mul_mem : ∀ ⦃i j : ι⦄ (gi : (carriers i)) (gj : (carriers j)), (gi) * gj carriers (i + j)) (i j : ι) :
direct_sum.ghas_mul.mul = {to_fun := λ (a : ((carriers i).to_add_submonoid)), {to_fun := λ (b : ((carriers j).to_add_submonoid)), (a) * b, _⟩, map_zero' := _, map_add' := _}, map_zero' := _, map_add' := _}
@[simp]
theorem direct_sum.gmonoid.of_submodules_to_ghas_one {ι : Type u_1} [decidable_eq ι] {R : Type u_2} {A : Type u_3} [comm_semiring R] [semiring A] [algebra R A] [add_monoid ι] (carriers : ι → submodule R A) (one_mem : 1 carriers 0) (mul_mem : ∀ ⦃i j : ι⦄ (gi : (carriers i)) (gj : (carriers j)), (gi) * gj carriers (i + j)) :
@[simp]
theorem direct_sum.gmonoid.of_submodules_to_ghas_mul {ι : Type u_1} [decidable_eq ι] {R : Type u_2} {A : Type u_3} [comm_semiring R] [semiring A] [algebra R A] [add_monoid ι] (carriers : ι → submodule R A) (one_mem : 1 carriers 0) (mul_mem : ∀ ⦃i j : ι⦄ (gi : (carriers i)) (gj : (carriers j)), (gi) * gj carriers (i + j)) :
def direct_sum.gmonoid.of_submodules {ι : Type u_1} [decidable_eq ι] {R : Type u_2} {A : Type u_3} [comm_semiring R] [semiring A] [algebra R A] [add_monoid ι] (carriers : ι → submodule R A) (one_mem : 1 carriers 0) (mul_mem : ∀ ⦃i j : ι⦄ (gi : (carriers i)) (gj : (carriers j)), (gi) * gj carriers (i + j)) :
direct_sum.gmonoid (λ (i : ι), (carriers i))

Build a gmonoid instance for a collection of submoduless.

Equations
def direct_sum.gcomm_monoid.of_submodules {ι : Type u_1} [decidable_eq ι] {R : Type u_2} {A : Type u_3} [comm_semiring R] [comm_semiring A] [algebra R A] [add_comm_monoid ι] (carriers : ι → submodule R A) (one_mem : 1 carriers 0) (mul_mem : ∀ ⦃i j : ι⦄ (gi : (carriers i)) (gj : (carriers j)), (gi) * gj carriers (i + j)) :
direct_sum.gcomm_monoid (λ (i : ι), (carriers i))

Build a gcomm_monoid instance for a collection of submoduless.

Equations
@[simp]
theorem direct_sum.gcomm_monoid.of_submodules_to_gmonoid {ι : Type u_1} [decidable_eq ι] {R : Type u_2} {A : Type u_3} [comm_semiring R] [comm_semiring A] [algebra R A] [add_comm_monoid ι] (carriers : ι → submodule R A) (one_mem : 1 carriers 0) (mul_mem : ∀ ⦃i j : ι⦄ (gi : (carriers i)) (gj : (carriers j)), (gi) * gj carriers (i + j)) :

Instances for ⨁ i, A i #

@[instance]
def direct_sum.has_one {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [has_zero ι] [direct_sum.ghas_one A] [Π (i : ι), add_comm_monoid (A i)] :
has_one (⨁ (i : ι), A i)
Equations
def direct_sum.mul_hom {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [has_add ι] [Π (i : ι), add_comm_monoid (A i)] [direct_sum.ghas_mul A] :
(⨁ (i : ι), A i) →+ (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i

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

Equations
@[instance]
def direct_sum.has_mul {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [has_add ι] [Π (i : ι), add_comm_monoid (A i)] [direct_sum.ghas_mul A] :
has_mul (⨁ (i : ι), A i)
Equations
@[instance]
def direct_sum.mul_zero_class {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [has_add ι] [Π (i : ι), add_comm_monoid (A i)] [direct_sum.ghas_mul A] :
mul_zero_class (⨁ (i : ι), A i)
Equations
@[instance]
def direct_sum.distrib {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [has_add ι] [Π (i : ι), add_comm_monoid (A i)] [direct_sum.ghas_mul A] :
distrib (⨁ (i : ι), A i)
Equations
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.ghas_mul 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 A (i + j)) ((direct_sum.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.ghas_mul 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 A (i + j)) ((direct_sum.ghas_mul.mul a) b)
@[instance]
def direct_sum.semiring {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [Π (i : ι), add_comm_monoid (A i)] [add_monoid ι] [direct_sum.gmonoid A] :
semiring (⨁ (i : ι), A i)

The semiring structure derived from gmonoid A.

Equations
@[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_monoid A] :
comm_semiring (⨁ (i : ι), A i)

The comm_semiring structure derived from gcomm_monoid A.

Equations
@[instance]
def direct_sum.ring {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [Π (i : ι), add_comm_group (A i)] [add_comm_monoid ι] [direct_sum.gmonoid A] :
ring (⨁ (i : ι), A i)

The ring derived from gmonoid A.

Equations
@[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_monoid A] :
comm_ring (⨁ (i : ι), A i)

The comm_ring derived from gcomm_monoid A.

Equations

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.

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

1 : A 0 is the value provided in direct_sum.ghas_one.one.

Equations
@[simp]
theorem direct_sum.of_zero_one {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [has_zero ι] [direct_sum.ghas_one A] [Π (i : ι), add_comm_monoid (A i)] :
@[instance]
def direct_sum.grade_zero.has_scalar {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [add_monoid ι] [Π (i : ι), add_comm_monoid (A i)] [direct_sum.ghas_mul A] (i : ι) :
has_scalar (A 0) (A i)

(•) : A 0 → A i → A i is the value provided in direct_sum.ghas_mul.mul, composed with an eq.rec to turn A (0 + i) into A i.

Equations
@[instance]
def direct_sum.grade_zero.has_mul {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [add_monoid ι] [Π (i : ι), add_comm_monoid (A i)] [direct_sum.ghas_mul A] :
has_mul (A 0)

(*) : A 0 → A 0 → A 0 is the value provided in direct_sum.ghas_mul.mul, composed with an eq.rec to turn A (0 + 0) into A 0.

Equations
@[simp]
theorem direct_sum.grade_zero.smul_eq_mul {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [add_monoid ι] [Π (i : ι), add_comm_monoid (A i)] [direct_sum.ghas_mul A] (a b : A 0) :
a b = a * b
@[simp]
theorem direct_sum.of_zero_smul {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [add_monoid ι] [Π (i : ι), add_comm_monoid (A i)] [direct_sum.ghas_mul A] {i : ι} (a : A 0) (b : A i) :
@[simp]
theorem direct_sum.of_zero_mul {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [add_monoid ι] [Π (i : ι), add_comm_monoid (A i)] [direct_sum.ghas_mul A] (a b : A 0) :
(direct_sum.of A 0) (a * b) = ((direct_sum.of A 0) a) * (direct_sum.of A 0) b
@[instance]
def direct_sum.grade_zero.mul_zero_class {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [add_monoid ι] [Π (i : ι), add_comm_monoid (A i)] [direct_sum.ghas_mul A] :
Equations
@[instance]
def direct_sum.grade_zero.distrib {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [add_monoid ι] [Π (i : ι), add_comm_monoid (A i)] [direct_sum.ghas_mul A] :
distrib (A 0)
Equations
@[instance]
def direct_sum.grade_zero.smul_with_zero {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [add_monoid ι] [Π (i : ι), add_comm_monoid (A i)] [direct_sum.ghas_mul A] (i : ι) :
smul_with_zero (A 0) (A i)
Equations
@[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.gmonoid A] :
semiring (A 0)

The semiring structure derived from gmonoid A.

Equations
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.gmonoid A] :
A 0 →+* ⨁ (i : ι), A i

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

Equations
@[instance]
def direct_sum.grade_zero.semimodule {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [Π (i : ι), add_comm_monoid (A i)] [add_monoid ι] [direct_sum.gmonoid A] {i : ι} :
semimodule (A 0) (A i)

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

Equations
@[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_monoid A] :

The comm_semiring structure derived from gcomm_monoid A.

Equations
@[instance]
def direct_sum.grade_zero.ring {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [Π (i : ι), add_comm_group (A i)] [add_comm_monoid ι] [direct_sum.gmonoid A] :
ring (A 0)

The ring derived from gmonoid A.

Equations
@[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_monoid A] :
comm_ring (A 0)

The comm_ring derived from gcomm_monoid A.

Equations

Concrete instances #

@[instance]
def submodule.nat_power_direct_sum_gmonoid {R : Type u_2} {A : Type u_3} [comm_semiring R] [semiring A] [algebra R A] (S : submodule R A) :
direct_sum.gmonoid (λ (i : ), (S ^ i))

A direct sum of powers of a submodule of an algebra has a multiplicative structure.

Equations
@[instance]
def submodule.nat_power_direct_sum_gcomm_monoid {R : Type u_2} {A : Type u_3} [comm_semiring R] [comm_semiring A] [algebra R A] (S : submodule R A) :
direct_sum.gcomm_monoid (λ (i : ), (S ^ i))

A direct sum of powers of a submodule of a commutative algebra has a commutative multiplicative structure.

Equations