# Homogeneous Localization #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

## 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 ∈ 𝒜ᵢ}.

• homogeneous_localization.num_denom_same_deg: a structure with a numerator and denominator field where they are required to have the same grading.

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.

• homogeneous_localization.num_denom_same_deg.embedding : for x : submonoid A and any c : num_denom_same_deg 𝒜 x, or equivalent a numerator and a denominator of the same degree, we get an element c.num / c.denom of Aₓ.

• homogeneous_localization: num_denom_same_deg 𝒜 x quotiented by kernel of embedding 𝒜 x.

• homogeneous_localization.val: if f : homogeneous_localization 𝒜 x, then f.val is an element of Aₓ. In another word, one can view homogeneous_localization 𝒜 x as a subring of Aₓ through homogeneous_localization.val.

• homogeneous_localization.num: if f : homogeneous_localization 𝒜 x, then f.num : A is the numerator of f.

• homogeneous_localization.denom: if f : homogeneous_localization 𝒜 x, then f.denom : A is the denominator of f.

• homogeneous_localization.deg: if f : homogeneous_localization 𝒜 x, then f.deg : ι is the degree of f such that f.num ∈ 𝒜 f.deg and f.denom ∈ 𝒜 f.deg (see homogeneous_localization.num_mem_deg and homogeneous_localization.denom_mem_deg).

• homogeneous_localization.num_mem_deg: if f : homogeneous_localization 𝒜 x, then f.num_mem_deg is a proof that f.num ∈ 𝒜 f.deg.

• homogeneous_localization.denom_mem_deg: if f : homogeneous_localization 𝒜 x, then f.denom_mem_deg is a proof that f.denom ∈ 𝒜 f.deg.

• homogeneous_localization.eq_num_div_denom: if f : homogeneous_localization 𝒜 x, then f.val : Aₓ is equal to f.num / f.denom.

• homogeneous_localization.local_ring: homogeneous_localization 𝒜 x is a local ring when x is the complement of some prime ideals.

## References #

@[nolint]
structure homogeneous_localization.num_denom_same_deg {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] (𝒜 : ι A) (x : submonoid A) :
Type (max u_1 u_3)

