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

@[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)

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) :

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
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 π’œ] :
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 ΞΉ] [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
@[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) :
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
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) :
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) :
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 : ΞΉ) :
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