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 five typeclasses are:

• DirectSum.GNonUnitalNonAssocSemiring A
• DirectSum.GSemiring A
• DirectSum.GRing A
• DirectSum.GCommSemiring A
• DirectSum.GCommRing A

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

• DirectSum.nonUnitalNonAssocSemiring, DirectSum.nonUnitalNonAssocRing
• DirectSum.semiring
• DirectSum.ring
• DirectSum.commSemiring
• DirectSum.commRing

the base ring A 0 with instances of these types:

• NonUnitalNonAssocSemiring (A 0), NonUnitalNonAssocRing (A 0)
• Semiring (A 0)
• Ring (A 0)
• CommSemiring (A 0)
• CommRing (A 0)

and the ith grade A i with A 0-actions (•) of these types:

• SMulWithZero (A 0) (A i)
• Module (A 0) (A i)
• (nothing)
• (nothing)
• (nothing)

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

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

DirectSum.toSemiring extends DirectSum.toAddMonoid to produce a RingHom.

Direct sums of subobjects

Additionally, this module provides helper functions to construct GSemiring and GCommSemiring instances for:

• A : ι → Submonoid S: DirectSum.GSemiring.ofAddSubmonoids, DirectSum.GCommSemiring.ofAddSubmonoids.
• A : ι → Subgroup S: DirectSum.GSemiring.ofAddSubgroups, DirectSum.GCommSemiring.ofAddSubgroups.
• A : ι → Submodule S: DirectSum.GSemiring.ofSubmodules, DirectSum.GCommSemiring.ofSubmodules.

If sSupIndep A, these provide a gradation of ⨆ i, A i, and the mapping ⨁ i, A i →+ ⨆ i, A i can be obtained as DirectSum.toMonoid (fun i ↦ AddSubmonoid.inclusion <| le_iSup A i).

Implementation details

The instances on A 0 are scoped to the DirectSum namespace, because they have very general discriminantion tree keys.

Tags

graded ring, filtered ring, direct sum, additive submonoid

Typeclasses

class DirectSum.GNonUnitalNonAssocSemiring {ι : Type u_1} (A : ι → Type u_2) [Add ι] [(i : ι) → AddCommMonoid (A i)] extends GradedMonoid.GMul A : Type (max u_1 u_2)

A graded version of NonUnitalNonAssocSemiring.

• mul {i j : ι} : A i → A j → A (i + j)
• mul_zero {i j : ι} (a : A i) : GradedMonoid.GMul.mul a 0 = 0

  Multiplication from the right with any graded component's zero vanishes.

• zero_mul {i j : ι} (b : A j) : GradedMonoid.GMul.mul 0 b = 0

  Multiplication from the left with any graded component's zero vanishes.

• mul_add {i j : ι} (a : A i) (b c : A j) : GradedMonoid.GMul.mul a (b + c) = GradedMonoid.GMul.mul a b + GradedMonoid.GMul.mul a c

  Multiplication from the right between graded components distributes with respect to addition.

• add_mul {i j : ι} (a b : A i) (c : A j) : GradedMonoid.GMul.mul (a + b) c = GradedMonoid.GMul.mul a c + GradedMonoid.GMul.mul b c

  Multiplication from the left between graded components distributes with respect to addition.

class DirectSum.GSemiring {ι : Type u_1} (A : ι → Type u_2) [AddMonoid ι] [(i : ι) → AddCommMonoid (A i)] extends DirectSum.GNonUnitalNonAssocSemiring A, GradedMonoid.GMonoid A : Type (max u_1 u_2)

A graded version of Semiring.

