# Homogeneous Localization #

## Notation #

• ฮน is a commutative monoid;
• R is a commutative semiring;
• A is a commutative ring and an R-algebra;
• ๐ : ฮน โ Submodule R A is the grading of A;
• x : Submonoid A is a submonoid

## 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 โ ๐แตข}.

• HomogeneousLocalization.NumDenSameDeg: a structure with a numerator and denominator field where they are required to have the same grading.

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.

• HomogeneousLocalization.NumDenSameDeg.embedding: for x : Submonoid A and any c : NumDenSameDeg ๐ x, or equivalent a numerator and a denominator of the same degree, we get an element c.num / c.den of Aโ.

• HomogeneousLocalization: NumDenSameDeg ๐ x quotiented by kernel of embedding ๐ x.

• HomogeneousLocalization.val: if f : HomogeneousLocalization ๐ x, then f.val is an element of Aโ. In another word, one can view HomogeneousLocalization ๐ x as a subring of Aโ through HomogeneousLocalization.val.

• HomogeneousLocalization.num: if f : HomogeneousLocalization ๐ x, then f.num : A is the numerator of f.

• HomogeneousLocalization.den: if f : HomogeneousLocalization ๐ x, then f.den : A is the denominator of f.

• HomogeneousLocalization.deg: if f : HomogeneousLocalization ๐ x, then f.deg : ฮน is the degree of f such that f.num โ ๐ f.deg and f.den โ ๐ f.deg (see HomogeneousLocalization.num_mem_deg and HomogeneousLocalization.den_mem_deg).

• HomogeneousLocalization.num_mem_deg: if f : HomogeneousLocalization ๐ x, then f.num_mem_deg is a proof that f.num โ ๐ f.deg.

• HomogeneousLocalization.den_mem_deg: if f : HomogeneousLocalization ๐ x, then f.den_mem_deg is a proof that f.den โ ๐ f.deg.

• HomogeneousLocalization.eq_num_div_den: if f : HomogeneousLocalization ๐ x, then f.val : Aโ is equal to f.num / f.den.

• HomogeneousLocalization.localRing: HomogeneousLocalization ๐ x is a local ring when x is the complement of some prime ideals.

• HomogeneousLocalization.map: Let A and B be two graded rings and g : A โ B a grading preserving ring map. If P โค A and Q โค B are submonoids such that P โค gโปยน(Q), then g induces a ring map between the homogeneous localization of A at P and the homogeneous localization of B at Q.

## References #

