Internally graded rings and algebras #
This module provides DirectSum.GSemiring
and DirectSum.GCommSemiring
instances for a collection
of subobjects A
when a SetLike.GradedMonoid
instance is available:
With these instances in place, it provides the bundled canonical maps out of a direct sum of subobjects into their carrier type:
DirectSum.coeRingHom
(aRingHom
version ofDirectSum.coeAddMonoidHom
)DirectSum.coeAlgHom
(anAlgHom
version ofDirectSum.coeLinearMap
)
Strictly the definitions in this file are not sufficient to fully define an "internal" direct sum;
to represent this case, (h : DirectSum.IsInternal A) [SetLike.GradedMonoid A]
is
needed. In the future there will likely be a data-carrying, constructive, typeclass version of
DirectSum.IsInternal
for providing an explicit decomposition function.
When iSupIndep (Set.range A)
(a weaker condition than
DirectSum.IsInternal A
), these provide a grading of ⨆ i, A i
, and the
mapping ⨁ i, A i →+ ⨆ i, A i
can be obtained as
DirectSum.toAddMonoid (fun i ↦ AddSubmonoid.inclusion <| le_iSup A i)
.
This file also provides some extra structure on A 0
, namely:
SetLike.GradeZero.subsemiring
, which leads toSetLike.GradeZero.subring
, which leads toSetLike.GradeZero.subalgebra
, which leads to
Tags #
internally graded ring
Alias of SetLike.natCast_mem_graded
.
Alias of SetLike.intCast_mem_graded
.
From AddSubmonoid
s and AddSubgroup
s #
Build a DirectSum.GNonUnitalNonAssocSemiring
instance for a collection of additive
submonoids.
Equations
Build a DirectSum.GSemiring
instance for a collection of additive submonoids.
Equations
- SetLike.gsemiring A = DirectSum.GSemiring.mk ⋯ ⋯ ⋯ GradedMonoid.GMonoid.gnpow ⋯ ⋯ (fun (n : ℕ) => ⟨↑n, ⋯⟩) ⋯ ⋯
Build a DirectSum.GCommSemiring
instance for a collection of additive submonoids.
Equations
Build a DirectSum.GRing
instance for a collection of additive subgroups.
Equations
- SetLike.gring A = DirectSum.GRing.mk (fun (z : ℤ) => ⟨↑z, ⋯⟩) ⋯ ⋯
Build a DirectSum.GCommRing
instance for a collection of additive submonoids.
Equations
The canonical ring isomorphism between ⨁ i, A i
and R
Equations
- DirectSum.coeRingHom A = DirectSum.toSemiring (fun (i : ι) => AddSubmonoidClass.subtype (A i)) ⋯ ⋯
Instances For
The canonical ring isomorphism between ⨁ i, A i
and R
Build a DirectSum.GAlgebra
instance for a collection of Submodule
s.
Equations
- Submodule.galgebra A = { toFun := (LinearMap.codRestrict (A 0) (Algebra.linearMap S R) ⋯).toAddMonoidHom, map_one := ⋯, map_mul := ⋯, commutes := ⋯, smul_def := ⋯ }
A direct sum of powers of a submodule of an algebra has a multiplicative structure.
Equations
- ⋯ = ⋯
The canonical algebra isomorphism between ⨁ i, A i
and R
.
Equations
- DirectSum.coeAlgHom A = DirectSum.toAlgebra S (fun (i : ι) => ↥(A i)) (fun (i : ι) => (A i).subtype) ⋯ ⋯
Instances For
The supremum of submodules that form a graded monoid is a subalgebra, and equal to the range of
DirectSum.coeAlgHom
.
Facts about grade zero #
The subsemiring A 0
of R
.
Equations
- SetLike.GradeZero.subsemiring A = { carrier := ↑(A 0), mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯ }
Instances For
The semiring A 0
inherited from R
in the presence of SetLike.GradedMonoid A
.
Equations
- SetLike.GradeZero.instSemiring A = (SetLike.GradeZero.subsemiring A).toSemiring
The commutative semiring A 0
inherited from R
in the presence of SetLike.GradedMonoid A
.
Equations
- SetLike.GradeZero.instCommSemiring A = (SetLike.GradeZero.subsemiring A).toCommSemiring
The subring A 0
of R
.
Equations
- SetLike.GradeZero.subring A = { carrier := ↑(A 0), mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
Instances For
The ring A 0
inherited from R
in the presence of SetLike.GradedMonoid A
.
Equations
- SetLike.GradeZero.instRing A = (SetLike.GradeZero.subring A).toRing
The commutative ring A 0
inherited from R
in the presence of SetLike.GradedMonoid A
.
Equations
- SetLike.GradeZero.instCommRing A = (SetLike.GradeZero.subring A).toCommRing
The subalgebra A 0
of R
.
Equations
- SetLike.GradeZero.subalgebra A = { carrier := ↑(A 0), mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯ }
Instances For
The S
-algebra A 0
inherited from R
in the presence of SetLike.GradedMonoid A
.