Documentation

Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Homogeneous Localization #

Notation #

Main definitions and results #

This file constructs the subring of Aₓ where the numerator and denominator have the same grading, i.e. {a/b ∈ Aₓ | ∃ (i : ι), a ∈ 𝒜ᵢ ∧ b ∈ 𝒜ᵢ}.

However NumDenSameDeg 𝒜 x cannot have a ring structure for many reasons, for example if c is a NumDenSameDeg, then generally, c + (-c) is not necessarily 0 for degree reasons --- 0 is considered to have grade zero (see deg_zero) but c + (-c) has the same degree as c. To circumvent this, we quotient NumDenSameDeg 𝒜 x by the kernel of c ↦ c.num / c.den.

References #

structure HomogeneousLocalization.NumDenSameDeg {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ιSubmodule R A) (x : Submonoid A) :
Type (max u_1 u_3)

Let x be a submonoid of A, then NumDenSameDeg 𝒜 x is a structure with a numerator and a denominator with same grading such that the denominator is contained in x.

  • deg : ι
  • num : (𝒜 self.deg)
  • den : (𝒜 self.deg)
  • den_mem : self.den x
theorem HomogeneousLocalization.NumDenSameDeg.ext {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) {c1 c2 : NumDenSameDeg 𝒜 x} (hdeg : c1.deg = c2.deg) (hnum : c1.num = c2.num) (hden : c1.den = c2.den) :
c1 = c2
theorem HomogeneousLocalization.NumDenSameDeg.ext_iff {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} {x : Submonoid A} {c1 c2 : NumDenSameDeg 𝒜 x} :
c1 = c2 c1.deg = c2.deg c1.num = c2.num c1.den = c2.den
instance HomogeneousLocalization.NumDenSameDeg.instNeg {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) :
Equations
@[simp]
theorem HomogeneousLocalization.NumDenSameDeg.deg_neg {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) (c : NumDenSameDeg 𝒜 x) :
(-c).deg = c.deg
@[simp]
theorem HomogeneousLocalization.NumDenSameDeg.num_neg {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) (c : NumDenSameDeg 𝒜 x) :
(-c).num = -c.num
@[simp]
theorem HomogeneousLocalization.NumDenSameDeg.den_neg {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) (c : NumDenSameDeg 𝒜 x) :
(-c).den = c.den
instance HomogeneousLocalization.NumDenSameDeg.instSMul {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) {α : Type u_4} [SMul α R] [SMul α A] [IsScalarTower α R A] :
SMul α (NumDenSameDeg 𝒜 x)
Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem HomogeneousLocalization.NumDenSameDeg.deg_smul {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) {α : Type u_4} [SMul α R] [SMul α A] [IsScalarTower α R A] (c : NumDenSameDeg 𝒜 x) (m : α) :
(m c).deg = c.deg
@[simp]
theorem HomogeneousLocalization.NumDenSameDeg.num_smul {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) {α : Type u_4} [SMul α R] [SMul α A] [IsScalarTower α R A] (c : NumDenSameDeg 𝒜 x) (m : α) :
(m c).num = m c.num
@[simp]
theorem HomogeneousLocalization.NumDenSameDeg.den_smul {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) {α : Type u_4} [SMul α R] [SMul α A] [IsScalarTower α R A] (c : NumDenSameDeg 𝒜 x) (m : α) :
(m c).den = c.den
instance HomogeneousLocalization.NumDenSameDeg.instOne {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] :
Equations
@[simp]
theorem HomogeneousLocalization.NumDenSameDeg.deg_one {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] :
deg 1 = 0
@[simp]
theorem HomogeneousLocalization.NumDenSameDeg.num_one {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] :
(num 1) = 1
@[simp]
theorem HomogeneousLocalization.NumDenSameDeg.den_one {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] :
(den 1) = 1
instance HomogeneousLocalization.NumDenSameDeg.instZero {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] :
Equations
@[simp]
theorem HomogeneousLocalization.NumDenSameDeg.deg_zero {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] :
deg 0 = 0
@[simp]
theorem HomogeneousLocalization.NumDenSameDeg.num_zero {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] :
num 0 = 0
@[simp]
theorem HomogeneousLocalization.NumDenSameDeg.den_zero {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] :
(den 0) = 1
instance HomogeneousLocalization.NumDenSameDeg.instMul {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] :
Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem HomogeneousLocalization.NumDenSameDeg.deg_mul {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] (c1 c2 : NumDenSameDeg 𝒜 x) :
(c1 * c2).deg = c1.deg + c2.deg
@[simp]
theorem HomogeneousLocalization.NumDenSameDeg.num_mul {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] (c1 c2 : NumDenSameDeg 𝒜 x) :
(c1 * c2).num = c1.num * c2.num
@[simp]
theorem HomogeneousLocalization.NumDenSameDeg.den_mul {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] (c1 c2 : NumDenSameDeg 𝒜 x) :
(c1 * c2).den = c1.den * c2.den
instance HomogeneousLocalization.NumDenSameDeg.instAdd {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] :
Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem HomogeneousLocalization.NumDenSameDeg.deg_add {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] (c1 c2 : NumDenSameDeg 𝒜 x) :
(c1 + c2).deg = c1.deg + c2.deg
@[simp]
theorem HomogeneousLocalization.NumDenSameDeg.num_add {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] (c1 c2 : NumDenSameDeg 𝒜 x) :
(c1 + c2).num = c1.den * c2.num + c2.den * c1.num
@[simp]
theorem HomogeneousLocalization.NumDenSameDeg.den_add {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] (c1 c2 : NumDenSameDeg 𝒜 x) :
(c1 + c2).den = c1.den * c2.den
instance HomogeneousLocalization.NumDenSameDeg.instCommMonoid {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] :
Equations
  • One or more equations did not get rendered due to their size.
