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.isLocalRing: 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} [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) : Neg (NumDenSameDeg 𝒜 x)

@[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)

@[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 𝒜] : One (NumDenSameDeg 𝒜 x)

@[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 𝒜] : Zero (NumDenSameDeg 𝒜 x)

@[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 𝒜] : Mul (NumDenSameDeg 𝒜 x)

@[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 𝒜] : Add (NumDenSameDeg 𝒜 x)

@[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 𝒜] : CommMonoid (NumDenSameDeg 𝒜 x)

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 𝒜] : Pow (NumDenSameDeg 𝒜 x) ℕ

@[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) : Localization 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ₓ.

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.

@[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) : HomogeneousLocalization 𝒜 x

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

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} : Function.Surjective mk

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) : Localization x

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

@[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) : Function.Injective val

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) : Subsingleton (HomogeneousLocalization 𝒜 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] : SMul α (HomogeneousLocalization 𝒜 x)

@[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) : Neg (HomogeneousLocalization 𝒜 x)

@[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 𝒜] : Pow (HomogeneousLocalization 𝒜 x) ℕ

@[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 𝒜] : Add (HomogeneousLocalization 𝒜 x)

@[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 𝒜] : Sub (HomogeneousLocalization 𝒜 x)

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 𝒜] : Mul (HomogeneousLocalization 𝒜 x)

@[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 𝒜] : One (HomogeneousLocalization 𝒜 x)

@[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 𝒜] : Zero (HomogeneousLocalization 𝒜 x)

@[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 𝒜] : 0 = Quotient.mk'' 0

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 𝒜] : 1 = Quotient.mk'' 1

@[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 𝒜] : NatCast (HomogeneousLocalization 𝒜 x)

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 𝒜] : IntCast (HomogeneousLocalization 𝒜 x)

@[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.homogeneousLocalizationCommRing {ι : 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 𝒜] : CommRing (HomogeneousLocalization 𝒜 x)

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 𝒜] : Algebra (HomogeneousLocalization 𝒜 x) (Localization x)

@[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) : (algebraMap (HomogeneousLocalization 𝒜 x) (Localization x)) y = y.val

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.

instance HomogeneousLocalization.instAlgebraSubtypeMemSubmoduleOfNat {ι : 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 𝒜] : Algebra (↥(𝒜 0)) (HomogeneousLocalization 𝒜 x)

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

instance HomogeneousLocalization.instIsScalarTowerSubtypeMemSubmoduleOfNatLocalization {ι : 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 𝒜] : IsScalarTower (↥(𝒜 0)) (HomogeneousLocalization 𝒜 x) (Localization 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.

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.

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.

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) : f.val = Localization.mk f.num ⟨f.den, ⋯⟩

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) : f.den • f.val = (algebraMap A (Localization x)) f.num

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.

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 𝒜 𝔭) : IsUnit (val f) ↔ IsUnit f

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.

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) : HomogeneousLocalization 𝒜 P →+* HomogeneousLocalization ℬ Q

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.

@[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) : HomogeneousLocalization 𝒜 P →+* HomogeneousLocalization 𝒜 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.

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) : Set.range ⇑(HomogeneousLocalization.awayMapAux✝ 𝒜 ⋯) ⊆ Set.range val

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.

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) : val ((awayMap 𝒜 hg hx) a) = (Localization.awayLift (algebraMap A (Localization (Submonoid.powers x))) f ⋯) (val a)

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)) : (awayMap 𝒜 hg hx) ((fromZeroRingHom 𝒜 (Submonoid.powers f)) a) = (fromZeroRingHom 𝒜 (Submonoid.powers x)) a

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.

@[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.

@[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].

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) : IsLocalization.Away (isLocalizationElem hf hg) (Away 𝒜 x)

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)