The chart's scalar, read on Proj #
#585's two halves speak different languages. ChartExtension.lean produces sections of a
degree-one chart and clears the chart ring's element f / g
(HomogeneousLocalization.Away.isLocalizationElem); TwistApp.lean compares twists of sections of
F on Proj 𝒜 and scales by the structure-sheaf section fracPowSection. This file is the
dictionary, and it is the last genuinely open step of the issue.
What has to be identified #
Nothing has to move on the module side: Scheme.Modules.restrictAppIso is Iso.refl, so
Γ(chartRestrict 𝒜 F hg, U) is Γ(F, awayι 𝒜 g hg hd ''ᵁ U). What differs is the ring
acting. The chart's sections are a module over the away ring A_{(g)}; the same elements as
sections on Proj are a module over Γ(Proj 𝒜, D₊(g)). The comparison map between those two rings
is Mathlib's Proj.awayToSection, and awayToSection_isLocalizationElem_pow says it sends
(f / g)ⁿ to fracPowSection.
Two independent facts, and why the second one is the hard one #
awayToSection_isLocalizationElem_pow is elementary once the shapes line up: the degree-one case is
rfl, awayToSection is a ring hom so it commutes with ^ n, and the structure sheaf's ring
operations are pointwise, so the whole statement reduces to
(fⁿ / gⁿ) = (f / g)ⁿ inside one homogeneous localization.
ΓSpecIso_inv_appIso_inv is the one that costs something. The scalar action on the chart's sections
runs A_{(g)} → Γ(Spec A_{(g)}, ⊤) → Γ(Proj 𝒜, D₊(g)) through Scheme.ΓSpecIso and the open
immersion's Scheme.Hom.appIso, and nothing in Mathlib says that composite is awayToSection. It
is proved here by unfolding awayι into basicOpenIsoSpec.inv ≫ ι and using
basicOpenToSpec_app_top, which is the only place Mathlib pins awayToSection against the scheme
structure.
Elaboration notes #
ΓSpecIso_inv_appIso_inv needs backward.isDefEq.respectTransparency false, as Mathlib's own
basicOpenIsoAway does. Without it the goal is reported as "not type-correct under the instances
transparency level" after the first rewrite and every later rw — including Category.assoc —
silently fails to match. With it the associativity normalises and the reassoc forms of
Scheme.Hom.naturality apply.
Transports between opens of Proj 𝒜 are collapsed by Subsingleton.elim: Opens is a poset, so
parallel morphisms are equal and congrArg presheaf.map closes what rw [← Functor.map_comp]
cannot see through.
Scope #
The dictionary only. The Proj-side restatements of the chart lemmas, the cover, the single exponent, and the gluing are not here.
The structure sheaf's powers, pointwise #
A power of a section of the structure sheaf is the pointwise power.
Mathlib records Proj.mul_apply and Proj.one_apply but no power law; the ring structure on
sections is pointwise, so this is those two and an induction.
awayToSection on the chart's distinguished element #
The fraction the chart's distinguished element becomes on Proj 𝒜.
HomogeneousLocalization.Away.isLocalizationElem hg hf is f ^ d / g ^ e for f ∈ 𝒜 e and
g ∈ 𝒜 d; this is its n-th power as a section of the structure sheaf over any open inside
D₊(g). Named because the degree bookkeeping -- both numerator and denominator sit in
(e • d) • n -- is unreadable inline, and fracSection_eq turns it into whatever spelling a use
site wants.
Equations
- AlgebraicGeometry.Proj.isLocalizationFrac 𝒜 hf hg n hU = AlgebraicGeometry.Proj.fracSection 𝒜 ⋯ ⋯ ⋯
Instances For
The base case, and it is definitional.
awayToSection sends f ^ d / g ^ e to the section x ↦ f ^ d / g ^ e, by the definition of
HomogeneousLocalization.mapId on a representative.
awayToSection carries (f ^ d / g ^ e) ^ n to the section of the same name.
This is the dictionary entry #585 needs: the chart lemmas clear the away-ring element
isLocalizationElem hg hf, and every statement on Proj 𝒜 is scaled by a fracSection.
The chart's structure map is awayToSection #
A chart of any positive degree covers exactly its own basic open.
degreeOneChart_image_top is the case d = 1; #585's pairwise overlaps are cut out by a product
of two degree-one elements, so the degree-two case is needed as well.
A chart meets another basic open in the intersection of the two.
degreeOneChart_image_basicOpen at arbitrary positive degrees, which is what #585 needs on a
pairwise overlap: the chart is that of gᵢ gⱼ and the second element is f.
Every open of the chart lands inside D₊(g).
The chart's ring map is Mathlib's awayToSection.
The scalar acting on a chart section reaches Γ(Proj 𝒜, D₊(g)) through Scheme.ΓSpecIso and the
open immersion's Scheme.Hom.appIso; this says that composite is awayToSection, transported
along degreeOneChart_image_top.
Proved by unfolding awayι into basicOpenIsoSpec.inv ≫ (basicOpen 𝒜 g).ι and quoting
basicOpenToSpec_app_top, the single place Mathlib pins awayToSection against the scheme
structure. Everything else cancels: the two halves of basicOpenIsoSpec on the chart, and poset
transports on Proj 𝒜.
The chart ring acts through awayToSection, over every open of the chart.
ΓSpecIso_inv_appIso_inv is the case U = ⊤; Scheme.Hom.appIso_inv_naturality spreads it over
the rest, and the two transports on Proj 𝒜 collapse because Opens is a poset.
The chart's scalar action, rewritten on Proj 𝒜.
The elements are the same on both sides -- Scheme.Modules.restrictAppIso is Iso.refl -- and
only the acting ring changes: a : A_{(g)} acts as the structure-sheaf section
awayToSection 𝒜 g a, restricted to the chart's image.
The chart's distinguished scalar is fⁿ / gⁿ on Proj 𝒜.
chart_smul_eq and awayToSection_isLocalizationElem_pow together: this is the single lemma the
Proj-side restatements of ChartExtension.lean consume.