Documentation

TauCeti.RingTheory.GradedAlgebra.Homogeneous.Units

Homogeneous units of a graded ring and shift classes #

Let A be a ring graded by an additive group ฮน, with grading ๐’œ. The degrees of the homogeneous units of A form a subgroup homogeneousUnitDegrees ๐’œ of ฮน, and the quotient ShiftClassGroup ๐’œ classifies the shifts A(d) of the graded A-module A up to graded isomorphism. Here A(d) is A with the grading n โ†ฆ ๐’œ (n + d).

For ฮน = โ„ค, a โ„ค-grading of a commutative ring A is a ๐”พ_m-action on Spec A, and A(d) is the module of sections of the trivial line bundle twisted by the character t โ†ฆ t ^ d. The shift class group is then the group of such twisted trivial line bundles up to equivariant isomorphism.

More generally, a second grading โ„ณ of A, compatible with ๐’œ in the sense that ๐’œ i โ€ข โ„ณ j โ‰ค โ„ณ (i + j), makes A a graded A-module. If โ„ณ has a homogeneous generator, a unit u โˆˆ โ„ณ c, then multiplication by u identifies โ„ณ with the shift A(-c); conversely every grading graded-isomorphic to a shift has such a generator.

Main definitions #

Main results #

The group-algebra and Laurent-polynomial examples, TauCeti.homogeneousUnitDegrees_gradeBy and TauCeti.shiftClassGroupLaurentPolynomialEquiv, are in TauCeti.Algebra.MonoidAlgebra.Grading and TauCeti.Algebra.Polynomial.Laurent.Units.

source
theorem Units.val_inv_mem_graded {ฮน : Type u_1} {A : Type u_2} {ฯƒ : Type u_3} [DecidableEq ฮน] [AddGroup ฮน] [Semiring A] [SetLike ฯƒ A] [AddSubmonoidClass ฯƒ A] {๐’œ : ฮน โ†’ ฯƒ} [GradedRing ๐’œ] (u : Aหฃ) {d : ฮน} (hu : โ†‘u โˆˆ ๐’œ d) :
โ†‘uโปยน โˆˆ ๐’œ (-d)

In a ring graded by an additive group, the inverse of a homogeneous unit of degree d is homogeneous of degree -d.

source
def TauCeti.homogeneousUnitDegrees {ฮน : Type u_1} {A : Type u_2} {ฯƒ : Type u_3} [AddGroup ฮน] [Monoid A] [SetLike ฯƒ A] (๐’œ : ฮน โ†’ ฯƒ) :
AddSubgroup ฮน

The degrees of the homogeneous units of a graded ring: the subgroup of the degree group generated by the degrees d such that some unit lies in ๐’œ d. For a grading by a group, every element of this subgroup is itself the degree of a homogeneous unit (mem_homogeneousUnitDegrees_iff).

