# 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 ≃+* ⨁ (i : ι), { x // x 𝒜 i }

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

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 : ⨁ (i : ι), { x // x 𝒜 i }) (y : ⨁ (i : ι), { x // x 𝒜 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

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 : ⨁ (i : ι), { x // x 𝒜 i }) (i : ι) :
↑() (().symm a) = ().symm (↑(DirectSum.of (fun i => (fun i => { x // x 𝒜 i }) i) i) (a i))
theorem GradedRing.mem_support_iff {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [] [] [] [SetLike σ A] [] (𝒜 : ισ) [] [(i : ι) → (x : { x // x 𝒜 i }) → Decidable (x 0)] (r : A) (i : ι) :
i DFinsupp.support (↑() r) ↑() 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 : { x // x 𝒜 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 : { x // x 𝒜 j }) :
↑(↑() (a * b)) (i + j) = GradedMonoid.GMul.mul (↑(↑() a) i) b
@[reducible]
def 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.

Instances For
@[reducible]
def GradedAlgebra.ofAlgHom {ι : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] (𝒜 : ι) (decompose : A →ₐ[R] ⨁ (i : ι), { x // x 𝒜 i }) (right_inv : AlgHom.comp () decompose = ) (left_inv : ∀ (i : ι) (x : { x // x 𝒜 i }), decompose x = ↑(DirectSum.of (fun i => { x // x 𝒜 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].

Instances For
@[simp]
theorem DirectSum.decomposeAlgEquiv_apply {ι : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] (𝒜 : ι) [] :
∀ (a : A), = ↑(MulEquiv.symm { toEquiv := ().symm, map_mul' := (_ : ∀ (x y : ⨁ (i : ι), { x // x 𝒜 i }), ↑() (x * y) = ↑() x * ↑() y), map_add' := (_ : ∀ (x y : ⨁ (i : ι), { x // x 𝒜 i }), Equiv.toFun ().toEquiv (x + y) = Equiv.toFun ().toEquiv x + Equiv.toFun ().toEquiv y), commutes' := (_ : ∀ (r : R), ↑() (↑(algebraMap R (⨁ (i : ι), { x // x 𝒜 i })) r) = ↑() r) }) a
@[simp]
theorem DirectSum.decomposeAlgEquiv_symm_apply {ι : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] (𝒜 : ι) [] :
∀ (a : ⨁ (i : ι), { x // x 𝒜 i }), = { toEquiv := ().symm, map_mul' := (_ : ∀ (x y : ⨁ (i : ι), { x // x 𝒜 i }), ↑() (x * y) = ↑() x * ↑() y), map_add' := (_ : ∀ (x y : ⨁ (i : ι), { x // x 𝒜 i }), Equiv.toFun ().toEquiv (x + y) = Equiv.toFun ().toEquiv x + Equiv.toFun ().toEquiv y), commutes' := (_ : ∀ (r : R), ↑() (↑(algebraMap R (⨁ (i : ι), { x // x 𝒜 i })) r) = ↑() r) } a
def DirectSum.decomposeAlgEquiv {ι : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] (𝒜 : ι) [] :
A ≃ₐ[R] ⨁ (i : ι), { x // x 𝒜 i }

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

Instances For
def GradedAlgebra.proj {ι : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] (𝒜 : ι) [] (i : ι) :

The projection maps of graded algebra

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 : ⨁ (i : ι), { x // x 𝒜 i }) (i : ι) :
↑() (().symm a) = ().symm (↑(DirectSum.of (fun i => (fun i => { x // x 𝒜 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 DFinsupp.support (↑() r) ↑() 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.

Instances For
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