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 Semiring.toNatAlgebra, and all Rings are ℤ-algebras via Ring.toIntAlgebra.

Tags

graded algebra, graded ring, graded semiring, decomposition

class GradedRing {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddMonoid ι] [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) extends SetLike.GradedMonoid 𝒜, DirectSum.Decomposition 𝒜 : 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.

• one_mem : 1 ∈ 𝒜 0
• mul_mem ⦃i j : ι⦄ {gi gj : A} : gi ∈ 𝒜 i → gj ∈ 𝒜 j → gi * gj ∈ 𝒜 (i + j)
• decompose' : A → DirectSum ι fun (i : ι) => ↥(𝒜 i)
• left_inv : Function.LeftInverse (⇑(DirectSum.coeAddMonoidHom 𝒜)) decompose'
• right_inv : Function.RightInverse (⇑(DirectSum.coeAddMonoidHom 𝒜)) decompose'

def DirectSum.decomposeRingEquiv {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddMonoid ι] [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] : 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.

@[simp]

theorem DirectSum.decompose_one {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddMonoid ι] [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] : (decompose 𝒜) 1 = 1

@[simp]

theorem DirectSum.decompose_symm_one {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddMonoid ι] [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] : (decompose 𝒜).symm 1 = 1

@[simp]

theorem DirectSum.decompose_mul {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddMonoid ι] [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] (x y : A) : (decompose 𝒜) (x * y) = (decompose 𝒜) x * (decompose 𝒜) y

@[simp]

theorem DirectSum.decompose_symm_mul {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddMonoid ι] [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] (x y : DirectSum ι fun (i : ι) => ↥(𝒜 i)) : (decompose 𝒜).symm (x * y) = (decompose 𝒜).symm x * (decompose 𝒜).symm y

def GradedRing.proj {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddMonoid ι] [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] (i : ι) : A →+ A

The projection maps of a graded ring

@[simp]

theorem GradedRing.proj_apply {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddMonoid ι] [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] (i : ι) (r : A) : (proj 𝒜 i) r = ↑(((DirectSum.decompose 𝒜) r) i)

theorem GradedRing.proj_recompose {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddMonoid ι] [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] (a : DirectSum ι fun (i : ι) => ↥(𝒜 i)) (i : ι) : (proj 𝒜 i) ((DirectSum.decompose 𝒜).symm a) = (DirectSum.decompose 𝒜).symm ((DirectSum.of (fun (i : ι) => ↥(𝒜 i)) i) (a i))

theorem GradedRing.mem_support_iff {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddMonoid ι] [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] [(i : ι) → (x : ↥(𝒜 i)) → Decidable (x ≠ 0)] (r : A) (i : ι) : i ∈ DFinsupp.support ((DirectSum.decompose 𝒜) r) ↔ (proj 𝒜 i) r ≠ 0

