The Laurent quotients A⟨X⟩/(f - X) and A⟨X⟩/(1 - f X) are flat #
Wedhorn's Lemma 8.31(2): for a complete noetherian Tate ring A and f ∈ A, the rings
A⟨X⟩/(f - X) and A⟨X⟩/(1 - f X) are flat over A. They are the coordinate rings of the
Laurent rational subsets {|f| ≤ 1} and {|f| ≥ 1} of Spa A (Wedhorn, Example 6.38), which is
why Proposition 8.30 consumes them.
Wedhorn's "complete noetherian Tate ring" is spelled here as the full standing hypothesis list of
the final section: A is a complete T0 uniform additive group whose uniformity is countably
generated, and is a nonarchimedean, Tate and noetherian ring (CompleteSpace, T0Space,
(𝓤 A).IsCountablyGenerated, NonarchimedeanRing, IsTateRing, IsNoetherianRing). The
uniform-structure hypotheses are what make Wedhorn's completeness and separation assumptions
usable in Lean; none of them is derivable from the others here.
Wedhorn's proof: A⟨X⟩/(g) is flat as soon as multiplication by g is injective on M⟨X⟩ for
every finitely generated M — the Tor-sequence claim that is
Module.Flat.quotient_span_singleton_of_lTensor_mulLeft_injective — and for g = 1 - f X and
g = f - X that injectivity is a computation on the coefficients of M⟨X⟩ = M ⊗[A] A⟨X⟩
(Remark 8.29).
Main results #
TauCeti.Huber.flat_quotient_algebraMap_sub_restrictedX:A⟨X⟩/(f - X)is flat overA.TauCeti.Huber.flat_quotient_one_sub_algebraMap_mul_restrictedX:A⟨X⟩/(1 - f X)is flat overA.TauCeti.Huber.mulX: multiplication byXon series with coefficients in a module, which shifts every coefficient up by one;TauCeti.Huber.restrictedMulXrestricts it toM⟨X⟩.
Implementation notes #
The comparison map intertwines X • · on M ⊗[A] A⟨X⟩ with multiplication by X on M⟨X⟩
(restrictedMvPowerSeriesBaseChange_comp_lTensor_mulLeft_restrictedX), and scalars act as
scalars. So (1 - f X) • · and (f - X) • · on M ⊗[A] A⟨X⟩ are id - f • mulX and
f • id - mulX on coefficients — that is
lTensor_mulLeft_one_sub_algebraMap_mul_restrictedX and
lTensor_mulLeft_algebraMap_sub_restrictedX. The first is injective by induction
on the coefficient index. The second is Wedhorn's argument: if f • s = X s then f • s₀ = 0
and f • sⱼ₊₁ = sⱼ, so every coefficient is a power of f times a later one; the chain of
submodules spanned by the initial coefficients stabilises because M is noetherian, the
stabilised submodule is generated by a single coefficient sₗ, and
sₗ = f ^ (l + 1) • s₂ₗ₊₁ = a • f ^ (l + 1) • sₗ = 0. Both are transported through the injective
comparison map to (A ⧸ I) ⊗[A] A⟨X⟩, which is what the ideal criterion asks for. That criterion
is this repository's own Module.Flat.quotient_span_singleton_of_lTensor_mulLeft_injective
(TauCeti/RingTheory/Flat/QuotientRegular.lean), built on Mathlib's
Module.Flat.iff_rTensor_injective. No topology enters
beyond the module topology of A ⧸ I (IsModuleTopology.instQuot).
Exponents of one-variable series are identified with ℕ through Finsupp.uniqueEquiv;
multiplication by X is stated on MvPowerSeries (Fin 1) M, with no topology, and restricted
afterwards.
References #
- Wedhorn, Adic Spaces, Lemma 8.31 and Example 6.38.
- AINTLIB, branch
dev/adic-spaces, at commit37bbdaeb9,projects/AdicSpaces/Adic spaces/Wedhorn828.lean.
Provenance #
Nothing here is ported. The ideal criterion is this repository's
Module.Flat.quotient_span_singleton_of_lTensor_mulLeft_injective; the comparison map and
the module-coefficient layer M⟨X⟩ it runs on are Restricted/BaseChange.lean and
Restricted/PowerSeries.lean; the rest is new here.
AINTLIB (github.com/CBirkbeck/AINTLIB @ 37bbdaeb9, Apache-2.0), the roadmap's designated
prior formalisation for this layer, does prove Lemma 8.31(2), and both shapes of it:
Adic spaces/Wedhorn828.lean has lemma_8_31_fSubX_flat (A⟨X⟩/(f − X) flat) and
lemma_8_31_oneSubfX_flat (A⟨X⟩/(1 − fX) flat), with lemma_8_31_tateAlgebra_faithfullyFlat
for 8.31(1). They were consulted, not ported, and the reason is the object rather than the
statement. Both are stated over AINTLIB's TateAlgebra A, which this repository does not
have, and both are proved by saturation — Module.Flat.quotient_of_flat_of_saturated applied
to mul_fSubX_regular / mul_oneSubfX_regular and the two *_saturated_faithful lemmas —
not by Wedhorn's coefficient argument. That argument needs series with coefficients in a
module, and Restricted/PowerSeries.lean records under its own Provenance that AINTLIB's
TateAlgebra layer is a ring-coefficient object with no M⟨X⟩ at all. So the route here is
not available there, and porting theirs would mean porting the TateAlgebra layer and its
saturation machinery instead. The hypotheses are comparable rather than weaker: AINTLIB
carries [IsTateRing A] [IsNoetherianRing A] [T2Space A] (and [IsStronglyNoetherian A] on
the f − X shape), this file [IsTateRing A] [IsNoetherianRing A] with a completeness bundle.
That check was made by reading AINTLIB's declarations under their own names, not by grepping
this repository's vocabulary — the method that produced the false negative BaseChange.lean
records. Their sorry-freeness was measured with comments stripped: a plain grep sorry on
Wedhorn828.lean reports 17 hits and every one is a docstring mention, mostly the phrase
"sorry-free", so the file has none; the same instrument reports 9 in Presheaf.lean, which
is the control that it can find one.
One variable: multiplication by X #
Stated over a semiring and an additive monoid: it is pure reindexing, and nothing here
needs subtraction. The regularity results below, which do, keep CommRing and AddCommGroup.
Multiplication by X on series with coefficients in a module: on coefficients it is
∑ mⱼ Xʲ ↦ ∑ mⱼ Xʲ⁺¹. This is what X • · on M⟨X⟩ = M ⊗[A] A⟨X⟩ looks like on coefficients
(restrictedMvPowerSeriesBaseChange_tmul_restrictedX_mul).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The coefficients of mulX A s: it vanishes in degree 0, and in every other
degree it takes the coefficient of s one degree down.
mulX A s has no constant term.
Not @[simp]: the general equation coeff_mulX above is @[simp] and rewrites this
left-hand side first, so annotating the degree-0 specialisation too would leave it out of
simp normal form. simp proves this statement on its own.
In degree j + 1, mulX A s takes the degree-j coefficient of s.
Deliberately not @[simp]: Finsupp.single 0 (j + 1) is not in simp normal form, since
Finsupp.single_add rewrites it to Finsupp.single 0 j + Finsupp.single 0 1, so the
annotation could never fire. The uses in this file rewrite with it explicitly.
Multiplication by X preserves restrictedness: it reindexes coefficients along j ↦ j + 1.
Multiplication by X and by scalars, through the comparison map #
Multiplication by X on M⟨X⟩.
Equations
Instances For
restrictedMulX acts as mulX on the underlying series.
On a pure tensor, multiplying the series factor by X shifts the coefficients of the
comparison map's value up by one.
The comparison map intertwines X • · on M ⊗[A] A⟨X⟩ with multiplication by X.
Through the comparison map, X • · on M ⊗[A] A⟨X⟩ is multiplication by X on M⟨X⟩.
(1 - f X) • · on M ⊗[A] A⟨X⟩, in terms of X • ·.
(f - X) • · on M ⊗[A] A⟨X⟩, in terms of X • ·.
Regularity of 1 - f X and of f - X on MvPowerSeries (Fin 1) M #
Restrictedness is irrelevant to these two lemmas, so they are stated on all of
MvPowerSeries (Fin 1) M, with no topology; the statements on M⟨X⟩ follow by restriction.
Multiplication by 1 - f X is injective on series with coefficients in any module.
Multiplication by f - X is injective on series with coefficients in a noetherian
module.
Lemma 8.31(2) #
1 - f X acts injectively on N ⊗[A] A⟨X⟩ for a finite N with its module topology.
f - X acts injectively on N ⊗[A] A⟨X⟩ for a finite N with its module topology.
A⟨X⟩/(f - X) is flat over a complete noetherian Tate ring (Wedhorn, Lemma 8.31(2)).
"Complete noetherian Tate ring" abbreviates this section's standing hypotheses on A:
CompleteSpace, T0Space and (𝓤 A).IsCountablyGenerated for the uniform structure, and
NonarchimedeanRing, IsTateRing, IsNoetherianRing for the ring.
A⟨X⟩/(1 - f X) is flat over a complete noetherian Tate ring (Wedhorn, Lemma 8.31(2)).
Same standing hypotheses on A as flat_quotient_algebraMap_sub_restrictedX.