Homogeneous Localization #
Notation #
ΞΉis a commutative monoid;Ris a commutative semiring;Ais a commutative ring and anR-algebra;π : ΞΉ β submodule R Ais the grading ofA;x : ideal Ais a prime ideal.
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 : prime ideal of 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.num: 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_memandhomogeneous_localization.denom_mem). -
homogeneous_localization.num_mem: iff : homogeneous_localization π x, thenf.num_memis a proof thatf.num β f.deg. -
homogeneous_localization.denom_mem: iff : homogeneous_localization π x, thenf.denom_memis 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.
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
- 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_scalar
@[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] :
@[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] :
@[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] :
@[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
- homogeneous_localization.num_denom_same_deg.has_zero x = {zero := {deg := 0, num := 0, denom := β¨1, _β©, denom_not_mem := _}}
@[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] :
@[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] :
@[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] :
@[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) :
@[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) :
@[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) :
@[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) :
@[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) :
@[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) :
@[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] :
@[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) :
@[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
- 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 : ideal A)
[x.is_prime] :
@[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 : β) :
@[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 : β) :
@[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 : β) :
@[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
- homogeneous_localization.num_denom_same_deg.has_scalar x = {smul := Ξ» (m : Ξ±) (c : homogeneous_localization.num_denom_same_deg π x), {deg := c.deg, num := m β’ c.num, denom := c.denom, denom_not_mem := _}}
@[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 : Ξ±) :
@[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
- 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 : 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
- homogeneous_localization.has_pow
- homogeneous_localization.has_scalar
- 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.comm_ring
- homogeneous_localization.nontrivial
- homogeneous_localization.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 : 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
- 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 : 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), _β©
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] :
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_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] :
has_scalar Ξ± (homogeneous_localization π x)
Equations
- homogeneous_localization.has_scalar x = {smul := Ξ» (m : Ξ±), quotient.map' (has_scalar.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 : 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 : Ξ±) :
@[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
@[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
@[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
- 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 : ideal A)
[x.is_prime] :
has_mul (homogeneous_localization π x)
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] :
has_one (homogeneous_localization π x)
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] :
has_zero (homogeneous_localization π x)
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] :
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 : ideal A)
[x.is_prime] :
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 : ideal A}
[x.is_prime] :
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] :
@[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) :
@[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) :
@[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) :
@[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) :
@[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 : β) :
@[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)
@[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)
@[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] :
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
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
- 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 : ideal A}
[x.is_prime]
(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 : 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
- f.deg = (quotient.out' f).deg
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) :
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) :
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) :
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] :
nontrivial (homogeneous_localization π x)
@[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)