theorem DirectSum.coe_decompose_mul_add_of_left_mem {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [DecidableEq ι] [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) {i j : ι} [AddLeftCancelMonoid ι] [GradedRing 𝒜] {a b : A} (a_mem : a ∈ 𝒜 i) : ↑(((decompose 𝒜) (a * b)) (i + j)) = a * ↑(((decompose 𝒜) b) j)

theorem DirectSum.coe_decompose_mul_add_of_right_mem {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [DecidableEq ι] [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) {i j : ι} [AddRightCancelMonoid ι] [GradedRing 𝒜] {a b : A} (b_mem : b ∈ 𝒜 j) : ↑(((decompose 𝒜) (a * b)) (i + j)) = ↑(((decompose 𝒜) a) i) * b

theorem DirectSum.decompose_mul_add_left {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [DecidableEq ι] [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) {i j : ι} [AddLeftCancelMonoid ι] [GradedRing 𝒜] (a : ↥(𝒜 i)) {b : A} : ((decompose 𝒜) (↑a * b)) (i + j) = GradedMonoid.GMul.mul a (((decompose 𝒜) b) j)

theorem DirectSum.decompose_mul_add_right {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [DecidableEq ι] [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) {i j : ι} [AddRightCancelMonoid ι] [GradedRing 𝒜] {a : A} (b : ↥(𝒜 j)) : ((decompose 𝒜) (a * ↑b)) (i + j) = GradedMonoid.GMul.mul (((decompose 𝒜) a) i) b

theorem DirectSum.coe_decompose_mul_of_left_mem_zero {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [DecidableEq ι] [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) {j : ι} [AddMonoid ι] [GradedRing 𝒜] {a b : A} (a_mem : a ∈ 𝒜 0) : ↑(((decompose 𝒜) (a * b)) j) = a * ↑(((decompose 𝒜) b) j)

theorem DirectSum.coe_decompose_mul_of_right_mem_zero {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [DecidableEq ι] [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) {i : ι} [AddMonoid ι] [GradedRing 𝒜] {a b : A} (b_mem : b ∈ 𝒜 0) : ↑(((decompose 𝒜) (a * b)) i) = ↑(((decompose 𝒜) a) i) * b

@[reducible, inline]

abbrev GradedAlgebra {ι : Type u_1} {R : Type u_2} {A : Type u_3} [DecidableEq ι] [AddMonoid ι] [CommSemiring R] [Semiring A] [Algebra R A] (𝒜 : ι → Submodule 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.

@[reducible, inline]

abbrev GradedAlgebra.ofAlgHom {ι : Type u_1} {R : Type u_2} {A : Type u_3} [DecidableEq ι] [AddMonoid ι] [CommSemiring R] [Semiring A] [Algebra R A] (𝒜 : ι → Submodule R A) [SetLike.GradedMonoid 𝒜] (decompose : A →ₐ[R] DirectSum ι fun (i : ι) => ↥(𝒜 i)) (right_inv : (DirectSum.coeAlgHom 𝒜).comp decompose = AlgHom.id R A) (left_inv : ∀ (i : ι) (x : ↥(𝒜 i)), decompose ↑x = (DirectSum.of (fun (i : ι) => ↥(𝒜 i)) i) x) : GradedAlgebra 𝒜

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].

def DirectSum.decomposeAlgEquiv {ι : Type u_1} {R : Type u_2} {A : Type u_3} [DecidableEq ι] [AddMonoid ι] [CommSemiring R] [Semiring A] [Algebra R A] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] : 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.

@[simp]

theorem DirectSum.decomposeAlgEquiv_apply {ι : Type u_1} {R : Type u_2} {A : Type u_3} [DecidableEq ι] [AddMonoid ι] [CommSemiring R] [Semiring A] [Algebra R A] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] (a : A) : (decomposeAlgEquiv 𝒜) a = (decompose 𝒜) a

@[simp]

theorem DirectSum.decomposeAlgEquiv_symm_apply {ι : Type u_1} {R : Type u_2} {A : Type u_3} [DecidableEq ι] [AddMonoid ι] [CommSemiring R] [Semiring A] [Algebra R A] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] (a : DirectSum ι fun (i : ι) => ↥(𝒜 i)) : (decomposeAlgEquiv 𝒜).symm a = (decompose 𝒜).symm a

@[simp]

theorem DirectSum.decompose_algebraMap {ι : Type u_1} {R : Type u_2} {A : Type u_3} [DecidableEq ι] [AddMonoid ι] [CommSemiring R] [Semiring A] [Algebra R A] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] (r : R) : (decompose 𝒜) ((algebraMap R A) 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} [DecidableEq ι] [AddMonoid ι] [CommSemiring R] [Semiring A] [Algebra R A] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] (r : R) : (decompose 𝒜).symm ((algebraMap R (DirectSum ι fun (i : ι) => ↥(𝒜 i))) r) = (algebraMap R A) r

def GradedAlgebra.proj {ι : Type u_1} {R : Type u_2} {A : Type u_3} [DecidableEq ι] [AddMonoid ι] [CommSemiring R] [Semiring A] [Algebra R A] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] (i : ι) : A →ₗ[R] A

The projection maps of graded algebra

@[simp]

theorem GradedAlgebra.proj_apply {ι : Type u_1} {R : Type u_2} {A : Type u_3} [DecidableEq ι] [AddMonoid ι] [CommSemiring R] [Semiring A] [Algebra R A] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] (i : ι) (r : A) : (proj 𝒜 i) r = ↑(((DirectSum.decompose 𝒜) r) i)

theorem GradedAlgebra.proj_recompose {ι : Type u_1} {R : Type u_2} {A : Type u_3} [DecidableEq ι] [AddMonoid ι] [CommSemiring R] [Semiring A] [Algebra R A] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] (a : DirectSum ι fun (i : ι) => ↥(𝒜 i)) (i : ι) : (proj 𝒜 i) ((DirectSum.decompose 𝒜).symm a) = (DirectSum.decompose 𝒜).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} [DecidableEq ι] [AddMonoid ι] [CommSemiring R] [Semiring A] [Algebra R A] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] [DecidableEq A] (r : A) (i : ι) : i ∈ DFinsupp.support ((DirectSum.decompose 𝒜) r) ↔ (proj 𝒜 i) r ≠ 0

def GradedRing.projZeroRingHom {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [Semiring A] [DecidableEq ι] [AddCommMonoid ι] [PartialOrder ι] [CanonicallyOrderedAdd ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] : A →+* A

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

@[simp]

theorem GradedRing.projZeroRingHom_apply {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [Semiring A] [DecidableEq ι] [AddCommMonoid ι] [PartialOrder ι] [CanonicallyOrderedAdd ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] (a : A) : (projZeroRingHom 𝒜) a = ↑(((DirectSum.decompose 𝒜) a) 0)

def GradedRing.projZeroRingHom' {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [Semiring A] [DecidableEq ι] [AddCommMonoid ι] [PartialOrder ι] [CanonicallyOrderedAdd ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] : A →+* ↥(𝒜 0)

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

@[simp]

theorem GradedRing.coe_projZeroRingHom'_apply {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [Semiring A] [DecidableEq ι] [AddCommMonoid ι] [PartialOrder ι] [CanonicallyOrderedAdd ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] (a : A) : ↑((projZeroRingHom' 𝒜) a) = (projZeroRingHom 𝒜) a