Instances For
    source
    theorem TauCeti.mem_homogeneousUnitDegrees_of_mem {ฮน : Type u_1} {A : Type u_2} {ฯƒ : Type u_3} [AddGroup ฮน] [Monoid A] [SetLike ฯƒ A] {๐’œ : ฮน โ†’ ฯƒ} {u : Aหฃ} {d : ฮน} (hu : โ†‘u โˆˆ ๐’œ d) :
    d โˆˆ homogeneousUnitDegrees ๐’œ

    The degree of a homogeneous unit lies in homogeneousUnitDegrees ๐’œ.

    source
    theorem TauCeti.homogeneousUnitDegrees_le_iff {ฮน : Type u_1} {A : Type u_2} {ฯƒ : Type u_3} [AddGroup ฮน] [Monoid A] [SetLike ฯƒ A] {๐’œ : ฮน โ†’ ฯƒ} {H : AddSubgroup ฮน} :
    homogeneousUnitDegrees ๐’œ โ‰ค H โ†” โˆ€ (u : Aหฃ) (d : ฮน), โ†‘u โˆˆ ๐’œ d โ†’ d โˆˆ H

    homogeneousUnitDegrees ๐’œ is the smallest subgroup containing the degree of every homogeneous unit.

    source
    @[simp]
    theorem TauCeti.homogeneousUnitDegrees_eq_top_of_subsingleton {ฮน : Type u_1} {A : Type u_2} {ฯƒ : Type u_3} [AddGroup ฮน] [Semiring A] [SetLike ฯƒ A] [AddSubmonoidClass ฯƒ A] {๐’œ : ฮน โ†’ ฯƒ} [Subsingleton A] :
    homogeneousUnitDegrees ๐’œ = โŠค

    Over the zero ring every degree is the degree of a homogeneous unit, since 1 = 0 lies in every graded piece.

    source
    theorem TauCeti.mem_homogeneousUnitDegrees_iff {ฮน : Type u_1} {A : Type u_2} {ฯƒ : Type u_3} [DecidableEq ฮน] [AddGroup ฮน] [Semiring A] [SetLike ฯƒ A] [AddSubmonoidClass ฯƒ A] {๐’œ : ฮน โ†’ ฯƒ} [GradedRing ๐’œ] {d : ฮน} :
    d โˆˆ homogeneousUnitDegrees ๐’œ โ†” โˆƒ (u : Aหฃ), โ†‘u โˆˆ ๐’œ d

    In a ring graded by an additive group, a degree lies in homogeneousUnitDegrees ๐’œ if and only if it is the degree of a homogeneous unit: products and inverses of homogeneous units are homogeneous units, so the generating set is already a subgroup.

    source
    @[reducible, inline]
    abbrev TauCeti.ShiftClassGroup {ฮน : Type u_1} {A : Type u_2} {ฯƒ : Type u_3} [AddCommGroup ฮน] [Monoid A] [SetLike ฯƒ A] (๐’œ : ฮน โ†’ ฯƒ) :
    Type u_1

    The shift classes of a graded ring: the degree group modulo the degrees of the homogeneous units. The shifts A(d) and A(e) of the graded module A are graded-isomorphic exactly when d and e have the same class (ShiftClassGroup.mk_eq_mk_iff).

    Instances For
      source
      theorem TauCeti.mul_mem_iff_of_isUnit_mem {ฮน : Type u_1} {A : Type u_2} {ฯƒ : Type u_3} {ฯƒM : Type u_4} [DecidableEq ฮน] [Semiring A] [SetLike ฯƒ A] [AddSubmonoidClass ฯƒ A] [SetLike ฯƒM A] [AddGroup ฮน] (๐’œ : ฮน โ†’ ฯƒ) [GradedRing ๐’œ] (โ„ณ : ฮน โ†’ ฯƒM) [AddSubmonoidClass ฯƒM A] [DirectSum.Decomposition โ„ณ] [SetLike.GradedSMul ๐’œ โ„ณ] {u : A} (hu : IsUnit u) {c : ฮน} (hmem : u โˆˆ โ„ณ c) {n : ฮน} {x : A} :
      x * u โˆˆ โ„ณ n โ†” x โˆˆ ๐’œ (n - c)

      Shift classification. Let โ„ณ be a grading of A, viewed as a graded module over A graded by ๐’œ, with a homogeneous generator: a unit u โˆˆ โ„ณ c. Then x * u โˆˆ โ„ณ n if and only if x โˆˆ ๐’œ (n - c), so that multiplication by u carries the shift A(-c) isomorphically onto โ„ณ.

      source
      theorem TauCeti.exists_linearEquiv_of_isUnit_mem {ฮน : Type u_1} {A : Type u_2} {ฯƒ : Type u_3} {ฯƒM : Type u_4} [DecidableEq ฮน] [Semiring A] [SetLike ฯƒ A] [AddSubmonoidClass ฯƒ A] [SetLike ฯƒM A] [AddGroup ฮน] (๐’œ : ฮน โ†’ ฯƒ) [GradedRing ๐’œ] (โ„ณ : ฮน โ†’ ฯƒM) [AddSubmonoidClass ฯƒM A] [DirectSum.Decomposition โ„ณ] [SetLike.GradedSMul ๐’œ โ„ณ] {u : A} (hu : IsUnit u) {c : ฮน} (hmem : u โˆˆ โ„ณ c) :
      โˆƒ (ฯ† : A โ‰ƒโ‚—[A] A), โˆ€ (n : ฮน) (x : A), ฯ† x โˆˆ โ„ณ n โ†” x โˆˆ ๐’œ (n - c)

      Linear form of the shift classification: a grading โ„ณ of A compatible with ๐’œ with a homogeneous unit u โˆˆ โ„ณ c is the image of the shift A(-c) under multiplication by u.

      source
      theorem LinearEquiv.isUnit_apply_one_and_apply_one_mem {ฮน : Type u_1} {A : Type u_2} {ฯƒ : Type u_3} {ฯƒM : Type u_4} [DecidableEq ฮน] [Semiring A] [SetLike ฯƒ A] [AddSubmonoidClass ฯƒ A] [SetLike ฯƒM A] [AddGroup ฮน] {๐’œ : ฮน โ†’ ฯƒ} [GradedRing ๐’œ] {โ„ณ : ฮน โ†’ ฯƒM} {d : ฮน} (ฯ† : A โ‰ƒโ‚—[A] A) (hฯ† : โˆ€ (n : ฮน) (x : A), ฯ† x โˆˆ โ„ณ n โ†” x โˆˆ ๐’œ (n + d)) :
      IsUnit (ฯ† 1) โˆง ฯ† 1 โˆˆ โ„ณ (-d)

      A graded isomorphism from a shift A(d) onto a grading โ„ณ of A sends 1 to a homogeneous generator of โ„ณ: a unit of degree -d.

      source
      theorem TauCeti.exists_linearEquiv_iff_exists_isUnit_mem {ฮน : Type u_1} {A : Type u_2} {ฯƒ : Type u_3} {ฯƒM : Type u_4} [DecidableEq ฮน] [Semiring A] [SetLike ฯƒ A] [AddSubmonoidClass ฯƒ A] [SetLike ฯƒM A] [AddGroup ฮน] (๐’œ : ฮน โ†’ ฯƒ) [GradedRing ๐’œ] (โ„ณ : ฮน โ†’ ฯƒM) [AddSubmonoidClass ฯƒM A] [DirectSum.Decomposition โ„ณ] [SetLike.GradedSMul ๐’œ โ„ณ] {d : ฮน} :
      (โˆƒ (ฯ† : A โ‰ƒโ‚—[A] A), โˆ€ (n : ฮน) (x : A), ฯ† x โˆˆ โ„ณ n โ†” x โˆˆ ๐’œ (n + d)) โ†” โˆƒ (u : A), IsUnit u โˆง u โˆˆ โ„ณ (-d)

      A grading โ„ณ of A compatible with ๐’œ is graded-isomorphic to the shift A(d), whose degree-n piece is ๐’œ (n + d), if and only if it has a homogeneous generator of degree -d: a unit lying in โ„ณ (-d).

      source
      theorem TauCeti.sub_mem_homogeneousUnitDegrees_iff {ฮน : Type u_1} {A : Type u_2} {ฯƒ : Type u_3} [DecidableEq ฮน] [Semiring A] [SetLike ฯƒ A] [AddSubmonoidClass ฯƒ A] [AddCommGroup ฮน] (๐’œ : ฮน โ†’ ฯƒ) [GradedRing ๐’œ] {d e : ฮน} :
      d - e โˆˆ homogeneousUnitDegrees ๐’œ โ†” โˆƒ (ฯ† : A โ‰ƒโ‚—[A] A), โˆ€ (n : ฮน) (x : A), ฯ† x โˆˆ ๐’œ (n + e) โ†” x โˆˆ ๐’œ (n + d)

      Classification of shifts. The shifts A(d) and A(e) of the graded module A, with degree-n pieces ๐’œ (n + d) and ๐’œ (n + e), are graded-isomorphic if and only if d - e is the degree of a homogeneous unit.

      source
      theorem TauCeti.ShiftClassGroup.mk_eq_mk_iff {ฮน : Type u_1} {A : Type u_2} {ฯƒ : Type u_3} [DecidableEq ฮน] [Semiring A] [SetLike ฯƒ A] [AddSubmonoidClass ฯƒ A] [AddCommGroup ฮน] (๐’œ : ฮน โ†’ ฯƒ) [GradedRing ๐’œ] {d e : ฮน} :
      โ†‘d = โ†‘e โ†” โˆƒ (ฯ† : A โ‰ƒโ‚—[A] A), โˆ€ (n : ฮน) (x : A), ฯ† x โˆˆ ๐’œ (n + e) โ†” x โˆˆ ๐’œ (n + d)

      The shifts A(d) and A(e) are graded-isomorphic exactly when d and e have the same shift class.

      source
      theorem TauCeti.eq_map_mulLeft_of_isUnit_mem {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [DecidableEq ฮน] [AddGroup ฮน] [CommSemiring R] [CommSemiring A] [Algebra R A] (๐’œ โ„ณ : ฮน โ†’ Submodule R A) [GradedAlgebra ๐’œ] [DirectSum.Decomposition โ„ณ] [SetLike.GradedSMul ๐’œ โ„ณ] {u : A} (hu : IsUnit u) {c : ฮน} (hmem : u โˆˆ โ„ณ c) (n : ฮน) :
      โ„ณ n = Submodule.map (LinearMap.mulLeft R u) (๐’œ (n - c))

      Shift classification, submodule form. If a grading โ„ณ of a commutative algebra A, compatible with the grading ๐’œ, has a homogeneous unit u โˆˆ โ„ณ c, then โ„ณ n = u โ€ข ๐’œ (n - c) for every n: the graded module (A, โ„ณ) is the shift A(-c).