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 #
graded_ring 𝒜: the typeclass, which is a combination ofset_like.graded_monoid, anddirect_sum.decomposition 𝒜.graded_algebra 𝒜: A convenience alias forgraded_ringwhen𝒜is a family of submodules.direct_sum.decompose_ring_equiv 𝒜 : A ≃ₐ[R] ⨁ i, 𝒜 i, a more bundled version ofdirect_sum.decompose 𝒜.direct_sum.decompose_alg_equiv 𝒜 : A ≃ₐ[R] ⨁ i, 𝒜 i, a more bundled version ofdirect_sum.decompose 𝒜.graded_algebra.proj 𝒜 iis the linear map fromAto its degreei : ιcomponent, such thatproj 𝒜 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 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)
- to_graded_monoid : set_like.graded_monoid 𝒜
- to_decomposition : direct_sum.decomposition 𝒜
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.
@[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
@[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
@[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
@[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
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
@[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)
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 : ι) :
i ∈ dfinsupp.support (⇑(direct_sum.decompose 𝒜) r) ↔ ⇑(graded_ring.proj 𝒜 i) r ≠ 0
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} :
⇑(⇑(direct_sum.decompose 𝒜) (↑a * b)) (i + j) = graded_monoid.ghas_mul.mul a (⇑(⇑(direct_sum.decompose 𝒜) b) j)
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
@[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
- graded_algebra.of_alg_hom 𝒜 decompose right_inv left_inv = graded_ring.mk
@[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))) :
⇑((direct_sum.decompose_alg_equiv 𝒜).symm) ᾰ = ⇑((direct_sum.decompose 𝒜).symm) ᾰ
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.
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
- graded_algebra.proj 𝒜 i = (𝒜 i).subtype.comp ((dfinsupp.lapply i).comp (direct_sum.decompose_alg_equiv 𝒜).to_alg_hom.to_linear_map)
@[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)
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 : ι) :
i ∈ dfinsupp.support (⇑(direct_sum.decompose 𝒜) r) ↔ ⇑(graded_algebra.proj 𝒜 i) r ≠ 0
@[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)
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.
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) :
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) :
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) :
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) :
