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:
DirectSum.GNonUnitalNonAssocSemiring A
DirectSum.GSemiring A
DirectSum.GRing A
DirectSum.GCommSemiring A
DirectSum.GCommRing A
Respectively, these 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:
DirectSum.GradeZero.nonUnitalNonAssocSemiring
,DirectSum.GradeZero.nonUnitalNonAssocRing
DirectSum.GradeZero.semiring
DirectSum.GradeZero.ring
DirectSum.GradeZero.commSemiring
DirectSum.GradeZero.commRing
and the i
th grade A i
with A 0
-actions (•
) defined as left-multiplication:
DirectSum.GradeZero.smul (A 0)
,DirectSum.GradeZero.smulWithZero (A 0)
DirectSum.GradeZero.module (A 0)
- (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 CompleteLattice.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
DirectSum.toMonoid (fun i ↦ AddSubmonoid.inclusion <| le_iSup A i)
.
Tags #
graded ring, filtered ring, direct sum, add_submonoid
Typeclasses #
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.
Instances
Multiplication from the right with any graded component's zero vanishes.
Multiplication from the left with any graded component's zero vanishes.
Multiplication from the right between graded components distributes with respect to addition.
Multiplication from the left between graded components distributes with respect to addition.
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
Multiplication by
one
on the left is the identity - mul_one : ∀ (a : GradedMonoid A), a * 1 = a
Multiplication by
one
on the right is the identity Multiplication is associative
Optional field to allow definitional control of natural powers
- gnpow_zero' : ∀ (a : GradedMonoid A), GradedMonoid.mk (0 • a.fst) (DirectSum.GSemiring.gnpow 0 a.snd) = 1
The zeroth power will yield 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
Successor powers behave as expected
- natCast : ℕ → A 0
The canonical map from ℕ to the zeroth component of a graded semiring.
- natCast_zero : DirectSum.GSemiring.natCast 0 = 0
The canonical map from ℕ to a graded semiring respects zero.
- natCast_succ : ∀ (n : ℕ), DirectSum.GSemiring.natCast (n + 1) = DirectSum.GSemiring.natCast n + GradedMonoid.GOne.one
The canonical map from ℕ to a graded semiring respects successors.
Instances
The canonical map from ℕ to a graded semiring respects zero.
The canonical map from ℕ to a graded semiring respects successors.
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
- 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 : DirectSum.GSemiring.natCast 0 = 0
- natCast_succ : ∀ (n : ℕ), DirectSum.GSemiring.natCast (n + 1) = DirectSum.GSemiring.natCast n + GradedMonoid.GOne.one
- mul_comm : ∀ (a b : GradedMonoid A), a * b = b * a
Multiplication is commutative
Instances
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
- 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 : DirectSum.GSemiring.natCast 0 = 0
- natCast_succ : ∀ (n : ℕ), DirectSum.GSemiring.natCast (n + 1) = DirectSum.GSemiring.natCast n + GradedMonoid.GOne.one
- intCast : ℤ → A 0
The canonical map from ℤ to the zeroth component of a graded ring.
- intCast_ofNat : ∀ (n : ℕ), DirectSum.GRing.intCast ↑n = DirectSum.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 : ℕ), DirectSum.GRing.intCast (Int.negSucc n) = -DirectSum.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.
Instances
The canonical map from ℤ to a graded ring extends the canonical map from ℕ to the underlying graded semiring.
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.
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
- 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 : DirectSum.GSemiring.natCast 0 = 0
- natCast_succ : ∀ (n : ℕ), DirectSum.GSemiring.natCast (n + 1) = DirectSum.GSemiring.natCast n + GradedMonoid.GOne.one
- intCast : ℤ → A 0
- intCast_ofNat : ∀ (n : ℕ), DirectSum.GRing.intCast ↑n = DirectSum.GSemiring.natCast n
- intCast_negSucc_ofNat : ∀ (n : ℕ), DirectSum.GRing.intCast (Int.negSucc n) = -DirectSum.GSemiring.natCast (n + 1)
- mul_comm : ∀ (a b : GradedMonoid A), a * b = b * a
Multiplication is commutative
Instances
Instances for ⨁ i, A i
#
Equations
- DirectSum.instOne A = { one := (DirectSum.of A 0) GradedMonoid.GOne.one }
The piecewise multiplication from the Mul
instance, as a bundled homomorphism.
Equations
- DirectSum.gMulHom A = { toFun := fun (a : A i) => { toFun := fun (b : A j) => GradedMonoid.GMul.mul a b, map_zero' := ⋯, map_add' := ⋯ }, map_zero' := ⋯, map_add' := ⋯ }
Instances For
The multiplication from the Mul
instance, as a bundled homomorphism.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- DirectSum.instMul A = { mul := fun (a b : DirectSum ι fun (i : ι) => A i) => ((DirectSum.mulHom A) a) b }
Equations
Equations
- DirectSum.instNatCast A = { natCast := fun (n : ℕ) => (DirectSum.of A 0) (DirectSum.GSemiring.natCast n) }
The Semiring
structure derived from GSemiring A
.
Equations
- DirectSum.semiring A = Semiring.mk ⋯ ⋯ ⋯ ⋯ npowRecAuto ⋯ ⋯
A heavily unfolded version of the definition of multiplication
The CommSemiring
structure derived from GCommSemiring A
.
Equations
The Ring
derived from GSemiring A
.
Equations
- DirectSum.nonAssocRing A = NonUnitalNonAssocRing.mk ⋯ ⋯ ⋯ ⋯
The Ring
derived from GSemiring A
.
Equations
- DirectSum.ring A = Ring.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
The CommRing
derived from GCommSemiring A
.
Equations
Instances for A 0
#
The various G*
instances are enough to promote the AddCommMonoid (A 0)
structure to various
types of multiplicative structure.
Equations
Equations
Equations
- DirectSum.instNatCastOfNat A = { natCast := DirectSum.GSemiring.natCast }
The Semiring
structure derived from GSemiring A
.
Equations
- DirectSum.GradeZero.semiring A = Function.Injective.semiring ⇑(DirectSum.of A 0) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
of A 0
is a RingHom
, using the DirectSum.GradeZero.semiring
structure.
Equations
- DirectSum.ofZeroRingHom A = { toFun := (↑(DirectSum.of A 0)).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
Instances For
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
.
Equations
- DirectSum.GradeZero.module A = Function.Injective.module (A 0) (DirectSum.of A i) ⋯ ⋯
The CommSemiring
structure derived from GCommSemiring A
.
Equations
- DirectSum.GradeZero.commSemiring A = Function.Injective.commSemiring ⇑(DirectSum.of A 0) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
The NonUnitalNonAssocRing
derived from GNonUnitalNonAssocSemiring A
.
Equations
- DirectSum.GradeZero.nonUnitalNonAssocRing A = Function.Injective.nonUnitalNonAssocRing ⇑(DirectSum.of A 0) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- DirectSum.instIntCastOfNat A = { intCast := DirectSum.GRing.intCast }
The Ring
derived from GSemiring A
.
Equations
- DirectSum.GradeZero.ring A = Function.Injective.ring ⇑(DirectSum.of A 0) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
The CommRing
derived from GCommSemiring A
.
Equations
- DirectSum.GradeZero.commRing A = Function.Injective.commRing ⇑(DirectSum.of A 0) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
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].
Two RingHom
s out of a direct sum are equal if they agree on the generators.
A family of AddMonoidHom
s preserving DirectSum.One.one
and DirectSum.Mul.mul
describes a RingHom
s on ⨁ i, A i
. This is a stronger version of DirectSum.toMonoid
.
Of particular interest is the case when A i
are bundled subojects, 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
.
Equations
- DirectSum.toSemiring f hone hmul = { toFun := ⇑(DirectSum.toAddMonoid f), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
Instances For
Families of AddMonoidHom
s preserving DirectSum.One.one
and DirectSum.Mul.mul
are isomorphic to RingHom
s on ⨁ i, A i
. This is a stronger version of DFinsupp.liftAddHom
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Concrete instances #
A direct sum of copies of a NonUnitalNonAssocSemiring
inherits the multiplication structure.
A direct sum of copies of a Semiring
inherits the multiplication structure.
Equations
- Semiring.directSumGSemiring ι = DirectSum.GSemiring.mk ⋯ ⋯ ⋯ GradedMonoid.GMonoid.gnpow ⋯ ⋯ (fun (n : ℕ) => ↑n) ⋯ ⋯
A direct sum of copies of a Ring
inherits the multiplication structure.
Equations
- Ring.directSumGRing ι = DirectSum.GRing.mk (fun (z : ℤ) => ↑z) ⋯ ⋯
A direct sum of copies of a CommSemiring
inherits the commutative multiplication structure.
A direct sum of copies of a CommRing
inherits the commutative multiplication structure.