mathlib3 documentation

ring_theory.graded_algebra.basic

Internally-graded rings and algebras #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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_ring {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [decidable_eq ι] [add_monoid ι] [semiring A] [set_like σ A] [add_submonoid_class σ 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.

Instances of this typeclass
Instances of other typeclasses for graded_ring
  • graded_ring.has_sizeof_inst
def direct_sum.decompose_ring_equiv {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [decidable_eq ι] [add_monoid ι] [semiring A] [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι → σ) [graded_ring 𝒜] :
A ≃+* direct_sum ι (λ (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
@[simp]
theorem direct_sum.decompose_one {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [decidable_eq ι] [add_monoid ι] [semiring A] [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι → σ) [graded_ring 𝒜] :
@[simp]
theorem direct_sum.decompose_symm_one {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [decidable_eq ι] [add_monoid ι] [semiring A] [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι → σ) [graded_ring 𝒜] :
@[simp]
theorem direct_sum.decompose_mul {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [decidable_eq ι] [add_monoid ι] [semiring A] [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι → σ) [graded_ring 𝒜] (x y : A) :
@[simp]
theorem direct_sum.decompose_symm_mul {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [decidable_eq ι] [add_monoid ι] [semiring A] [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι → σ) [graded_ring 𝒜] (x y : direct_sum ι (λ (i : ι), ↥(𝒜 i))) :
def graded_ring.proj {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [decidable_eq ι] [add_monoid ι] [semiring A] [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι → σ) [graded_ring 𝒜] (i : ι) :

The projection maps of a graded ring

Equations
@[simp]
theorem graded_ring.proj_apply {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [decidable_eq ι] [add_monoid ι] [semiring A] [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι → σ) [graded_ring 𝒜] (i : ι) (r : A) :
theorem graded_ring.proj_recompose {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [decidable_eq ι] [add_monoid ι] [semiring A] [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι → σ) [graded_ring 𝒜] (a : direct_sum ι (λ (i : ι), ↥(𝒜 i))) (i : ι) :
⇑(graded_ring.proj 𝒜 i) (⇑((direct_sum.decompose 𝒜).symm) a) = ⇑((direct_sum.decompose 𝒜).symm) (⇑(direct_sum.of (λ (i : ι), ↥(𝒜 i)) i) (⇑a i))
theorem graded_ring.mem_support_iff {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [decidable_eq ι] [add_monoid ι] [semiring A] [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι → σ) [graded_ring 𝒜] [Π (i : ι) (x : ↥(𝒜 i)), decidable (x ≠ 0)] (r : A) (i : ι) :
theorem direct_sum.coe_decompose_mul_add_of_left_mem {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [decidable_eq ι] [semiring A] [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι → σ) {i j : ι} [add_left_cancel_monoid ι] [graded_ring 𝒜] {a b : A} (a_mem : a ∈ 𝒜 i) :
theorem direct_sum.coe_decompose_mul_add_of_right_mem {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [decidable_eq ι] [semiring A] [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι → σ) {i j : ι} [add_right_cancel_monoid ι] [graded_ring 𝒜] {a b : A} (b_mem : b ∈ 𝒜 j) :
theorem direct_sum.decompose_mul_add_left {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [decidable_eq ι] [semiring A] [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι → σ) {i j : ι} [add_left_cancel_monoid ι] [graded_ring 𝒜] (a : ↥(𝒜 i)) {b : A} :
theorem direct_sum.decompose_mul_add_right {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [decidable_eq ι] [semiring A] [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι → σ) {i j : ι} [add_right_cancel_monoid ι] [graded_ring 𝒜] {a : A} (b : ↥(𝒜 j)) :
@[reducible]
def graded_algebra {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [add_monoid ι] [comm_semiring R] [semiring A] [algebra R A] (𝒜 : ι → submodule R A) :
Type (max u_1 u_3)

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

Equations
@[reducible]
def graded_algebra.of_alg_hom {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [add_monoid ι] [comm_semiring R] [semiring A] [algebra R A] (𝒜 : ι → submodule R A) [set_like.graded_monoid 𝒜] (decompose : A →ₐ[R] direct_sum ι (λ (i : ι), ↥(𝒜 i))) (right_inv : (direct_sum.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
@[simp]
theorem direct_sum.decompose_alg_equiv_apply {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [add_monoid ι] [comm_semiring R] [semiring A] [algebra R A] (𝒜 : ι → submodule R A) [graded_algebra 𝒜] (á¾° : A) :
@[simp]
theorem direct_sum.decompose_alg_equiv_symm_apply {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [add_monoid ι] [comm_semiring R] [semiring A] [algebra R A] (𝒜 : ι → submodule R A) [graded_algebra 𝒜] (á¾° : direct_sum ι (λ (i : ι), ↥(𝒜 i))) :
def direct_sum.decompose_alg_equiv {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [add_monoid ι] [comm_semiring R] [semiring A] [algebra R A] (𝒜 : ι → submodule R A) [graded_algebra 𝒜] :
A ≃ₐ[R] direct_sum ι (λ (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
def graded_algebra.proj {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [add_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_monoid ι] [comm_semiring R] [semiring A] [algebra R A] (𝒜 : ι → submodule R A) [graded_algebra 𝒜] (i : ι) (r : A) :
theorem graded_algebra.proj_recompose {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [add_monoid ι] [comm_semiring R] [semiring A] [algebra R A] (𝒜 : ι → submodule R A) [graded_algebra 𝒜] (a : direct_sum ι (λ (i : ι), ↥(𝒜 i))) (i : ι) :
⇑(graded_algebra.proj 𝒜 i) (⇑((direct_sum.decompose 𝒜).symm) a) = ⇑((direct_sum.decompose 𝒜).symm) (⇑(direct_sum.of (λ (i : ι), ↥(𝒜 i)) i) (⇑a i))
theorem graded_algebra.mem_support_iff {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [add_monoid ι] [comm_semiring R] [semiring A] [algebra R A] (𝒜 : ι → submodule R A) [graded_algebra 𝒜] [decidable_eq A] (r : A) (i : ι) :
@[simp]
theorem graded_ring.proj_zero_ring_hom_apply {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [semiring A] [decidable_eq ι] [canonically_ordered_add_monoid ι] [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι → σ) [graded_ring 𝒜] (a : A) :
def graded_ring.proj_zero_ring_hom {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [semiring A] [decidable_eq ι] [canonically_ordered_add_monoid ι] [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι → σ) [graded_ring 𝒜] :

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

Equations
theorem direct_sum.coe_decompose_mul_of_left_mem_of_not_le {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [semiring A] [decidable_eq ι] [canonically_ordered_add_monoid ι] [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι → σ) [graded_ring 𝒜] {a b : A} {n i : ι} (a_mem : a ∈ 𝒜 i) (h : ¬i ≤ n) :
↑(⇑(⇑(direct_sum.decompose 𝒜) (a * b)) n) = 0
theorem direct_sum.coe_decompose_mul_of_right_mem_of_not_le {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [semiring A] [decidable_eq ι] [canonically_ordered_add_monoid ι] [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι → σ) [graded_ring 𝒜] {a b : A} {n i : ι} (b_mem : b ∈ 𝒜 i) (h : ¬i ≤ n) :
↑(⇑(⇑(direct_sum.decompose 𝒜) (a * b)) n) = 0
theorem direct_sum.coe_decompose_mul_of_left_mem_of_le {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [semiring A] [decidable_eq ι] [canonically_ordered_add_monoid ι] [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι → σ) [graded_ring 𝒜] {a b : A} {n i : ι} [has_sub ι] [has_ordered_sub ι] [contravariant_class ι ι has_add.add has_le.le] (a_mem : a ∈ 𝒜 i) (h : i ≤ n) :
theorem direct_sum.coe_decompose_mul_of_right_mem_of_le {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [semiring A] [decidable_eq ι] [canonically_ordered_add_monoid ι] [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι → σ) [graded_ring 𝒜] {a b : A} {n i : ι} [has_sub ι] [has_ordered_sub ι] [contravariant_class ι ι has_add.add has_le.le] (b_mem : b ∈ 𝒜 i) (h : i ≤ n) :
theorem direct_sum.coe_decompose_mul_of_left_mem {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [semiring A] [decidable_eq ι] [canonically_ordered_add_monoid ι] [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι → σ) [graded_ring 𝒜] {a b : A} {i : ι} [has_sub ι] [has_ordered_sub ι] [contravariant_class ι ι has_add.add has_le.le] (n : ι) [decidable (i ≤ n)] (a_mem : a ∈ 𝒜 i) :
↑(⇑(⇑(direct_sum.decompose 𝒜) (a * b)) n) = ite (i ≤ n) (a * ↑(⇑(⇑(direct_sum.decompose 𝒜) b) (n - i))) 0
theorem direct_sum.coe_decompose_mul_of_right_mem {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [semiring A] [decidable_eq ι] [canonically_ordered_add_monoid ι] [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι → σ) [graded_ring 𝒜] {a b : A} {i : ι} [has_sub ι] [has_ordered_sub ι] [contravariant_class ι ι has_add.add has_le.le] (n : ι) [decidable (i ≤ n)] (b_mem : b ∈ 𝒜 i) :
↑(⇑(⇑(direct_sum.decompose 𝒜) (a * b)) n) = ite (i ≤ n) (↑(⇑(⇑(direct_sum.decompose 𝒜) a) (n - i)) * b) 0