Internally-graded algebras #
This file defines the typeclass graded_algebra π
, for working with an algebra A
that is
internally graded by a collection of submodules π : ΞΉ β submodule R A
.
See the docstring of that typeclass for more information.
Main definitions #
graded_algebra π
: the typeclass, which is a combination ofset_like.graded_monoid
, anddirect_sum.decomposition π
.direct_sum.decompose_alg_equiv π : A ββ[R] β¨ i, π i
, a more bundled version ofdirect_sum.decompose π
.graded_algebra.proj π i
is the linear map fromA
to its degreei : ΞΉ
component, such thatproj π i x = decompose π x i
.
Implementation notes #
For now, we do not have internally-graded semirings and internally-graded rings; these can be
represented with π : ΞΉ β submodule β A
and π : ΞΉ β submodule β€ A
respectively, since all
semiring
s are β-algebras via algebra_nat
, and all ring
s are β€
-algebras via algebra_int
.
Tags #
graded algebra, graded ring, graded semiring, decomposition
- to_graded_monoid : set_like.graded_monoid π
- to_decomposition : direct_sum.decomposition π
An internally-graded R
-algebra A
is one that can be decomposed into a collection
of submodule R A
s indexed by ΞΉ
such that the canonical map A β β¨ i, π i
is bijective and
respects multiplication, i.e. the product of an element of degree i
and an element of degree j
is an element of degree i + j
.
Note that the fact that A
is internally-graded, graded_algebra π
, implies an externally-graded
algebra structure direct_sum.galgebra R (Ξ» i, β₯(π i))
, which in turn makes available an
algebra R (β¨ i, π i)
instance.
Instances of this typeclass
Instances of other typeclasses for graded_algebra
- graded_algebra.has_sizeof_inst
A helper to construct a graded_algebra
when the set_like.graded_monoid
structure is already
available. This makes the left_inv
condition easier to prove, and phrases the right_inv
condition in a way that allows custom @[ext]
lemmas to apply.
See note [reducible non-instances].
Equations
- graded_algebra.of_alg_hom π decompose right_inv left_inv = graded_algebra.mk
If A
is graded by ΞΉ
with degree i
component π i
, then it is isomorphic as
an algebra to a direct sum of components.
The projection maps of graded algebra
Equations
- graded_algebra.proj π i = (π i).subtype.comp ((dfinsupp.lapply i).comp (direct_sum.decompose_alg_equiv π).to_alg_hom.to_linear_map)
If A
is graded by a canonically ordered add monoid, then the projection map x β¦ xβ
is a ring
homomorphism.