• [Robin Hartshorne, Algebraic Geometry][Har77]
structure HomogeneousLocalization.NumDenSameDeg {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Algebra R A] (๐ : ฮน โ ) (x : ) :
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
Instances For
theorem HomogeneousLocalization.NumDenSameDeg.den_mem {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Algebra R A] {๐ : ฮน โ } {x : } (self : ) :
โself.den โ x
theorem HomogeneousLocalization.NumDenSameDeg.ext {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Algebra R A] {๐ : ฮน โ } (x : ) {c1 : } {c2 : } (hdeg : c1.deg = c2.deg) (hnum : โc1.num = โc2.num) (hden : โc1.den = โc2.den) :
c1 = c2
instance HomogeneousLocalization.NumDenSameDeg.instOne {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] (x : ) :
Equations
• = { one := { deg := 0, num := โจ1, โฏโฉ, den := โจ1, โฏโฉ, den_mem := โฏ } }
@[simp]
theorem HomogeneousLocalization.NumDenSameDeg.deg_one {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] (x : ) :
@[simp]
theorem HomogeneousLocalization.NumDenSameDeg.num_one {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] (x : ) :
@[simp]
theorem HomogeneousLocalization.NumDenSameDeg.den_one {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] (x : ) :
instance HomogeneousLocalization.NumDenSameDeg.instZero {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] (x : ) :
Equations
• = { zero := { deg := 0, num := 0, den := โจ1, โฏโฉ, den_mem := โฏ } }
@[simp]
theorem HomogeneousLocalization.NumDenSameDeg.deg_zero {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] (x : ) :
@[simp]
theorem HomogeneousLocalization.NumDenSameDeg.num_zero {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] (x : ) :
@[simp]
theorem HomogeneousLocalization.NumDenSameDeg.den_zero {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] (x : ) :
instance HomogeneousLocalization.NumDenSameDeg.instMul {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] (x : ) :
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} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] (x : ) (c1 : ) (c2 : ) :
(c1 * c2).deg = c1.deg + c2.deg
@[simp]
theorem HomogeneousLocalization.NumDenSameDeg.num_mul {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] (x : ) (c1 : ) (c2 : ) :
โ(c1 * c2).num = โc1.num * โc2.num
@[simp]
theorem HomogeneousLocalization.NumDenSameDeg.den_mul {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] (x : ) (c1 : ) (c2 : ) :
โ(c1 * c2).den = โc1.den * โc2.den
instance HomogeneousLocalization.NumDenSameDeg.instAdd {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] (x : ) :
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} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] (x : ) (c1 : ) (c2 : ) :
(c1 + c2).deg = c1.deg + c2.deg
@[simp]
theorem HomogeneousLocalization.NumDenSameDeg.num_add {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] (x : ) (c1 : ) (c2 : ) :
โ(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} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] (x : ) (c1 : ) (c2 : ) :
โ(c1 + c2).den = โc1.den * โc2.den
instance HomogeneousLocalization.NumDenSameDeg.instNeg {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Algebra R A] {๐ : ฮน โ } (x : ) :
Equations
• = { neg := fun (c : ) => { deg := c.deg, num := โจ-โc.num, โฏโฉ, den := c.den, den_mem := โฏ } }
@[simp]
theorem HomogeneousLocalization.NumDenSameDeg.deg_neg {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Algebra R A] {๐ : ฮน โ } (x : ) (c : ) :
(-c).deg = c.deg
@[simp]
theorem HomogeneousLocalization.NumDenSameDeg.num_neg {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Algebra R A] {๐ : ฮน โ } (x : ) (c : ) :
โ(-c).num = -โc.num
@[simp]
theorem HomogeneousLocalization.NumDenSameDeg.den_neg {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Algebra R A] {๐ : ฮน โ } (x : ) (c : ) :
โ(-c).den = โc.den
instance HomogeneousLocalization.NumDenSameDeg.instCommMonoid {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] (x : ) :
Equations
instance HomogeneousLocalization.NumDenSameDeg.instPowNat {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] (x : ) :
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} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] (x : ) (c : ) (n : โ) :
(c ^ n).deg = n โข c.deg
@[simp]
theorem HomogeneousLocalization.NumDenSameDeg.num_pow {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] (x : ) (c : ) (n : โ) :
โ(c ^ n).num = โc.num ^ n
@[simp]
theorem HomogeneousLocalization.NumDenSameDeg.den_pow {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] (x : ) (c : ) (n : โ) :
โ(c ^ n).den = โc.den ^ n
instance HomogeneousLocalization.NumDenSameDeg.instSMul {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Algebra R A] {๐ : ฮน โ } (x : ) {ฮฑ : Type u_4} [SMul ฮฑ R] [SMul ฮฑ A] [IsScalarTower ฮฑ R A] :
SMul ฮฑ
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} [] [] [Algebra R A] {๐ : ฮน โ } (x : ) {ฮฑ : Type u_4} [SMul ฮฑ R] [SMul ฮฑ A] [IsScalarTower ฮฑ R A] (c : ) (m : ฮฑ) :
(m โข c).deg = c.deg
@[simp]
theorem HomogeneousLocalization.NumDenSameDeg.num_smul {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Algebra R A] {๐ : ฮน โ } (x : ) {ฮฑ : Type u_4} [SMul ฮฑ R] [SMul ฮฑ A] [IsScalarTower ฮฑ R A] (c : ) (m : ฮฑ) :
โ(m โข c).num = m โข โc.num
@[simp]
theorem HomogeneousLocalization.NumDenSameDeg.den_smul {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Algebra R A] {๐ : ฮน โ } (x : ) {ฮฑ : Type u_4} [SMul ฮฑ R] [SMul ฮฑ A] [IsScalarTower ฮฑ R A] (c : ) (m : ฮฑ) :
โ(m โข c).den = โc.den
def HomogeneousLocalization.NumDenSameDeg.embedding {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Algebra R A] (๐ : ฮน โ ) (x : ) (p : ) :

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
Instances For
def HomogeneousLocalization {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Algebra R A] (๐ : ฮน โ ) (x : ) :
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
Instances For
@[reducible, inline]
abbrev HomogeneousLocalization.mk {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Algebra R A] {๐ : ฮน โ } {x : } (y : ) :

