Homogeneous Localization #
Notation #
ฮน
is a commutative monoid;R
is a commutative semiring;A
is a commutative ring and anR
-algebra;๐ : ฮน โ submodule R A
is the grading ofA
;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
: forx : submonoid A
and anyc : num_denom_same_deg ๐ x
, or equivalent a numerator and a denominator of the same degree, we get an elementc.num / c.denom
ofAโ
. -
homogeneous_localization
:num_denom_same_deg ๐ x
quotiented by kernel ofembedding ๐ x
. -
homogeneous_localization.val
: iff : homogeneous_localization ๐ x
, thenf.val
is an element ofAโ
. In another word, one can viewhomogeneous_localization ๐ x
as a subring ofAโ
throughhomogeneous_localization.val
. -
homogeneous_localization.num
: iff : homogeneous_localization ๐ x
, thenf.num : A
is the numerator off
. -
homogeneous_localization.denom
: iff : homogeneous_localization ๐ x
, thenf.denom : A
is the denominator off
. -
homogeneous_localization.deg
: iff : homogeneous_localization ๐ x
, thenf.deg : ฮน
is the degree off
such thatf.num โ ๐ f.deg
andf.denom โ ๐ f.deg
(seehomogeneous_localization.num_mem_deg
andhomogeneous_localization.denom_mem_deg
). -
homogeneous_localization.num_mem_deg
: iff : homogeneous_localization ๐ x
, thenf.num_mem_deg
is a proof thatf.num โ ๐ f.deg
. -
homogeneous_localization.denom_mem_deg
: iff : homogeneous_localization ๐ x
, thenf.denom_mem_deg
is 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 ๐ x
is a local ring whenx
is the complement of some prime ideals.
References #
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
Equations
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 := _}
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 := _}}
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), _โฉ
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
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
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}
Equations
- homogeneous_localization.has_smul x = {smul := ฮป (m : ฮฑ), quotient.map' (has_smul.smul m) _}
Equations
Equations
Equations
- homogeneous_localization.has_sub x = {sub := ฮป (z1 z2 : homogeneous_localization ๐ x), z1 + -z2}
Equations
Equations
Equations
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
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' := _}
numerator of an element in homogeneous_localization x
Equations
- f.num = โ((quotient.out' f).num)
denominator of an element in homogeneous_localization x
Equations
- f.denom = โ((quotient.out' f).denom)
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
Localizing a ring homogeneously at a prime ideal
Localising away from powers of f
homogeneously.