Completeness of the weighted restricted power series over a complete base #
Over a nonarchimedean ring A whose weights Tν = T₁^ν₁ ⋯ Tₖ^νₖ are bounded
(TauCeti.Huber.IsBounded), the weighted restricted power-series ring
TauCeti.Huber.weightedRestrictedSubring is Hausdorff whenever A is, and complete over a
complete uniform A. Boundedness is the whole of what the arguments need beyond Wedhorn's
standing hypothesis: the neighbourhood subgroup U⟨X⟩ maps into Tν · U coefficientwise, and
boundedness of Tν says exactly that Tν · U still shrinks to zero with U, so the
coefficient maps are continuous — and uniformly continuous once A carries a uniformity.
Points are then separated coefficientwise, and a Cauchy filter of restricted series is
coefficientwise Cauchy, its coefficientwise limit is again restricted, and the filter converges
to it. Both facts are Wedhorn's Proposition 5.49 (Adic Spaces, arXiv:1910.05934v1) —
Hausdorffness is its part (2), and completeness is the step its part (3) is proved by, the one
that then identifies A⟨X⟩_T with the completion of A[X]_T. Its part (1), density of the
polynomials, is TauCeti.Huber.dense_weightedPolynomials in the parent module.
The trivial weight family Tᵢ = {1} is bounded, since Tν is then the singleton {1}, so the
ordinary restricted power-series ring A⟨X⟩ gets each of the four facts by specialisation. It
is that case the comparison below runs on, and the two T0Space/CompleteSpace statements are
registered as instances there.
Hausdorffness is purely topological — it uses only continuity of the coefficient maps — so it
is proved in a section over a nonarchimedean ring with no uniformity of its own, which is the
setting the rest of the Huber development works in; the uniform hypotheses on A enter only
with completeness.
Consequently TauCeti.Huber.restrictedMvPowerSeriesCompletion k A collapses:
TauCeti.Huber.restrictedMvPowerSeriesCompletionEquiv identifies A⟨X₁,…,Xₖ⟩ with the
plain restricted-series ring — the "comparison with the usual completed restricted
power-series algebra" milestone of roadmap Layer 0.5. Its hypotheses are completeness and
Hausdorffness of that ring itself rather than of A, which the instances here supply over a
complete Hausdorff base and which hold over a discrete base too, so that the comparison also
covers TauCeti.Huber.IsStronglyNoetherian.of_discreteTopology. It is packaged twice over
one and the same underlying map — as that ring isomorphism and as the A-algebra equivalence
TauCeti.Huber.restrictedMvPowerSeriesCompletionAlgEquiv, the two tied together by
TauCeti.Huber.coe_restrictedMvPowerSeriesCompletionAlgEquiv and
TauCeti.Huber.coe_restrictedMvPowerSeriesCompletionAlgEquiv_symm — and both it and its
inverse are uniformly continuous, hence continuous by UniformContinuous.continuous. Nothing
in that block is special to restricted series: every declaration in it specializes a generic
statement about UniformSpace.Completion.completeRingEquivSelf proved in
TauCeti.Topology.Algebra.UniformRing.
Three steps are named as private lemmas rather than exported as API. That the subring's
uniformity is the one its subgroup basis induces is definitional, and is named so that the
argument does not silently depend on the two being reducibly equal; it specializes Mathlib's
AddGroupFilterBasis.cauchy_iff, with a single use here. The passage of a Cauchy filter to its
coefficientwise limits — where Tν · U has to be closed, by
TauCeti.Huber.IsWeightFamily.isOpen_weightMul and AddSubgroup.isClosed_of_isOpen — is used
twice in the completeness proof. Boundedness of the trivial weight, read off
TauCeti.Huber.weightPow_one_weight and TauCeti.Huber.isBounded_singleton, is what all four
specialisations are discharged with.
Main results #
TauCeti.Huber.IsWeightFamily.continuous_coeffandTauCeti.Huber.IsWeightFamily.uniformContinuous_coeff: theν-th coefficient map ofA⟨X⟩_Tis continuous, and uniformly continuous over a uniform base, as soon as the single weightTνis bounded.TauCeti.Huber.t0Space_weightedRestrictedSubring: Wedhorn 5.49(2) — with every weight bounded,A⟨X⟩_Tover a Hausdorff base is Hausdorff.TauCeti.Huber.completeSpace_weightedRestrictedSubring: Wedhorn 5.49(3) — with every weight bounded,A⟨X⟩_Tover a complete base is complete.TauCeti.Huber.continuous_coeff_one_weight,TauCeti.Huber.t0Space_weightedRestrictedSubring_one_weight,TauCeti.Huber.uniformContinuous_coeff_one_weightandTauCeti.Huber.completeSpace_weightedRestrictedSubring_one_weight: those four at the trivial weight family. TheT0SpaceandCompleteSpaceones are the registered instances; the two coefficient-map results are theorems. This is the case the comparison needs.TauCeti.Huber.restrictedMvPowerSeriesCompletionEquiv: the comparison —A⟨X₁,…,Xₖ⟩is the plain restricted-series ring, whenever that ring is complete and Hausdorff.TauCeti.Huber.restrictedMvPowerSeriesCompletionAlgEquiv: the same comparison as anA-algebra equivalence.TauCeti.Huber.uniformContinuous_restrictedMvPowerSeriesCompletionEquivandTauCeti.Huber.uniformContinuous_restrictedMvPowerSeriesCompletionEquiv_symm: the comparison and its inverse are uniformly continuous. The inverse is the canonical map into the completion, which isTauCeti.Huber.coe_restrictedMvPowerSeriesCompletionEquiv_symm.
Provenance #
AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0) is the roadmap's designated prior
formalisation for this row. At commit 2baa76f742bdb4fb8ee323fabba41203bd390e08 its file
projects/AdicSpaces/Adic spaces/RestrictedPowerSeries.lean states nothing about
completeness, Hausdorffness, or the completion of the restricted-series ring, so there was
nothing to port here; nothing was copied.
References #
- T. Wedhorn, Adic Spaces, Proposition 5.49(2) and (3), for a bounded weight
family — of which the trivial family
Tᵢ = {1}is the case used below.
The coefficient maps and Hausdorffness #
Neither fact needs a uniformity on A: they hold over any nonarchimedean topological ring,
which is how A is fixed throughout the rest of the Huber development.
The ν-th coefficient map of A⟨X⟩_T is continuous as soon as the weight Tν is
bounded: the neighbourhood subgroup U⟨X⟩ maps into Tν · U coefficientwise, and boundedness
is exactly what makes Tν · U shrink with U.
A⟨X⟩_T over a Hausdorff base is Hausdorff (Wedhorn 5.49(2)) as soon as every weight is
bounded: the coefficient maps are then continuous, and they separate points.
At the trivial weight family the coefficient maps of A⟨X⟩ are continuous: the
neighbourhood subgroup U⟨X⟩ maps into U coefficientwise.
Restricted series over a Hausdorff base are Hausdorff (Wedhorn 5.49(2) at the trivial weight family), the case registered as an instance.
Completeness #
The ν-th coefficient map of A⟨X⟩_T is uniformly continuous as soon as the weight
Tν is bounded: it is then a continuous additive group homomorphism.
A⟨X⟩_T is complete over a complete base when every weight is bounded. This is the step
Wedhorn 5.49(3) is proved by: a Cauchy filter is coefficientwise Cauchy, its coefficientwise
limit is again T-restricted, and the filter converges to it.
At the trivial weight family the coefficient maps of A⟨X⟩ are uniformly continuous:
they are continuous additive group homomorphisms.
The trivial-weight restricted-series subring is complete whenever the base uniform nonarchimedean commutative ring is complete, the case registered as an instance.
The comparison with A⟨X₁,…,Xₖ⟩ #
The hypotheses are completeness and Hausdorffness of the restricted-series ring itself, not
of A: the instances above supply them over a complete Hausdorff base, and over a discrete
base they hold because the ring is then discrete. Each declaration specializes a generic
statement about UniformSpace.Completion.completeRingEquivSelf.
The comparison equivalence of roadmap Layer 0.5: when the plain restricted-series ring
is complete and Hausdorff, the completed restricted power-series algebra A⟨X₁,…,Xₖ⟩ is that
ring.
Equations
Instances For
The comparison undoes the canonical inclusion: on a restricted series regarded as an element of the completion, it returns that series.
The inverse comparison is the canonical inclusion: it sends a restricted series to itself, regarded as an element of the completion.
The inverse comparison is the canonical map into the completion, as a function.
The comparison is uniformly continuous: it is the uniform bijection between a complete Hausdorff space and its completion.
The inverse comparison is uniformly continuous: it is the canonical map into the completion.
The comparison as an A-algebra equivalence: the same identification, structure map
included. It is TauCeti.Huber.restrictedMvPowerSeriesCompletionEquiv rebundled, so the two
share an underlying map and the coercion lemmas for the latter apply to it.
Equations
- TauCeti.Huber.restrictedMvPowerSeriesCompletionAlgEquiv k A = UniformSpace.Completion.completeAlgEquivSelf (↥(TauCeti.Huber.weightedRestrictedSubring (fun (x : Fin k) => {1}) ⋯)) A
Instances For
The A-algebra equivalence has the same underlying map as the ring equivalence, so simp
normalises the algebra bundling onto the ring one.
The inverses agree too, so the two bundlings normalise together in both directions.