instance HomogeneousLocalization.NumDenSameDeg.instPowNat {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] :
Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem HomogeneousLocalization.NumDenSameDeg.deg_pow {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] (c : NumDenSameDeg 𝒜 x) (n : ) :
(c ^ n).deg = n c.deg
@[simp]
theorem HomogeneousLocalization.NumDenSameDeg.num_pow {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] (c : NumDenSameDeg 𝒜 x) (n : ) :
(c ^ n).num = c.num ^ n
@[simp]
theorem HomogeneousLocalization.NumDenSameDeg.den_pow {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] (c : NumDenSameDeg 𝒜 x) (n : ) :
(c ^ n).den = c.den ^ n
def HomogeneousLocalization.NumDenSameDeg.embedding {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ιSubmodule R A) (x : Submonoid A) (p : NumDenSameDeg 𝒜 x) :

For x : prime ideal of A and any p : NumDenSameDeg 𝒜 x, or equivalent a numerator and a denominator of the same degree, we get an element p.num / p.den of Aₓ.

Equations
def HomogeneousLocalization {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ιSubmodule R A) (x : Submonoid A) :
Type (max u_1 u_3)

For x : prime ideal of A, HomogeneousLocalization 𝒜 x is NumDenSameDeg 𝒜 x modulo the kernel of embedding 𝒜 x. This is essentially the subring of Aₓ where the numerator and denominator share the same grading.

Equations
@[reducible, inline]
abbrev HomogeneousLocalization.mk {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} {x : Submonoid A} (y : NumDenSameDeg 𝒜 x) :

Construct an element of HomogeneousLocalization 𝒜 x from a homogeneous fraction.

Equations
theorem HomogeneousLocalization.mk_surjective {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} {x : Submonoid A} :
def HomogeneousLocalization.val {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} {x : Submonoid A} (y : HomogeneousLocalization 𝒜 x) :

View an element of HomogeneousLocalization 𝒜 x as an element of Aₓ by forgetting that the numerator and denominator are of the same grading.

