Clearing a denominator on an affine #
A section of a quasi-coherent sheaf over a basic open D(r), multiplied by a high enough power of
r, is the restriction of a global section. This is the chart-local engine of #585: on
Proj 𝒜 a degree-one chart is Spec (A_{(g)}), D₊(f) meets it in the basic open of f / g
(Proj.awayι_preimage_basicOpen), and this is what clears that denominator.
Why it is six lines, and what that changes #
Not by an argument but by an instance. Mathlib carries
instance (f : R) : IsLocalizedModule.Away f (tilde.toOpen M (basicOpen f)).hom
so Γ(D(r), M~) is the localization M_r, and clearing the denominator is
IsLocalizedModule.surj: a section is m / rⁿ by the definition of the localization rather than
by a theorem about it. The passage from "comes from M" to "restricts from a global section" is
then tilde.toOpen_res, which is rfl.
Worth recording against the plan #585 was written to.
Submodule.exists_pow_smul_mem_of_isLocalized_radical — extracted into
Algebra/Module/LocalizedRadical.lean for this very issue — is not needed here, and in the end
#585 did not reach for it anywhere. The plan expected it to reconcile two charts on their overlap;
what closed that step instead was separatedness on the overlap, which is the chart of gᵢ gⱼ and so
of degree two (Proj/Modules/AwayChart.lean). The lemma's live consumer is the Čech
affine-vanishing argument it was extracted from.
Both halves, and dropping the tilde hypothesis #
Extension makes a local section global; exists_pow_smul_res_eq_zero is its injectivity
companion — a global section restricting to 0 on D(r) is killed by a power of r — and the two
together are what a gluing argument over a cover needs. The second rests on Mathlib's
isIso_toOpen_top, so every section over ⊤ is toOpen M ⊤ m and the elementwise statement
applies directly.
Both are stated for a tilde, and #585 needs them for an arbitrary quasi-coherent sheaf. The
transport is the same both times, so it is done once, as a linear equivalence on sections
(tildeΓSectionEquiv) with its two restriction laws, rather than twice by hand.
That is not a stylistic preference; the by-hand version does not scale, and the second attempt at it did not go through at all. Two hazards, both worth knowing before writing in this file:
rwdoes not findmap_subthroughConcreteCategory.hom.rw [LinearMap.map_sub]on a goal of the form(ConcreteCategory.hom (P.map i)) (t - t') = 0fails with "did not find an occurrence of the pattern?f (?x - ?y)", and so doessimp only [map_sub]. Spelling the additivity out as ahavewith both sides written and closing it byexact LinearMap.map_sub _ _ _works, because the explicit statement guides elaboration through the coercion. Same shape as the hazard below: the term is right, the matcher cannot see it.rwdoes not see proof irrelevance. Transporting the injectivity statement by rewriting fails on patterns that print character-identical to the goal: the difference is inside the elided⋯, where two elaborations ofle_topgive different proof terms.simp onlydoes not match either. What works is abandoning rewriting —congrArg … |>.trans, sinceexactunifies up to defeq and proof irrelevance is definitional. Naming the transport as aLinearEquivconfines this to one place._root_shadowing. InsideAlgebraicGeometry.tildeandAlgebraicGeometry.Scheme.Modules, the bare namesmap_smulandmap_zeroresolve to other lemmas — aboutpresheaf.mapand abouttilde.map. Both must be written_root_.map_smul/_root_.map_zero. This cost four cycles across the file. Same class of hazard asreferences/instance-transparency.md: a name that silently resolves to the wrong thing.
Scope #
One affine, one basic open. The Proj chart application, the choice of one n across a finite
cover, and the passage from (f / g)ⁿ · to multiplication into the twist F(n) are not here; they
are Proj/Modules/ChartExtension.lean and Proj/Modules/Glue.lean, where #585 is closed by
exists_globalSection_twistBy.
A section of M~ over a basic open extends after clearing one power of the defining
element.
The same, as an extension statement: a power of r times a section over D(r) is the
restriction of a global section.
A global section vanishing on D(r) is killed by a power of r.
The injectivity companion of exists_pow_smul_eq_toOpen, and the other half of what a gluing
argument needs: extension makes local sections global, this makes two of them agree.
The same on sections: a global section restricting to 0 on D(r) is killed by a power
of r.
Transporting across quasi-coherence #
Both statements above are about a tilde, and #585 needs them for an arbitrary quasi-coherent
sheaf. The transport is the same both times, so it is done once here as a linear equivalence on
sections rather than twice by hand as natural-transformation rewriting.
That is not a stylistic preference. Written inline, the transport is three rws against a natural
transformation, and they refuse to fire on patterns that print identically to the goal — the
le_top proofs inside homOfLE ⋯ differ, and rw matches syntactically. Named as a
LinearEquiv, the same steps are map_smul and map_zero from the LinearEquiv API, which
carry no such hazard.
The quasi-coherence isomorphism on the sections over one open, as a linear equivalence.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The equivalence commutes with restriction. The one fact the transports need, proved once where the spelling is under this file's control.
The inverse equivalence commutes with restriction, which is the direction the injectivity transport needs.
The affine extension lemma for any quasi-coherent module sheaf, not only a tilde.
The injectivity companion for any quasi-coherent module sheaf.
Two sections agreeing on D(r) agree after clearing a power of r.
The two-section form of exists_pow_smul_res_eq_zero_of_isQuasicoherent, applied
to the difference. This is the shape a gluing argument consumes: a cover's local
pieces are first shown to agree on the smaller open where a section is given,
and this upgrades that to agreement on the whole overlap at the cost of raising
the exponent — a raise the uniform-exponent step then absorbs.
Note the conclusion is agreement of r ^ n • t with r ^ n • t', not of t
with t': nothing here says the restriction is injective, and for a sheaf with
r-torsion sections it is not.