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

source
@[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
source
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
source
@[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 ๐’œ] :
โ‡‘(direct_sum.decompose ๐’œ) 1 = 1
source
@[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 ๐’œ] :
โ‡‘((direct_sum.decompose ๐’œ).symm) 1 = 1
source
@[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) :
โ‡‘(direct_sum.decompose ๐’œ) (x * y) = โ‡‘(direct_sum.decompose ๐’œ) x * โ‡‘(direct_sum.decompose ๐’œ) y
source
@[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))) :
โ‡‘((direct_sum.decompose ๐’œ).symm) (x * y) = โ‡‘((direct_sum.decompose ๐’œ).symm) x * โ‡‘((direct_sum.decompose ๐’œ).symm) y
source
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 : ฮน) :
A โ†’+ A

The projection maps of a graded ring

Equations
source
@[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) :
โ‡‘(graded_ring.proj ๐’œ i) r = โ†‘(โ‡‘(โ‡‘(direct_sum.decompose ๐’œ) r) i)
source
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))
source
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 : ฮน) :
i โˆˆ dfinsupp.support (โ‡‘(direct_sum.decompose ๐’œ) r) โ†” โ‡‘(graded_ring.proj ๐’œ i) r โ‰  0
source
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) :
โ†‘(โ‡‘(โ‡‘(direct_sum.decompose ๐’œ) (a * b)) (i + j)) = a * โ†‘(โ‡‘(โ‡‘(direct_sum.decompose ๐’œ) b) j)
source
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) :
โ†‘(โ‡‘(โ‡‘(direct_sum.decompose ๐’œ) (a * b)) (i + j)) = โ†‘(โ‡‘(โ‡‘(direct_sum.decompose ๐’œ) a) i) * b
source
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} :
โ‡‘(โ‡‘(direct_sum.decompose ๐’œ) (โ†‘a * b)) (i + j) = graded_monoid.ghas_mul.mul a (โ‡‘(โ‡‘(direct_sum.decompose ๐’œ) b) j)
source
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)) :
โ‡‘(โ‡‘(direct_sum.decompose ๐’œ) (a * โ†‘b)) (i + j) = graded_monoid.ghas_mul.mul (โ‡‘(โ‡‘(direct_sum.decompose ๐’œ) a) i) b
source
@[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
source
@[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) :
graded_algebra ๐’œ

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
source
@[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) :
โ‡‘(direct_sum.decompose_alg_equiv ๐’œ) แพฐ = โ‡‘(โ†‘{to_fun := โ‡‘((direct_sum.decompose ๐’œ).symm), inv_fun := โ‡‘(direct_sum.decompose ๐’œ), left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}.symm) แพฐ
source
@[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))) :
โ‡‘((direct_sum.decompose_alg_equiv ๐’œ).symm) แพฐ = โ‡‘((direct_sum.decompose ๐’œ).symm) แพฐ
source
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
source
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 : ฮน) :
A โ†’โ‚—[R] A

The projection maps of graded algebra

Equations
source
@[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) :
โ‡‘(graded_algebra.proj ๐’œ i) r = โ†‘(โ‡‘(โ‡‘(direct_sum.decompose ๐’œ) r) i)
source
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))
source
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 : ฮน) :
i โˆˆ dfinsupp.support (โ‡‘(direct_sum.decompose ๐’œ) r) โ†” โ‡‘(graded_algebra.proj ๐’œ i) r โ‰  0
source
@[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) :
โ‡‘(graded_ring.proj_zero_ring_hom ๐’œ) a = โ†‘(โ‡‘(โ‡‘(direct_sum.decompose ๐’œ) a) 0)
source
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 ๐’œ] :
A โ†’+* A

If A is graded by a canonically ordered add monoid, then the projection map x โ†ฆ xโ‚€ is a ring homomorphism.

Equations
source
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
source
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
source
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) :
โ†‘(โ‡‘(โ‡‘(direct_sum.decompose ๐’œ) (a * b)) n) = a * โ†‘(โ‡‘(โ‡‘(direct_sum.decompose ๐’œ) b) (n - i))
source
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) :
โ†‘(โ‡‘(โ‡‘(direct_sum.decompose ๐’œ) (a * b)) n) = โ†‘(โ‡‘(โ‡‘(direct_sum.decompose ๐’œ) a) (n - i)) * b
source
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
source
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