Equations
@[simp]
theorem HomogeneousLocalization.val_mk {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} {x : Submonoid A} (i : NumDenSameDeg 𝒜 x) :
(mk i).val = Localization.mk i.num i.den,
theorem HomogeneousLocalization.val_injective {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) :
theorem HomogeneousLocalization.val_injective_iff {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} {x : Submonoid A} {a₁ a₂ : HomogeneousLocalization 𝒜 x} :
a₁ = a₂ a₁.val = a₂.val
theorem HomogeneousLocalization.subsingleton {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ιSubmodule R A) {x : Submonoid A} (hx : 0 x) :
instance HomogeneousLocalization.instSMul {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) {α : Type u_4} [SMul α R] [SMul α A] [IsScalarTower α R A] [IsScalarTower α A A] :
Equations
@[simp]
theorem HomogeneousLocalization.mk_smul {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) {α : Type u_4} [SMul α R] [SMul α A] [IsScalarTower α R A] [IsScalarTower α A A] (i : NumDenSameDeg 𝒜 x) (m : α) :
mk (m i) = m mk i
@[simp]
theorem HomogeneousLocalization.val_smul {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) {α : Type u_4} [SMul α R] [SMul α A] [IsScalarTower α R A] [IsScalarTower α A A] (n : α) (y : HomogeneousLocalization 𝒜 x) :
(n y).val = n y.val
theorem HomogeneousLocalization.val_nsmul {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) (n : ) (y : HomogeneousLocalization 𝒜 x) :
(n y).val = n y.val
theorem HomogeneousLocalization.val_zsmul {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) (n : ) (y : HomogeneousLocalization 𝒜 x) :
(n y).val = n y.val
instance HomogeneousLocalization.instNeg {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) :
Equations
@[simp]
theorem HomogeneousLocalization.mk_neg {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) (i : NumDenSameDeg 𝒜 x) :
mk (-i) = -mk i
@[simp]
theorem HomogeneousLocalization.val_neg {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} {x : Submonoid A} (y : HomogeneousLocalization 𝒜 x) :
(-y).val = -y.val
instance HomogeneousLocalization.hasPow {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] :
Equations
@[simp]
theorem HomogeneousLocalization.mk_pow {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] (i : NumDenSameDeg 𝒜 x) (n : ) :
mk (i ^ n) = mk i ^ n
instance HomogeneousLocalization.instAdd {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] :
Equations
@[simp]
theorem HomogeneousLocalization.mk_add {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] (i j : NumDenSameDeg 𝒜 x) :
mk (i + j) = mk i + mk j
instance HomogeneousLocalization.instSub {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] :
Equations
instance HomogeneousLocalization.instMul {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] :
Equations
@[simp]
theorem HomogeneousLocalization.mk_mul {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] (i j : NumDenSameDeg 𝒜 x) :
mk (i * j) = mk i * mk j
instance HomogeneousLocalization.instOne {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] :
Equations
@[simp]
theorem HomogeneousLocalization.mk_one {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] :
mk 1 = 1
instance HomogeneousLocalization.instZero {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] :
Equations
@[simp]
theorem HomogeneousLocalization.mk_zero {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] :
mk 0 = 0
theorem HomogeneousLocalization.zero_eq {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] :
theorem HomogeneousLocalization.one_eq {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} (x : Submonoid A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] :
@[simp]
theorem HomogeneousLocalization.val_zero {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} {x : Submonoid A} [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] :
val 0 = 0
@[simp]
theorem HomogeneousLocalization.val_one {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} {x : Submonoid A} [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] :
val 1 = 1
@[simp]
theorem HomogeneousLocalization.val_add {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} {x : Submonoid A} [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] (y1 y2 : HomogeneousLocalization 𝒜 x) :
(y1 + y2).val = y1.val + y2.val
@[simp]
theorem HomogeneousLocalization.val_mul {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} {x : Submonoid A} [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] (y1 y2 : HomogeneousLocalization 𝒜 x) :
(y1 * y2).val = y1.val * y2.val
@[simp]
theorem HomogeneousLocalization.val_sub {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} {x : Submonoid A} [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] (y1 y2 : HomogeneousLocalization 𝒜 x) :
(y1 - y2).val = y1.val - y2.val
@[simp]
theorem HomogeneousLocalization.val_pow {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} {x : Submonoid A} [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] (y : HomogeneousLocalization 𝒜 x) (n : ) :
(y ^ n).val = y.val ^ n
instance HomogeneousLocalization.instNatCast {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} {x : Submonoid A} [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] :
Equations
instance HomogeneousLocalization.instIntCast {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} {x : Submonoid A} [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] :
Equations
@[simp]
theorem HomogeneousLocalization.val_natCast {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} {x : Submonoid A} [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] (n : ) :
(↑n).val = n
@[simp]
theorem HomogeneousLocalization.val_intCast {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} {x : Submonoid A} [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] (n : ) :
(↑n).val = n
instance HomogeneousLocalization.homogeneousLocalizationAlgebra {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} {x : Submonoid A} [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] :
Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem HomogeneousLocalization.algebraMap_apply {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} {x : Submonoid A} [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] (y : HomogeneousLocalization 𝒜 x) :
theorem HomogeneousLocalization.mk_eq_zero_of_num {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} {x : Submonoid A} [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] (f : NumDenSameDeg 𝒜 x) (h : f.num = 0) :
mk f = 0
theorem HomogeneousLocalization.mk_eq_zero_of_den {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} {x : Submonoid A} [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] (f : NumDenSameDeg 𝒜 x) (h : f.den = 0) :
mk f = 0
def HomogeneousLocalization.fromZeroRingHom {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ιSubmodule R A) (x : Submonoid A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] :
(𝒜 0) →+* HomogeneousLocalization 𝒜 x

