Homogeneous Localization #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Notation #
ιis a commutative monoid;Ris a commutative semiring;Ais a commutative ring and anR-algebra;𝒜 : ι → submodule R Ais the grading ofA;x : submonoid Ais 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: forx : submonoid Aand anyc : num_denom_same_deg 𝒜 x, or equivalent a numerator and a denominator of the same degree, we get an elementc.num / c.denomofAₓ. -
homogeneous_localization:num_denom_same_deg 𝒜 xquotiented by kernel ofembedding 𝒜 x. -
homogeneous_localization.val: iff : homogeneous_localization 𝒜 x, thenf.valis an element ofAₓ. In another word, one can viewhomogeneous_localization 𝒜 xas a subring ofAₓthroughhomogeneous_localization.val. -
homogeneous_localization.num: iff : homogeneous_localization 𝒜 x, thenf.num : Ais the numerator off. -
homogeneous_localization.denom: iff : homogeneous_localization 𝒜 x, thenf.denom : Ais the denominator off. -
homogeneous_localization.deg: iff : homogeneous_localization 𝒜 x, thenf.deg : ιis the degree offsuch thatf.num ∈ 𝒜 f.degandf.denom ∈ 𝒜 f.deg(seehomogeneous_localization.num_mem_degandhomogeneous_localization.denom_mem_deg). -
homogeneous_localization.num_mem_deg: iff : homogeneous_localization 𝒜 x, thenf.num_mem_degis a proof thatf.num ∈ 𝒜 f.deg. -
homogeneous_localization.denom_mem_deg: iff : homogeneous_localization 𝒜 x, thenf.denom_mem_degis a proof thatf.denom ∈ 𝒜 f.deg. -
homogeneous_localization.eq_num_div_denom: iff : homogeneous_localization 𝒜 x, thenf.val : Aₓis equal tof.num / f.denom. -
homogeneous_localization.local_ring:homogeneous_localization 𝒜 xis a local ring whenxis 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}
[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
- homogeneous_localization.num_denom_same_deg.has_sizeof_inst
- homogeneous_localization.num_denom_same_deg.has_one
- homogeneous_localization.num_denom_same_deg.has_zero
- homogeneous_localization.num_denom_same_deg.has_mul
- homogeneous_localization.num_denom_same_deg.has_add
- homogeneous_localization.num_denom_same_deg.has_neg
- homogeneous_localization.num_denom_same_deg.comm_monoid
- homogeneous_localization.num_denom_same_deg.nat.has_pow
- homogeneous_localization.num_denom_same_deg.has_smul
@[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]
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 : submonoid A) :
@[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) :
@[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) :
@[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) :
@[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 : submonoid A) :
@[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) :
@[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) :
@[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) :
@[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 : submonoid A) :
@[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) :
@[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) :
@[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) :
@[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 : submonoid A) :
@[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) :
@[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) :
@[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) :
@[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 : submonoid A) :
@[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) :
@[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 : submonoid A)
(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 : submonoid A)
(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 : submonoid A) :
Equations
- homogeneous_localization.num_denom_same_deg.comm_monoid x = {mul := has_mul.mul (homogeneous_localization.num_denom_same_deg.has_mul x), mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := monoid.npow._default 1 has_mul.mul _ _, npow_zero' := _, npow_succ' := _, mul_comm := _}
@[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 : submonoid A) :
Equations
- homogeneous_localization.num_denom_same_deg.nat.has_pow x = {pow := λ (c : homogeneous_localization.num_denom_same_deg 𝒜 x) (n : ℕ), {deg := n • c.deg, num := graded_monoid.gmonoid.gnpow n c.num, denom := graded_monoid.gmonoid.gnpow n c.denom, denom_mem := _}}
@[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 : ℕ) :
@[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 : ℕ) :
@[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 : ℕ) :
@[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] :
@[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 : α) :
@[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 : α) :
@[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 : α) :
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 : submonoid A)
(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
- homogeneous_localization.num_denom_same_deg.embedding 𝒜 x p = localization.mk ↑(p.num) ⟨↑(p.denom), _⟩
@[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 : 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
- homogeneous_localization.has_pow
- homogeneous_localization.has_smul
- homogeneous_localization.has_neg
- homogeneous_localization.has_add
- homogeneous_localization.has_sub
- homogeneous_localization.has_mul
- homogeneous_localization.has_one
- homogeneous_localization.has_zero
- homogeneous_localization.has_nat_cast
- homogeneous_localization.has_int_cast
- homogeneous_localization.homogenous_localization_comm_ring
- homogeneous_localization.homogeneous_localization_algebra
- homogeneous_localization.at_prime.nontrivial
- homogeneous_localization.at_prime.local_ring
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
- y.val = quotient.lift_on' y (homogeneous_localization.num_denom_same_deg.embedding 𝒜 x) homogeneous_localization.val._proof_1
@[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 : submonoid A}
(i : homogeneous_localization.num_denom_same_deg 𝒜 x) :
homogeneous_localization.val (quotient.mk' i) = localization.mk ↑(i.num) ⟨↑(i.denom), _⟩
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 : submonoid A) :
@[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) :
has_pow (homogeneous_localization 𝒜 x) ℕ
Equations
- homogeneous_localization.has_pow x = {pow := λ (z : homogeneous_localization 𝒜 x) (n : ℕ), quotient.map' (λ (_x : homogeneous_localization.num_denom_same_deg 𝒜 x), _x ^ n) _ z}
@[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] :
has_smul α (homogeneous_localization 𝒜 x)
Equations
- homogeneous_localization.has_smul x = {smul := λ (m : α), quotient.map' (has_smul.smul m) _}
@[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 : α) :
@[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
- homogeneous_localization.has_sub x = {sub := λ (z1 z2 : homogeneous_localization 𝒜 x), z1 + -z2}
@[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) :
0 = quotient.mk' 0
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) :
1 = quotient.mk' 1
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} :
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} :
@[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) :
@[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) :
@[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) :
@[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) :
@[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 : ℕ) :
@[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 : submonoid A} :
@[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 : submonoid A} :
@[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]
def
homogeneous_localization.homogenous_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 : submonoid A} :
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
@[protected, instance]
def
homogeneous_localization.homogeneous_localization_algebra
{ι : Type u_1}
{R : Type u_2}
{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} :
algebra (homogeneous_localization 𝒜 x) (localization x)
Equations
- homogeneous_localization.homogeneous_localization_algebra = {to_has_smul := {smul := λ (p : homogeneous_localization 𝒜 x) (q : localization x), p.val * q}, to_ring_hom := {to_fun := homogeneous_localization.val x, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}
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
- f.num = ↑((quotient.out' f).num)
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
- f.denom = ↑((quotient.out' f).denom)
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
- f.deg = (quotient.out' 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 : 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) :
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) :
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) :
@[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
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 𝒜]
(𝔭 : ideal A)
[𝔭.is_prime]
(f : homogeneous_localization.at_prime 𝒜 𝔭) :
@[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.