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, and a constructive version ofdirect_sum.submodule_is_internal π.graded_algebra.decompose : A ββ[R] β¨ i, π i, which breaks apart an element of the algebra into its constituent pieces.graded_algebra.proj π iis the linear map fromAto its degreei : ΞΉcomponent, such thatproj π i x = decompose π x i.graded_algebra.support π ris thefinset ΞΉcontaining thei : ΞΉsuch that the degreeicomponent ofris not zero.
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
semirings are β-algebras via algebra_nat, and all rings are β€-algebras via algebra_int.
Tags #
graded algebra, graded ring, graded semiring, decomposition
@[class]
structure
graded_algebra
{ΞΉ : Type u_1}
{R : Type u_2}
{A : Type u_3}
[decidable_eq ΞΉ]
[add_comm_monoid ΞΉ]
[comm_semiring R]
[semiring A]
[algebra R A]
(π : ΞΉ β submodule R A) :
Type (max u_1 u_3)
- to_graded_monoid : set_like.graded_monoid π
- decompose' : A β (β¨ (i : ΞΉ), β₯(π i))
- left_inv : function.left_inverse graded_algebra.decompose' β(direct_sum.submodule_coe π)
- right_inv : function.right_inverse graded_algebra.decompose' β(direct_sum.submodule_coe π)
An internally-graded R-algebra A is one that can be decomposed into a collection
of submodule R As 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.
theorem
graded_algebra.is_internal
{ΞΉ : Type u_1}
{R : Type u_2}
{A : Type u_3}
[decidable_eq ΞΉ]
[add_comm_monoid ΞΉ]
[comm_semiring R]
[semiring A]
[algebra R A]
(π : ΞΉ β submodule R A)
[graded_algebra π] :
def
graded_algebra.of_alg_hom
{ΞΉ : Type u_1}
{R : Type u_2}
{A : Type u_3}
[decidable_eq ΞΉ]
[add_comm_monoid ΞΉ]
[comm_semiring R]
[semiring A]
[algebra R A]
(π : ΞΉ β submodule R A)
[set_like.graded_monoid π]
(decompose : A ββ[R] β¨ (i : ΞΉ), β₯(π i))
(right_inv : (direct_sum.submodule_coe_alg_hom π).comp decompose = alg_hom.id R A)
(left_inv : β (i : ΞΉ) (x : β₯(π i)), βdecompose βx = β(direct_sum.of (Ξ» (i : ΞΉ), β₯(π i)) i) x) :
graded_algebra π
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 = {to_graded_monoid := _inst_6, decompose' := βdecompose, left_inv := _, right_inv := _}
def
graded_algebra.decompose
{ΞΉ : Type u_1}
{R : Type u_2}
{A : Type u_3}
[decidable_eq ΞΉ]
[add_comm_monoid ΞΉ]
[comm_semiring R]
[semiring A]
[algebra R A]
(π : ΞΉ β submodule R A)
[graded_algebra π] :
If A is graded by ΞΉ with degree i component π i, then it is isomorphic as
an algebra to a direct sum of components.
Equations
- graded_algebra.decompose π = {to_fun := β(direct_sum.submodule_coe_alg_hom π), inv_fun := graded_algebra.decompose' _inst_6, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}.symm
@[simp]
theorem
graded_algebra.decompose'_def
{ΞΉ : Type u_1}
{R : Type u_2}
{A : Type u_3}
[decidable_eq ΞΉ]
[add_comm_monoid ΞΉ]
[comm_semiring R]
[semiring A]
[algebra R A]
(π : ΞΉ β submodule R A)
[graded_algebra π] :
@[simp]
theorem
graded_algebra.decompose_symm_of
{ΞΉ : Type u_1}
{R : Type u_2}
{A : Type u_3}
[decidable_eq ΞΉ]
[add_comm_monoid ΞΉ]
[comm_semiring R]
[semiring A]
[algebra R A]
(π : ΞΉ β submodule R A)
[graded_algebra π]
{i : ΞΉ}
(x : β₯(π i)) :
β((graded_algebra.decompose π).symm) (β(direct_sum.of (Ξ» {i : ΞΉ}, β₯(π i)) i) x) = βx
def
graded_algebra.proj
{ΞΉ : Type u_1}
{R : Type u_2}
{A : Type u_3}
[decidable_eq ΞΉ]
[add_comm_monoid ΞΉ]
[comm_semiring R]
[semiring A]
[algebra R A]
(π : ΞΉ β submodule R A)
[graded_algebra π]
(i : ΞΉ) :
The projection maps of graded algebra
Equations
- graded_algebra.proj π i = (π i).subtype.comp ((dfinsupp.lapply i).comp (graded_algebra.decompose π).to_alg_hom.to_linear_map)
@[simp]
theorem
graded_algebra.proj_apply
{ΞΉ : Type u_1}
{R : Type u_2}
{A : Type u_3}
[decidable_eq ΞΉ]
[add_comm_monoid ΞΉ]
[comm_semiring R]
[semiring A]
[algebra R A]
(π : ΞΉ β submodule R A)
[graded_algebra π]
(i : ΞΉ)
(r : A) :
β(graded_algebra.proj π i) r = β(β(β(graded_algebra.decompose π) r) i)
def
graded_algebra.support
{ΞΉ : Type u_1}
{R : Type u_2}
{A : Type u_3}
[decidable_eq ΞΉ]
[add_comm_monoid ΞΉ]
[comm_semiring R]
[semiring A]
[algebra R A]
(π : ΞΉ β submodule R A)
[graded_algebra π]
[Ξ (i : ΞΉ) (x : β₯(π i)), decidable (x β 0)]
(r : A) :
finset ΞΉ
The support of r is the finset where proj R A i r β 0 β i β r.support
Equations
- graded_algebra.support π r = dfinsupp.support (β(graded_algebra.decompose π) r)
theorem
graded_algebra.proj_recompose
{ΞΉ : Type u_1}
{R : Type u_2}
{A : Type u_3}
[decidable_eq ΞΉ]
[add_comm_monoid ΞΉ]
[comm_semiring R]
[semiring A]
[algebra R A]
(π : ΞΉ β submodule R A)
[graded_algebra π]
(a : β¨ (i : ΞΉ), β₯(π i))
(i : ΞΉ) :
β(graded_algebra.proj π i) (β((graded_algebra.decompose π).symm) a) = β((graded_algebra.decompose π).symm) (β(direct_sum.of (Ξ» (i : ΞΉ), β₯(π i)) i) (βa i))
@[simp]
theorem
graded_algebra.decompose_coe
{ΞΉ : Type u_1}
{R : Type u_2}
{A : Type u_3}
[decidable_eq ΞΉ]
[add_comm_monoid ΞΉ]
[comm_semiring R]
[semiring A]
[algebra R A]
(π : ΞΉ β submodule R A)
[graded_algebra π]
{i : ΞΉ}
(x : β₯(π i)) :
β(graded_algebra.decompose π) βx = β(direct_sum.of (Ξ» {i : ΞΉ}, β₯(π i)) i) x
theorem
graded_algebra.decompose_of_mem
{ΞΉ : Type u_1}
{R : Type u_2}
{A : Type u_3}
[decidable_eq ΞΉ]
[add_comm_monoid ΞΉ]
[comm_semiring R]
[semiring A]
[algebra R A]
(π : ΞΉ β submodule R A)
[graded_algebra π]
{x : A}
{i : ΞΉ}
(hx : x β π i) :
β(graded_algebra.decompose π) x = β(direct_sum.of (Ξ» {i : ΞΉ}, {x // x β π i}) i) β¨x, hxβ©
theorem
graded_algebra.decompose_of_mem_same
{ΞΉ : Type u_1}
{R : Type u_2}
{A : Type u_3}
[decidable_eq ΞΉ]
[add_comm_monoid ΞΉ]
[comm_semiring R]
[semiring A]
[algebra R A]
(π : ΞΉ β submodule R A)
[graded_algebra π]
{x : A}
{i : ΞΉ}
(hx : x β π i) :
β(β(β(graded_algebra.decompose π) x) i) = x
theorem
graded_algebra.decompose_of_mem_ne
{ΞΉ : Type u_1}
{R : Type u_2}
{A : Type u_3}
[decidable_eq ΞΉ]
[add_comm_monoid ΞΉ]
[comm_semiring R]
[semiring A]
[algebra R A]
(π : ΞΉ β submodule R A)
[graded_algebra π]
{x : A}
{i j : ΞΉ}
(hx : x β π i)
(hij : i β j) :
β(β(β(graded_algebra.decompose π) x) j) = 0
theorem
graded_algebra.mem_support_iff
{ΞΉ : Type u_1}
{R : Type u_2}
{A : Type u_3}
[decidable_eq ΞΉ]
[add_comm_monoid ΞΉ]
[comm_semiring R]
[semiring A]
[algebra R A]
(π : ΞΉ β submodule R A)
[graded_algebra π]
[Ξ (i : ΞΉ) (x : β₯(π i)), decidable (x β 0)]
(r : A)
(i : ΞΉ) :
i β graded_algebra.support π r β β(graded_algebra.proj π i) r β 0
theorem
graded_algebra.sum_support_decompose
{ΞΉ : Type u_1}
{R : Type u_2}
{A : Type u_3}
[decidable_eq ΞΉ]
[add_comm_monoid ΞΉ]
[comm_semiring R]
[semiring A]
[algebra R A]
(π : ΞΉ β submodule R A)
[graded_algebra π]
[Ξ (i : ΞΉ) (x : β₯(π i)), decidable (x β 0)]
(r : A) :
β (i : ΞΉ) in graded_algebra.support π r, β(β(β(graded_algebra.decompose π) r) i) = r