mathlib documentation

ring_theory.graded_algebra.homogeneous_localization

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 num_denom_same_deg ๐’œ x cannot have a ring structure for many reasons, for example if c is a num_denom_same_deg, 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 num_denom_same_deg ๐’œ x by the kernel of c โ†ฆ c.num / c.denom.

References #

@[nolint]
structure homogeneous_localization.num_denom_same_deg {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] (๐’œ : ฮน โ†’ submodule R A) [graded_algebra ๐’œ] (x : ideal A) [x.is_prime] :
Type (max u_1 u_3)

Let x be a prime ideal, then num_denom_same_deg ๐’œ x is a structure with a numerator and a denominator with same grading such that the denominator is not contained in x.

Instances for homogeneous_localization.num_denom_same_deg
@[ext]
theorem homogeneous_localization.num_denom_same_deg.ext {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] (x : ideal A) [x.is_prime] {c1 c2 : homogeneous_localization.num_denom_same_deg ๐’œ x} (hdeg : c1.deg = c2.deg) (hnum : โ†‘(c1.num) = โ†‘(c2.num)) (hdenom : โ†‘(c1.denom) = โ†‘(c2.denom)) :
c1 = c2
@[protected, instance]
def homogeneous_localization.num_denom_same_deg.has_one {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] (x : ideal A) [x.is_prime] :
Equations
@[simp]
theorem homogeneous_localization.num_denom_same_deg.deg_one {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] (x : ideal A) [x.is_prime] :
1.deg = 0
@[simp]
theorem homogeneous_localization.num_denom_same_deg.num_one {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] (x : ideal A) [x.is_prime] :
@[simp]
theorem homogeneous_localization.num_denom_same_deg.denom_one {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] (x : ideal A) [x.is_prime] :
@[protected, instance]
def homogeneous_localization.num_denom_same_deg.has_zero {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] (x : ideal A) [x.is_prime] :
Equations
@[simp]
theorem homogeneous_localization.num_denom_same_deg.deg_zero {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] (x : ideal A) [x.is_prime] :
0.deg = 0
@[simp]
theorem homogeneous_localization.num_denom_same_deg.num_zero {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] (x : ideal A) [x.is_prime] :
0.num = 0
@[simp]
theorem homogeneous_localization.num_denom_same_deg.denom_zero {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] (x : ideal A) [x.is_prime] :
@[protected, instance]
def homogeneous_localization.num_denom_same_deg.has_mul {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] (x : ideal A) [x.is_prime] :
Equations
@[simp]
theorem homogeneous_localization.num_denom_same_deg.deg_mul {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] (x : ideal A) [x.is_prime] (c1 c2 : homogeneous_localization.num_denom_same_deg ๐’œ x) :
(c1 * c2).deg = c1.deg + c2.deg
@[simp]
theorem homogeneous_localization.num_denom_same_deg.num_mul {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] (x : ideal A) [x.is_prime] (c1 c2 : homogeneous_localization.num_denom_same_deg ๐’œ x) :
โ†‘((c1 * c2).num) = โ†‘(c1.num) * โ†‘(c2.num)
@[simp]
theorem homogeneous_localization.num_denom_same_deg.denom_mul {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] (x : ideal A) [x.is_prime] (c1 c2 : homogeneous_localization.num_denom_same_deg ๐’œ x) :
@[protected, instance]
def homogeneous_localization.num_denom_same_deg.has_add {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] (x : ideal A) [x.is_prime] :
Equations
@[simp]
theorem homogeneous_localization.num_denom_same_deg.deg_add {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] (x : ideal A) [x.is_prime] (c1 c2 : homogeneous_localization.num_denom_same_deg ๐’œ x) :
(c1 + c2).deg = c1.deg + c2.deg
@[simp]
theorem homogeneous_localization.num_denom_same_deg.num_add {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] (x : ideal A) [x.is_prime] (c1 c2 : homogeneous_localization.num_denom_same_deg ๐’œ x) :
@[simp]
theorem homogeneous_localization.num_denom_same_deg.denom_add {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] (x : ideal A) [x.is_prime] (c1 c2 : homogeneous_localization.num_denom_same_deg ๐’œ x) :
@[protected, instance]
def homogeneous_localization.num_denom_same_deg.has_neg {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] (x : ideal A) [x.is_prime] :
Equations
@[simp]
theorem homogeneous_localization.num_denom_same_deg.deg_neg {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] (x : ideal A) [x.is_prime] (c : homogeneous_localization.num_denom_same_deg ๐’œ x) :
(-c).deg = c.deg
@[simp]
theorem homogeneous_localization.num_denom_same_deg.num_neg {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] (x : ideal A) [x.is_prime] (c : homogeneous_localization.num_denom_same_deg ๐’œ x) :
@[simp]
theorem homogeneous_localization.num_denom_same_deg.denom_neg {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] (x : ideal A) [x.is_prime] (c : homogeneous_localization.num_denom_same_deg ๐’œ x) :
@[protected, instance]
def homogeneous_localization.num_denom_same_deg.comm_monoid {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] (x : ideal A) [x.is_prime] :
Equations
@[protected, instance]
def homogeneous_localization.num_denom_same_deg.nat.has_pow {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] (x : ideal A) [x.is_prime] :
Equations
@[simp]
theorem homogeneous_localization.num_denom_same_deg.deg_pow {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] (x : ideal A) [x.is_prime] (c : homogeneous_localization.num_denom_same_deg ๐’œ x) (n : โ„•) :
(c ^ n).deg = n โ€ข c.deg
@[simp]
theorem homogeneous_localization.num_denom_same_deg.num_pow {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] (x : ideal A) [x.is_prime] (c : homogeneous_localization.num_denom_same_deg ๐’œ x) (n : โ„•) :
โ†‘((c ^ n).num) = โ†‘(c.num) ^ n
@[simp]
theorem homogeneous_localization.num_denom_same_deg.denom_pow {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] (x : ideal A) [x.is_prime] (c : homogeneous_localization.num_denom_same_deg ๐’œ x) (n : โ„•) :
โ†‘((c ^ n).denom) = โ†‘(c.denom) ^ n
@[protected, instance]
def homogeneous_localization.num_denom_same_deg.has_smul {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] (x : ideal A) [x.is_prime] {ฮฑ : Type u_4} [has_smul ฮฑ R] [has_smul ฮฑ A] [is_scalar_tower ฮฑ R A] :
Equations
@[simp]
theorem homogeneous_localization.num_denom_same_deg.deg_smul {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] (x : ideal A) [x.is_prime] {ฮฑ : Type u_4} [has_smul ฮฑ R] [has_smul ฮฑ A] [is_scalar_tower ฮฑ R A] (c : homogeneous_localization.num_denom_same_deg ๐’œ x) (m : ฮฑ) :
(m โ€ข c).deg = c.deg
@[simp]
theorem homogeneous_localization.num_denom_same_deg.num_smul {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] (x : ideal A) [x.is_prime] {ฮฑ : Type u_4} [has_smul ฮฑ R] [has_smul ฮฑ A] [is_scalar_tower ฮฑ R A] (c : homogeneous_localization.num_denom_same_deg ๐’œ x) (m : ฮฑ) :
@[simp]
theorem homogeneous_localization.num_denom_same_deg.denom_smul {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] (x : ideal A) [x.is_prime] {ฮฑ : Type u_4} [has_smul ฮฑ R] [has_smul ฮฑ A] [is_scalar_tower ฮฑ R A] (c : homogeneous_localization.num_denom_same_deg ๐’œ x) (m : ฮฑ) :
def homogeneous_localization.num_denom_same_deg.embedding {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] (๐’œ : ฮน โ†’ submodule R A) [graded_algebra ๐’œ] (x : ideal A) [x.is_prime] (p : homogeneous_localization.num_denom_same_deg ๐’œ x) :

