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

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.

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

@[simp]

theorem DirectSum.decompose_one {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddMonoid ι] [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] : ↑(DirectSum.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 𝒜] : ↑(DirectSum.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 : A) (y : A) : ↑(DirectSum.decompose 𝒜) (x * y) = ↑(DirectSum.decompose 𝒜) x * ↑(DirectSum.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 : ⨁ (i : ι), { x // x ∈ 𝒜 i }) (y : ⨁ (i : ι), { x // x ∈ 𝒜 i }) : ↑(DirectSum.decompose 𝒜).symm (x * y) = ↑(DirectSum.decompose 𝒜).symm x * ↑(DirectSum.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) : ↑(GradedRing.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 : ⨁ (i : ι), { x // x ∈ 𝒜 i }) (i : ι) : ↑(GradedRing.proj 𝒜 i) (↑(DirectSum.decompose 𝒜).symm a) = ↑(DirectSum.decompose 𝒜).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} [DecidableEq ι] [AddMonoid ι] [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] [(i : ι) → (x : { x // x ∈ 𝒜 i }) → Decidable (x ≠ 0)] (r : A) (i : ι) : i ∈ DFinsupp.support (↑(DirectSum.decompose 𝒜) r) ↔ ↑(GradedRing.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 : A} {b : A} (a_mem : a ∈ 𝒜 i) : ↑(↑(↑(DirectSum.decompose 𝒜) (a * b)) (i + j)) = a * ↑(↑(↑(DirectSum.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 : A} {b : A} (b_mem : b ∈ 𝒜 j) : ↑(↑(↑(DirectSum.decompose 𝒜) (a * b)) (i + j)) = ↑(↑(↑(DirectSum.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 : { x // x ∈ 𝒜 i }) {b : A} : ↑(↑(DirectSum.decompose 𝒜) (↑a * b)) (i + j) = GradedMonoid.GMul.mul a (↑(↑(DirectSum.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 : { x // x ∈ 𝒜 j }) : ↑(↑(DirectSum.decompose 𝒜) (a * ↑b)) (i + j) = GradedMonoid.GMul.mul (↑(↑(DirectSum.decompose 𝒜) a) i) b

@[reducible]

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

def 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] ⨁ (i : ι), { x // x ∈ 𝒜 i }) (right_inv : AlgHom.comp (DirectSum.coeAlgHom 𝒜) decompose = AlgHom.id R A) (left_inv : ∀ (i : ι) (x : { x // x ∈ 𝒜 i }), ↑decompose ↑x = ↑(DirectSum.of (fun i => { x // x ∈ 𝒜 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].

@[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), ↑(DirectSum.decomposeAlgEquiv 𝒜) a = ↑(MulEquiv.symm ↑↑{ toEquiv := (↑(DirectSum.decomposeAddEquiv 𝒜)).symm, map_mul' := (_ : ∀ (x y : ⨁ (i : ι), { x // x ∈ 𝒜 i }), ↑(DirectSum.coeAlgHom 𝒜) (x * y) = ↑(DirectSum.coeAlgHom 𝒜) x * ↑(DirectSum.coeAlgHom 𝒜) y), map_add' := (_ : ∀ (x y : ⨁ (i : ι), { x // x ∈ 𝒜 i }), Equiv.toFun (AddEquiv.symm (DirectSum.decomposeAddEquiv 𝒜)).toEquiv (x + y) = Equiv.toFun (AddEquiv.symm (DirectSum.decomposeAddEquiv 𝒜)).toEquiv x + Equiv.toFun (AddEquiv.symm (DirectSum.decomposeAddEquiv 𝒜)).toEquiv y), commutes' := (_ : ∀ (r : R), ↑(DirectSum.coeAlgHom 𝒜) (↑(algebraMap R (⨁ (i : ι), { x // x ∈ 𝒜 i })) r) = ↑(algebraMap R A) r) }) 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 : ⨁ (i : ι), { x // x ∈ 𝒜 i }), ↑(AlgEquiv.symm (DirectSum.decomposeAlgEquiv 𝒜)) a = ↑{ toEquiv := (↑(DirectSum.decomposeAddEquiv 𝒜)).symm, map_mul' := (_ : ∀ (x y : ⨁ (i : ι), { x // x ∈ 𝒜 i }), ↑(DirectSum.coeAlgHom 𝒜) (x * y) = ↑(DirectSum.coeAlgHom 𝒜) x * ↑(DirectSum.coeAlgHom 𝒜) y), map_add' := (_ : ∀ (x y : ⨁ (i : ι), { x // x ∈ 𝒜 i }), Equiv.toFun (AddEquiv.symm (DirectSum.decomposeAddEquiv 𝒜)).toEquiv (x + y) = Equiv.toFun (AddEquiv.symm (DirectSum.decomposeAddEquiv 𝒜)).toEquiv x + Equiv.toFun (AddEquiv.symm (DirectSum.decomposeAddEquiv 𝒜)).toEquiv y), commutes' := (_ : ∀ (r : R), ↑(DirectSum.coeAlgHom 𝒜) (↑(algebraMap R (⨁ (i : ι), { x // x ∈ 𝒜 i })) r) = ↑(algebraMap R A) r) } a

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

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) : ↑(GradedAlgebra.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 : ⨁ (i : ι), { x // x ∈ 𝒜 i }) (i : ι) : ↑(GradedAlgebra.proj 𝒜 i) (↑(DirectSum.decompose 𝒜).symm a) = ↑(DirectSum.decompose 𝒜).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} [DecidableEq ι] [AddMonoid ι] [CommSemiring R] [Semiring A] [Algebra R A] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] [DecidableEq A] (r : A) (i : ι) : i ∈ DFinsupp.support (↑(DirectSum.decompose 𝒜) r) ↔ ↑(GradedAlgebra.proj 𝒜 i) r ≠ 0

@[simp]

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

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

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

theorem DirectSum.coe_decompose_mul_of_left_mem_of_not_le {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [Semiring A] [DecidableEq ι] [CanonicallyOrderedAddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] {a : A} {b : A} {n : ι} {i : ι} (a_mem : a ∈ 𝒜 i) (h : ¬i ≤ n) : ↑(↑(↑(DirectSum.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 ι] [CanonicallyOrderedAddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] {a : A} {b : A} {n : ι} {i : ι} (b_mem : b ∈ 𝒜 i) (h : ¬i ≤ n) : ↑(↑(↑(DirectSum.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 ι] [CanonicallyOrderedAddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] {a : A} {b : A} {n : ι} {i : ι} [Sub ι] [OrderedSub ι] [ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a_mem : a ∈ 𝒜 i) (h : i ≤ n) : ↑(↑(↑(DirectSum.decompose 𝒜) (a * b)) n) = a * ↑(↑(↑(DirectSum.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 ι] [CanonicallyOrderedAddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] {a : A} {b : A} {n : ι} {i : ι} [Sub ι] [OrderedSub ι] [ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (b_mem : b ∈ 𝒜 i) (h : i ≤ n) : ↑(↑(↑(DirectSum.decompose 𝒜) (a * b)) n) = ↑(↑(↑(DirectSum.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 ι] [CanonicallyOrderedAddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] {a : A} {b : A} {i : ι} [Sub ι] [OrderedSub ι] [ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (n : ι) [Decidable (i ≤ n)] (a_mem : a ∈ 𝒜 i) : ↑(↑(↑(DirectSum.decompose 𝒜) (a * b)) n) = if i ≤ n then a * ↑(↑(↑(DirectSum.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 ι] [CanonicallyOrderedAddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] {a : A} {b : A} {i : ι} [Sub ι] [OrderedSub ι] [ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (n : ι) [Decidable (i ≤ n)] (b_mem : b ∈ 𝒜 i) : ↑(↑(↑(DirectSum.decompose 𝒜) (a * b)) n) = if i ≤ n then ↑(↑(↑(DirectSum.decompose 𝒜) a) (n - i)) * b else 0