• mul {i j : ι} : A i → A j → A (i + j)
• mul_zero {i j : ι} (a : A i) : GradedMonoid.GMul.mul a 0 = 0
• zero_mul {i j : ι} (b : A j) : GradedMonoid.GMul.mul 0 b = 0
• mul_add {i j : ι} (a : A i) (b c : A j) : GradedMonoid.GMul.mul a (b + c) = GradedMonoid.GMul.mul a b + GradedMonoid.GMul.mul a c
• add_mul {i j : ι} (a b : A i) (c : A j) : GradedMonoid.GMul.mul (a + b) c = GradedMonoid.GMul.mul a c + GradedMonoid.GMul.mul b c
• 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) (DirectSum.GSemiring.gnpow 0 a.snd) = 1
• gnpow_succ' (n : ℕ) (a : GradedMonoid A) : GradedMonoid.mk (n.succ • a.fst) (DirectSum.GSemiring.gnpow n.succ a.snd) = ⟨n • a.fst, DirectSum.GSemiring.gnpow n a.snd⟩ * a
• natCast : ℕ → A 0

  The canonical map from ℕ to the zeroth component of a graded semiring.

• natCast_zero : natCast 0 = 0

  The canonical map from ℕ to a graded semiring respects zero.

• natCast_succ (n : ℕ) : natCast (n + 1) = natCast n + GradedMonoid.GOne.one

  The canonical map from ℕ to a graded semiring respects successors.

class DirectSum.GCommSemiring {ι : Type u_1} (A : ι → Type u_2) [AddCommMonoid ι] [(i : ι) → AddCommMonoid (A i)] extends DirectSum.GSemiring A, GradedMonoid.GCommMonoid A : Type (max u_1 u_2)

A graded version of CommSemiring.

• mul {i j : ι} : A i → A j → A (i + j)
• mul_zero {i j : ι} (a : A i) : GradedMonoid.GMul.mul a 0 = 0
• zero_mul {i j : ι} (b : A j) : GradedMonoid.GMul.mul 0 b = 0
• mul_add {i j : ι} (a : A i) (b c : A j) : GradedMonoid.GMul.mul a (b + c) = GradedMonoid.GMul.mul a b + GradedMonoid.GMul.mul a c
• add_mul {i j : ι} (a b : A i) (c : A j) : GradedMonoid.GMul.mul (a + b) c = GradedMonoid.GMul.mul a c + GradedMonoid.GMul.mul b c
• 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) (DirectSum.GSemiring.gnpow 0 a.snd) = 1
• gnpow_succ' (n : ℕ) (a : GradedMonoid A) : GradedMonoid.mk (n.succ • a.fst) (DirectSum.GSemiring.gnpow n.succ a.snd) = ⟨n • a.fst, DirectSum.GSemiring.gnpow n a.snd⟩ * a
• natCast : ℕ → A 0
• natCast_zero : natCast 0 = 0
• natCast_succ (n : ℕ) : natCast (n + 1) = natCast n + GradedMonoid.GOne.one
• mul_comm (a b : GradedMonoid A) : a * b = b * a

class DirectSum.GRing {ι : Type u_1} (A : ι → Type u_2) [AddMonoid ι] [(i : ι) → AddCommGroup (A i)] extends DirectSum.GSemiring A : Type (max u_1 u_2)

A graded version of Ring.

• mul {i j : ι} : A i → A j → A (i + j)
• mul_zero {i j : ι} (a : A i) : GradedMonoid.GMul.mul a 0 = 0
• zero_mul {i j : ι} (b : A j) : GradedMonoid.GMul.mul 0 b = 0
• mul_add {i j : ι} (a : A i) (b c : A j) : GradedMonoid.GMul.mul a (b + c) = GradedMonoid.GMul.mul a b + GradedMonoid.GMul.mul a c
• add_mul {i j : ι} (a b : A i) (c : A j) : GradedMonoid.GMul.mul (a + b) c = GradedMonoid.GMul.mul a c + GradedMonoid.GMul.mul b c
• 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) (DirectSum.GSemiring.gnpow 0 a.snd) = 1
• gnpow_succ' (n : ℕ) (a : GradedMonoid A) : GradedMonoid.mk (n.succ • a.fst) (DirectSum.GSemiring.gnpow n.succ a.snd) = ⟨n • a.fst, DirectSum.GSemiring.gnpow n a.snd⟩ * a
• natCast : ℕ → A 0
• natCast_zero : natCast 0 = 0
• natCast_succ (n : ℕ) : natCast (n + 1) = natCast n + GradedMonoid.GOne.one
• intCast : ℤ → A 0

  The canonical map from ℤ to the zeroth component of a graded ring.