For x : prime ideal of A and any p : num_denom_same_deg ๐’œ x, or equivalent a numerator and a denominator of the same degree, we get an element p.num / p.denom of Aโ‚“.

Equations
@[nolint]
def homogeneous_localization {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] (๐’œ : ฮน โ†’ submodule R A) [graded_algebra ๐’œ] (x : ideal A) [x.is_prime] :
Type (max u_1 u_3)

For x : prime ideal of A, homogeneous_localization ๐’œ x is num_denom_same_deg ๐’œ 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 homogeneous_localization
def homogeneous_localization.val {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] {x : ideal A} [x.is_prime] (y : homogeneous_localization ๐’œ x) :

View an element of homogeneous_localization ๐’œ x as an element of Aโ‚“ by forgetting that the numerator and denominator are of the same grading.

Equations
@[simp]
theorem homogeneous_localization.val_mk' {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] {x : ideal A} [x.is_prime] (i : homogeneous_localization.num_denom_same_deg ๐’œ x) :
theorem homogeneous_localization.val_injective {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] (x : ideal A) [x.is_prime] :
@[protected, instance]
def homogeneous_localization.has_pow {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] (x : ideal A) [x.is_prime] :
Equations
@[protected, instance]
def homogeneous_localization.has_smul {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] (x : ideal A) [x.is_prime] {ฮฑ : Type u_4} [has_smul ฮฑ R] [has_smul ฮฑ A] [is_scalar_tower ฮฑ R A] [is_scalar_tower ฮฑ A A] :
has_smul ฮฑ (homogeneous_localization ๐’œ x)
Equations
@[simp]
theorem homogeneous_localization.smul_val {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] (x : ideal A) [x.is_prime] {ฮฑ : Type u_4} [has_smul ฮฑ R] [has_smul ฮฑ A] [is_scalar_tower ฮฑ R A] [is_scalar_tower ฮฑ A A] (y : homogeneous_localization ๐’œ x) (n : ฮฑ) :
@[protected, instance]
def homogeneous_localization.has_neg {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] (x : ideal A) [x.is_prime] :
Equations
@[protected, instance]
def homogeneous_localization.has_add {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] (x : ideal A) [x.is_prime] :
Equations
@[protected, instance]
def homogeneous_localization.has_sub {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] (x : ideal A) [x.is_prime] :
Equations
@[protected, instance]
def homogeneous_localization.has_mul {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] (x : ideal A) [x.is_prime] :
Equations
@[protected, instance]
def homogeneous_localization.has_one {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] (x : ideal A) [x.is_prime] :
Equations
@[protected, instance]
def homogeneous_localization.has_zero {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] (x : ideal A) [x.is_prime] :
Equations
theorem homogeneous_localization.zero_eq {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] (x : ideal A) [x.is_prime] :
theorem homogeneous_localization.one_eq {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] (x : ideal A) [x.is_prime] :
theorem homogeneous_localization.zero_val {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] {x : ideal A} [x.is_prime] :
0.val = 0
theorem homogeneous_localization.one_val {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] {x : ideal A} [x.is_prime] :
1.val = 1
@[simp]
theorem homogeneous_localization.add_val {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] {x : ideal A} [x.is_prime] (y1 y2 : homogeneous_localization ๐’œ x) :
(y1 + y2).val = y1.val + y2.val
@[simp]
theorem homogeneous_localization.mul_val {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] {x : ideal A} [x.is_prime] (y1 y2 : homogeneous_localization ๐’œ x) :
(y1 * y2).val = y1.val * y2.val
@[simp]
theorem homogeneous_localization.neg_val {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] {x : ideal A} [x.is_prime] (y : homogeneous_localization ๐’œ x) :
(-y).val = -y.val
@[simp]
theorem homogeneous_localization.sub_val {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] {x : ideal A} [x.is_prime] (y1 y2 : homogeneous_localization ๐’œ x) :
(y1 - y2).val = y1.val - y2.val
@[simp]
theorem homogeneous_localization.pow_val {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] {x : ideal A} [x.is_prime] (y : homogeneous_localization ๐’œ x) (n : โ„•) :
(y ^ n).val = y.val ^ n
@[protected, instance]
def homogeneous_localization.has_nat_cast {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] {x : ideal A} [x.is_prime] :
Equations
@[protected, instance]
def homogeneous_localization.has_int_cast {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] {x : ideal A} [x.is_prime] :
Equations
@[simp]
theorem homogeneous_localization.nat_cast_val {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] {x : ideal A} [x.is_prime] (n : โ„•) :
@[simp]
theorem homogeneous_localization.int_cast_val {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] {x : ideal A} [x.is_prime] (n : โ„ค) :
@[protected, instance]
def homogeneous_localization.comm_ring {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] {x : ideal A} [x.is_prime] :
Equations
  • homogeneous_localization.comm_ring = function.injective.comm_ring homogeneous_localization.val homogeneous_localization.comm_ring._proof_5 homogeneous_localization.comm_ring._proof_6 homogeneous_localization.comm_ring._proof_7 homogeneous_localization.comm_ring._proof_8 homogeneous_localization.comm_ring._proof_9 homogeneous_localization.comm_ring._proof_10 homogeneous_localization.comm_ring._proof_11 homogeneous_localization.comm_ring._proof_12 homogeneous_localization.comm_ring._proof_13 homogeneous_localization.comm_ring._proof_14 homogeneous_localization.comm_ring._proof_15 homogeneous_localization.comm_ring._proof_16
