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 algebraNat, and all Rings are โ„ค-algebras via algebraInt.

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 ๐’œ] :
        (DirectSum.decompose ๐’œ) 1 = 1
        @[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) :
        (DirectSum.decompose ๐’œ) (x * y) = (DirectSum.decompose ๐’œ) x * (DirectSum.decompose ๐’œ) y
        @[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 : ฮน) :

        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) :
            GradedAlgebra ๐’œ

            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)) :
                (DirectSum.decomposeAlgEquiv ๐’œ).symm a = (DirectSum.decompose ๐’œ).symm a
                @[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) :
                  (GradedRing.projZeroRingHom ๐’œ) a = โ†‘(((DirectSum.decompose ๐’œ) a) 0)
                  def GradedRing.projZeroRingHom {ฮน : Type u_1} {A : Type u_3} {ฯƒ : Type u_4} [Semiring A] [DecidableEq ฮน] [CanonicallyOrderedAddCommMonoid ฮน] [SetLike ฯƒ A] [AddSubmonoidClass ฯƒ A] (๐’œ : ฮน โ†’ ฯƒ) [GradedRing ๐’œ] :

                  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) :
                      โ†‘((GradedRing.projZeroRingHom' ๐’œ) a) = (GradedRing.projZeroRingHom ๐’œ) 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)) :
                      (GradedRing.projZeroRingHom' ๐’œ) โ†‘a = a
                      theorem GradedRing.projZeroRingHom'_surjective {ฮน : Type u_1} {A : Type u_3} {ฯƒ : Type u_4} [Semiring A] [DecidableEq ฮน] [CanonicallyOrderedAddCommMonoid ฮน] [SetLike ฯƒ A] [AddSubmonoidClass ฯƒ A] (๐’œ : ฮน โ†’ ฯƒ) [GradedRing ๐’œ] :

                      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 ฮน] [ContravariantClass ฮน ฮน (fun (x x_1 : ฮน) => x + x_1) fun (x x_1 : ฮน) => x โ‰ค x_1] (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 ฮน] [ContravariantClass ฮน ฮน (fun (x x_1 : ฮน) => x + x_1) fun (x x_1 : ฮน) => x โ‰ค x_1] (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 ฮน] [ContravariantClass ฮน ฮน (fun (x x_1 : ฮน) => x + x_1) fun (x x_1 : ฮน) => x โ‰ค x_1] (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 ฮน] [ContravariantClass ฮน ฮน (fun (x x_1 : ฮน) => x + x_1) fun (x x_1 : ฮน) => x โ‰ค x_1] (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