• intCast_ofNat (n : ℕ) : intCast ↑n = GSemiring.natCast n

  The canonical map from ℤ to a graded ring extends the canonical map from ℕ to the underlying graded semiring.

• intCast_negSucc_ofNat (n : ℕ) : intCast (Int.negSucc n) = -GSemiring.natCast (n + 1)

  On negative integers, the canonical map from ℤ to a graded ring is the negative extension of the canonical map from ℕ to the underlying graded semiring.

class DirectSum.GCommRing {ι : Type u_1} (A : ι → Type u_2) [AddCommMonoid ι] [(i : ι) → AddCommGroup (A i)] extends DirectSum.GRing A, DirectSum.GCommSemiring A : Type (max u_1 u_2)

A graded version of CommRing.

• mul {i j : ι} : A i → A j → A (i + j)
• mul_zero {i j : ι} (a : A i) : GradedMonoid.GMul.mul a 0 = 0
• zero_mul {i j : ι} (b : A j) : GradedMonoid.GMul.mul 0 b = 0
• mul_add {i j : ι} (a : A i) (b c : A j) : GradedMonoid.GMul.mul a (b + c) = GradedMonoid.GMul.mul a b + GradedMonoid.GMul.mul a c
• add_mul {i j : ι} (a b : A i) (c : A j) : GradedMonoid.GMul.mul (a + b) c = GradedMonoid.GMul.mul a c + GradedMonoid.GMul.mul b c
• 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) (DirectSum.GSemiring.gnpow 0 a.snd) = 1
• gnpow_succ' (n : ℕ) (a : GradedMonoid A) : GradedMonoid.mk (n.succ • a.fst) (DirectSum.GSemiring.gnpow n.succ a.snd) = ⟨n • a.fst, DirectSum.GSemiring.gnpow n a.snd⟩ * a
• natCast : ℕ → A 0
• natCast_zero : natCast 0 = 0
• natCast_succ (n : ℕ) : natCast (n + 1) = natCast n + GradedMonoid.GOne.one
• intCast : ℤ → A 0
• intCast_ofNat (n : ℕ) : intCast ↑n = GSemiring.natCast n
• intCast_negSucc_ofNat (n : ℕ) : intCast (Int.negSucc n) = -GSemiring.natCast (n + 1)
• mul_comm (a b : GradedMonoid A) : a * b = b * a

theorem DirectSum.of_eq_of_gradedMonoid_eq {ι : Type u_1} [DecidableEq ι] {A : ι → Type u_2} [(i : ι) → AddCommMonoid (A i)] {i j : ι} {a : A i} {b : A j} (h : GradedMonoid.mk i a = GradedMonoid.mk j b) : (of A i) a = (of A j) b

Instances for ⨁ i, A i

@[instance_reducible]

instance DirectSum.instOne {ι : Type u_1} [DecidableEq ι] (A : ι → Type u_2) [Zero ι] [GradedMonoid.GOne A] [(i : ι) → AddCommMonoid (A i)] : One (DirectSum ι fun (i : ι) => A i)

theorem DirectSum.one_def {ι : Type u_1} [DecidableEq ι] (A : ι → Type u_2) [Zero ι] [GradedMonoid.GOne A] [(i : ι) → AddCommMonoid (A i)] : 1 = (of A 0) GradedMonoid.GOne.one

def DirectSum.gMulHom {ι : Type u_1} (A : ι → Type u_2) [Add ι] [(i : ι) → AddCommMonoid (A i)] [GNonUnitalNonAssocSemiring A] {i j : ι} : A i →+ A j →+ A (i + j)

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

