Exactness for a two-piece Laurent cover #
Let A be a complete Hausdorff strongly noetherian Tate ring and f ∈ A. The rational subsets
U₁ = R({f, 1}/1) = {|f| ≤ 1}, U₂ = R({1}/f) = {|f| ≥ 1}, U₁ ∩ U₂ = R({f², f, 1}/(1 · f))
cover Spa(A, A⁺); the presentation of U₁ ∩ U₂ is the one rationalSubset_inter produces.
Wedhorn's Lemma 8.33 says that the augmented Čech complex of the structure presheaf on this
cover is exact:
0 → A → A⟨U₁⟩ × A⟨U₂⟩ → A⟨U₁ ∩ U₂⟩ → 0, a ↦ (a, a), (x, y) ↦ x|U₁∩U₂ - y|U₁∩U₂.
Here A⟨U⟩ is the completed rational localisation UniformSpace.Completion S of a presentation,
the first map is the product of the structure maps toCompletionLoc, and the restrictions are the
maps restrictionRingHom of the refinements 1 · f = 1 · f (cofactor f) and 1 · f = f · 1
(cofactor 1). Each presentation carries its own localisation S, but only U₂ needs a
HasDenominatorPower hypothesis: the one for U₁ is automatic at the denominator 1
(TauCeti.Huber.PairOfDefinition.hasDenominatorPower_denom_one), and the one for U₁ ∩ U₂ is
built from those two by TauCeti.Huber.PairOfDefinition.hasDenominatorPower_mul.
Main results #
TauCeti.ValuationSpectrum.laurentCover_injective:A → A⟨U₁⟩ × A⟨U₂⟩is injective.TauCeti.ValuationSpectrum.laurentCover_exact: the kernel of the difference of restrictionsA⟨U₁⟩ × A⟨U₂⟩ → A⟨U₁ ∩ U₂⟩is the image ofA.TauCeti.ValuationSpectrum.laurentCover_surjective: the difference of restrictions is surjective.TauCeti.ValuationSpectrum.spa_subset_iUnion_laurentCover: the geometric half — the two pieces really do coverSpa(A, A⁺).
Implementation notes #
As in Wedhorn's (8.2.1), the coordinate rings are presented as quotients of restricted power
series by TauCeti.Huber.PairOfDefinition.rationalQuotientRingEquiv, for U₂ at the single
numerator 1 over the denominator f:
A⟨U₁⟩ = A⟨X⟩ ⧸ (f - X), A⟨U₂⟩ = A⟨Y⟩ ⧸ (1 - f Y), A⟨U₁ ∩ U₂⟩ = A⟨X, Y⟩ ⧸ (f² - f X, 1 - f Y).
The last ideal lies in (f - X, 1 - XY), and under these presentations the two restriction maps
are induced by the embeddings A⟨T⟩ → A⟨X, Y⟩, T ↦ X and T ↦ Y. The diagram chase then
reduces surjectivity to TauCeti.Huber.laurentDiff_surjective on A⟨ζ, ζ⁻¹⟩ = A⟨X, Y⟩ ⧸ (1 - XY),
and exactness to TauCeti.Huber.exact_algebraMap_laurentCoverDiff on the quotient presentations
of the cover. Transporting the latter needs only that the presentation maps factor through those
quotients, which is what the relation hypotheses say; no isomorphism between them is required.
Injectivity is Corollary 8.32 for the pair (A, A°).
The numerator sets are Finset literals, so writing them down needs decidable equality on A.
That is an artefact of the notation rather than a hypothesis of the mathematics, so the public
results take their instance from Classical.decEq instead of assuming DecidableEq A; the
private helpers below stay polymorphic in the instance.
References #
- T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), (8.2.1) and Lemma 8.33.
Provenance #
AINTLIB (github.com/CBirkbeck/AINTLIB, branch dev/adic-spaces, commit 37bbdaeb9,
Apache-2.0), projects/AdicSpaces/Adic spaces/LaurentCoverExact.lean, proves the lemma for its
quotient rings B₁_gen f = A⟨X⟩ ⧸ (f - X), B₂_gen f = A⟨X⟩ ⧸ (1 - f X) and
B₁₂_gen f = A⟨ζ, ζ⁻¹⟩ ⧸ (f - ζ), over its own TateAlgebra and
LaurentTateAlgebra A = TateAlgebra₂ A ⧸ (XY - 1). The exactness and surjectivity are
ker_deltaMap_gen_le_range_epsilonHom_gen and deltaMap_gen_surjective (bundled in row3_exact),
by a chase through ker_lambdaMap_le_range_iotaHom (row2_exact_at_middle) and
lambdaMap_surjective; its injectivity, epsilonHom_gen_injective, is proved for a noetherian
domain and a non-unit f by the Krull intersection theorem. The chase here has the same shape.
The statements differ: they concern the completed rational localisations and their restriction
maps, reached through Example 6.38, and injectivity comes from Corollary 8.32 without a domain
hypothesis. No AINTLIB code is copied.
The diagram chase #
The three presentations of the Laurent cover #
The coordinate rings of the Laurent cover as quotients #
Exactness #
Wedhorn's Lemma 8.33, exactness in the middle. Let A be a complete Hausdorff strongly
noetherian Tate ring and f ∈ A, and let U₁ = R({f, 1}/1), U₂ = R({1}/f) and
U₁ ∩ U₂ = R({f², f, 1}/(1 · f)). In
A → A⟨U₁⟩ × A⟨U₂⟩ → A⟨U₁ ∩ U₂⟩, a ↦ (a, a), (x, y) ↦ x|U₁∩U₂ - y|U₁∩U₂,
the kernel of the second map is the image of the first. The restriction maps are those of the
refinements with cofactors f and 1. The first map is injective (laurentCover_injective) and
the second surjective (laurentCover_surjective). Only U₂ comes with a standing hypothesis: the
one for U₁ is automatic at the denominator 1
(TauCeti.Huber.PairOfDefinition.hasDenominatorPower_denom_one), and the one for U₁ ∩ U₂ is
built from those two by TauCeti.Huber.PairOfDefinition.hasDenominatorPower_mul.
Wedhorn's Lemma 8.33, surjectivity. In the notation of laurentCover_exact, the
difference of restrictions
A⟨U₁⟩ × A⟨U₂⟩ → A⟨U₁ ∩ U₂⟩, (x, y) ↦ x|U₁∩U₂ - y|U₁∩U₂
is surjective. As in laurentCover_exact, only U₂ comes with a standing hypothesis: the one for
U₁ is automatic at the denominator 1 and the one for U₁ ∩ U₂ is built from those two.
Exactness in the middle and injectivity of a ↦ (a, a) are laurentCover_exact and
laurentCover_injective.
Injectivity #
The two Laurent pieces cover the adic spectrum. For f ∈ A, every point of
Spa(A, A⁺) lies in U₁ = R({f, 1}/1) or in U₂ = R({1}/f), indexed here by Bool so that
the two pieces form a single family. Every point lies in R({f, 1}/f) or in R({f, 1}/1), and
the first of these lies in R({1}/f).
This is the geometric half of the two-piece Laurent cover; laurentCover_exact,
laurentCover_surjective and laurentCover_injective are the algebraic half.
Wedhorn's Lemma 8.33, injectivity. Let A be a complete Hausdorff strongly noetherian
Tate ring and f ∈ A. The map A → A⟨U₁⟩ × A⟨U₂⟩, a ↦ (a, a), into the coordinate rings of
U₁ = R({f, 1}/1) and U₂ = R({1}/f) is injective. Unlike the other two results of this file it
needs no presentation of U₁ ∩ U₂, and no ring of integral elements has to be chosen.
The two localisations may lie in independent universes. Exactness in the middle and
surjectivity are laurentCover_exact and laurentCover_surjective.