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 #

source
@[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
source
@[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
source
@[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] :
has_one (homogeneous_localization.num_denom_same_deg π’œ x)
Equations
source
@[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
source
@[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] :
↑(1.num) = 1
source
@[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] :
↑(1.denom) = 1
source
@[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] :
has_zero (homogeneous_localization.num_denom_same_deg π’œ x)
Equations
source
@[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
source
@[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
source
@[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] :
↑(0.denom) = 1
source
@[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] :
has_mul (homogeneous_localization.num_denom_same_deg π’œ x)
Equations
source
@[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
source
@[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)
source
@[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) :
↑((c1 * c2).denom) = ↑(c1.denom) * ↑(c2.denom)
source
@[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] :
has_add (homogeneous_localization.num_denom_same_deg π’œ x)
Equations
source
@[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
source
@[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) :
↑((c1 + c2).num) = ↑(c1.denom) * ↑(c2.num) + ↑(c2.denom) * ↑(c1.num)
source
@[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) :
↑((c1 + c2).denom) = ↑(c1.denom) * ↑(c2.denom)
source
@[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] :
has_neg (homogeneous_localization.num_denom_same_deg π’œ x)
Equations
source
@[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
source
@[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) :
↑((-c).num) = -↑(c.num)
source
@[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) :
↑((-c).denom) = ↑(c.denom)
source
@[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] :
comm_monoid (homogeneous_localization.num_denom_same_deg π’œ x)
Equations
source
@[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] :
has_pow (homogeneous_localization.num_denom_same_deg π’œ x) β„•
Equations
source
@[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
source
@[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
source
@[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
source
@[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] :
has_smul Ξ± (homogeneous_localization.num_denom_same_deg π’œ x)
Equations
source
@[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
source
@[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 : Ξ±) :
↑((m β€’ c).num) = m β€’ ↑(c.num)
source
@[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 : Ξ±) :
↑((m β€’ c).denom) = ↑(c.denom)
source
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) :
localization.at_prime 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
source
@[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
source
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) :
localization.at_prime 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
source
@[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) :
homogeneous_localization.val (quotient.mk' i) = localization.mk ↑(i.num) βŸ¨β†‘(i.denom), _⟩
source
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] :
function.injective homogeneous_localization.val
source
@[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] :
has_pow (homogeneous_localization π’œ x) β„•
Equations
source
@[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
source
@[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 : Ξ±) :
(n β€’ y).val = n β€’ y.val
source
@[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] :
has_neg (homogeneous_localization π’œ x)
Equations
source
@[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] :
has_add (homogeneous_localization π’œ x)
Equations
source
@[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] :
has_sub (homogeneous_localization π’œ x)
Equations
source
@[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] :
has_mul (homogeneous_localization π’œ x)
Equations
source
@[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] :
has_one (homogeneous_localization π’œ x)
Equations
source
@[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] :
has_zero (homogeneous_localization π’œ x)
Equations
source
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] :
0 = quotient.mk' 0
source
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] :
1 = quotient.mk' 1
source
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
source
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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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] :
has_nat_cast (homogeneous_localization π’œ x)
Equations
source
@[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] :
has_int_cast (homogeneous_localization π’œ x)
Equations
source
@[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 : β„•) :
↑n.val = ↑n
source
@[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 : β„€) :
↑n.val = ↑n
source
@[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] :
comm_ring (homogeneous_localization π’œ x)
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
source
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
source
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
source
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
source
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) :
f.denom βˆ‰ x
source
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
source
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
source
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) :
f.val = localization.mk f.num ⟨f.denom, _⟩
source
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
source
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) :
is_unit f.val ↔ is_unit f
source
@[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] :
nontrivial (homogeneous_localization π’œ x)
source
@[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] :
local_ring (homogeneous_localization π’œ x)