@[simp]

theorem DirectSum.gMulHom_apply_apply {ι : Type u_1} (A : ι → Type u_2) [Add ι] [(i : ι) → AddCommMonoid (A i)] [GNonUnitalNonAssocSemiring A] {i j : ι} (a : A i) (b : A j) : ((gMulHom A) a) b = GradedMonoid.GMul.mul a b

@[reducible]

def DirectSum.mulHom {ι : Type u_1} [DecidableEq ι] (A : ι → Type u_2) [Add ι] [(i : ι) → AddCommMonoid (A i)] [GNonUnitalNonAssocSemiring A] : (DirectSum ι fun (i : ι) => A i) →+ (DirectSum ι fun (i : ι) => A i) →+ DirectSum ι fun (i : ι) => A i

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

@[instance_reducible]

instance DirectSum.instMul {ι : Type u_1} [DecidableEq ι] (A : ι → Type u_2) [Add ι] [(i : ι) → AddCommMonoid (A i)] [GNonUnitalNonAssocSemiring A] : Mul (DirectSum ι fun (i : ι) => A i)

@[instance_reducible]

instance DirectSum.instNonUnitalNonAssocSemiring {ι : Type u_1} [DecidableEq ι] (A : ι → Type u_2) [Add ι] [(i : ι) → AddCommMonoid (A i)] [GNonUnitalNonAssocSemiring A] : NonUnitalNonAssocSemiring (DirectSum ι fun (i : ι) => A i)

theorem DirectSum.mulHom_apply {ι : Type u_1} [DecidableEq ι] {A : ι → Type u_2} [Add ι] [(i : ι) → AddCommMonoid (A i)] [GNonUnitalNonAssocSemiring A] (a b : DirectSum ι fun (i : ι) => A i) : ((mulHom A) a) b = a * b

theorem DirectSum.mulHom_of_of {ι : Type u_1} [DecidableEq ι] {A : ι → Type u_2} [Add ι] [(i : ι) → AddCommMonoid (A i)] [GNonUnitalNonAssocSemiring A] {i j : ι} (a : A i) (b : A j) : ((mulHom A) ((of A i) a)) ((of A j) b) = (of A (i + j)) (GradedMonoid.GMul.mul a b)

theorem DirectSum.of_mul_of {ι : Type u_1} [DecidableEq ι] {A : ι → Type u_2} [Add ι] [(i : ι) → AddCommMonoid (A i)] [GNonUnitalNonAssocSemiring A] {i j : ι} (a : A i) (b : A j) : (of A i) a * (of A j) b = (of A (i + j)) (GradedMonoid.GMul.mul a b)

@[instance_reducible]

