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] :
↑(1.num) = 1
@[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) :
↑((c1 * c2).denom) = ↑(c1.denom) * ↑(c2.denom)
@[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) :
↑((c1 + c2).num) = ↑(c1.denom) * ↑(c2.num) + ↑(c2.denom) * ↑(c1.num)
@[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)
@[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_scalar {ΞΉ : 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_scalar Ξ± R] [has_scalar Ξ± 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_scalar Ξ± R] [has_scalar Ξ± 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_scalar Ξ± R] [has_scalar Ξ± 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_scalar Ξ± R] [has_scalar Ξ± 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_scalar {ΞΉ : 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_scalar Ξ± R] [has_scalar Ξ± A] [is_scalar_tower Ξ± R A] [is_scalar_tower Ξ± A A] :
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_scalar Ξ± R] [has_scalar Ξ± A] [is_scalar_tower Ξ± R A] [is_scalar_tower Ξ± A A] (y : homogeneous_localization π’œ x) (n : Ξ±) :
(n β€’ y).val = n β€’ y.val
@[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] :