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 : ideal A
is 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 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.num
: 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
andhomogeneous_localization.denom_mem
). -
homogeneous_localization.num_mem
: iff : homogeneous_localization π x
, thenf.num_mem
is a proof thatf.num β f.deg
. -
homogeneous_localization.denom_mem
: iff : homogeneous_localization π x
, thenf.denom_mem
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.
References #
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
Equations
- homogeneous_localization.num_denom_same_deg.has_zero x = {zero := {deg := 0, num := 0, denom := β¨1, _β©, denom_not_mem := _}}
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.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 := _}}
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_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
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_scalar x = {smul := Ξ» (m : Ξ±), quotient.map' (has_scalar.smul m) _}
Equations
Equations
Equations
- homogeneous_localization.has_sub x = {sub := Ξ» (z1 z2 : homogeneous_localization π x), z1 + -z2}
Equations
Equations
Equations
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
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