Degree-zero homogeneous localization of graded modules #
This file supplies the algebraic input missing from Mathlib's Proj API. Mathlib already
constructs the degree-zero homogeneous localization ring HomogeneousLocalization đ S and
the ordinary localized module LocalizedModule S M. We isolate inside the latter the fractions
whose module numerator and ring denominator lie in matching graded pieces.
The construction is intentionally indexed by the same additive grading monoid on the ring and the module. Integer shifts, which reconcile a natural grading on the ring with an integer-indexed family of module twists, belong to the separate graded-shift layer.
Localizing away from one element #
awayMk writes the fraction m / fâż, and two statements make it a usable normal form:
exists_awayMkâ every degree-zero fraction away fromfis anawayMk. The denominator is a power offby construction; what has to be proved is that theNumDenSameDegdegree certificate is forced to ben ⢠deg f, which isDirectSum.degree_eq_of_mem_memoncefâżis known to be nonzero.awayMk_eq_awayMk_iffâ two such fractions agree exactly when they cross-multiply, with no residualâ ufrom the localization. Theâ uis what the generalmk_eq_mk_iffleaves behind; cancelling it is where the domain and torsion-freeness hypotheses are spent, and they are spent nowhere else.
Together these turn DegreeZeroLocalization đ đ (.powers f) into fractions with an explicit
representative and a computable equality test, which is what any basis for it has to start from
(see the Laurent monomial basis of #491).
awayMk_eq_zero_iff specialises the equality test to the zero fraction, which is what makes the
numerator a faithful record: any independence statement about fractions reduces to one about
numerators.
awayMk_zero, awayMk_add, awayMk_sum and awayMk_shift are the arithmetic that goes with
the normal form: the first three are additivity in the numerator at a fixed denominator, and the
last puts two fractions over a common denominator. Spanning arguments need exactly this pair â
decompose a numerator into a sum, then align denominators â and none of the four costs a
cancellation hypothesis.
Homogeneous fractions #
A module fraction whose numerator and denominator lie in matching graded pieces.
- deg : Κ
The common grading index of the numerator and denominator.
- num : âĽ(đ self.deg)
The homogeneous numerator.
- den : âĽ(đ self.deg)
The homogeneous denominator.
The denominator belongs to the submonoid being localized.
Instances For
Forget the grading certificate and view a homogeneous module fraction in the ordinary localized module.
Instances For
The degree-zero submodule #
Restrict scalars on the ordinary localized module along the inclusion of the degree-zero homogeneous localization into the full localization.
Equations
- GradedModule.localizedModuleModule đ S = Module.compHom (LocalizedModule S M) (algebraMap (HomogeneousLocalization đ S) (Localization S))
An ordinary localized-module element is degree zero if it has a representative whose module numerator and ring denominator lie in matching graded pieces.
Equations
- GradedModule.IsDegreeZero đ đ S z = â (c : GradedModule.NumDenSameDeg đ đ S), c.embedding = z
Instances For
The degree-zero homogeneous localization as a submodule of the ordinary localized module.
Equations
- GradedModule.degreeZeroSubmodule đ đ S = { carrier := GradedModule.IsDegreeZero đ đ S, add_mem' := âŻ, zero_mem' := âŻ, smul_mem' := ⯠}
Instances For
The degree-zero homogeneous localization of the graded module M.
Equations
- GradedModule.DegreeZeroLocalization đ đ S = GradedModule.degreeZeroSubmodule đ đ S
Instances For
Construct a degree-zero localized element from a certified homogeneous fraction.
Equations
Instances For
Every degree-zero localized element has a homogeneous numerator and denominator.
Equality of homogeneous fractions is the ordinary localized-module equality criterion.
The scalar action in explicit fractions: (p/q) ⢠(m/s) = (p ⢠m)/(q * s).
The companion of twistMul_mk for the module action, and the rule a caller
needs to rebuild a local-fraction certificate after multiplying by a scalar.
Without it the action is opaque at a use site: coe_smul moves the problem into
LocalizedModule but says nothing about which fraction comes out.
The proof is the one already inside IsDegreeZero.smul, which constructs exactly
this NumDenSameDeg in order to show the action stays degree zero; naming the
computation separately means a caller no longer has to re-derive it.
Not @[simp]. Its right-hand side is stated with a.num and a.den, the
representative HomogeneousLocalization chooses, which is the less usable
form â see mk_smul_mk below. Marking both would also be a simpNF conflict,
since this one rewrites that one's left-hand side.
The scalar action on two explicit fractions.
smul_mk leaves the scalar as a.num / a.den, which are the representative
HomogeneousLocalization chooses â not the fields of whatever
NumDenSameDeg the caller built a from. When the scalar is itself written as
HomogeneousLocalization.mk c', that gap has to be closed again at every use
site. This states the rule with both sides explicit, so it does not.
Maps induced by enlarging the denominator submonoid #
Enlarging the denominator submonoid sends degree-zero homogeneous module fractions to degree-zero homogeneous module fractions.
Equations
- GradedModule.DegreeZeroLocalization.mapOfLE h = { toFun := fun (z : âĽ(GradedModule.DegreeZeroLocalization đ đ S)) => â¨(LocalizedModule.liftOfLE S T h) âz, âŻâŠ, map_zero' := âŻ, map_add' := ⯠}
Instances For
Inverting an element that is not a power of the new denominator #
mapOfLE covers enlarging the denominator submonoid along an inclusion S ⤠T. The Äech
differential needs a case it does not reach: along a face the denominators are
.powers gâ and .powers gâ with gâ * h = gâ, and Submonoid.powers gâ ⤠Submonoid.powers gâ
is false â powers a ⤠powers b needs a to be a power of b, and divisibility is weaker.
The map still exists, because gâ is already invertible once gâ is. These two lemmas supply
exactly that, in the form LocalizedModule.lift consumes, and are what a face map must be built
from. They are stated for a bare module because nothing about them is graded.
If gâ * h is a power of gâ, then gâ is already invertible after inverting gâ.
gâ * h is invertible there, and in a commutative ring a factor of a unit is a unit.
Every power of gâ therefore acts invertibly on the module localized at gâ.
This is the hypothesis of LocalizedModule.lift, so it is what turns the previous lemma into an
actual map out of the localization at gâ. The scalar action factors through
Localization (Submonoid.powers gâ), where the inverse is available.
The map of ordinary localized modules along a Äech face.
gâ is already invertible after inverting gâ, so the universal property of
LocalizedModule (Submonoid.powers gâ) M produces this map without any inclusion of
denominator submonoids. This is the underlying map of faceMap; it carries no grading.
Equations
- GradedModule.DegreeZeroLocalization.faceLift hgh = LocalizedModule.lift (Submonoid.powers gâ) (LocalizedModule.mkLinearMap (Submonoid.powers gâ) M) âŻ
Instances For
Along a face, clearing the denominator gââż multiplies numerator and denominator by hâż.
This is the formula the graded face map is defined by: the abstract LocalizedModule.lift is
inverted here into an explicit fraction, which is what the degree-zero certificate needs.
Both sides are pinned by multiplying through by gâ âż, which acts invertibly on the target --
that is the whole content of isUnit_algebraMap_end_of_mul_mem.
A face map preserves the degree-zero condition.
Clearing gââż costs hâż in both numerator and denominator, so the matching-degree certificate
survives with its degree raised by n ⢠e.
The Äech face map on degree-zero homogeneous localizations.
mapOfLE cannot supply this: along a face the denominator submonoids are Submonoid.powers gâ
and Submonoid.powers gâ with gâ * h = gâ, and divisibility does not nest powers submonoids.
The map exists anyway because gâ is invertible once gâ is.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The face map in explicit fractions: m / gâ⿠⌠hâż m / gââż.
Changing the grading by a membership equivalence #
Two gradings with the same members present the same degree-zero localization. The underlying
element of LocalizedModule S M does not move at all; only the certificate is rebuilt. This is
the localization-level counterpart of associatedIsoOfPiecewiseIff, and it is what lets a
statement about intShift đ 0 be read as one about đ.
Degree-zero localizations depend only on the membership predicates of the graded pieces.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Localization away from one homogeneous element #
The degree-zero fraction m / f⿠when f has degree d and m has degree n ⢠d.
Equations
Instances For
awayMk is a normal form. Every degree-zero fraction away from f is m / fâż for some
n and some m of degree n ⢠deg f.
The denominator is a power of f because that is what Submonoid.powers f means; the content is
that the NumDenSameDeg degree certificate has no freedom left. It is pinned by
DirectSum.degree_eq_of_mem_mem: the denominator lies both in the certified piece and, as fâż,
in n ⢠deg f, and a nonzero homogeneous element lies in exactly one piece.
The hypothesis is â n, fâż â 0 rather than f â 0 so that no domain assumption is needed here;
in a domain pow_ne_zero supplies it. It cannot be dropped: over a ring where f is nilpotent
the localization is trivial and the degree is genuinely unconstrained.
Cross-multiplication decides equality of awayMks. p / fâż = q / fáľ exactly when
fᾠ⢠p = f⿠⢠q, with no surviving â u.
mk_eq_mk_iff is the general criterion and it leaves an unknown u â Submonoid.powers f
behind. Cancelling that u is the whole point of this lemma and the only place the two
hypotheses are used: IsDomain A makes every fáľ regular, and Module.IsTorsionFree A M
turns a regular ring element into an injective scalar action on M. For M = A the latter is
an instance, so the polynomial case needs neither supplied by hand.
Without torsion-freeness the statement is false, not merely unproved: an f-torsion element of
M is a nonzero numerator whose fraction is zero.
The zero numerator gives the zero fraction.
awayMk is additive in the numerator at a fixed denominator.
awayMk is additive over a finite sum of numerators.
The membership hypothesis is total (â b) rather than restricted to s, because the summands on
the right have to carry their own certificates and a â b â s hypothesis is not available inside
Finset.sum. In practice the summands are monomials of a fixed degree, so nothing is lost.
The proof descends into LocalizedModule before inducting. That is not incidental: the numerator
appears in the type of awayMk's membership argument, so rewriting Finset.sum_insert in the
goal directly fails on a non-type-correct motive. coe_awayMk discharges the certificate first,
and the induction then runs over an ordinary equation.
Raising the denominator by fáľ and the numerator with it leaves the fraction alone.
This is what puts two awayMks over a common denominator, which every argument about sums of
fractions with different denominators needs. It holds over any ring: no cancellation is
performed, so neither IsDomain nor torsion-freeness appears.
Two fractions share a denominator. Any two degree-zero fractions away from f have
awayMk representatives over one common power fâż.
This is exists_awayMk on each fraction followed by awayMk_shift to align the two exponents
at their sum. It is the move every statement about a sum of fractions opens with â additivity
of awayMk exists only at a fixed denominator â and it is what the additivity of the sign
projection (#340's contracting homotopy) reduces to. Like exists_awayMk, it costs no domain
or torsion-freeness hypothesis: no cancellation is performed.
A fraction vanishes exactly when its numerator does.
This is awayMk_eq_awayMk_iff against the zero fraction, and it is what makes the numerator a
faithful record of the element: any independence statement about fractions reduces to one about
numerators. The hypotheses are inherited from that lemma and are needed for the same reason â
without torsion-freeness an f-torsion numerator is a nonzero numerator with a zero fraction.
Two equal degree indices give the same awayMk.
awayMk records the degree of its denominator in the NumDenSameDeg certificate, so two
certificates that are propositionally equal still need transporting. Every caller that meets this
has the same shape: one side names the degree as (Îł' + single iâ c).degree and the other as
c + Îł'.degree.
The face map in awayMk normal form. Restricting p / gââż along gâ * h = gâ multiplies
the numerator by hâż and leaves the exponent alone.
This is faceMap_mk with the denominator already known to be a power, which is the shape every
caller has: the face of a Äech intersection is a restriction between two awayMks, not between
two arbitrary NumDenSameDegs. The target degree is written e + eâ rather than eâ + e so that
n ⢠(e + eâ) matches the n ⢠e + n ⢠eâ that faceMap_mk produces.
Functoriality #
An A-linear map which preserves every graded piece. Mathlib has a bundled graded ring map,
but currently no corresponding bundled map for internally graded modules.
The underlying linear map.
The map preserves every homogeneous component.
Instances For
The ordinary localized map underlying a grading-preserving linear map.
Equations
- GradedModule.GradedLinearMap.localized đ S đ f = (LocalizedModule.map S) f.toLinearMap
Instances For
A grading-preserving linear map sends degree-zero homogeneous localizations to degree-zero homogeneous localizations.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The graded ring as a module #
When the graded module is the graded ring itself, the construction above recovers Mathlib's
degree-zero homogeneous localization. Keeping this comparison explicit is useful for identifying
the associated sheaf of the graded ring with the structure sheaf on Proj.
Regard a homogeneous localization element as a degree-zero element of the localization of the graded ring considered as a module over itself.
Equations
- GradedModule.DegreeZeroLocalization.homogeneousLocalizationLinearMap đ S = { toFun := fun (z : HomogeneousLocalization đ S) => â¨z.val, âŻâŠ, map_add' := âŻ, map_smul' := ⯠}
Instances For
The degree-zero localization of the graded ring as a module is canonically linearly equivalent to Mathlib's homogeneous localization ring.