noncomputable def homogeneous_localization.num {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] {x : ideal A} [x.is_prime] (f : homogeneous_localization ๐’œ x) :
A

numerator of an element in homogeneous_localization x

Equations
noncomputable def homogeneous_localization.denom {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] {x : ideal A} [x.is_prime] (f : homogeneous_localization ๐’œ x) :
A

denominator of an element in homogeneous_localization x

Equations
noncomputable def homogeneous_localization.deg {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] {x : ideal A} [x.is_prime] (f : homogeneous_localization ๐’œ x) :
ฮน

For an element in homogeneous_localization x, degree is the natural number i such that ๐’œ i contains both numerator and denominator.

Equations
theorem homogeneous_localization.denom_not_mem {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] {x : ideal A} [x.is_prime] (f : homogeneous_localization ๐’œ x) :
theorem homogeneous_localization.num_mem {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] {x : ideal A} [x.is_prime] (f : homogeneous_localization ๐’œ x) :
f.num โˆˆ ๐’œ f.deg
theorem homogeneous_localization.denom_mem {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] {x : ideal A} [x.is_prime] (f : homogeneous_localization ๐’œ x) :
f.denom โˆˆ ๐’œ f.deg
theorem homogeneous_localization.eq_num_div_denom {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] {x : ideal A} [x.is_prime] (f : homogeneous_localization ๐’œ x) :
theorem homogeneous_localization.ext_iff_val {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] {x : ideal A} [x.is_prime] (f g : homogeneous_localization ๐’œ x) :
f = g โ†” f.val = g.val
theorem homogeneous_localization.is_unit_iff_is_unit_val {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] {x : ideal A} [x.is_prime] (f : homogeneous_localization ๐’œ x) :
@[protected, instance]
def homogeneous_localization.nontrivial {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] {x : ideal A} [x.is_prime] :
@[protected, instance]
def homogeneous_localization.local_ring {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [add_comm_monoid ฮน] [decidable_eq ฮน] [comm_ring R] [comm_ring A] [algebra R A] {๐’œ : ฮน โ†’ submodule R A} [graded_algebra ๐’œ] {x : ideal A} [x.is_prime] :