# 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 a constructive version of direct_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 𝒜 i is the linear map from A to its degree i : ι component, such that proj 𝒜 i x = decompose 𝒜 x i.
• graded_algebra.support 𝒜 r is the finset ι containing the i : ι such that the degree i component of r is 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 #

@[class]
structure graded_algebra {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [semiring A] [ A] (𝒜 : ι → A) :
Type (max u_1 u_3)
• decompose' : A → (⨁ (i : ι), (𝒜 i))
• left_inv :
• right_inv :

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 ι] [semiring A] [ A] (𝒜 : ι → A)  :
def graded_algebra.of_alg_hom {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [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
def graded_algebra.decompose {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [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 graded_algebra.decompose'_def {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [semiring A] [ A] (𝒜 : ι → A)  :
@[simp]
theorem graded_algebra.decompose_symm_of {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [semiring A] [ A] (𝒜 : ι → A) {i : ι} (x : (𝒜 i)) :
((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 ι] [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 ι] [semiring A] [ A] (𝒜 : ι → A) (i : ι) (r : A) :
i) r = ( r) i)
def graded_algebra.support {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [semiring A] [ A] (𝒜 : ι → A) [Π (i : ι) (x : (𝒜 i)), decidable (x 0)] (r : A) :

The support of r is the finset where proj R A i r ≠ 0 ↔ i ∈ r.support

Equations
theorem graded_algebra.proj_recompose {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [semiring A] [ A] (𝒜 : ι → A) (a : ⨁ (i : ι), (𝒜 i)) (i : ι) :
i) (.symm) a) = ((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 ι] [semiring A] [ A] (𝒜 : ι → A) {i : ι} (x : (𝒜 i)) :
= (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 ι] [semiring A] [ A] (𝒜 : ι → A) {x : A} {i : ι} (hx : x 𝒜 i) :
= (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 ι] [semiring A] [ A] (𝒜 : ι → A) {x : A} {i : ι} (hx : x 𝒜 i) :
( x) i) = x
theorem graded_algebra.decompose_of_mem_ne {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [semiring A] [ A] (𝒜 : ι → A) {x : A} {i j : ι} (hx : x 𝒜 i) (hij : i j) :
( x) j) = 0
theorem graded_algebra.mem_support_iff {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [semiring A] [ A] (𝒜 : ι → A) [Π (i : ι) (x : (𝒜 i)), decidable (x 0)] (r : A) (i : ι) :
i) r 0
theorem graded_algebra.sum_support_decompose {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [semiring A] [ A] (𝒜 : ι → A) [Π (i : ι) (x : (𝒜 i)), decidable (x 0)] (r : A) :
∑ (i : ι) in , ( r) i) = r