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 CompleteLattice.Independent (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)
.
tags #
internally graded ring
From AddSubmonoid
s and AddSubgroup
s #
Build a DirectSum.GNonUnitalNonAssocSemiring
instance for a collection of additive
submonoids.
Build a DirectSum.GSemiring
instance for a collection of additive submonoids.
Build a DirectSum.GCommSemiring
instance for a collection of additive submonoids.
Build a DirectSum.GRing
instance for a collection of additive subgroups.
Build a DirectSum.GCommRing
instance for a collection of additive submonoids.
The canonical ring isomorphism between ⨁ i, A i
and R
Instances For
The canonical ring isomorphism between ⨁ i, A i
and R
Build a DirectSum.GAlgebra
instance for a collection of Submodule
s.
A direct sum of powers of a submodule of an algebra has a multiplicative structure.
The canonical algebra isomorphism between ⨁ i, A i
and R
.
Instances For
The supremum of submodules that form a graded monoid is a subalgebra, and equal to the range of
DirectSum.coeAlgHom
.