Let x be a submonoid of A, then num_denom_same_deg 𝒜 x is a structure with a numerator and a denominator with same grading such that the denominator is 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} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} (x : submonoid A) {c1 c2 : 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} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} (x : submonoid A) :
Equations
@[simp]
theorem homogeneous_localization.num_denom_same_deg.deg_one {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} (x : submonoid A) :
1.deg = 0
@[simp]
theorem homogeneous_localization.num_denom_same_deg.num_one {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} (x : submonoid A) :
(1.num) = 1
@[simp]
theorem homogeneous_localization.num_denom_same_deg.denom_one {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} (x : submonoid A) :
(1.denom) = 1
@[protected, instance]
def homogeneous_localization.num_denom_same_deg.has_zero {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} (x : submonoid A) :
Equations
@[simp]
theorem homogeneous_localization.num_denom_same_deg.deg_zero {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} (x : submonoid A) :
0.deg = 0
@[simp]
theorem homogeneous_localization.num_denom_same_deg.num_zero {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} (x : submonoid A) :
0.num = 0
@[simp]
theorem homogeneous_localization.num_denom_same_deg.denom_zero {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} (x : submonoid A) :
(0.denom) = 1
@[protected, instance]
def homogeneous_localization.num_denom_same_deg.has_mul {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} (x : submonoid A) :
Equations
@[simp]
theorem homogeneous_localization.num_denom_same_deg.deg_mul {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} (x : submonoid A) (c1 c2 : 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} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} (x : submonoid A) (c1 c2 : 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} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} (x : submonoid A) (c1 c2 : 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} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} (x : submonoid A) :
Equations
@[simp]
theorem homogeneous_localization.num_denom_same_deg.deg_add {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} (x : submonoid A) (c1 c2 : 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} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} (x : submonoid A) (c1 c2 : 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} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} (x : submonoid A) (c1 c2 : 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} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} (x : submonoid A) :
Equations
@[simp]
theorem homogeneous_localization.num_denom_same_deg.deg_neg {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} (x : submonoid A)  :
(-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} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} (x : submonoid A)  :
((-c).num) = -(c.num)
@[simp]
theorem homogeneous_localization.num_denom_same_deg.denom_neg {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} (x : submonoid A)  :
((-c).denom) = (c.denom)
@[protected, instance]
def homogeneous_localization.num_denom_same_deg.comm_monoid {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} (x : submonoid A) :
Equations
@[protected, instance]
def homogeneous_localization.num_denom_same_deg.nat.has_pow {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} (x : submonoid A) :
Equations
@[simp]
theorem homogeneous_localization.num_denom_same_deg.deg_pow {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} (x : submonoid A) (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} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} (x : submonoid A) (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} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} (x : submonoid A) (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} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} (x : submonoid A) {α : Type u_4} [ R] [ A] [ A] :
Equations
@[simp]
theorem homogeneous_localization.num_denom_same_deg.deg_smul {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} (x : submonoid A) {α : Type u_4} [ R] [ A] [ A] (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} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} (x : submonoid A) {α : Type u_4} [ R] [ A] [ A] (m : α) :
((m c).num) = m (c.num)
@[simp]
theorem homogeneous_localization.num_denom_same_deg.denom_smul {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} (x : submonoid A) {α : Type u_4} [ R] [ A] [ A] (m : α) :
((m c).denom) = (c.denom)
def homogeneous_localization.num_denom_same_deg.embedding {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] (𝒜 : ι A) (x : submonoid A)  :

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} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] (𝒜 : ι A) (x : submonoid A) :
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} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} {x : submonoid A} (y : 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
• y.val = homogeneous_localization.val._proof_1
@[simp]
theorem homogeneous_localization.val_mk' {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} {x : submonoid A}  :
= (i.denom), _⟩
theorem homogeneous_localization.val_injective {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} (x : submonoid A) :
@[protected, instance]
def homogeneous_localization.has_pow {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} (x : submonoid A) :
Equations
@[protected, instance]
def homogeneous_localization.has_smul {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} (x : submonoid A) {α : Type u_4} [ R] [ A] [ A] [ A] :
Equations
@[simp]
theorem homogeneous_localization.smul_val {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} (x : submonoid A) {α : Type u_4} [ R] [ A] [ A] [ A] (y : 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} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} (x : submonoid A) :
Equations
@[protected, instance]
def homogeneous_localization.has_add {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} (x : submonoid A) :
Equations
@[protected, instance]
def homogeneous_localization.has_sub {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} (x : submonoid A) :
Equations
• = {sub := λ (z1 z2 : , z1 + -z2}
@[protected, instance]
def homogeneous_localization.has_mul {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} (x : submonoid A) :
Equations
@[protected, instance]
def homogeneous_localization.has_one {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} (x : submonoid A) :
Equations
@[protected, instance]
def homogeneous_localization.has_zero {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} (x : submonoid A) :
Equations
theorem homogeneous_localization.zero_eq {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} (x : submonoid A) :
theorem homogeneous_localization.one_eq {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} (x : submonoid A) :
theorem homogeneous_localization.zero_val {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} {x : submonoid A} :
0.val = 0
theorem homogeneous_localization.one_val {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} {x : submonoid A} :
1.val = 1
@[simp]
theorem homogeneous_localization.add_val {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} {x : submonoid A} (y1 y2 : 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} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} {x : submonoid A} (y1 y2 : 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} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} {x : submonoid A} (y : x) :
(-y).val = -y.val
@[simp]
theorem homogeneous_localization.sub_val {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} {x : submonoid A} (y1 y2 : 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} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} {x : submonoid A} (y : 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} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} {x : submonoid A} :
Equations
@[protected, instance]
def homogeneous_localization.has_int_cast {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} {x : submonoid A} :
Equations
@[simp]
theorem homogeneous_localization.nat_cast_val {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} {x : submonoid A} (n : ) :
@[simp]
theorem homogeneous_localization.int_cast_val {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} {x : submonoid A} (n : ) :
@[protected, instance]
def homogeneous_localization.homogenous_localization_comm_ring {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} {x : submonoid A} :
Equations
• homogeneous_localization.homogenous_localization_comm_ring = homogeneous_localization.homogenous_localization_comm_ring._proof_5 homogeneous_localization.homogenous_localization_comm_ring._proof_6 homogeneous_localization.homogenous_localization_comm_ring._proof_7 homogeneous_localization.homogenous_localization_comm_ring._proof_8 homogeneous_localization.homogenous_localization_comm_ring._proof_9 homogeneous_localization.homogenous_localization_comm_ring._proof_10 homogeneous_localization.homogenous_localization_comm_ring._proof_11 homogeneous_localization.homogenous_localization_comm_ring._proof_12 homogeneous_localization.homogenous_localization_comm_ring._proof_13 homogeneous_localization.homogenous_localization_comm_ring._proof_14 homogeneous_localization.homogenous_localization_comm_ring._proof_15 homogeneous_localization.homogenous_localization_comm_ring._proof_16
@[protected, instance]
def homogeneous_localization.homogeneous_localization_algebra {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} {x : submonoid A} :
Equations
noncomputable def homogeneous_localization.num {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} {x : submonoid A} (f : 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} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} {x : submonoid A} (f : 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} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} {x : submonoid A} (f : 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_mem {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} {x : submonoid A} (f : x) :
theorem homogeneous_localization.num_mem_deg {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} {x : submonoid A} (f : x) :
f.num 𝒜 f.deg
theorem homogeneous_localization.denom_mem_deg {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} {x : submonoid A} (f : x) :
f.denom 𝒜 f.deg
theorem homogeneous_localization.eq_num_div_denom {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} {x : submonoid A} (f : x) :
f.val = f.denom, _⟩
theorem homogeneous_localization.ext_iff_val {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] {𝒜 : ι A} {x : submonoid A} (f g : x) :
f = g f.val = g.val
@[reducible]
def homogeneous_localization.at_prime {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] (𝒜 : ι A) (𝔭 : ideal A) [𝔭.is_prime] :
Type (max u_1 u_3)

Localizing a ring homogeneously at a prime ideal

theorem homogeneous_localization.is_unit_iff_is_unit_val {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] (𝒜 : ι A) (𝔭 : ideal A) [𝔭.is_prime]  :
@[protected, instance]
def homogeneous_localization.at_prime.nontrivial {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] (𝒜 : ι A) (𝔭 : ideal A) [𝔭.is_prime] :
@[protected, instance]
def homogeneous_localization.at_prime.local_ring {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] (𝒜 : ι A) (𝔭 : ideal A) [𝔭.is_prime] :
@[reducible]
def homogeneous_localization.away {ι : Type u_1} {R : Type u_2} {A : Type u_3} [decidable_eq ι] [comm_ring R] [comm_ring A] [ A] (𝒜 : ι A) (f : A) :
Type (max u_1 u_3)

Localising away from powers of f homogeneously.