mathlib3 documentation

ring_theory.graded_algebra.homogeneous_localization

Homogeneous Localization #

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

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 : 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} [add_comm_monoid ι] [decidable_eq ι] [comm_ring R] [comm_ring A] [algebra R A] {𝒜 : ι submodule R A} [graded_algebra 𝒜] (x : submonoid A) {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]
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 : 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} [add_comm_monoid ι] [decidable_eq ι] [comm_ring R] [comm_ring A] [algebra R A] {𝒜 : ι submodule R A} [graded_algebra 𝒜] (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} [add_comm_monoid ι] [decidable_eq ι] [comm_ring R] [comm_ring A] [algebra R A] {𝒜 : ι submodule R A} [graded_algebra 𝒜] (x : submonoid A) :
(1.denom) = 1
@[protected, instance]
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 : 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} [add_comm_monoid ι] [decidable_eq ι] [comm_ring R] [comm_ring A] [algebra R A] {𝒜 : ι submodule R A} [graded_algebra 𝒜] (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} [add_comm_monoid ι] [decidable_eq ι] [comm_ring R] [comm_ring A] [algebra R A] {𝒜 : ι submodule R A} [graded_algebra 𝒜] (x : submonoid A) :
(0.denom) = 1
@[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 : submonoid A) (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 : submonoid A) (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 : submonoid A) (c1 c2 : homogeneous_localization.num_denom_same_deg 𝒜 x) :
((c1 * c2).denom) = (c1.denom) * (c2.denom)
@[protected, instance]
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 : submonoid A) (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 : submonoid A) (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 : submonoid A) (c1 c2 : homogeneous_localization.num_denom_same_deg 𝒜 x) :
((c1 + c2).denom) = (c1.denom) * (c2.denom)
@[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 : submonoid A) (c : homogeneous_localization.num_denom_same_deg 𝒜 x) :
(-c).deg = c.deg
@[simp]
@[simp]
@[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 : submonoid A) (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 : submonoid A) (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 : submonoid A) (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 : submonoid A) {α : 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 : submonoid A) {α : 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 : submonoid A) {α : 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)
@[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 : submonoid A) {α : 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)

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
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 : submonoid A} (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
@[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 : submonoid A) :
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 : submonoid A) {α : Type u_4} [has_smul α R] [has_smul α 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 : submonoid A) {α : 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
@[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 : submonoid A) :
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 : submonoid A) :
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 : submonoid A) :
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 : submonoid A) :
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 : submonoid A) :
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 : submonoid A) :
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 : submonoid A) :
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 : submonoid A) :
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 : submonoid A} :
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 : submonoid A} :
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 : submonoid A} (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 : submonoid A} (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 : submonoid A} (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 : submonoid A} (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 : submonoid A} (y : homogeneous_localization 𝒜 x) (n : ) :
(y ^ n).val = y.val ^ n
@[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 : submonoid A} (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 : submonoid A} (n : ) :
@[protected, instance]
Equations
  • homogeneous_localization.homogenous_localization_comm_ring = function.injective.comm_ring homogeneous_localization.val 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
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 : submonoid A} (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 : submonoid A} (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 : submonoid A} (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_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 : submonoid A} (f : homogeneous_localization 𝒜 x) :
theorem homogeneous_localization.num_mem_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 : submonoid A} (f : homogeneous_localization 𝒜 x) :
f.num 𝒜 f.deg
theorem homogeneous_localization.denom_mem_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 : submonoid A} (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 : submonoid A} (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 : submonoid A} (f g : homogeneous_localization 𝒜 x) :
f = g f.val = g.val
@[reducible]
def homogeneous_localization.at_prime {ι : 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 𝒜] (𝔭 : ideal A) [𝔭.is_prime] :
Type (max u_1 u_3)

Localizing a ring homogeneously at a prime ideal

@[protected, instance]
def homogeneous_localization.at_prime.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 𝒜] (𝔭 : ideal A) [𝔭.is_prime] :
@[protected, instance]
def homogeneous_localization.at_prime.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 𝒜] (𝔭 : ideal A) [𝔭.is_prime] :
@[reducible]
def homogeneous_localization.away {ι : 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 𝒜] (f : A) :
Type (max u_1 u_3)

Localising away from powers of f homogeneously.