Degree-zero fractions with an arbitrary numerator, and the twist comparison they give #
TwistBridge.lean and TwistApp.lean carry the fraction fⁿ / gⁿ for f and g of degree one.
#585's glue needs the same statements for an arbitrary pair of homogeneous elements of the same
degree -- fᵐ gᵢⁿ / gᵢ^{n+m} appears the moment the extension exponent and the agreement exponent
are allowed to differ, and no power of a single element has that shape.
What is here #
frac is a / b at a point of D₊(b), for a b ∈ 𝒜 k; fracSection is the section of the
structure sheaf it defines over any open inside D₊(b). fracPow and fracPowSection are the
special case a = fⁿ, b = gⁿ, and the two ..._eq_fracPow... lemmas record that -- by rfl,
so nothing has to be transported between the two spellings.
twistBy_app_eq_smul' is the comparison the glue consumes: over an open inside D₊(b), twisting a
section by a is twisting it by b and scaling by a / b. The degree-one case was its
a = fⁿ, b = gⁿ case.
Why this is not just a generalisation for its own sake #
The two exponents #585 carries are independent: n extends a section across each chart, m
forces agreement on the pairwise overlaps, and the section that finally glues is
twistBy (fᵐ gᵢⁿ) of the chart extension. Comparing two such across an overlap needs a / b with
a = fᵐ gⱼⁿ and b = gᵢ^{n+m}, which is a genuine two-element fraction.
Scope #
Fractions and the twist comparison. No chart, no cover, no gluing.
A power lands in the degree its exponent multiplies.
SetLike.pow_mem_graded states the degree as d • e; #585 meets it as e • d, because the
numerator of HomogeneousLocalization.Away.isLocalizationElem hg hf is a power of f sitting in
the degree that g's exponent produces.
The same, with the degree written as a product.
pow_mem_smul is the spelling the localization elements produce; this is the spelling a twist
degree is stated in, and #823 needs both because the glue compares one against the other. The
degree-one case is Frac.pow_mem_deg.
Two fractions with the same value are the same element, whatever degrees they are written in.
The workhorse for #585's bookkeeping: the exponents that reach the glue are built by different
routes -- (f ^ d) ^ n from a chart's distinguished element, f ^ (d * n) from a twist -- and this
identifies them without transporting a degree.
The same, on sections.
A power of a fraction is the fraction of the powers.
Fractions multiply componentwise.
a / b and b / a are inverse to each other, over an open inside both D₊(a) and
D₊(b).
Serre's global generation inverts the chart scalar (f / gᵉ)ⁿ on D₊(g) ⊓ D₊(f): the extension
lemma produces (f / gᵉ)ⁿ • u as a restriction of a global section, and this is what recovers
u itself as a combination of the chart's generators. The product is fracSection_mul, and
(a b) / (b a) = 1 / 1 is one Localization.r_iff_exists with witness 1.
Rescaling the section b of O(k) by a / b gives the section a, at every point of an
open inside D₊(b).
The general form of fracPow_smul_sectionOfMem, and the identity that makes two chart extensions
with different exponents comparable.
The same on sections rather than at a point.
The overlap comparison for two homogeneous elements of the same degree.
Over an open inside D₊(b), twisting a section by a is twisting it by b and scaling by
a / b. The case a = fⁿ, b = gⁿ was stated separately in TwistApp.lean until #825; it had
no consumer once this one existed.
The scalar is ascribed at Γ(Proj 𝒜, U) for the reason recorded there: written bare it elaborates
at the structure sheaf's own section type, where the action on the twist's sections does not
synthesize.