The map from 𝒜 0 to the degree 0 part of 𝒜ₓ sending f ↦ f/1.

Equations
  • One or more equations did not get rendered due to their size.
theorem HomogeneousLocalization.algebraMap_eq {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} {x : Submonoid A} [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] :
algebraMap (↥(𝒜 0)) (HomogeneousLocalization 𝒜 x) = fromZeroRingHom 𝒜 x
def HomogeneousLocalization.num {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} {x : Submonoid A} (f : HomogeneousLocalization 𝒜 x) :
A

Numerator of an element in HomogeneousLocalization x.

Equations
def HomogeneousLocalization.den {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} {x : Submonoid A} (f : HomogeneousLocalization 𝒜 x) :
A

Denominator of an element in HomogeneousLocalization x.

Equations
def HomogeneousLocalization.deg {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} {x : Submonoid A} (f : HomogeneousLocalization 𝒜 x) :
ι

For an element in HomogeneousLocalization x, degree is the natural number i such that 𝒜 i contains both numerator and denominator.

Equations
theorem HomogeneousLocalization.den_mem {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} {x : Submonoid A} (f : HomogeneousLocalization 𝒜 x) :
f.den x
theorem HomogeneousLocalization.num_mem_deg {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} {x : Submonoid A} (f : HomogeneousLocalization 𝒜 x) :
f.num 𝒜 f.deg
theorem HomogeneousLocalization.den_mem_deg {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} {x : Submonoid A} (f : HomogeneousLocalization 𝒜 x) :
f.den 𝒜 f.deg
theorem HomogeneousLocalization.eq_num_div_den {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} {x : Submonoid A} (f : HomogeneousLocalization 𝒜 x) :
theorem HomogeneousLocalization.den_smul_val {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} {x : Submonoid A} (f : HomogeneousLocalization 𝒜 x) :
theorem HomogeneousLocalization.ext_iff_val {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} {x : Submonoid A} (f g : HomogeneousLocalization 𝒜 x) :
f = g f.val = g.val
@[reducible, inline]
abbrev HomogeneousLocalization.AtPrime {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ιSubmodule R A) (𝔭 : Ideal A) [𝔭.IsPrime] :
Type (max u_1 u_3)

Localizing a ring homogeneously at a prime ideal.

Equations
theorem HomogeneousLocalization.isUnit_iff_isUnit_val {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ιSubmodule R A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] (𝔭 : Ideal A) [𝔭.IsPrime] (f : AtPrime 𝒜 𝔭) :
instance HomogeneousLocalization.instNontrivialAtPrime {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ιSubmodule R A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] (𝔭 : Ideal A) [𝔭.IsPrime] :
Nontrivial (AtPrime 𝒜 𝔭)
instance HomogeneousLocalization.isLocalRing {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ιSubmodule R A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] (𝔭 : Ideal A) [𝔭.IsPrime] :
IsLocalRing (AtPrime 𝒜 𝔭)
@[reducible, inline]
abbrev HomogeneousLocalization.Away {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ιSubmodule R A) (f : A) :
Type (max u_1 u_3)

Localizing away from powers of f homogeneously.

Equations
theorem HomogeneousLocalization.Away.eventually_smul_mem {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ιSubmodule R A} {f : A} [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] {m : ι} (hf : f 𝒜 m) (z : Away 𝒜 f) :
∀ᶠ (n : ) in Filter.atTop, f ^ n val z (algebraMap A (Localization (Submonoid.powers f))) '' (𝒜 (n m))
def HomogeneousLocalization.map {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ιSubmodule R A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] {B : Type u_4} [CommRing B] [Algebra R B] ( : ιSubmodule R B) [GradedAlgebra ] {P : Submonoid A} {Q : Submonoid B} (g : A →+* B) (comap_le : P Submonoid.comap g Q) (hg : ∀ (i : ι), a𝒜 i, g a i) :

Let A, B be two graded algebras with the same indexing set and g : A → B be a graded algebra homomorphism (i.e. g(Aₘ) ⊆ Bₘ). Let P ≤ A be a submonoid and Q ≤ B be a submonoid such that P ≤ g⁻¹ Q, then g induce a map from the homogeneous localizations A⁰_P to the homogeneous localizations B⁰_Q.

