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.

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 : HomogeneousLocalization.NumDenSameDeg 𝒜 x} {c2 : HomogeneousLocalization.NumDenSameDeg 𝒜 x} (hdeg : c1.deg = c2.deg) (hnum : ↑c1.num = ↑c2.num) (hden : ↑c1.den = ↑c2.den) : c1 = c2

instance HomogeneousLocalization.NumDenSameDeg.instOneNumDenSameDeg {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] (x : Submonoid A) : One (HomogeneousLocalization.NumDenSameDeg 𝒜 x)

Equations

• HomogeneousLocalization.NumDenSameDeg.instOneNumDenSameDeg x = { one := { deg := 0, num := { val := 1, property := ⋯ }, den := { val := 1, property := ⋯ }, den_mem := ⋯ } }

@[simp]

theorem HomogeneousLocalization.NumDenSameDeg.deg_one {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] (x : Submonoid A) : 1.deg = 0

@[simp]

theorem HomogeneousLocalization.NumDenSameDeg.num_one {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] (x : Submonoid A) : ↑1.num = 1

@[simp]

theorem HomogeneousLocalization.NumDenSameDeg.den_one {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] (x : Submonoid A) : ↑1.den = 1

instance HomogeneousLocalization.NumDenSameDeg.instZeroNumDenSameDeg {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] (x : Submonoid A) : Zero (HomogeneousLocalization.NumDenSameDeg 𝒜 x)

Equations

• HomogeneousLocalization.NumDenSameDeg.instZeroNumDenSameDeg x = { zero := { deg := 0, num := 0, den := { val := 1, property := ⋯ }, den_mem := ⋯ } }

@[simp]

theorem HomogeneousLocalization.NumDenSameDeg.deg_zero {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] (x : Submonoid A) : 0.deg = 0

@[simp]

theorem HomogeneousLocalization.NumDenSameDeg.num_zero {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] (x : Submonoid A) : 0.num = 0

@[simp]

theorem HomogeneousLocalization.NumDenSameDeg.den_zero {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] (x : Submonoid A) : ↑0.den = 1

instance HomogeneousLocalization.NumDenSameDeg.instMulNumDenSameDeg {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] (x : Submonoid A) : Mul (HomogeneousLocalization.NumDenSameDeg 𝒜 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} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] (x : Submonoid A) (c1 : HomogeneousLocalization.NumDenSameDeg 𝒜 x) (c2 : HomogeneousLocalization.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} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] (x : Submonoid A) (c1 : HomogeneousLocalization.NumDenSameDeg 𝒜 x) (c2 : HomogeneousLocalization.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} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] (x : Submonoid A) (c1 : HomogeneousLocalization.NumDenSameDeg 𝒜 x) (c2 : HomogeneousLocalization.NumDenSameDeg 𝒜 x) : ↑(c1 * c2).den = ↑c1.den * ↑c2.den

instance HomogeneousLocalization.NumDenSameDeg.instAddNumDenSameDeg {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] (x : Submonoid A) : Add (HomogeneousLocalization.NumDenSameDeg 𝒜 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} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] (x : Submonoid A) (c1 : HomogeneousLocalization.NumDenSameDeg 𝒜 x) (c2 : HomogeneousLocalization.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} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] (x : Submonoid A) (c1 : HomogeneousLocalization.NumDenSameDeg 𝒜 x) (c2 : HomogeneousLocalization.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} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] (x : Submonoid A) (c1 : HomogeneousLocalization.NumDenSameDeg 𝒜 x) (c2 : HomogeneousLocalization.NumDenSameDeg 𝒜 x) : ↑(c1 + c2).den = ↑c1.den * ↑c2.den

instance HomogeneousLocalization.NumDenSameDeg.instNegNumDenSameDeg {ι : 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.NumDenSameDeg 𝒜 x)

Equations

• One or more equations did not get rendered due to their size.

@[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 : HomogeneousLocalization.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 : HomogeneousLocalization.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 : HomogeneousLocalization.NumDenSameDeg 𝒜 x) : ↑(-c).den = ↑c.den

instance HomogeneousLocalization.NumDenSameDeg.instCommMonoidNumDenSameDeg {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] (x : Submonoid A) : CommMonoid (HomogeneousLocalization.NumDenSameDeg 𝒜 x)

Equations

• HomogeneousLocalization.NumDenSameDeg.instCommMonoidNumDenSameDeg x = CommMonoid.mk ⋯

instance HomogeneousLocalization.NumDenSameDeg.instPowNumDenSameDegNat {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] (x : Submonoid A) : Pow (HomogeneousLocalization.NumDenSameDeg 𝒜 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} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] (x : Submonoid A) (c : HomogeneousLocalization.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} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] (x : Submonoid A) (c : HomogeneousLocalization.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} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] (x : Submonoid A) (c : HomogeneousLocalization.NumDenSameDeg 𝒜 x) (n : ℕ) : ↑(c ^ n).den = ↑c.den ^ n

