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 โ ๐แตข}
.
HomogeneousLocalization.NumDenSameDeg
: a structure with a numerator and denominator field where they are required to have the same grading.
However NumDenSameDeg ๐ x
cannot have a ring structure for many reasons, for example if c
is a NumDenSameDeg
, 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 NumDenSameDeg ๐ x
by the kernel of c โฆ c.num / c.den
.
-
HomogeneousLocalization.NumDenSameDeg.embedding
: forx : Submonoid A
and anyc : NumDenSameDeg ๐ x
, or equivalent a numerator and a denominator of the same degree, we get an elementc.num / c.den
ofAโ
. -
HomogeneousLocalization
:NumDenSameDeg ๐ x
quotiented by kernel ofembedding ๐ x
. -
HomogeneousLocalization.val
: iff : HomogeneousLocalization ๐ x
, thenf.val
is an element ofAโ
. In another word, one can viewHomogeneousLocalization ๐ x
as a subring ofAโ
throughHomogeneousLocalization.val
. -
HomogeneousLocalization.num
: iff : HomogeneousLocalization ๐ x
, thenf.num : A
is the numerator off
. -
HomogeneousLocalization.den
: iff : HomogeneousLocalization ๐ x
, thenf.den : A
is the denominator off
. -
HomogeneousLocalization.deg
: iff : HomogeneousLocalization ๐ x
, thenf.deg : ฮน
is the degree off
such thatf.num โ ๐ f.deg
andf.den โ ๐ f.deg
(seeHomogeneousLocalization.num_mem_deg
andHomogeneousLocalization.den_mem_deg
). -
HomogeneousLocalization.num_mem_deg
: iff : HomogeneousLocalization ๐ x
, thenf.num_mem_deg
is a proof thatf.num โ ๐ f.deg
. -
HomogeneousLocalization.den_mem_deg
: iff : HomogeneousLocalization ๐ x
, thenf.den_mem_deg
is a proof thatf.den โ ๐ f.deg
. -
HomogeneousLocalization.eq_num_div_den
: iff : HomogeneousLocalization ๐ x
, thenf.val : Aโ
is equal tof.num / f.den
. -
HomogeneousLocalization.localRing
:HomogeneousLocalization ๐ x
is a local ring whenx
is the complement of some prime ideals.
References #
- [Robin Hartshorne, Algebraic Geometry][Har77]
- deg : ฮน
- num : { x_1 // x_1 โ ๐ s.deg }
- den : { x_1 // x_1 โ ๐ s.deg }
- den_mem : โs.den โ x
Let x
be a submonoid of A
, then NumDenSameDeg ๐ x
is a structure with a numerator and a
denominator with same grading such that the denominator is contained in x
.
Instances For
For x : prime ideal of A
and any p : NumDenSameDeg ๐ x
, or equivalent a numerator and a
denominator of the same degree, we get an element p.num / p.den
of Aโ
.
Instances For
For x : prime ideal of A
, HomogeneousLocalization ๐ x
is NumDenSameDeg ๐ x
modulo the
kernel of embedding ๐ x
. This is essentially the subring of Aโ
where the numerator and
denominator share the same grading.
Instances For
View an element of HomogeneousLocalization ๐ x
as an element of Aโ
by forgetting that the
numerator and denominator are of the same grading.
Instances For
Numerator of an element in HomogeneousLocalization x
.
Instances For
Denominator of an element in HomogeneousLocalization x
.
Instances For
For an element in HomogeneousLocalization x
, degree is the natural number i
such that
๐ i
contains both numerator and denominator.