Equations
  • One or more equations did not get rendered due to their size.
@[reducible, inline]
abbrev HomogeneousLocalization.mapId {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ιSubmodule R A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] {P Q : Submonoid A} (h : P Q) :

Let A be a graded algebra and P ≤ Q be two submonoids, then the homogeneous localization of A at P embeds into the homogeneous localization of A at Q.

Equations
theorem HomogeneousLocalization.map_mk {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ιSubmodule R A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] {B : Type u_4} [CommRing B] [Algebra R B] ( : ιSubmodule R B) [GradedAlgebra ] {P : Submonoid A} {Q : Submonoid B} (g : A →+* B) (comap_le : P Submonoid.comap g Q) (hg : ∀ (i : ι), a𝒜 i, g a i) (x : NumDenSameDeg 𝒜 P) :
(map 𝒜 g comap_le hg) (mk x) = mk { deg := x.deg, num := g x.num, , den := g x.den, , den_mem := }
theorem HomogeneousLocalization.awayMapAux_mk {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ιSubmodule R A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] {f g x : A} (hx : x = f * g) (n : ι) (a : (𝒜 n)) (i : ) (hi : f ^ i 𝒜 n) :
(HomogeneousLocalization.awayMapAux✝ 𝒜 ) (mk { deg := n, num := a, den := f ^ i, hi, den_mem := }) = Localization.mk (a * g ^ i) x ^ i,
theorem HomogeneousLocalization.range_awayMapAux_subset {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ιSubmodule R A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] {e : ι} {f g : A} (hg : g 𝒜 e) {x : A} (hx : x = f * g) :
def HomogeneousLocalization.awayMap {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ιSubmodule R A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] {e : ι} {f g : A} (hg : g 𝒜 e) {x : A} (hx : x = f * g) :
Away 𝒜 f →+* Away 𝒜 x

Given x = f * g with g homogeneous of positive degree, this is the map A_{(f)} → A_{(x)} taking a/f^i to ag^i/(fg)^i.

Equations
theorem HomogeneousLocalization.val_awayMap_eq_aux {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ιSubmodule R A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] {e : ι} {f g : A} (hg : g 𝒜 e) {x : A} (hx : x = f * g) (a : Away 𝒜 f) :
val ((awayMap 𝒜 hg hx) a) = (HomogeneousLocalization.awayMapAux✝ 𝒜 ) a
theorem HomogeneousLocalization.val_awayMap {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ιSubmodule R A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] {e : ι} {f g : A} (hg : g 𝒜 e) {x : A} (hx : x = f * g) (a : Away 𝒜 f) :
theorem HomogeneousLocalization.awayMap_fromZeroRingHom {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ιSubmodule R A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] {e : ι} {f g : A} (hg : g 𝒜 e) {x : A} (hx : x = f * g) (a : (𝒜 0)) :
theorem HomogeneousLocalization.val_awayMap_mk {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ιSubmodule R A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] {e : ι} {f g : A} (hg : g 𝒜 e) {x : A} (hx : x = f * g) (n : ι) (a : (𝒜 n)) (i : ) (hi : f ^ i 𝒜 n) :
val ((awayMap 𝒜 hg hx) (mk { deg := n, num := a, den := f ^ i, hi, den_mem := })) = Localization.mk (a * g ^ i) x ^ i,
def HomogeneousLocalization.awayMapₐ {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ιSubmodule R A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] {e : ι} {f g : A} (hg : g 𝒜 e) {x : A} (hx : x = f * g) :
Away 𝒜 f →ₐ[(𝒜 0)] Away 𝒜 x

Given x = f * g with g homogeneous of positive degree, this is the map A_{(f)} → A_{(x)} taking a/f^i to ag^i/(fg)^i.

Equations
@[simp]
theorem HomogeneousLocalization.awayMapₐ_apply {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ιSubmodule R A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] {e : ι} {f g : A} (hg : g 𝒜 e) {x : A} (hx : x = f * g) (a : Away 𝒜 f) :
(awayMapₐ 𝒜 hg hx) a = (awayMap 𝒜 hg hx) a
def HomogeneousLocalization.Away.mk {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ιSubmodule R A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] {f : A} {d : ι} (hf : f 𝒜 d) (n : ) (x : A) (hx : x 𝒜 (n d)) :
Away 𝒜 f

This is a convenient constructor for Away 𝒜 f when f is homogeneous. Away.mk 𝒜 hf n x hx is the fraction x / f ^ n.

