Documentation

TauCeti.RingTheory.GradedAlgebra.HomogeneousLocalization.Basic

Coefficients and lifts for homogeneous localizations #

For a graded ring A, an element f : A and a ring homomorphism ฯ† : A โ†’+* R with ฯ† f a unit, HomogeneousLocalization.Away.lift ๐’œ ฯ† hf is the ring homomorphism A_{(f)} โ†’+* R sending a / fโฟ to ฯ† a / (ฯ† f)โฟ: the restriction to the degree-zero part A_{(f)} of the lift A_f โ†’+* R of ฯ†. Geometrically, when A is โ„•-graded and f is homogeneous of positive degree, Spec A_{(f)} is the standard affine chart Dโ‚Š(f) of Proj A, and Spec of lift is the morphism Spec R โŸถ Dโ‚Š(f) โŠ† Proj A given by the "homogeneous coordinates" ฯ†.

For a graded algebra over a coefficient ring, homogeneous localization inherits the coefficient algebra structure, and fractions with a fixed homogeneous denominator depend linearly on their numerator. This permits scalar extension of the homogeneous affine charts.

Main definitions #

Main results #

Provenance #

HomogeneousLocalization.isReduced is adapted from AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0) at commit c3415f32a313e19ace43e05479aeaa0d56ca287a, file projects/ModularCurves/ModularCurves/ForMathlib/ProjIntegral.lean, declaration AlgebraicGeometry.Proj.isReduced_away, which treats Away ๐’œ f for an โ„•-graded domain; here the localization is at any submonoid and only its reducedness is assumed.

source
noncomputable def HomogeneousLocalization.Away.lift {ฮน : Type u_1} {A : Type u_2} {R : Type u_4} {ฯƒ : Type u_5} [CommRing A] [CommRing R] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] [AddCommMonoid ฮน] [DecidableEq ฮน] (๐’œ : ฮน โ†’ ฯƒ) [GradedRing ๐’œ] (ฯ† : A โ†’+* R) {f : A} (hf : IsUnit (ฯ† f)) :
Away ๐’œ f โ†’+* R

The ring homomorphism A_{(f)} โ†’+* R, a / fโฟ โ†ฆ ฯ† a / (ฯ† f)โฟ, induced by a ring homomorphism ฯ† : A โ†’+* R inverting f: the restriction of the lift A_f โ†’+* R of ฯ† to the degree-zero part A_{(f)} of the localization.