Construct an element of HomogeneousLocalization ๐ x from a homogeneous fraction.

Equations
Instances For
theorem HomogeneousLocalization.mk_surjective {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Algebra R A] {๐ : ฮน โ } {x : } :
Function.Surjective HomogeneousLocalization.mk
def HomogeneousLocalization.val {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Algebra R A] {๐ : ฮน โ } {x : } (y : ) :

View an element of HomogeneousLocalization ๐ x as an element of Aโ by forgetting that the numerator and denominator are of the same grading.

Equations
• y.val =
Instances For
@[simp]
theorem HomogeneousLocalization.val_mk {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Algebra R A] {๐ : ฮน โ } {x : } (i : ) :
.val = Localization.mk โi.num โจโi.den, โฏโฉ
theorem HomogeneousLocalization.val_injective {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Algebra R A] {๐ : ฮน โ } (x : ) :
Function.Injective HomogeneousLocalization.val
theorem HomogeneousLocalization.subsingleton {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Algebra R A] (๐ : ฮน โ ) {x : } (hx : 0 โ x) :
instance HomogeneousLocalization.hasPow {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] (x : ) :
Equations
@[simp]
theorem HomogeneousLocalization.mk_pow {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] (x : ) (i : ) (n : โ) :
instance HomogeneousLocalization.instSMul {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Algebra R A] {๐ : ฮน โ } (x : ) {ฮฑ : Type u_4} [SMul ฮฑ R] [SMul ฮฑ A] [IsScalarTower ฮฑ R A] [IsScalarTower ฮฑ A A] :
SMul ฮฑ ()
Equations
@[simp]
theorem HomogeneousLocalization.mk_smul {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Algebra R A] {๐ : ฮน โ } (x : ) {ฮฑ : Type u_4} [SMul ฮฑ R] [SMul ฮฑ A] [IsScalarTower ฮฑ R A] [IsScalarTower ฮฑ A A] (i : ) (m : ฮฑ) :
@[simp]
theorem HomogeneousLocalization.val_smul {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Algebra R A] {๐ : ฮน โ } (x : ) {ฮฑ : Type u_4} [SMul ฮฑ R] [SMul ฮฑ A] [IsScalarTower ฮฑ R A] [IsScalarTower ฮฑ A A] (n : ฮฑ) (y : ) :
(n โข y).val = n โข y.val
instance HomogeneousLocalization.instNeg {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Algebra R A] {๐ : ฮน โ } (x : ) :
Neg ()
Equations
@[simp]
theorem HomogeneousLocalization.mk_neg {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Algebra R A] {๐ : ฮน โ } (x : ) (i : ) :
instance HomogeneousLocalization.instAdd {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] (x : ) :
Equations
@[simp]
theorem HomogeneousLocalization.mk_add {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] (x : ) (i : ) (j : ) :
instance HomogeneousLocalization.instSub {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] (x : ) :
Sub ()
Equations
• = { sub := fun (z1 z2 : ) => z1 + -z2 }
instance HomogeneousLocalization.instMul {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] (x : ) :
Mul ()
Equations
@[simp]
theorem HomogeneousLocalization.mk_mul {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] (x : ) (i : ) (j : ) :
instance HomogeneousLocalization.instOne {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] (x : ) :
One ()
Equations
• = { one := }
@[simp]
theorem HomogeneousLocalization.mk_one {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] (x : ) :
instance HomogeneousLocalization.instZero {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] (x : ) :
Zero ()
Equations
• = { zero := }
@[simp]
theorem HomogeneousLocalization.mk_zero {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] (x : ) :
theorem HomogeneousLocalization.zero_eq {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] (x : ) :
theorem HomogeneousLocalization.one_eq {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] (x : ) :
@[simp]
theorem HomogeneousLocalization.val_zero {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] {x : } :
@[simp]
theorem HomogeneousLocalization.val_one {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] {x : } :
@[simp]
theorem HomogeneousLocalization.val_add {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] {x : } (y1 : ) (y2 : ) :
(y1 + y2).val = y1.val + y2.val
@[simp]
theorem HomogeneousLocalization.val_mul {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] {x : } (y1 : ) (y2 : ) :
(y1 * y2).val = y1.val * y2.val
@[simp]
theorem HomogeneousLocalization.val_neg {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Algebra R A] {๐ : ฮน โ } {x : } (y : ) :
(-y).val = -y.val
@[simp]
theorem HomogeneousLocalization.val_sub {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] {x : } (y1 : ) (y2 : ) :
(y1 - y2).val = y1.val - y2.val
@[simp]
theorem HomogeneousLocalization.val_pow {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] {x : } (y : ) (n : โ) :
(y ^ n).val = y.val ^ n
instance HomogeneousLocalization.instNatCast {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] {x : } :
Equations
• HomogeneousLocalization.instNatCast = { natCast := Nat.unaryCast }
instance HomogeneousLocalization.instIntCast {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] {x : } :
Equations
• HomogeneousLocalization.instIntCast = { intCast := Int.castDef }
@[simp]
theorem HomogeneousLocalization.val_natCast {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] {x : } (n : โ) :
(โn).val = โn
@[simp]
theorem HomogeneousLocalization.val_intCast {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] {x : } (n : โค) :
(โn).val = โn
instance HomogeneousLocalization.homogenousLocalizationCommRing {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] {x : } :
Equations
• HomogeneousLocalization.homogenousLocalizationCommRing = Function.Injective.commRing HomogeneousLocalization.val โฏ โฏ โฏ โฏ โฏ โฏ โฏ โฏ โฏ โฏ โฏ โฏ
instance HomogeneousLocalization.homogeneousLocalizationAlgebra {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] {x : } :
Algebra () ()
Equations
• HomogeneousLocalization.homogeneousLocalizationAlgebra = Algebra.mk { toFun := HomogeneousLocalization.val, map_one' := โฏ, map_mul' := โฏ, map_zero' := โฏ, map_add' := โฏ } โฏ โฏ
@[simp]
theorem HomogeneousLocalization.algebraMap_apply {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] {x : } (y : ) :
(algebraMap () ()) y = y.val
theorem HomogeneousLocalization.mk_eq_zero_of_num {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] {x : } (f : ) (h : f.num = 0) :
theorem HomogeneousLocalization.mk_eq_zero_of_den {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] {x : } (f : ) (h : f.den = 0) :
def HomogeneousLocalization.num {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Algebra R A] {๐ : ฮน โ } {x : } (f : ) :
A