Equations
@[simp]
theorem HomogeneousLocalization.Away.val_mk {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ιSubmodule R A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] {f : A} {d : ι} (n : ) (hf : f 𝒜 d) (x : A) (hx : x 𝒜 (n d)) :
val (Away.mk 𝒜 hf n x hx) = Localization.mk x f ^ n,
theorem HomogeneousLocalization.Away.mk_surjective {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ιSubmodule R A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] {f : A} {d : ι} (hf : f 𝒜 d) (x : Away 𝒜 f) :
∃ (n : ) (a : A) (ha : a 𝒜 (n d)), Away.mk 𝒜 hf n a ha = x
@[simp]
theorem HomogeneousLocalization.awayMap_mk {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ιSubmodule R A) [AddCommMonoid ι] [DecidableEq ι] [GradedAlgebra 𝒜] {e : ι} {f g : A} (hg : g 𝒜 e) {x : A} (hx : x = f * g) {d : ι} (n : ) (hf : f 𝒜 d) (a : A) (ha : a 𝒜 (n d)) :
(awayMap 𝒜 hg hx) (Away.mk 𝒜 hf n a ha) = Away.mk 𝒜 n (a * g ^ n)
@[reducible, inline]
abbrev HomogeneousLocalization.Away.isLocalizationElem {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : Submodule R A} [GradedAlgebra 𝒜] {e d : } {f : A} (hf : f 𝒜 d) {g : A} (hg : g 𝒜 e) :
Away 𝒜 f

The element t := g ^ d / f ^ e such that A_{(fg)} = A_{(f)}[1/t].

Equations
theorem HomogeneousLocalization.Away.isLocalization_mul {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : Submodule R A} [GradedAlgebra 𝒜] {e d : } {f : A} (hf : f 𝒜 d) {g : A} (hg : g 𝒜 e) {x : A} (hx : x = f * g) (hd : d 0) :

Let t := g ^ d / f ^ e, then A_{(fg)} = A_{(f)}[1/t].

theorem HomogeneousLocalization.Away.span_mk_prod_pow_eq_top {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] [AddCommMonoid ι] [DecidableEq ι] {𝒜 : ιSubmodule R A} [GradedAlgebra 𝒜] {f : A} {d : ι} (hf : f 𝒜 d) {ι' : Type u_4} [Fintype ι'] (v : ι'A) (hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ) (dv : ι'ι) (hxd : ∀ (i : ι'), v i 𝒜 (dv i)) :
Submodule.span (𝒜 0) {x : Away 𝒜 f | ∃ (a : ) (ai : ι') (hai : i : ι', ai i dv i = a d), Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) = x} =

Let 𝒜 be a graded algebra, finitely generated (as an algebra) over 𝒜₀ by { vᵢ }, where vᵢ has degree dvᵢ. If f : A has degree d, then 𝒜_(f) is generated (as a module) over 𝒜₀ by elements of the form (∏ i, vᵢ ^ aᵢ) / fᵃ such that ∑ aᵢ • dvᵢ = a • d.

theorem HomogeneousLocalization.Away.adjoin_mk_prod_pow_eq_top {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : Submodule R A} [GradedAlgebra 𝒜] {f : A} {d : } (hf : f 𝒜 d) (ι' : Type u_4) [Fintype ι'] (v : ι'A) (hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ) (dv : ι') (hxd : ∀ (i : ι'), v i 𝒜 (dv i)) :
Algebra.adjoin (𝒜 0) {x : Away 𝒜 f | ∃ (a : ) (ai : ι') (hai : i : ι', ai i dv i = a d) (_ : ∀ (i : ι'), ai i d), Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) = x} =

Let 𝒜 be a graded algebra, finitely generated (as an algebra) over 𝒜₀ by { vᵢ }, where vᵢ has degree dvᵢ. If f : A has degree d, then 𝒜_(f) is generated (as an algebra) over 𝒜₀ by elements of the form (∏ i, vᵢ ^ aᵢ) / fᵃ such that ∑ aᵢ • dvᵢ = a • d and ∀ i, aᵢ ≤ d.

theorem HomogeneousLocalization.Away.finiteType {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : Submodule R A} [GradedAlgebra 𝒜] [Algebra.FiniteType (↥(𝒜 0)) A] (f : A) (d : ) (hf : f 𝒜 d) :
Algebra.FiniteType (↥(𝒜 0)) (Away 𝒜 f)