instance DirectSum.instNatCast {ι : Type u_1} [DecidableEq ι] (A : ι → Type u_2) [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [GSemiring A] : NatCast (DirectSum ι fun (i : ι) => A i)

@[instance_reducible]

instance DirectSum.semiring {ι : Type u_1} [DecidableEq ι] (A : ι → Type u_2) [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [GSemiring A] : Semiring (DirectSum ι fun (i : ι) => A i)

The Semiring structure derived from GSemiring A.

theorem DirectSum.ofPow {ι : Type u_1} [DecidableEq ι] (A : ι → Type u_2) [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [GSemiring A] {i : ι} (a : A i) (n : ℕ) : (of A i) a ^ n = (of A (n • i)) (GradedMonoid.GMonoid.gnpow n a)

theorem DirectSum.ofList_dProd {ι : Type u_1} [DecidableEq ι] (A : ι → Type u_2) [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [GSemiring A] {α : Type u_3} (l : List α) (fι : α → ι) (fA : (a : α) → A (fι a)) : (of A (l.dProdIndex fι)) (l.dProd fι fA) = (List.map (fun (a : α) => (of A (fι a)) (fA a)) l).prod

theorem DirectSum.list_prod_ofFn_of_eq_dProd {ι : Type u_1} [DecidableEq ι] (A : ι → Type u_2) [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [GSemiring A] (n : ℕ) (fι : Fin n → ι) (fA : (a : Fin n) → A (fι a)) : (List.ofFn fun (a : Fin n) => (of A (fι a)) (fA a)).prod = (of A ((List.finRange n).dProdIndex fι)) ((List.finRange n).dProd fι fA)

theorem DirectSum.mul_eq_dfinsuppSum {ι : Type u_1} [DecidableEq ι] (A : ι → Type u_2) [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [GSemiring A] [(i : ι) → (x : A i) → Decidable (x ≠ 0)] (a a' : DirectSum ι fun (i : ι) => A i) : a * a' = DFinsupp.sum a fun (x : ι) (ai : A x) => DFinsupp.sum a' fun (x_1 : ι) (aj : A x_1) => (of A (x + x_1)) (GradedMonoid.GMul.mul ai aj)

theorem DirectSum.mul_eq_sum_support_ghas_mul {ι : Type u_1} [DecidableEq ι] (A : ι → Type u_2) [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [GSemiring A] [(i : ι) → (x : A i) → Decidable (x ≠ 0)] (a a' : DirectSum ι fun (i : ι) => A i) : a * a' = ∑ ij ∈ DFinsupp.support a ×ˢ DFinsupp.support a', (of A (ij.1 + ij.2)) (GradedMonoid.GMul.mul (a ij.1) (a' ij.2))

A heavily unfolded version of the definition of multiplication

@[instance_reducible]

instance DirectSum.commSemiring {ι : Type u_1} [DecidableEq ι] (A : ι → Type u_2) [(i : ι) → AddCommMonoid (A i)] [AddCommMonoid ι] [GCommSemiring A] : CommSemiring (DirectSum ι fun (i : ι) => A i)

The CommSemiring structure derived from GCommSemiring A.

@[instance_reducible]

instance DirectSum.nonAssocRing {ι : Type u_1} [DecidableEq ι] (A : ι → Type u_2) [(i : ι) → AddCommGroup (A i)] [Add ι] [GNonUnitalNonAssocSemiring A] : NonUnitalNonAssocRing (DirectSum ι fun (i : ι) => A i)

The Ring derived from GSemiring A.

@[instance_reducible]

instance DirectSum.ring {ι : Type u_1} [DecidableEq ι] (A : ι → Type u_2) [(i : ι) → AddCommGroup (A i)] [AddMonoid ι] [GRing A] : Ring (DirectSum ι fun (i : ι) => A i)

The Ring derived from GSemiring A.

@[instance_reducible]

instance DirectSum.commRing {ι : Type u_1} [DecidableEq ι] (A : ι → Type u_2) [(i : ι) → AddCommGroup (A i)] [AddCommMonoid ι] [GCommRing A] : CommRing (DirectSum ι fun (i : ι) => A i)

The CommRing derived from GCommSemiring A.

Instances for A 0

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

Implementation detail: Note that these instances on A 0 have very general discrimination tree keys (e.g. DirectSum.instRingOfNat has discrimination tree key Ring _ and often sends typeclass inference on a wild goose chase with any goal of the form Ring (F X)), so we scope these instances to the DirectSum namespace.

@[simp]

theorem DirectSum.of_zero_one {ι : Type u_1} [DecidableEq ι] (A : ι → Type u_2) [Zero ι] [GradedMonoid.GOne A] [(i : ι) → AddCommMonoid (A i)] : (of A 0) 1 = 1

@[simp]

theorem DirectSum.of_zero_smul {ι : Type u_1} [DecidableEq ι] (A : ι → Type u_2) [AddZeroClass ι] [(i : ι) → AddCommMonoid (A i)] [GNonUnitalNonAssocSemiring A] {i : ι} (a : A 0) (b : A i) : (of A i) (a • b) = (of A 0) a * (of A i) b

@[simp]

theorem DirectSum.of_zero_mul {ι : Type u_1} [DecidableEq ι] (A : ι → Type u_2) [AddZeroClass ι] [(i : ι) → AddCommMonoid (A i)] [GNonUnitalNonAssocSemiring A] (a b : A 0) : (of A 0) (a * b) = (of A 0) a * (of A 0) b

@[instance_reducible]

def DirectSum.instNonUnitalNonAssocSemiringOfNat {ι : Type u_1} [DecidableEq ι] (A : ι → Type u_2) [AddZeroClass ι] [(i : ι) → AddCommMonoid (A i)] [GNonUnitalNonAssocSemiring A] : NonUnitalNonAssocSemiring (A 0)

The NonUnitalNonAssocSemiring structure on the grade zero part of a GNonUnitalNonAssocSemiring.

@[instance_reducible]

def DirectSum.instSMulWithZeroOfNat {ι : Type u_1} [DecidableEq ι] (A : ι → Type u_2) [AddZeroClass ι] [(i : ι) → AddCommMonoid (A i)] [GNonUnitalNonAssocSemiring A] (i : ι) : SMulWithZero (A 0) (A i)

The SMulWithZero structure on the grade zero part of a GNonUnitalNonAssocSemiring.

@[simp]

theorem DirectSum.of_zero_pow {ι : Type u_1} [DecidableEq ι] (A : ι → Type u_2) [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [GSemiring A] (a : A 0) (n : ℕ) : (of A 0) (a ^ n) = (of A 0) a ^ n

@[instance_reducible]

def DirectSum.instNatCastOfNat {ι : Type u_1} (A : ι → Type u_2) [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [GSemiring A] : NatCast (A 0)

The NatCast instance on A 0, given GSemiring A.

@[simp]

theorem DirectSum.of_natCast {ι : Type u_1} [DecidableEq ι] (A : ι → Type u_2) [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [GSemiring A] (n : ℕ) : (of A 0) ↑n = ↑n

@[simp]

theorem DirectSum.of_zero_ofNat {ι : Type u_1} [DecidableEq ι] (A : ι → Type u_2) [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [GSemiring A] (n : ℕ) [n.AtLeastTwo] : (of A 0) (OfNat.ofNat n) = OfNat.ofNat n

@[instance_reducible]

def DirectSum.instSemiringOfNat {ι : Type u_1} [DecidableEq ι] (A : ι → Type u_2) [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [GSemiring A] : Semiring (A 0)

The Semiring structure derived from GSemiring A.

def DirectSum.ofZeroRingHom {ι : Type u_1} [DecidableEq ι] (A : ι → Type u_2) [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [GSemiring A] : A 0 →+* DirectSum ι fun (i : ι) => A i

of A 0 is a RingHom, using the DirectSum.GradeZero.semiring structure.

@[instance_reducible]

def DirectSum.instModuleOfNat {ι : Type u_1} [DecidableEq ι] (A : ι → Type u_2) [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [GSemiring A] {i : ι} : Module (A 0) (A i)

Each grade A i derives an A 0-module structure from GSemiring A. Note that this results in an overall Module (A 0) (⨁ i, A i) structure via DirectSum.module.

@[instance_reducible]

def DirectSum.instCommSemiringOfNat {ι : Type u_1} [DecidableEq ι] (A : ι → Type u_2) [(i : ι) → AddCommMonoid (A i)] [AddCommMonoid ι] [GCommSemiring A] : CommSemiring (A 0)

The CommSemiring structure derived from GCommSemiring A.

@[instance_reducible]

def DirectSum.instNonUnitalNonAssocRingOfNat {ι : Type u_1} [DecidableEq ι] (A : ι → Type u_2) [(i : ι) → AddCommGroup (A i)] [AddZeroClass ι] [GNonUnitalNonAssocSemiring A] : NonUnitalNonAssocRing (A 0)

The NonUnitalNonAssocRing derived from GNonUnitalNonAssocSemiring A.

@[instance_reducible]

def DirectSum.instIntCastOfNat {ι : Type u_1} (A : ι → Type u_2) [(i : ι) → AddCommGroup (A i)] [AddMonoid ι] [GRing A] : IntCast (A 0)

The IntCast instance on A 0, given GRing A.

@[simp]

theorem DirectSum.of_intCast {ι : Type u_1} [DecidableEq ι] (A : ι → Type u_2) [(i : ι) → AddCommGroup (A i)] [AddMonoid ι] [GRing A] (n : ℤ) : (of A 0) ↑n = ↑n

@[instance_reducible]

def DirectSum.instRingOfNat {ι : Type u_1} [DecidableEq ι] (A : ι → Type u_2) [(i : ι) → AddCommGroup (A i)] [AddMonoid ι] [GRing A] : Ring (A 0)

The Ring derived from GSemiring A.

@[instance_reducible]

def DirectSum.instCommRingOfNat {ι : Type u_1} [DecidableEq ι] (A : ι → Type u_2) [(i : ι) → AddCommGroup (A i)] [AddCommMonoid ι] [GCommRing A] : CommRing (A 0)

The CommRing derived from GCommSemiring A.

theorem DirectSum.ringHom_ext' {ι : Type u_1} [DecidableEq ι] {A : ι → Type u_2} {R : Type u_3} [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [GSemiring A] [Semiring R] ⦃F G : (DirectSum ι fun (i : ι) => A i) →+* R⦄ (h : ∀ (i : ι), (↑F).comp (of A i) = (↑G).comp (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 DirectSum.ringHom_ext'_iff {ι : Type u_1} [DecidableEq ι] {A : ι → Type u_2} {R : Type u_3} [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [GSemiring A] [Semiring R] {F G : (DirectSum ι fun (i : ι) => A i) →+* R} : F = G ↔ ∀ (i : ι), (↑F).comp (of A i) = (↑G).comp (of A i)

theorem DirectSum.ringHom_ext {ι : Type u_1} [DecidableEq ι] {A : ι → Type u_2} {R : Type u_3} [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [GSemiring A] [Semiring R] ⦃f g : (DirectSum ι fun (i : ι) => A i) →+* R⦄ (h : ∀ (i : ι) (x : A i), f ((of A i) x) = g ((of A i) x)) : f = g

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

def DirectSum.toSemiring {ι : Type u_1} [DecidableEq ι] {A : ι → Type u_2} {R : Type u_3} [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [GSemiring A] [Semiring R] (f : (i : ι) → A i →+ R) (hone : (f 0) GradedMonoid.GOne.one = 1) (hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj) : (DirectSum ι fun (i : ι) => A i) →+* R

A family of AddMonoidHoms preserving DirectSum.One.one and DirectSum.Mul.mul describes a RingHoms on ⨁ i, A i. This is a stronger version of DirectSum.toMonoid.

Of particular interest is the case when A i are bundled subobjects, f is the family of coercions such as AddSubmonoid.subtype (A i), and the [GSemiring A] structure originates from DirectSum.gsemiring.ofAddSubmonoids, in which case the proofs about GOne and GMul can be discharged by rfl.

@[simp]

theorem DirectSum.toSemiring_apply {ι : Type u_1} [DecidableEq ι] {A : ι → Type u_2} {R : Type u_3} [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [GSemiring A] [Semiring R] (f : (i : ι) → A i →+ R) (hone : (f 0) GradedMonoid.GOne.one = 1) (hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj) (a : DirectSum ι fun (i : ι) => A i) : (toSemiring f hone hmul) a = (toAddMonoid f) a

theorem DirectSum.toSemiring_of {ι : Type u_1} [DecidableEq ι] {A : ι → Type u_2} {R : Type u_3} [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [GSemiring A] [Semiring R] (f : (i : ι) → A i →+ R) (hone : (f 0) GradedMonoid.GOne.one = 1) (hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj) (i : ι) (x : A i) : (toSemiring f hone hmul) ((of A i) x) = (f i) x

@[simp]

theorem DirectSum.toSemiring_toAddMonoidHom {ι : Type u_1} [DecidableEq ι] {A : ι → Type u_2} {R : Type u_3} [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [GSemiring A] [Semiring R] (f : (i : ι) → A i →+ R) (hone : (f 0) GradedMonoid.GOne.one = 1) (hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj) : ↑(toSemiring f hone hmul) = toAddMonoid f

@[deprecated DirectSum.toSemiring_toAddMonoidHom (since := "2026-09-15")]

theorem DirectSum.toSemiring_coe_addMonoidHom {ι : Type u_1} [DecidableEq ι] {A : ι → Type u_2} {R : Type u_3} [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [GSemiring A] [Semiring R] (f : (i : ι) → A i →+ R) (hone : (f 0) GradedMonoid.GOne.one = 1) (hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj) : ↑(toSemiring f hone hmul) = toAddMonoid f

Alias of DirectSum.toSemiring_toAddMonoidHom.

def DirectSum.liftRingHom {ι : Type u_1} [DecidableEq ι] {A : ι → Type u_2} {R : Type u_3} [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [GSemiring A] [Semiring R] : { f : {i : ι} → A i →+ R // f GradedMonoid.GOne.one = 1 ∧ ∀ {i j : ι} (ai : A i) (aj : A j), f (GradedMonoid.GMul.mul ai aj) = f ai * f aj } ≃ ((DirectSum ι fun (i : ι) => A i) →+* R)

Families of AddMonoidHoms preserving DirectSum.One.one and DirectSum.Mul.mul are isomorphic to RingHoms on ⨁ i, A i. This is a stronger version of DFinsupp.liftAddHom.

@[simp]

theorem DirectSum.liftRingHom_symm_apply_coe {ι : Type u_1} [DecidableEq ι] {A : ι → Type u_2} {R : Type u_3} [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [GSemiring A] [Semiring R] (F : (DirectSum ι fun (i : ι) => A i) →+* R) {i : ι} : ↑(liftRingHom.symm F) = (↑F).comp (of A i)

@[simp]

theorem DirectSum.liftRingHom_apply {ι : Type u_1} [DecidableEq ι] {A : ι → Type u_2} {R : Type u_3} [(i : ι) → AddCommMonoid (A i)] [AddMonoid ι] [GSemiring A] [Semiring R] (f : { f : {i : ι} → A i →+ R // f GradedMonoid.GOne.one = 1 ∧ ∀ {i j : ι} (ai : A i) (aj : A j), f (GradedMonoid.GMul.mul ai aj) = f ai * f aj }) : liftRingHom f = toSemiring (fun (x : ι) => ↑f) ⋯ ⋯

Concrete instances

@[instance_reducible]

instance NonUnitalNonAssocSemiring.directSumGNonUnitalNonAssocSemiring (ι : Type u_1) {R : Type u_2} [AddMonoid ι] [NonUnitalNonAssocSemiring R] : DirectSum.GNonUnitalNonAssocSemiring fun (x : ι) => R

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

@[instance_reducible]

instance Semiring.directSumGSemiring (ι : Type u_1) {R : Type u_2} [AddMonoid ι] [Semiring R] : DirectSum.GSemiring fun (x : ι) => R

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

@[instance_reducible]

instance Ring.directSumGRing (ι : Type u_1) {R : Type u_2} [AddMonoid ι] [Ring R] : DirectSum.GRing fun (x : ι) => R

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

@[instance_reducible]

instance CommSemiring.directSumGCommSemiring (ι : Type u_1) {R : Type u_2} [AddCommMonoid ι] [CommSemiring R] : DirectSum.GCommSemiring fun (x : ι) => R

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

@[instance_reducible]

instance CommRing.directSumGCommRing (ι : Type u_1) {R : Type u_2} [AddCommMonoid ι] [CommRing R] : DirectSum.GCommRing fun (x : ι) => R

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