Numerator of an element in HomogeneousLocalization x.

Equations
• f.num = โ().num
Instances For
def HomogeneousLocalization.den {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Algebra R A] {๐ : ฮน โ } {x : } (f : ) :
A

Denominator of an element in HomogeneousLocalization x.

Equations
• f.den = โ().den
Instances For
def HomogeneousLocalization.deg {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Algebra R A] {๐ : ฮน โ } {x : } (f : ) :
ฮน

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

Equations
• f.deg = ().deg
Instances For
theorem HomogeneousLocalization.den_mem {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Algebra R A] {๐ : ฮน โ } {x : } (f : ) :
f.den โ x
theorem HomogeneousLocalization.num_mem_deg {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Algebra R A] {๐ : ฮน โ } {x : } (f : ) :
f.num โ ๐ f.deg
theorem HomogeneousLocalization.den_mem_deg {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Algebra R A] {๐ : ฮน โ } {x : } (f : ) :
f.den โ ๐ f.deg
theorem HomogeneousLocalization.eq_num_div_den {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Algebra R A] {๐ : ฮน โ } {x : } (f : ) :
f.val = Localization.mk f.num โจf.den, โฏโฉ
theorem HomogeneousLocalization.den_smul_val {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Algebra R A] {๐ : ฮน โ } {x : } (f : ) :
f.den โข f.val = () f.num
theorem HomogeneousLocalization.ext_iff_val {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Algebra R A] {๐ : ฮน โ } {x : } (f : ) (g : ) :
f = g โ f.val = g.val
@[reducible, inline]
abbrev HomogeneousLocalization.AtPrime {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Algebra R A] (๐ : ฮน โ ) (๐ญ : ) [๐ญ.IsPrime] :
Type (max u_1 u_3)