@[simp]

theorem GradedRing.projZeroRingHom'_apply_coe {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [Semiring A] [DecidableEq ι] [AddCommMonoid ι] [PartialOrder ι] [CanonicallyOrderedAdd ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] (a : ↥(𝒜 0)) : (projZeroRingHom' 𝒜) ↑a = a

theorem GradedRing.projZeroRingHom'_surjective {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [Semiring A] [DecidableEq ι] [AddCommMonoid ι] [PartialOrder ι] [CanonicallyOrderedAdd ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] : Function.Surjective ⇑(projZeroRingHom' 𝒜)

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} [Semiring A] [DecidableEq ι] [AddCommMonoid ι] [PartialOrder ι] [CanonicallyOrderedAdd ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] {a b : A} {n i : ι} (a_mem : a ∈ 𝒜 i) (h : ¬i ≤ n) : ↑(((decompose 𝒜) (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} [Semiring A] [DecidableEq ι] [AddCommMonoid ι] [PartialOrder ι] [CanonicallyOrderedAdd ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] {a b : A} {n i : ι} (b_mem : b ∈ 𝒜 i) (h : ¬i ≤ n) : ↑(((decompose 𝒜) (a * b)) n) = 0

theorem DirectSum.coe_decompose_mul_of_left_mem_of_le {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [Semiring A] [DecidableEq ι] [AddCommMonoid ι] [PartialOrder ι] [CanonicallyOrderedAdd ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] {a b : A} {n i : ι} [Sub ι] [OrderedSub ι] [AddLeftReflectLE ι] (a_mem : a ∈ 𝒜 i) (h : i ≤ n) : ↑(((decompose 𝒜) (a * b)) n) = a * ↑(((decompose 𝒜) b) (n - i))

theorem DirectSum.coe_decompose_mul_of_right_mem_of_le {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [Semiring A] [DecidableEq ι] [AddCommMonoid ι] [PartialOrder ι] [CanonicallyOrderedAdd ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] {a b : A} {n i : ι} [Sub ι] [OrderedSub ι] [AddLeftReflectLE ι] (b_mem : b ∈ 𝒜 i) (h : i ≤ n) : ↑(((decompose 𝒜) (a * b)) n) = ↑(((decompose 𝒜) a) (n - i)) * b

theorem DirectSum.coe_decompose_mul_of_left_mem {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [Semiring A] [DecidableEq ι] [AddCommMonoid ι] [PartialOrder ι] [CanonicallyOrderedAdd ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] {a b : A} {i : ι} [Sub ι] [OrderedSub ι] [AddLeftReflectLE ι] (n : ι) [Decidable (i ≤ n)] (a_mem : a ∈ 𝒜 i) : ↑(((decompose 𝒜) (a * b)) n) = if i ≤ n then a * ↑(((decompose 𝒜) b) (n - i)) else 0

theorem DirectSum.coe_decompose_mul_of_right_mem {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [Semiring A] [DecidableEq ι] [AddCommMonoid ι] [PartialOrder ι] [CanonicallyOrderedAdd ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] {a b : A} {i : ι} [Sub ι] [OrderedSub ι] [AddLeftReflectLE ι] (n : ι) [Decidable (i ≤ n)] (b_mem : b ∈ 𝒜 i) : ↑(((decompose 𝒜) (a * b)) n) = if i ≤ n then ↑(((decompose 𝒜) a) (n - i)) * b else 0

noncomputable def DirectSum.IsInternal.coeAlgEquiv {R : Type u_5} [CommSemiring R] {A : Type u_6} [Semiring A] [Algebra R A] {ι : Type u_7} [DecidableEq ι] [AddMonoid ι] {M : ι → Submodule R A} [SetLike.GradedMonoid M] (hM : IsInternal M) : (DirectSum ι fun (i : ι) => ↥(M i)) ≃ₐ[R] A

The canonical isomorphism of an internal direct sum with the ambient algebra

noncomputable def DirectSum.IsInternal.gradedAlgebra {R : Type u_5} [CommSemiring R] {A : Type u_6} [Semiring A] [Algebra R A] {ι : Type u_7} [DecidableEq ι] [AddMonoid ι] {M : ι → Submodule R A} [SetLike.GradedMonoid M] (hM : IsInternal M) : GradedAlgebra M

Given an R-algebra A and a family ι → Submodule R A of submodules parameterized by an additive monoid ι and satisfying SetLike.GradedMonoid M (essentially, is multiplicative) such that DirectSum.IsInternal M (A is the direct sum of the M i), we endow A with the structure of a graded algebra. The submodules are the homogeneous parts.