instance HomogeneousLocalization.NumDenSameDeg.instSMulNumDenSameDeg {ι : 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 α (HomogeneousLocalization.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 : HomogeneousLocalization.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 : HomogeneousLocalization.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 : HomogeneousLocalization.NumDenSameDeg 𝒜 x) (m : α) : ↑(m • c).den = ↑c.den

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 : HomogeneousLocalization.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ₓ.

Equations

• HomogeneousLocalization.NumDenSameDeg.embedding 𝒜 x p = Localization.mk ↑p.num { val := ↑p.den, property := ⋯ }

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

• HomogeneousLocalization 𝒜 x = Quotient (Setoid.ker (HomogeneousLocalization.NumDenSameDeg.embedding 𝒜 x))

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.

Equations

• HomogeneousLocalization.val y = Quotient.liftOn' y (HomogeneousLocalization.NumDenSameDeg.embedding 𝒜 x) ⋯

@[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 : HomogeneousLocalization.NumDenSameDeg 𝒜 x) : HomogeneousLocalization.val (Quotient.mk'' i) = Localization.mk ↑i.num { val := ↑i.den, property := ⋯ }

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 HomogeneousLocalization.val

instance HomogeneousLocalization.hasPow {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] (x : Submonoid A) : Pow (HomogeneousLocalization 𝒜 x) ℕ

Equations

• HomogeneousLocalization.hasPow x = { pow := fun (z : HomogeneousLocalization 𝒜 x) (n : ℕ) => Quotient.map' (fun (x_1 : HomogeneousLocalization.NumDenSameDeg 𝒜 x) => x_1 ^ n) ⋯ z }

instance HomogeneousLocalization.instSMulHomogeneousLocalization {ι : 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)

Equations

• HomogeneousLocalization.instSMulHomogeneousLocalization x = { smul := fun (m : α) => Quotient.map' (fun (x_1 : HomogeneousLocalization.NumDenSameDeg 𝒜 x) => m • x_1) ⋯ }

@[simp]

theorem HomogeneousLocalization.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) {α : Type u_4} [SMul α R] [SMul α A] [IsScalarTower α R A] [IsScalarTower α A A] (n : α) (y : HomogeneousLocalization 𝒜 x) : HomogeneousLocalization.val (n • y) = n • HomogeneousLocalization.val y

instance HomogeneousLocalization.instNegHomogeneousLocalization {ι : 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)

Equations

• HomogeneousLocalization.instNegHomogeneousLocalization x = { neg := Quotient.map' Neg.neg ⋯ }

instance HomogeneousLocalization.instAddHomogeneousLocalization {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] (x : Submonoid A) : Add (HomogeneousLocalization 𝒜 x)

Equations

• HomogeneousLocalization.instAddHomogeneousLocalization x = { add := Quotient.map₂' (fun (x_1 x_2 : HomogeneousLocalization.NumDenSameDeg 𝒜 x) => x_1 + x_2) ⋯ }

instance HomogeneousLocalization.instSubHomogeneousLocalization {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] (x : Submonoid A) : Sub (HomogeneousLocalization 𝒜 x)

Equations

• HomogeneousLocalization.instSubHomogeneousLocalization x = { sub := fun (z1 z2 : HomogeneousLocalization 𝒜 x) => z1 + -z2 }

instance HomogeneousLocalization.instMulHomogeneousLocalization {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] (x : Submonoid A) : Mul (HomogeneousLocalization 𝒜 x)

Equations

• HomogeneousLocalization.instMulHomogeneousLocalization x = { mul := Quotient.map₂' (fun (x_1 x_2 : HomogeneousLocalization.NumDenSameDeg 𝒜 x) => x_1 * x_2) ⋯ }

instance HomogeneousLocalization.instOneHomogeneousLocalization {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] (x : Submonoid A) : One (HomogeneousLocalization 𝒜 x)

Equations

• HomogeneousLocalization.instOneHomogeneousLocalization x = { one := Quotient.mk'' 1 }

instance HomogeneousLocalization.instZeroHomogeneousLocalization {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] (x : Submonoid A) : Zero (HomogeneousLocalization 𝒜 x)

Equations

• HomogeneousLocalization.instZeroHomogeneousLocalization x = { zero := Quotient.mk'' 0 }

theorem HomogeneousLocalization.zero_eq {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] (x : Submonoid A) : 0 = Quotient.mk'' 0

theorem HomogeneousLocalization.one_eq {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] (x : Submonoid A) : 1 = Quotient.mk'' 1

theorem HomogeneousLocalization.zero_val {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] {x : Submonoid A} : HomogeneousLocalization.val 0 = 0

theorem HomogeneousLocalization.one_val {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] {x : Submonoid A} : HomogeneousLocalization.val 1 = 1

@[simp]

theorem HomogeneousLocalization.add_val {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] {x : Submonoid A} (y1 : HomogeneousLocalization 𝒜 x) (y2 : HomogeneousLocalization 𝒜 x) : HomogeneousLocalization.val (y1 + y2) = HomogeneousLocalization.val y1 + HomogeneousLocalization.val y2

@[simp]

theorem HomogeneousLocalization.mul_val {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] {x : Submonoid A} (y1 : HomogeneousLocalization 𝒜 x) (y2 : HomogeneousLocalization 𝒜 x) : HomogeneousLocalization.val (y1 * y2) = HomogeneousLocalization.val y1 * HomogeneousLocalization.val y2

@[simp]

theorem HomogeneousLocalization.neg_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) : HomogeneousLocalization.val (-y) = -HomogeneousLocalization.val y

@[simp]

theorem HomogeneousLocalization.sub_val {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] {x : Submonoid A} (y1 : HomogeneousLocalization 𝒜 x) (y2 : HomogeneousLocalization 𝒜 x) : HomogeneousLocalization.val (y1 - y2) = HomogeneousLocalization.val y1 - HomogeneousLocalization.val y2

@[simp]

theorem HomogeneousLocalization.pow_val {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] {x : Submonoid A} (y : HomogeneousLocalization 𝒜 x) (n : ℕ) : HomogeneousLocalization.val (y ^ n) = HomogeneousLocalization.val y ^ n

instance HomogeneousLocalization.instNatCastHomogeneousLocalization {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] {x : Submonoid A} : NatCast (HomogeneousLocalization 𝒜 x)

Equations

• HomogeneousLocalization.instNatCastHomogeneousLocalization = { natCast := Nat.unaryCast }

instance HomogeneousLocalization.instIntCastHomogeneousLocalization {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] {x : Submonoid A} : IntCast (HomogeneousLocalization 𝒜 x)

Equations

• HomogeneousLocalization.instIntCastHomogeneousLocalization = { intCast := Int.castDef }

@[simp]

theorem HomogeneousLocalization.natCast_val {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] {x : Submonoid A} (n : ℕ) : HomogeneousLocalization.val ↑n = ↑n

@[simp]

theorem HomogeneousLocalization.intCast_val {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] {x : Submonoid A} (n : ℤ) : HomogeneousLocalization.val ↑n = ↑n

instance HomogeneousLocalization.homogenousLocalizationCommRing {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] {x : Submonoid A} : CommRing (HomogeneousLocalization 𝒜 x)

Equations

• HomogeneousLocalization.homogenousLocalizationCommRing = Function.Injective.commRing HomogeneousLocalization.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance HomogeneousLocalization.homogeneousLocalizationAlgebra {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] {x : Submonoid A} : Algebra (HomogeneousLocalization 𝒜 x) (Localization x)

Equations

• One or more equations did not get rendered due to their size.

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

• HomogeneousLocalization.num f = ↑(Quotient.out' f).num

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

• HomogeneousLocalization.den f = ↑(Quotient.out' f).den

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

• HomogeneousLocalization.deg f = (Quotient.out' f).deg

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) : HomogeneousLocalization.den f ∈ 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) : HomogeneousLocalization.num f ∈ 𝒜 (HomogeneousLocalization.deg f)

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) : HomogeneousLocalization.den f ∈ 𝒜 (HomogeneousLocalization.deg f)

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) : HomogeneousLocalization.val f = Localization.mk (HomogeneousLocalization.num f) { val := HomogeneousLocalization.den f, property := ⋯ }

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 : HomogeneousLocalization 𝒜 x) (g : HomogeneousLocalization 𝒜 x) : f = g ↔ HomogeneousLocalization.val f = HomogeneousLocalization.val g

@[inline, reducible]

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) [Ideal.IsPrime 𝔭] : Type (max u_1 u_3)

Localizing a ring homogeneously at a prime ideal.

Equations

• HomogeneousLocalization.AtPrime 𝒜 𝔭 = HomogeneousLocalization 𝒜 (Ideal.primeCompl 𝔭)

theorem HomogeneousLocalization.isUnit_iff_isUnit_val {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] (𝔭 : Ideal A) [Ideal.IsPrime 𝔭] (f : HomogeneousLocalization.AtPrime 𝒜 𝔭) : IsUnit (HomogeneousLocalization.val f) ↔ IsUnit f

instance HomogeneousLocalization.instNontrivialAtPrime {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] (𝔭 : Ideal A) [Ideal.IsPrime 𝔭] : Nontrivial (HomogeneousLocalization.AtPrime 𝒜 𝔭)

Equations

• ⋯ = ⋯

instance HomogeneousLocalization.localRing {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] (𝔭 : Ideal A) [Ideal.IsPrime 𝔭] : LocalRing (HomogeneousLocalization.AtPrime 𝒜 𝔭)

Equations

• ⋯ = ⋯

@[inline, reducible]

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

• HomogeneousLocalization.Away 𝒜 f = HomogeneousLocalization 𝒜 (Submonoid.powers f)