Localizing a ring homogeneously at a prime ideal.

Equations
Instances For
theorem HomogeneousLocalization.isUnit_iff_isUnit_val {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] (๐ : ฮน โ ) [GradedAlgebra ๐] (๐ญ : ) [๐ญ.IsPrime] (f : HomogeneousLocalization.AtPrime ๐ ๐ญ) :
instance HomogeneousLocalization.instNontrivialAtPrime {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] (๐ : ฮน โ ) [GradedAlgebra ๐] (๐ญ : ) [๐ญ.IsPrime] :
Equations
• โฏ = โฏ
instance HomogeneousLocalization.localRing {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] (๐ : ฮน โ ) [GradedAlgebra ๐] (๐ญ : ) [๐ญ.IsPrime] :
Equations
• โฏ = โฏ
@[reducible, inline]
abbrev HomogeneousLocalization.Away {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Algebra R A] (๐ : ฮน โ ) (f : A) :
Type (max u_1 u_3)

Localizing away from powers of f homogeneously.

Equations
Instances For
theorem HomogeneousLocalization.Away.eventually_smul_mem {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] {๐ : ฮน โ } [GradedAlgebra ๐] {f : A} {m : ฮน} (hf : f โ ๐ m) (z : ) :
โแถ  (n : โ) in Filter.atTop, โ โ() '' โ(๐ (n โข m))
def HomogeneousLocalization.map {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] (๐ : ฮน โ ) [GradedAlgebra ๐] {B : Type u_4} [] [Algebra R B] (โฌ : ฮน โ ) [] {P : } {Q : } (g : A โ+* B) (comap_le : P โค ) (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.
Instances For
@[reducible, inline]
abbrev HomogeneousLocalization.mapId {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] (๐ : ฮน โ ) [GradedAlgebra ๐] {P : } {Q : } (h : P โค Q) :

Let A be a graded algebra and P โค Q be two submonoids, then the homogeneous localization of A at P embedds into the homogeneous localization of A at Q.

Equations
Instances For
theorem HomogeneousLocalization.map_mk {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [] [] [Algebra R A] (๐ : ฮน โ ) [GradedAlgebra ๐] {B : Type u_4} [] [Algebra R B] (โฌ : ฮน โ ) [] {P : } {Q : } (g : A โ+* B) (comap_le : P โค ) (hg : โ (i : ฮน), โ a โ ๐ i, g a โ โฌ i) (x : ) :
(HomogeneousLocalization.map ๐ โฌ g comap_le hg) = HomogeneousLocalization.mk { deg := x.deg, num := โจg โx.num, โฏโฉ, den := โจg โx.den, โฏโฉ, den_mem := โฏ }