Documentation

TauCeti.RingTheory.GradedAlgebra.Subalgebra

The grading of a homogeneous subalgebra #

Let ๐’œ : ฮน โ†’ Submodule R A be a grading of an R-algebra A and let T be an R-subalgebra of A which is homogeneous in Mathlib's sense (DirectSum.SetLike.IsHomogeneous ๐’œ T): every homogeneous component of an element of T lies in T. Then T is itself a graded algebra, with degree-i piece the elements of T lying in ๐’œ i, and the inclusion T โ†’ A is a homomorphism of graded algebras which commutes with taking homogeneous components.

Typical homogeneous subalgebras are rings of invariants of a grading-preserving action, and the algebra descended from a grading-preserving descent datum; the second is the graded algebra underlying effective descent for projective spectra.

Main definitions #

Main results #

source
def Subalgebra.grading {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (T : Subalgebra R A) (๐’œ : ฮน โ†’ Submodule R A) (i : ฮน) :
Submodule R โ†ฅT

The grading of a subalgebra T induced by a grading ๐’œ of the ambient algebra: its degree-i piece consists of the elements of T which lie in ๐’œ i.

Instances For
    source
    @[simp]
    theorem Subalgebra.mem_grading_iff {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (T : Subalgebra R A) (๐’œ : ฮน โ†’ Submodule R A) {i : ฮน} {x : โ†ฅT} :
    x โˆˆ T.grading ๐’œ i โ†” โ†‘x โˆˆ ๐’œ i
    source
    theorem Subalgebra.map_val_grading {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (T : Subalgebra R A) (๐’œ : ฮน โ†’ Submodule R A) (i : ฮน) :
    Submodule.map T.val.toLinearMap (T.grading ๐’œ i) = toSubmodule T โŠ“ ๐’œ i

    The inclusion T โ†’ A carries the degree-i piece of the induced grading of T onto T โˆฉ ๐’œ i.

    source
    theorem Subalgebra.finrank_grading {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (T : Subalgebra R A) (๐’œ : ฮน โ†’ Submodule R A) (i : ฮน) :
    Module.finrank R โ†ฅ(T.grading ๐’œ i) = Module.finrank R โ†ฅ(toSubmodule T โŠ“ ๐’œ i)

    The degree-i piece of the induced grading of T has the rank of T โˆฉ ๐’œ i.

    source
    instance Subalgebra.instGradedMonoidSubtypeMemSubmoduleGrading {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [AddMonoid ฮน] [CommSemiring R] [Semiring A] [Algebra R A] (T : Subalgebra R A) (๐’œ : ฮน โ†’ Submodule R A) [SetLike.GradedMonoid ๐’œ] :
    SetLike.GradedMonoid (T.grading ๐’œ)
    source
    theorem Subalgebra.isInternal_grading {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [DecidableEq ฮน] [AddMonoid ฮน] [CommSemiring R] [Semiring A] [Algebra R A] {T : Subalgebra R A} {๐’œ : ฮน โ†’ Submodule R A} [GradedAlgebra ๐’œ] (hT : DirectSum.SetLike.IsHomogeneous ๐’œ T) :
    DirectSum.IsInternal (T.grading ๐’œ)

    The grading of a homogeneous subalgebra induced by the ambient grading is internal: every element of T is uniquely a finite sum of elements of T lying in the pieces ๐’œ i.

    source
    @[instance_reducible]
    noncomputable def Subalgebra.gradedAlgebra {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [DecidableEq ฮน] [AddMonoid ฮน] [CommSemiring R] [Semiring A] [Algebra R A] {T : Subalgebra R A} {๐’œ : ฮน โ†’ Submodule R A} [GradedAlgebra ๐’œ] (hT : DirectSum.SetLike.IsHomogeneous ๐’œ T) :
    GradedAlgebra (T.grading ๐’œ)

    A homogeneous subalgebra is a graded algebra, graded by its intersections with the pieces of the ambient grading.

    Instances For
      source
      def Subalgebra.gradedVal {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [DecidableEq ฮน] [AddMonoid ฮน] [CommSemiring R] [Semiring A] [Algebra R A] (T : Subalgebra R A) (๐’œ : ฮน โ†’ Submodule R A) [GradedAlgebra ๐’œ] [GradedAlgebra (T.grading ๐’œ)] :
      T.grading ๐’œ โ†’โ‚แต[R] ๐’œ

      The inclusion of a subalgebra into the ambient algebra, as a homomorphism of graded algebras for the induced grading.

      Instances For
        source
        @[simp]
        theorem Subalgebra.coe_gradedVal {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [DecidableEq ฮน] [AddMonoid ฮน] [CommSemiring R] [Semiring A] [Algebra R A] (T : Subalgebra R A) (๐’œ : ฮน โ†’ Submodule R A) [GradedAlgebra ๐’œ] [GradedAlgebra (T.grading ๐’œ)] :
        โ‡‘(T.gradedVal ๐’œ) = Subtype.val
        source
        @[simp]
        theorem Subalgebra.coe_decompose_grading {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [DecidableEq ฮน] [AddMonoid ฮน] [CommSemiring R] [Semiring A] [Algebra R A] (T : Subalgebra R A) (๐’œ : ฮน โ†’ Submodule R A) [GradedAlgebra ๐’œ] [GradedAlgebra (T.grading ๐’œ)] (x : โ†ฅT) (i : ฮน) :
        โ†‘โ†‘(((DirectSum.decompose (T.grading ๐’œ)) x) i) = โ†‘(((DirectSum.decompose ๐’œ) โ†‘x) i)

        The homogeneous components of an element of a graded subalgebra are its homogeneous components in the ambient algebra.

        source
        theorem Subalgebra.toIdeal_irrelevant_grading {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [DecidableEq ฮน] [AddCommMonoid ฮน] [PartialOrder ฮน] [CanonicallyOrderedAdd ฮน] [CommSemiring R] [CommSemiring A] [Algebra R A] (T : Subalgebra R A) (๐’œ : ฮน โ†’ Submodule R A) [GradedAlgebra ๐’œ] [GradedAlgebra (T.grading ๐’œ)] :
        (HomogeneousIdeal.irrelevant (T.grading ๐’œ)).toIdeal = Ideal.under (โ†ฅT) (HomogeneousIdeal.irrelevant ๐’œ).toIdeal

        The irrelevant ideal of a subalgebra for the induced grading is the contraction of the irrelevant ideal of the ambient algebra: an element of T has zero degree-zero component in T exactly when it does in A.