mathlib documentation

ring_theory.graded_algebra.basic

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 #

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

source
@[class]
structure graded_algebra {ΞΉ : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ΞΉ] [add_monoid ΞΉ] [comm_semiring R] [semiring A] [algebra R A] (π’œ : ΞΉ β†’ submodule R A) :
Type (max u_1 u_3)

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.

Instances of this typeclass
Instances of other typeclasses for graded_algebra
  • graded_algebra.has_sizeof_inst
source
@[protected]
theorem graded_algebra.is_internal {ΞΉ : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ΞΉ] [add_monoid ΞΉ] [comm_semiring R] [semiring A] [algebra R A] (π’œ : ΞΉ β†’ submodule R A) [graded_algebra π’œ] :
direct_sum.is_internal π’œ
source
def graded_algebra.of_alg_hom {ΞΉ : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ΞΉ] [add_monoid ΞΉ] [comm_semiring R] [semiring A] [algebra R A] (π’œ : ΞΉ β†’ submodule R A) [set_like.graded_monoid π’œ] (decompose : A →ₐ[R] direct_sum ΞΉ (Ξ» (i : ΞΉ), β†₯(π’œ i))) (right_inv : (direct_sum.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
source
@[simp]
theorem direct_sum.decompose_alg_equiv_apply {ΞΉ : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ΞΉ] [add_monoid ΞΉ] [comm_semiring R] [semiring A] [algebra R A] (π’œ : ΞΉ β†’ submodule R A) [graded_algebra π’œ] (αΎ° : A) :
⇑(direct_sum.decompose_alg_equiv π’œ) αΎ° = ⇑(↑{to_fun := ⇑((direct_sum.decompose π’œ).symm), inv_fun := ⇑(direct_sum.decompose π’œ), left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}.symm) αΎ°
source
@[simp]
theorem direct_sum.decompose_alg_equiv_symm_apply {ΞΉ : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ΞΉ] [add_monoid ΞΉ] [comm_semiring R] [semiring A] [algebra R A] (π’œ : ΞΉ β†’ submodule R A) [graded_algebra π’œ] (αΎ° : direct_sum ΞΉ (Ξ» (i : ΞΉ), β†₯(π’œ i))) :
⇑((direct_sum.decompose_alg_equiv π’œ).symm) αΎ° = ⇑((direct_sum.decompose π’œ).symm) αΎ°
source
def direct_sum.decompose_alg_equiv {ΞΉ : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ΞΉ] [add_monoid ΞΉ] [comm_semiring R] [semiring A] [algebra R A] (π’œ : ΞΉ β†’ submodule R A) [graded_algebra π’œ] :
A ≃ₐ[R] direct_sum ΞΉ (Ξ» (i : ΞΉ), β†₯(π’œ i))

If A is graded by ΞΉ with degree i component π’œ i, then it is isomorphic as an algebra to a direct sum of components.

Equations
source
@[simp]
theorem direct_sum.decompose_one {ΞΉ : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ΞΉ] [add_monoid ΞΉ] [comm_semiring R] [semiring A] [algebra R A] (π’œ : ΞΉ β†’ submodule R A) [graded_algebra π’œ] :
⇑(direct_sum.decompose π’œ) 1 = 1
source
@[simp]
theorem direct_sum.decompose_symm_one {ΞΉ : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ΞΉ] [add_monoid ΞΉ] [comm_semiring R] [semiring A] [algebra R A] (π’œ : ΞΉ β†’ submodule R A) [graded_algebra π’œ] :
⇑((direct_sum.decompose π’œ).symm) 1 = 1
source
@[simp]
theorem direct_sum.decompose_mul {ΞΉ : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ΞΉ] [add_monoid ΞΉ] [comm_semiring R] [semiring A] [algebra R A] (π’œ : ΞΉ β†’ submodule R A) [graded_algebra π’œ] (x y : A) :
⇑(direct_sum.decompose π’œ) (x * y) = ⇑(direct_sum.decompose π’œ) x * ⇑(direct_sum.decompose π’œ) y
source
@[simp]
theorem direct_sum.decompose_symm_mul {ΞΉ : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ΞΉ] [add_monoid ΞΉ] [comm_semiring R] [semiring A] [algebra R A] (π’œ : ΞΉ β†’ submodule R A) [graded_algebra π’œ] (x y : direct_sum ΞΉ (Ξ» (i : ΞΉ), β†₯(π’œ i))) :
⇑((direct_sum.decompose π’œ).symm) (x * y) = ⇑((direct_sum.decompose π’œ).symm) x * ⇑((direct_sum.decompose π’œ).symm) y
source
def graded_algebra.proj {ΞΉ : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ΞΉ] [add_monoid ΞΉ] [comm_semiring R] [semiring A] [algebra R A] (π’œ : ΞΉ β†’ submodule R A) [graded_algebra π’œ] (i : ΞΉ) :
A β†’β‚—[R] A

The projection maps of graded algebra

Equations
source
@[simp]
theorem graded_algebra.proj_apply {ΞΉ : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ΞΉ] [add_monoid ΞΉ] [comm_semiring R] [semiring A] [algebra R A] (π’œ : ΞΉ β†’ submodule R A) [graded_algebra π’œ] (i : ΞΉ) (r : A) :
⇑(graded_algebra.proj π’œ i) r = ↑(⇑(⇑(direct_sum.decompose π’œ) r) i)
source
theorem graded_algebra.proj_recompose {ΞΉ : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ΞΉ] [add_monoid ΞΉ] [comm_semiring R] [semiring A] [algebra R A] (π’œ : ΞΉ β†’ submodule R A) [graded_algebra π’œ] (a : direct_sum ΞΉ (Ξ» (i : ΞΉ), β†₯(π’œ i))) (i : ΞΉ) :
⇑(graded_algebra.proj π’œ i) (⇑((direct_sum.decompose π’œ).symm) a) = ⇑((direct_sum.decompose π’œ).symm) (⇑(direct_sum.of (Ξ» (i : ΞΉ), β†₯(π’œ i)) i) (⇑a i))
source
theorem graded_algebra.mem_support_iff {ΞΉ : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ΞΉ] [add_monoid ΞΉ] [comm_semiring R] [semiring A] [algebra R A] (π’œ : ΞΉ β†’ submodule R A) [graded_algebra π’œ] [decidable_eq A] (r : A) (i : ΞΉ) :
i ∈ dfinsupp.support (⇑(direct_sum.decompose π’œ) r) ↔ ⇑(graded_algebra.proj π’œ i) r β‰  0
source
@[simp]
theorem graded_algebra.proj_zero_ring_hom_apply {ΞΉ : Type u_1} {R : Type u_2} {A : Type u_3} [comm_semiring R] [semiring A] [algebra R A] [decidable_eq ΞΉ] [canonically_ordered_add_monoid ΞΉ] (π’œ : ΞΉ β†’ submodule R A) [graded_algebra π’œ] (a : A) :
⇑(graded_algebra.proj_zero_ring_hom π’œ) a = ↑(⇑(⇑(direct_sum.decompose π’œ) a) 0)
source
def graded_algebra.proj_zero_ring_hom {ΞΉ : Type u_1} {R : Type u_2} {A : Type u_3} [comm_semiring R] [semiring A] [algebra R A] [decidable_eq ΞΉ] [canonically_ordered_add_monoid ΞΉ] (π’œ : ΞΉ β†’ submodule R A) [graded_algebra π’œ] :
A β†’+* A

If A is graded by a canonically ordered add monoid, then the projection map x ↦ xβ‚€ is a ring homomorphism.

Equations