Documentation

Mathlib.RingTheory.GradedAlgebra.Basic

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 #

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 Semiring.toNatAlgebra, and all Rings are -algebras via Ring.toIntAlgebra.

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.

    Instances
      def DirectSum.decomposeRingEquiv {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddMonoid ι] [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ισ) [GradedRing 𝒜] :
      A ≃+* DirectSum ι fun (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
      Instances For
        @[simp]
        theorem DirectSum.decompose_one {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddMonoid ι] [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ισ) [GradedRing 𝒜] :
        @[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) :
        @[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 : DirectSum ι fun (i : ι) => (𝒜 i)) (y : DirectSum ι fun (i : ι) => (𝒜 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

        Equations
        Instances For
          @[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 : DirectSum ι fun (i : ι) => (𝒜 i)) (i : ι) :
          (GradedRing.proj 𝒜 i) ((DirectSum.decompose 𝒜).symm a) = (DirectSum.decompose 𝒜).symm ((DirectSum.of (fun (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 : (𝒜 i)) → Decidable (x 0)] (r : A) (i : ι) :
          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 : (𝒜 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 : (𝒜 j)) :
          ((DirectSum.decompose 𝒜) (a * b)) (i + j) = GradedMonoid.GMul.mul (((DirectSum.decompose 𝒜) a) i) b
          @[reducible, inline]
          abbrev 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.

          Equations
          Instances For
            @[reducible, inline]
            abbrev 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] DirectSum ι fun (i : ι) => (𝒜 i)) (right_inv : (DirectSum.coeAlgHom 𝒜).comp decompose = AlgHom.id R A) (left_inv : ∀ (i : ι) (x : (𝒜 i)), decompose x = (DirectSum.of (fun (i : ι) => (𝒜 i)) i) x) :

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

            Equations
            Instances For
              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] DirectSum ι fun (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
              Instances For
                @[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) :
                @[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 : DirectSum ι fun (i : ι) => (𝒜 i)) :
                @[simp]
                theorem DirectSum.decompose_algebraMap {ι : Type u_1} {R : Type u_2} {A : Type u_3} [DecidableEq ι] [AddMonoid ι] [CommSemiring R] [Semiring A] [Algebra R A] (𝒜 : ιSubmodule R A) [GradedAlgebra 𝒜] (r : R) :
                (DirectSum.decompose 𝒜) ((algebraMap R A) r) = (algebraMap R (DirectSum ι fun (i : ι) => (𝒜 i))) r
                @[simp]
                theorem DirectSum.decompose_symm_algebraMap {ι : Type u_1} {R : Type u_2} {A : Type u_3} [DecidableEq ι] [AddMonoid ι] [CommSemiring R] [Semiring A] [Algebra R A] (𝒜 : ιSubmodule R A) [GradedAlgebra 𝒜] (r : R) :
                (DirectSum.decompose 𝒜).symm ((algebraMap R (DirectSum ι fun (i : ι) => (𝒜 i))) r) = (algebraMap R A) r
                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 : ι) :

                The projection maps of graded algebra

                Equations
                Instances For
                  @[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 : DirectSum ι fun (i : ι) => (𝒜 i)) (i : ι) :
                  (GradedAlgebra.proj 𝒜 i) ((DirectSum.decompose 𝒜).symm a) = (DirectSum.decompose 𝒜).symm ((DirectSum.of (fun (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 : ι) :
                  @[simp]
                  theorem GradedRing.projZeroRingHom_apply {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [Semiring A] [DecidableEq ι] [CanonicallyOrderedAddCommMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ισ) [GradedRing 𝒜] (a : A) :
                  def GradedRing.projZeroRingHom {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [Semiring A] [DecidableEq ι] [CanonicallyOrderedAddCommMonoid ι] [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.

                  Equations
                  Instances For
                    def GradedRing.projZeroRingHom' {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [Semiring A] [DecidableEq ι] [CanonicallyOrderedAddCommMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ισ) [GradedRing 𝒜] :
                    A →+* (𝒜 0)

                    The ring homomorphism from A to 𝒜 0 sending every a : A to a₀.

                    Equations
                    Instances For
                      @[simp]
                      theorem GradedRing.coe_projZeroRingHom'_apply {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [Semiring A] [DecidableEq ι] [CanonicallyOrderedAddCommMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ισ) [GradedRing 𝒜] (a : A) :
                      @[simp]
                      theorem GradedRing.projZeroRingHom'_apply_coe {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [Semiring A] [DecidableEq ι] [CanonicallyOrderedAddCommMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ισ) [GradedRing 𝒜] (a : (𝒜 0)) :

                      The ring homomorphism GradedRing.projZeroRingHom' 𝒜 is surjective.

                      theorem DirectSum.coe_decompose_mul_of_left_mem_of_not_le {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [Semiring A] [DecidableEq ι] [CanonicallyOrderedAddCommMonoid ι] [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 ι] [CanonicallyOrderedAddCommMonoid ι] [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 ι] [CanonicallyOrderedAddCommMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ισ) [GradedRing 𝒜] {a : A} {b : A} {n : ι} {i : ι} [Sub ι] [OrderedSub ι] [AddLeftReflectLE ι] (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 ι] [CanonicallyOrderedAddCommMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ισ) [GradedRing 𝒜] {a : A} {b : A} {n : ι} {i : ι} [Sub ι] [OrderedSub ι] [AddLeftReflectLE ι] (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 ι] [CanonicallyOrderedAddCommMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ισ) [GradedRing 𝒜] {a : A} {b : A} {i : ι} [Sub ι] [OrderedSub ι] [AddLeftReflectLE ι] (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 ι] [CanonicallyOrderedAddCommMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ισ) [GradedRing 𝒜] {a : A} {b : A} {i : ι} [Sub ι] [OrderedSub ι] [AddLeftReflectLE ι] (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
                      noncomputable def DirectSum.IsInternal.coeAlgEquiv {R : Type u_5} [CommSemiring R] {A : Type u_6} [Semiring A] [Algebra R A] {ι : Type u_7} [DecidableEq ι] [AddMonoid ι] {M : ιSubmodule R A} [SetLike.GradedMonoid M] (hM : DirectSum.IsInternal M) :
                      (DirectSum ι fun (i : ι) => (M i)) ≃ₐ[R] A

                      The canonical isomorphism of an internal direct sum with the ambient algebra

                      Instances For
                        noncomputable def DirectSum.IsInternal.gradedAlgebra {R : Type u_5} [CommSemiring R] {A : Type u_6} [Semiring A] [Algebra R A] {ι : Type u_7} [DecidableEq ι] [AddMonoid ι] {M : ιSubmodule R A} [SetLike.GradedMonoid M] (hM : DirectSum.IsInternal M) :

                        Given an R-algebra A and a family ι → Submodule R A of submodules parameterized by an additive monoid ι and satisfying SetLike.GradedMonoid M (essentially, is multiplicative) such that DirectSum.IsInternal M (A is the direct sum of the M i), we endow A with the structure of a graded algebra. The submodules are the homogeneous parts.

                        Equations
                        • hM.gradedAlgebra = GradedRing.mk
                        Instances For