Equations
Instances For
    source
    @[simp]
    theorem HomogeneousLocalization.Away.lift_mk {ฮน : Type u_1} {A : Type u_2} {R : Type u_4} {ฯƒ : Type u_5} [CommRing A] [CommRing R] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] [AddCommMonoid ฮน] [DecidableEq ฮน] {๐’œ : ฮน โ†’ ฯƒ} [GradedRing ๐’œ] (ฯ† : A โ†’+* R) {f : A} (hf : IsUnit (ฯ† f)) {d : ฮน} (hfd : f โˆˆ ๐’œ d) (n : โ„•) (a : A) (ha : a โˆˆ ๐’œ (n โ€ข d)) :
    (lift ๐’œ ฯ† hf) (Away.mk ๐’œ hfd n a ha) = ฯ† a * โ†‘(hf.unit ^ n)โปยน

    Away.lift sends a / fโฟ to ฯ† a / (ฯ† f)โฟ.

    source
    @[simp]
    theorem HomogeneousLocalization.Away.lift_algebraMap {ฮน : Type u_1} {A : Type u_2} {R : Type u_4} {ฯƒ : Type u_5} [CommRing A] [CommRing R] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] [AddCommMonoid ฮน] [DecidableEq ฮน] {๐’œ : ฮน โ†’ ฯƒ} [GradedRing ๐’œ] (ฯ† : A โ†’+* R) {f : A} (hf : IsUnit (ฯ† f)) (a : โ†ฅ(๐’œ 0)) :
    (lift ๐’œ ฯ† hf) ((algebraMap (โ†ฅ(๐’œ 0)) (Away ๐’œ f)) a) = ฯ† โ†‘a

    Away.lift restricts to ฯ† on the degree-zero part ๐’œ 0.

    source
    @[simp]
    theorem RingHom.comp_homogeneousLocalizationAwayLift {ฮน : Type u_1} {A : Type u_2} {R : Type u_4} {ฯƒ : Type u_5} [CommRing A] [CommRing R] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] [AddCommMonoid ฮน] [DecidableEq ฮน] {๐’œ : ฮน โ†’ ฯƒ} [GradedRing ๐’œ] {S : Type u_7} [CommRing S] (ฯˆ : R โ†’+* S) (ฯ† : A โ†’+* R) {f : A} (hf : IsUnit (ฯ† f)) :
    ฯˆ.comp (HomogeneousLocalization.Away.lift ๐’œ ฯ† hf) = HomogeneousLocalization.Away.lift ๐’œ (ฯˆ.comp ฯ†) โ‹ฏ

    Changing the value ring of homogeneous coordinates commutes with the chart lift.

    source
    theorem HomogeneousLocalization.Away.lift_comp_awayMap {ฮน : Type u_1} {A : Type u_2} {R : Type u_4} {ฯƒ : Type u_5} [CommRing A] [CommRing R] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] [AddCommMonoid ฮน] [DecidableEq ฮน] {๐’œ : ฮน โ†’ ฯƒ} [GradedRing ๐’œ] (ฯ† : A โ†’+* R) {e : ฮน} {f g x : A} (hg : g โˆˆ ๐’œ e) (hx : x = f * g) (hฯ†x : IsUnit (ฯ† x)) (hฯ†f : IsUnit (ฯ† f)) :
    (lift ๐’œ ฯ† hฯ†x).comp (awayMap ๐’œ hg hx) = lift ๐’œ ฯ† hฯ†f

    Away.lift is compatible with the restriction awayMap : A_{(f)} โ†’+* A_{(fg)}.

    source
    @[simp]
    theorem HomogeneousLocalization.Away.lift_comp_map {ฮน : Type u_1} {A : Type u_2} {B : Type u_3} {R : Type u_4} {ฯƒ : Type u_5} {ฯ„ : Type u_6} [CommRing A] [CommRing B] [CommRing R] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] [SetLike ฯ„ B] [AddSubgroupClass ฯ„ B] [AddCommMonoid ฮน] [DecidableEq ฮน] {๐’œ : ฮน โ†’ ฯƒ} {โ„ฌ : ฮน โ†’ ฯ„} [GradedRing ๐’œ] [GradedRing โ„ฌ] (ฯ† : B โ†’+* R) (F : ๐’œ โ†’+*แต โ„ฌ) {s : A} (hs : IsUnit (ฯ† (F s))) :
    (lift โ„ฌ ฯ† hs).comp (Away.map F s) = lift ๐’œ (ฯ†.comp โ†‘F) hs

    Away.lift is compatible with the map A_{(s)} โ†’+* B_{(F s)} induced by a graded ring homomorphism F.

    source
    theorem HomogeneousLocalization.Away.lift_eq_of_forall_mem {A : Type u_2} {R : Type u_4} {ฯƒ : Type u_5} [CommRing A] [CommRing R] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] {๐’œ : โ„• โ†’ ฯƒ} [GradedRing ๐’œ] (ฯ† ฯˆ : A โ†’+* R) (c : Rหฃ) (h : โˆ€ (n : โ„•), โˆ€ a โˆˆ ๐’œ n, ฯˆ a = โ†‘c ^ n * ฯ† a) {f : A} {d : โ„•} (hfd : f โˆˆ ๐’œ d) (hฯˆ : IsUnit (ฯˆ f)) (hฯ† : IsUnit (ฯ† f)) :
    lift ๐’œ ฯˆ hฯˆ = lift ๐’œ ฯ† hฯ†

    Rescaling homogeneous coordinates does not change Away.lift: if ฯˆ a = cโฟ ฯ† a for every a of degree n, then ฯ† and ฯˆ induce the same homomorphism A_{(f)} โ†’+* R.

    source
    instance HomogeneousLocalization.isReduced {ฮน : Type u_1} {A : Type u_2} {ฯƒ : Type u_5} [CommRing A] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] [AddCommMonoid ฮน] [DecidableEq ฮน] (๐’œ : ฮน โ†’ ฯƒ) [GradedRing ๐’œ] (x : Submonoid A) [IsReduced (Localization x)] :
    IsReduced (HomogeneousLocalization ๐’œ x)

    A homogeneous localization at x is reduced whenever the localization at x is reduced; in particular, it is reduced whenever the graded ring is.

    source
    @[simp]
    theorem HomogeneousLocalization.val_map {ฮน : Type u_7} {A : Type u_8} {B : Type u_9} {ฯƒ : Type u_10} {ฯ„ : Type u_11} [AddCommMonoid ฮน] [DecidableEq ฮน] [CommRing A] [CommRing B] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] [SetLike ฯ„ B] [AddSubgroupClass ฯ„ B] {๐’œ : ฮน โ†’ ฯƒ} {โ„ฌ : ฮน โ†’ ฯ„} [GradedRing ๐’œ] [GradedRing โ„ฌ] (g : ๐’œ โ†’+*แต โ„ฌ) {P : Submonoid A} {Q : Submonoid B} (h : P โ‰ค Submonoid.comap g Q) (z : HomogeneousLocalization ๐’œ P) :
    ((map g h) z).val = (IsLocalization.map (Localization Q) (โ†‘g) h) z.val

    The homogeneous localization map is the restriction of the ordinary localization map.

    source
    @[simp]
    theorem HomogeneousLocalization.val_fromZeroRingHom {ฮน : Type u_7} {A : Type u_8} {ฯƒ : Type u_9} [AddCommMonoid ฮน] [DecidableEq ฮน] [CommRing A] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] (๐’œ : ฮน โ†’ ฯƒ) [GradedRing ๐’œ] (P : Submonoid A) (a : โ†ฅ(๐’œ 0)) :
    ((fromZeroRingHom ๐’œ P) a).val = (algebraMap A (Localization P)) โ†‘a

    The degree-zero coefficient map sends a to the ordinary fraction a/1.

    source
    @[instance_reducible]
    instance HomogeneousLocalization.algebra {ฮน : Type u_7} {R : Type u_8} {A : Type u_9} [AddCommMonoid ฮน] [DecidableEq ฮน] [CommRing R] [CommRing A] [Algebra R A] (๐’œ : ฮน โ†’ Submodule R A) [GradedAlgebra ๐’œ] (P : Submonoid A) :
    Algebra R (HomogeneousLocalization ๐’œ P)

    Homogeneous localization of a graded algebra is an algebra over its coefficient ring.

    Equations
    • One or more equations did not get rendered due to their size.
    source
    theorem HomogeneousLocalization.algebraMap_eq_comp {ฮน : Type u_7} {R : Type u_8} {A : Type u_9} [AddCommMonoid ฮน] [DecidableEq ฮน] [CommRing R] [CommRing A] [Algebra R A] (๐’œ : ฮน โ†’ Submodule R A) [GradedAlgebra ๐’œ] (P : Submonoid A) :
    algebraMap R (HomogeneousLocalization ๐’œ P) = (fromZeroRingHom ๐’œ P).comp (algebraMap R โ†ฅ(๐’œ 0))

    The coefficient map is the composite through the degree-zero part.

    source
    @[simp]
    theorem HomogeneousLocalization.val_algebraMap {ฮน : Type u_7} {R : Type u_8} {A : Type u_9} [AddCommMonoid ฮน] [DecidableEq ฮน] [CommRing R] [CommRing A] [Algebra R A] (๐’œ : ฮน โ†’ Submodule R A) [GradedAlgebra ๐’œ] (P : Submonoid A) (r : R) :
    ((algebraMap R (HomogeneousLocalization ๐’œ P)) r).val = (algebraMap R (Localization P)) r

    Forgetting homogeneity respects coefficients.

    source
    instance HomogeneousLocalization.isScalarTower {ฮน : Type u_7} {R : Type u_8} {A : Type u_9} [AddCommMonoid ฮน] [DecidableEq ฮน] [CommRing R] [CommRing A] [Algebra R A] (๐’œ : ฮน โ†’ Submodule R A) [GradedAlgebra ๐’œ] (P : Submonoid A) :
    IsScalarTower R (HomogeneousLocalization ๐’œ P) (Localization P)

    The coefficient action factors through homogeneous localization into ordinary localization.

    source
    noncomputable def HomogeneousLocalization.Away.mkLinearMap {ฮน : Type u_7} {R : Type u_8} {A : Type u_9} [AddCommMonoid ฮน] [DecidableEq ฮน] [CommRing R] [CommRing A] [Algebra R A] {๐’œ : ฮน โ†’ Submodule R A} [GradedAlgebra ๐’œ] {f : A} {d : ฮน} (hf : f โˆˆ ๐’œ d) (n : โ„•) :
    โ†ฅ(๐’œ (n โ€ข d)) โ†’โ‚—[R] Away ๐’œ f

    Fractions with a fixed homogeneous denominator depend linearly on the numerator.

    Equations
    Instances For
      source
      @[simp]
      theorem HomogeneousLocalization.Away.mkLinearMap_apply {ฮน : Type u_7} {R : Type u_8} {A : Type u_9} [AddCommMonoid ฮน] [DecidableEq ฮน] [CommRing R] [CommRing A] [Algebra R A] {๐’œ : ฮน โ†’ Submodule R A} [GradedAlgebra ๐’œ] {f : A} {d : ฮน} (hf : f โˆˆ ๐’œ d) (n : โ„•) (a : โ†ฅ(๐’œ (n โ€ข d))) :
      (mkLinearMap hf n) a = Away.mk ๐’œ hf n โ†‘a โ‹ฏ

      The linear numerator map forms the homogeneous fraction with the chosen denominator.