mathlib documentation

ring_theory.graded_algebra.basic

Internally-graded rings and algebras #

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