# mathlibdocumentation

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 of set_like.graded_monoid, and direct_sum.decomposition 𝒜.
• direct_sum.decompose_alg_equiv 𝒜 : A ≃ₐ[R] ⨁ i, 𝒜 i, a more bundled version of direct_sum.decompose 𝒜.
• graded_algebra.proj 𝒜 i is the linear map from A to its degree i : ι component, such that proj 𝒜 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 semirings are ℕ-algebras via algebra_nat, and all rings are ℤ-algebras via algebra_int.

## Tags #

@[class]
structure graded_algebra {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [add_monoid ι] [semiring A] [ A] (𝒜 : ι → A) :
Type (max u_1 u_3)
• to_decomposition :

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
@[protected]
theorem graded_algebra.is_internal {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [add_monoid ι] [semiring A] [ A] (𝒜 : ι → A)  :
def graded_algebra.of_alg_hom {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [add_monoid ι] [semiring A] [ A] (𝒜 : ι → A) (decompose : A →ₐ[R] (λ (i : ι), (𝒜 i))) (right_inv : decompose = A) (left_inv : ∀ (i : ι) (x : (𝒜 i)), decompose x = (direct_sum.of (λ (i : ι), (𝒜 i)) i) x) :

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.

Equations
@[simp]
theorem direct_sum.decompose_alg_equiv_apply {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [add_monoid ι] [semiring A] [ A] (𝒜 : ι → A) (ᾰ : A) :
= ({to_fun := .symm), inv_fun := , left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}.symm)
@[simp]
theorem direct_sum.decompose_alg_equiv_symm_apply {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [add_monoid ι] [semiring A] [ A] (𝒜 : ι → A) (ᾰ : (λ (i : ι), (𝒜 i))) :
= .symm)
def direct_sum.decompose_alg_equiv {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [add_monoid ι] [semiring A] [ A] (𝒜 : ι → A)  :
A ≃ₐ[R] (λ (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
@[simp]
theorem direct_sum.decompose_one {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [add_monoid ι] [semiring A] [ A] (𝒜 : ι → A)  :
= 1
@[simp]
theorem direct_sum.decompose_symm_one {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [add_monoid ι] [semiring A] [ A] (𝒜 : ι → A)  :
.symm) 1 = 1
@[simp]
theorem direct_sum.decompose_mul {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [add_monoid ι] [semiring A] [ A] (𝒜 : ι → A) (x y : A) :
(x * y) = *
@[simp]
theorem direct_sum.decompose_symm_mul {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [add_monoid ι] [semiring A] [ A] (𝒜 : ι → A) (x y : (λ (i : ι), (𝒜 i))) :
.symm) (x * y) = .symm) x * .symm) y
def graded_algebra.proj {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [add_monoid ι] [semiring A] [ A] (𝒜 : ι → A) (i : ι) :

The projection maps of graded algebra

Equations
@[simp]
theorem graded_algebra.proj_apply {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [add_monoid ι] [semiring A] [ A] (𝒜 : ι → A) (i : ι) (r : A) :
i) r = ( r) i)
theorem graded_algebra.proj_recompose {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [add_monoid ι] [semiring A] [ A] (𝒜 : ι → A) (a : (λ (i : ι), (𝒜 i))) (i : ι) :
i) (.symm) a) = .symm) ((direct_sum.of (λ (i : ι), (𝒜 i)) i) (a i))
theorem graded_algebra.mem_support_iff {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [add_monoid ι] [semiring A] [ A] (𝒜 : ι → A) [decidable_eq A] (r : A) (i : ι) :
i i) r 0
@[simp]
theorem graded_algebra.proj_zero_ring_hom_apply {ι : Type u_1} {R : Type u_2} {A : Type u_3} [semiring A] [ A] [decidable_eq ι] (𝒜 : ι → A) (a : A) :
= ( a) 0)
def graded_algebra.proj_zero_ring_hom {ι : Type u_1} {R : Type u_2} {A : Type u_3} [semiring A] [ A] [decidable_eq ι] (𝒜 : ι → A)  :
A →+* A

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

Equations