# Internally-graded rings and algebras #

This file defines the typeclass GradedAlgebra 𝒜, 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 #

• GradedRing 𝒜: the typeclass, which is a combination of SetLike.GradedMonoid, and DirectSum.Decomposition 𝒜.
• GradedAlgebra 𝒜: A convenience alias for GradedRing when 𝒜 is a family of submodules.
• DirectSum.decomposeRingEquiv 𝒜 : A ≃ₐ[R] ⨁ i, 𝒜 i, a more bundled version of DirectSum.decompose 𝒜.
• DirectSum.decomposeAlgEquiv 𝒜 : A ≃ₐ[R] ⨁ i, 𝒜 i, a more bundled version of DirectSum.decompose 𝒜.
• GradedAlgebra.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 algebraNat, and all Rings are ℤ-algebras via algebraInt.

## Tags #

class GradedRing {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [] [] [] [SetLike σ A] [] (𝒜 : ισ) extends , :
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, GradedAlgebra 𝒜, implies an externally-graded algebra structure DirectSum.GAlgebra R (fun i ↦ ↥(𝒜 i)), which in turn makes available an Algebra R (⨁ i, 𝒜 i) instance.

Instances
def DirectSum.decomposeRingEquiv {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [] [] [] [SetLike σ A] [] (𝒜 : ισ) [] :
A ≃+* DirectSum ι fun (i : ι) => (𝒜 i)

If A is graded by ι with degree i component 𝒜 i, then it is isomorphic as a ring to a direct sum of components.

Equations
• = (let __src := .symm; { toEquiv := __src.toEquiv, map_mul' := , map_add' := }).symm
Instances For
@[simp]
theorem DirectSum.decompose_one {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [] [] [] [SetLike σ A] [] (𝒜 : ισ) [] :
1 = 1
@[simp]
theorem DirectSum.decompose_symm_one {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [] [] [] [SetLike σ A] [] (𝒜 : ισ) [] :
.symm 1 = 1
@[simp]
theorem DirectSum.decompose_mul {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [] [] [] [SetLike σ A] [] (𝒜 : ισ) [] (x : A) (y : A) :
(x * y) = x * y
@[simp]
theorem DirectSum.decompose_symm_mul {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [] [] [] [SetLike σ A] [] (𝒜 : ισ) [] (x : DirectSum ι fun (i : ι) => (𝒜 i)) (y : DirectSum ι fun (i : ι) => (𝒜 i)) :
.symm (x * y) = .symm x * .symm y
def GradedRing.proj {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [] [] [] [SetLike σ A] [] (𝒜 : ισ) [] (i : ι) :
A →+ A

The projection maps of a graded ring

Equations
Instances For
@[simp]
theorem GradedRing.proj_apply {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [] [] [] [SetLike σ A] [] (𝒜 : ισ) [] (i : ι) (r : A) :
() r = (( r) i)
theorem GradedRing.proj_recompose {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [] [] [] [SetLike σ A] [] (𝒜 : ισ) [] (a : DirectSum ι fun (i : ι) => (𝒜 i)) (i : ι) :
() (.symm a) = .symm ((DirectSum.of (fun (i : ι) => (𝒜 i)) i) (a i))
theorem GradedRing.mem_support_iff {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [] [] [] [SetLike σ A] [] (𝒜 : ισ) [] [(i : ι) → (x : (𝒜 i)) → Decidable (x 0)] (r : A) (i : ι) :
i () r 0
theorem DirectSum.coe_decompose_mul_add_of_left_mem {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [] [] [SetLike σ A] [] (𝒜 : ισ) {i : ι} {j : ι} [] {a : A} {b : A} (a_mem : a 𝒜 i) :
(( (a * b)) (i + j)) = a * (( b) j)
theorem DirectSum.coe_decompose_mul_add_of_right_mem {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [] [] [SetLike σ A] [] (𝒜 : ισ) {i : ι} {j : ι} [] {a : A} {b : A} (b_mem : b 𝒜 j) :
(( (a * b)) (i + j)) = (( a) i) * b
theorem DirectSum.decompose_mul_add_left {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [] [] [SetLike σ A] [] (𝒜 : ισ) {i : ι} {j : ι} [] (a : (𝒜 i)) {b : A} :
( (a * b)) (i + j) = GradedMonoid.GMul.mul a (( b) j)
theorem DirectSum.decompose_mul_add_right {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [] [] [SetLike σ A] [] (𝒜 : ισ) {i : ι} {j : ι} [] {a : A} (b : (𝒜 j)) :
( (a * b)) (i + j) = GradedMonoid.GMul.mul (( a) i) b
@[reducible, inline]
abbrev GradedAlgebra {ι : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] (𝒜 : ι) :
Type (max u_1 u_3)

A special case of GradedRing with σ = Submodule R A. This is useful both because it can avoid typeclass search, and because it provides a more concise name.

Equations
Instances For
@[reducible, inline]
abbrev GradedAlgebra.ofAlgHom {ι : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] (𝒜 : ι) (decompose : A →ₐ[R] DirectSum ι fun (i : ι) => (𝒜 i)) (right_inv : .comp decompose = ) (left_inv : ∀ (i : ι) (x : (𝒜 i)), decompose x = (DirectSum.of (fun (i : ι) => (𝒜 i)) i) x) :

A helper to construct a GradedAlgebra when the SetLike.GradedMonoid 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
Instances For
def DirectSum.decomposeAlgEquiv {ι : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] (𝒜 : ι) [] :
A ≃ₐ[R] DirectSum ι fun (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
• = (let __src := .symm; { toEquiv := __src.toEquiv, map_mul' := , map_add' := , commutes' := }).symm
Instances For
@[simp]
theorem DirectSum.decomposeAlgEquiv_apply {ι : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] (𝒜 : ι) [] (a : A) :
= a
@[simp]
theorem DirectSum.decomposeAlgEquiv_symm_apply {ι : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] (𝒜 : ι) [] (a : DirectSum ι fun (i : ι) => (𝒜 i)) :
.symm a = .symm a
@[simp]
theorem DirectSum.decompose_algebraMap {ι : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] (𝒜 : ι) [] (r : R) :
(() r) = (algebraMap R (DirectSum ι fun (i : ι) => (𝒜 i))) r
@[simp]
theorem DirectSum.decompose_symm_algebraMap {ι : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] (𝒜 : ι) [] (r : R) :
.symm ((algebraMap R (DirectSum ι fun (i : ι) => (𝒜 i))) r) = () r
def GradedAlgebra.proj {ι : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] (𝒜 : ι) [] (i : ι) :

The projection maps of graded algebra

Equations
• = (𝒜 i).subtype ∘ₗ ∘ₗ ().toLinearMap
Instances For
@[simp]
theorem GradedAlgebra.proj_apply {ι : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] (𝒜 : ι) [] (i : ι) (r : A) :
() r = (( r) i)
theorem GradedAlgebra.proj_recompose {ι : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] (𝒜 : ι) [] (a : DirectSum ι fun (i : ι) => (𝒜 i)) (i : ι) :
() (.symm a) = .symm ((DirectSum.of (fun (i : ι) => (𝒜 i)) i) (a i))
theorem GradedAlgebra.mem_support_iff {ι : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] (𝒜 : ι) [] [] (r : A) (i : ι) :
i () r 0
@[simp]
theorem GradedRing.projZeroRingHom_apply {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [] [] [SetLike σ A] [] (𝒜 : ισ) [] (a : A) :
= (( a) 0)
def GradedRing.projZeroRingHom {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [] [] [SetLike σ A] [] (𝒜 : ισ) [] :
A →+* A

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

Equations
• = { toFun := fun (a : A) => (( a) 0), map_one' := , map_mul' := , map_zero' := , map_add' := }
Instances For
def GradedRing.projZeroRingHom' {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [] [] [SetLike σ A] [] (𝒜 : ισ) [] :
A →+* (𝒜 0)

The ring homomorphism from A to 𝒜 0 sending every a : A to a₀.

Equations
• = .codRestrict
Instances For
@[simp]
theorem GradedRing.coe_projZeroRingHom'_apply {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [] [] [SetLike σ A] [] (𝒜 : ισ) [] (a : A) :
() =
@[simp]
theorem GradedRing.projZeroRingHom'_apply_coe {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [] [] [SetLike σ A] [] (𝒜 : ισ) [] (a : (𝒜 0)) :
= a
theorem GradedRing.projZeroRingHom'_surjective {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [] [] [SetLike σ A] [] (𝒜 : ισ) [] :

The ring homomorphism GradedRing.projZeroRingHom' 𝒜 is surjective.

theorem DirectSum.coe_decompose_mul_of_left_mem_of_not_le {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [] [] [SetLike σ A] [] (𝒜 : ισ) [] {a : A} {b : A} {n : ι} {i : ι} (a_mem : a 𝒜 i) (h : ¬i n) :
(( (a * b)) n) = 0
theorem DirectSum.coe_decompose_mul_of_right_mem_of_not_le {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [] [] [SetLike σ A] [] (𝒜 : ισ) [] {a : A} {b : A} {n : ι} {i : ι} (b_mem : b 𝒜 i) (h : ¬i n) :
(( (a * b)) n) = 0
theorem DirectSum.coe_decompose_mul_of_left_mem_of_le {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [] [] [SetLike σ A] [] (𝒜 : ισ) [] {a : A} {b : A} {n : ι} {i : ι} [Sub ι] [] [ContravariantClass ι ι (fun (x x_1 : ι) => x + x_1) fun (x x_1 : ι) => x x_1] (a_mem : a 𝒜 i) (h : i n) :
(( (a * b)) n) = a * (( b) (n - i))
theorem DirectSum.coe_decompose_mul_of_right_mem_of_le {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [] [] [SetLike σ A] [] (𝒜 : ισ) [] {a : A} {b : A} {n : ι} {i : ι} [Sub ι] [] [ContravariantClass ι ι (fun (x x_1 : ι) => x + x_1) fun (x x_1 : ι) => x x_1] (b_mem : b 𝒜 i) (h : i n) :
(( (a * b)) n) = (( a) (n - i)) * b
theorem DirectSum.coe_decompose_mul_of_left_mem {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [] [] [SetLike σ A] [] (𝒜 : ισ) [] {a : A} {b : A} {i : ι} [Sub ι] [] [ContravariantClass ι ι (fun (x x_1 : ι) => x + x_1) fun (x x_1 : ι) => x x_1] (n : ι) [Decidable (i n)] (a_mem : a 𝒜 i) :
(( (a * b)) n) = if i n then a * (( b) (n - i)) else 0
theorem DirectSum.coe_decompose_mul_of_right_mem {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [] [] [SetLike σ A] [] (𝒜 : ισ) [] {a : A} {b : A} {i : ι} [Sub ι] [] [ContravariantClass ι ι (fun (x x_1 : ι) => x + x_1) fun (x x_1 : ι) => x x_1] (n : ι) [Decidable (i n)] (b_mem : b 𝒜 i) :
(( (a * b)) n) = if i n then (( a) (n - i)) * b else 0