The row 0 → A → A⟨ζ⟩ × A⟨η⟩ → A⟨ζ, ζ⁻¹⟩ → 0 #
Let A be a nonarchimedean commutative ring. For the full short exact row, assume moreover that
A is complete and separated; the individual constructions and injectivity use weaker
hypotheses. Wedhorn's ring of the overlap of a two-piece Laurent cover is
A⟨ζ, ζ⁻¹⟩ = A⟨X, Y⟩ ⧸ (1 - XY),
the quotient of the restricted power series in two variables by TauCeti.Huber.laurentIdeal. In
it the class of X is a unit with inverse the class of Y
(TauCeti.Huber.isUnit_mk_weightedX_zero), which is what the notation ζ⁻¹ refers to.
The two pieces A⟨ζ⟩ and A⟨η⟩ are copies of the restricted power series in one variable, mapped
into A⟨X, Y⟩ by ζ ↦ X and η ↦ Y (TauCeti.Huber.weightedRename along Fin.castSuccEmb and
Fin.succEmb 1). This file assembles them into the row
0 → A --ι--> A⟨ζ⟩ × A⟨η⟩ --λ--> A⟨ζ, ζ⁻¹⟩ → 0,
with ι the constants on both pieces — the structure map of the product A-algebra — and
λ (g, h) = g(ζ) - h(ζ⁻¹), and proves that it is exact: ι is injective, λ is surjective, and
the kernel of λ is the image of ι. The two substantial inputs are the decomposition
A⟨ζ, ζ⁻¹⟩ = A⟨ζ⟩ + ζ⁻¹A⟨ζ⁻¹⟩ and the rigidity of the overlap — a series in ζ agreeing with a
series in ζ⁻¹ is constant — both proved in
TauCeti.RingTheory.Huber.WeightedRestrictedSeries.Diagonal; completeness of A enters only
through the first.
Main definitions #
TauCeti.Huber.laurentIdeal: the ideal(1 - XY)ofA⟨X, Y⟩.TauCeti.Huber.laurentDiff: the mapλ. The mapιis the structure map of the product algebraA⟨ζ⟩ × A⟨η⟩, so it needs no definition of its own.
Main results #
TauCeti.Huber.algebraMap_prod_weightedRestrictedSubring_injectiveandTauCeti.Huber.laurentDiff_surjective: the two ends of the row.TauCeti.Huber.exact_algebraMap_laurentDiff: exactness in the middle,ker λ = im ι.TauCeti.Huber.isUnit_mk_weightedX_zero: the class ofXis a unit inA⟨ζ, ζ⁻¹⟩.TauCeti.Huber.laurentIdeal_ne_top:A⟨ζ, ζ⁻¹⟩is not the zero ring whenAis not. In particular1 - XY, which is a unit inA[[X, Y]], is not one inA⟨X, Y⟩.
References #
- T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Example 6.39, (8.2.1) and the proof of Lemma 8.33, p. 84.
Provenance #
As recorded in the sibling file …WeightedRestrictedSeries.Diagonal, AINTLIB
(github.com/CBirkbeck/AINTLIB, Apache-2.0) at commit 37bbdaeb9,
projects/AdicSpaces/Adic spaces/LaurentCoverExact.lean, assembles the same row for its
LaurentTateAlgebra A := TateAlgebra₂ A ⧸ (XY - 1), out of homomorphisms iotaHom and
lambdaMap and the two statements ker_lambdaMap_le_range_iotaHom and lambdaMap_surjective.
Here the two inputs are the trivial-weight statements of …Diagonal, ι is the structure map of
the product algebra rather than a named homomorphism, and the row is packaged as
Function.Exact.
The ideal (1 - XY) of A⟨X, Y⟩, whose quotient is Wedhorn's ring A⟨ζ, ζ⁻¹⟩ of the
overlap of a two-piece Laurent cover: killing 1 - XY makes the class of Y inverse to the class
of X.
Equations
- TauCeti.Huber.laurentIdeal A = Ideal.span {1 - TauCeti.Huber.weightedX (fun (x : Fin 2) => {1}) ⋯ 0 * TauCeti.Huber.weightedX (fun (x : Fin 2) => {1}) ⋯ 1}
Instances For
Membership in (1 - XY) is divisibility by 1 - XY.
In A⟨ζ, ζ⁻¹⟩, the class of Y is a right inverse to the class of X.
The class of X is a unit in A⟨ζ, ζ⁻¹⟩, with inverse the class of Y. This is what
makes the quotient a ring of Laurent, rather than of ordinary, restricted series.
Wedhorn's λ : A⟨ζ⟩ × A⟨η⟩ → A⟨ζ, ζ⁻¹⟩, (g, h) ↦ g(ζ) - h(ζ⁻¹): the difference of the
classes of g read in X and of h read in Y. It is additive but not multiplicative.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The row is exact in the middle: a pair (g, h) with g(ζ) = h(ζ⁻¹) in A⟨ζ, ζ⁻¹⟩ is a
pair of equal constants, and conversely. This is Wedhorn's ker λ = im ι in the proof of
Lemma 8.33.
A⟨ζ, ζ⁻¹⟩ is not the zero ring when A is not: the ideal (1 - XY) is proper. Note
that 1 - XY is a unit in the ambient ring A[[X, Y]] of all power series, its inverse being
the series ∑ (XY)ⁿ, which is not restricted.
λ is surjective: every element of A⟨ζ, ζ⁻¹⟩ is g(ζ) - h(ζ⁻¹). This is Wedhorn's
decomposition A⟨ζ, ζ⁻¹⟩ = A⟨ζ⟩ + ζ⁻¹A⟨ζ⁻¹⟩, read through λ.