Base change for restricted power series #
Wedhorn's Remark 8.29 compares M ⊗[A] A⟨T₁, …, Tₖ⟩ with M⟨T₁, …, Tₖ⟩ for a finitely generated
module M over a complete noetherian Tate ring, and finds them isomorphic. This file builds the
comparison map in the generality where it exists — writing it down needs no finiteness and no
completeness, only continuity of the scalar action, beyond the hypotheses the two objects
themselves carry, namely that A is nonarchimedean (without which A⟨T₁, …, Tₖ⟩ is not a
subring) and ContinuousAdd M (without which M⟨T₁, …, Tₖ⟩ is not a submodule) — and then proves
Remark 8.29 by reducing along a strict finite presentation of M.
The ambient map is Mathlib's: TensorProduct.piScalarRightHom A A M (Fin k →₀ ℕ) already has the
type M ⊗[A] MvPowerSeries (Fin k) A →ₗ[A] MvPowerSeries (Fin k) M.
Main definitions #
mvPowerSeriesBaseChange: that map, with its codomain ascribed asMvPowerSeries (Fin k) M.restrictedMvPowerSeriesBaseChange: the comparison map of Remark 8.29 itself,M ⊗[A] A⟨T₁, …, Tₖ⟩ →ₗ[A] M⟨T₁, …, Tₖ⟩.restrictedMvPowerSeriesFinPiEquivandtensorFinPiEquiv: the two identifications the finite free case runs through.
Main results #
mvPowerSeriesBaseChange_tmul: the map sendsm ⊗ₜ fto the coefficientwise scalar actions ↦ coeff s f • m, andcoeff_mvPowerSeriesBaseChange_tmulreads off a single coefficient.IsRestricted.mvPowerSeriesBaseChange_tmul: that series is restricted wheneverfis. It is whereContinuousSMul A Mis used — continuity ofa ↦ a • min the scalar, whichContinuousConstSMuldoes not give.restrictedMvPowerSeriesSubmoduleMap_baseChange: the comparison map is natural inM— anA-linear map continuous at0commutes with base change, which is what lets a presentation ofMbe pushed through the functor.coe_restrictedMvPowerSeriesBaseChange, withcoe_restrictedMvPowerSeriesBaseChange_tmul: read in the ambient series, the restricted map is the ambient one, at a general element and at a pure tensor;coeff_restrictedMvPowerSeriesBaseChange_tmulreads off a single coefficient.restrictedMvPowerSeriesBaseChangeFinEquiv, withrestrictedMvPowerSeriesBaseChange_fin_bijective: Remark 8.29's conclusion in the finite free case — the comparison map packaged as a linear equivalence, and its bijectivity in the form a reduction argument consumes.restrictedMvPowerSeriesFinPiEquiv_baseChange: the transported equality behind it. ForM = Fin n → Athe comparison map is Mathlib's tensor-pi equivalence transported alongrestrictedMvPowerSeriesFinPiEquiv, so it is an isomorphism — the base case the finitely generated statement reduces to.restrictedMvPowerSeriesBaseChange_surjective_of_presentation: Remark 8.29's comparison map is surjective for anMpresented by a surjectionAᵐ ↠ Mthat is continuous at0and pushes the neighbourhoods of0forward. Only the presentation is used — no noetherian hypothesis and no property of its kernel, both of which belong to injectivity.restrictedMvPowerSeriesBaseChange_injective_of_presentation: the comparison map is injective for anMpresented byAⁿ →[u] Aᵐ →[p] M → 0whose first map is strict onto its image. This is the half surjectivity leaves open, and it is where exactness of the presentation is used; it runs on Mathlib's four lemma rather than on a hand-rolled diagram chase. It asksMto be anAddCommGroup, unlike the rest of this file: a diagram chase subtracts.restrictedMvPowerSeriesBaseChange_bijective: Remark 8.29 — over a complete noetherian Tate ring the comparison map is bijective for every finiteMwith its canonical topology, Mathlib's module topology. The two presentation-level halves are applied to the strict presentationTauCeti.Huber.IsTateRing.exists_presentation_isStrictMap_isOpenMapsupplies; that is where the Tate, noetherian and completeness hypotheses onAenter, and the only place they do. Nothing beyond the module topology is asked ofM.restrictedMvPowerSeriesBaseChangeEquiv: the same, packaged asM ⊗[A] A⟨T₁, …, Tₖ⟩ ≃ₗ[A] M⟨T₁, …, Tₖ⟩— the form the Layer 4.1 consequences consume — withrestrictedMvPowerSeriesBaseChangeEquiv_applyidentifying it with the comparison map.
The two presentation-level statements hypothesise the topological properties of the presentation,
hmap and hstrict, rather than deriving them, and so carry no Tate, noetherian or completeness
assumption; the headline theorem is where those are spent.
Implementation notes #
MvPowerSeries σ R is a plain def for (σ →₀ ℕ) → R, so Mathlib's lemmas about
TensorProduct.piScalarRightHom are stated about a type that rw and simp will not unfold to
reach a goal phrased in power series. Two declarations answer this, and nothing else here crosses
the gap:
mvPowerSeriesBaseChangeascribes the codomain ofTensorProduct.piScalarRightHomasMvPowerSeries (Fin k) M. Thesimpsteps of the tensor induction behindrestrictedMvPowerSeriesBaseChange—map_zero,map_add— match that ascription; against the unascribed(Fin k →₀ ℕ) → Mform they rewrite to a term the goal no longer matches syntactically.mvPowerSeriesBaseChange_tmulrestates Mathlib'spiScalarRightHom_tmulat the series type.
The finite free equality is stated as finPiEquiv (baseChange x) = tensorFinPiEquiv x rather
than through (finPiEquiv …).symm, because the equivalences' bodies are unexposed: _apply
computes across the module boundary while _symm_apply on a composite does not. The isomorphism
itself is then packaged separately, so consumers get a LinearEquiv without paying that cost.
Coefficients are read through the (· : (Fin k →₀ ℕ) → M) ascription, as IsRestricted itself is
phrased: MvPowerSeries.coeff is unavailable here because it is R-linear on R-valued series
and so asks for Semiring on the coefficients, which a module of coefficients does not have.
Provenance #
Nothing here is ported. The ambient map is Mathlib's TensorProduct.piScalarRightHom, and the
finite free case runs through Mathlib's TensorProduct.comm and TensorProduct.piScalarRight;
everything else — the restricted comparison map, its coefficient lemmas, and the identification
restrictedMvPowerSeriesFinPiEquiv — is this repository's own.
AINTLIB (github.com/CBirkbeck/AINTLIB @ 37bbdaeb9, Apache-2.0), the roadmap's designated prior
formalisation for this layer, does have counterparts, and they were consulted rather than
ported: Adic spaces/RestrictedModule.lean defines restrictedModule and restrictedModule.map
at module coefficients with restrictedModule_map_surjective, and
Adic spaces/Wedhorn828.lean proves muMap_bijective_of_finite — Remark 8.29 in full, both
halves, for Module.Finite A M.
An earlier revision of this section claimed the opposite. That claim came from grepping this
repository's vocabulary (restrictedMvPowerSeries) against a source that names the same objects
restrictedModule and muMap, and it was wrong.
The hypotheses differ, which is why this is a separate development rather than a port. AINTLIB
fixes M to carry the module topology and assumes Module.Finite A M, deriving openness of
Aⁿ ↠ M from its own IsModuleTopology.isOpenMap_of_surjective_of_finite, which the pinned
Mathlib does not have; its section variables also include HasLocLiftPowerBounded, the typeclass
this repository deliberately replaced. The presentation-level statements here instead take a
strict presentation as a hypothesis and so carry no Tate, noetherian, completeness or
module-topology assumption at all; restrictedMvPowerSeriesBaseChange_bijective then discharges
that hypothesis for a finite M with its module topology over a complete noetherian Tate ring —
openness of Aⁿ ↠ M is now Mathlib's own IsModuleTopology.isOpenMap_of_surjective, and
strictness of the relation map comes from this repository's open mapping theorem on Aᵐ.
References #
- Wedhorn, Adic Spaces, Remark 8.29.
Mathlib's base-change map at the index type of k-variable power series, with its codomain
ascribed as MvPowerSeries (Fin k) M rather than (Fin k →₀ ℕ) → M. It sends m ⊗ₜ f to
s ↦ coeff s f • m.
Equations
Instances For
mvPowerSeriesBaseChange sends a pure tensor m ⊗ₜ f to the coefficientwise scalar action
s ↦ coeff s f • m.
The coefficient of mvPowerSeriesBaseChange (m ⊗ₜ f) at s, read through the function-type
ascription that IsRestricted also uses.
A pure tensor with restricted second factor base-changes to a restricted series.
The hypothesis is ContinuousSMul A M, not ContinuousConstSMul A M: the continuity needed is of
a ↦ a • m in the scalar variable, since it is the coefficients that vary and the vector that
is fixed. ContinuousConstSMul gives continuity in the vector variable instead.
Between the restricted objects #
The comparison map of Wedhorn Remark 8.29: M ⊗[A] A⟨T₁, …, Tₖ⟩ →ₗ[A] M⟨T₁, …, Tₖ⟩.
Mathlib's base-change map restricted on both sides. Remark 8.29 asserts that it is an isomorphism
when M is finitely generated over a complete noetherian Tate ring; that is
restrictedMvPowerSeriesBaseChange_bijective below.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Read in the ambient series, restrictedMvPowerSeriesBaseChange is mvPowerSeriesBaseChange
of the underlying series. The definition's body is not exposed, so this is how a consumer computes
with it.
Read in the ambient series, restrictedMvPowerSeriesBaseChange agrees with
mvPowerSeriesBaseChange on a pure tensor.
The coefficient of restrictedMvPowerSeriesBaseChange (m ⊗ₜ f) at s, read through the
function-type ascription that IsRestricted also uses.
The comparison map is natural in M. An A-linear φ : M → N continuous at 0
commutes with
base change, so a presentation of M can be pushed through M ↦ M⟨T₁, …, Tₖ⟩. This is the
naturality the finitely generated case of Remark 8.29 runs on.
The finite free case of Remark 8.29 #
(Fin n → A)⟨T₁, …, Tₖ⟩ ≃ₗ[A] Fin n → A⟨T₁, …, Tₖ⟩: a restricted series with finite-tuple
coefficients is the tuple of its component series.
Equations
- One or more equations did not get rendered due to their size.
Instances For
(Fin n → A) ⊗[A] A⟨T₁, …, Tₖ⟩ ≃ₗ[A] Fin n → A⟨T₁, …, Tₖ⟩, from Mathlib: the tensor factors
through the finite index.
Equations
- One or more equations did not get rendered due to their size.
Instances For
restrictedMvPowerSeriesFinPiEquiv reads off the i-th component series: its s-th
coefficient is the i-th entry of f's.
restrictedMvPowerSeriesFinPiEquiv.symm assembles a tuple of component series into a
tuple-valued series: the i-th entry of its s-th coefficient is the s-th coefficient of the
i-th component.
tensorFinPiEquiv on a pure tensor is the scalar action componentwise.
Wedhorn Remark 8.29 for a finite free module: transported along the two identifications, the comparison map is Mathlib's tensor-pi equivalence. Both are isomorphisms, so the comparison map is one too.
The whole content is commutativity of A: the tensor side produces m i * coeff s f and the
comparison map produces coeff s f * m i.
Remark 8.29 for a finite free module, as an isomorphism. The comparison map
restrictedMvPowerSeriesBaseChange at M = Fin n → A, packaged as a linear equivalence; see
restrictedMvPowerSeriesBaseChangeFinEquiv_apply for the identification with the map itself.
Equations
Instances For
The finite free isomorphism is the comparison map.
The comparison map is bijective for a finite free module — Remark 8.29's conclusion in the base case, in the form a reduction argument consumes.
Remark 8.29's comparison map is surjective for a finitely generated module. If M is
presented by a surjection Aᵐ ↠ M that is continuous at 0 and pushes the neighbourhoods of 0
forward, then every restricted series with coefficients in M comes from M ⊗[A] A⟨T₁, …, Tₖ⟩.
The three ingredients meet here and each supplies one thing. The presentation lifts a restricted
series over M to one over Aᵐ (restrictedMvPowerSeriesSubmoduleMap_surjective, where hmap is
what makes the lifted coefficients converge); the finite free case identifies that with a tensor
(restrictedMvPowerSeriesBaseChange_fin_bijective); and naturality carries it back down
(restrictedMvPowerSeriesSubmoduleMap_baseChange). No noetherian hypothesis and no property of
the kernel are needed — those enter only for injectivity, which is the other half of Remark 8.29
and is restrictedMvPowerSeriesBaseChange_injective_of_presentation.
hmap is stated as the filter inequality the proof consumes rather than as IsOpenMap p, which is
strictly stronger: M carries ContinuousAdd rather than IsTopologicalAddGroup, so without
translation invariance global openness does not follow from openness at 0. A caller holding
IsOpenMap p passes map_zero p ▸ hopen.nhds_le 0; over a complete Tate ring that open map is
TauCeti.Huber.IsTateRing.isOpenMap.
Remark 8.29's comparison map is injective for a finitely generated module. Given a
presentation Aⁿ →[u] Aᵐ →[p] M → 0 whose first map is strict onto its image, the comparison map
M ⊗[A] A⟨T₁, …, Tₖ⟩ → M⟨T₁, …, Tₖ⟩ is injective. With
restrictedMvPowerSeriesBaseChange_surjective_of_presentation this gives Remark 8.29,
restrictedMvPowerSeriesBaseChange_bijective, once a strict presentation is in hand.
The proof is a four lemma applied to
Aⁿ ⊗ A⟨T⟩ ⟶ Aᵐ ⊗ A⟨T⟩ ⟶ M ⊗ A⟨T⟩ ⟶ 0
↓ ↓ ↓
Aⁿ⟨T⟩ ⟶ Aᵐ⟨T⟩ ⟶ M⟨T⟩
with the comparison map at Aⁿ, at Aᵐ and at M down the sides. Each input is already
available: the top row is exact because tensoring is right exact, the bottom row is
restrictedMvPowerSeriesSubmoduleMap_range_eq_ker, the two outer verticals are bijective by
restrictedMvPowerSeriesBaseChange_fin_bijective, and the squares commute by
restrictedMvPowerSeriesSubmoduleMap_baseChange.
M is asked to be an AddCommGroup, where the rest of this file works with AddCommMonoid: a
diagram chase subtracts, and Mathlib's four lemma is stated over AddCommGroup for that reason.
Nothing else here needs it.
hstrict is the one input the presentation does not supply. It holds as soon as range u is
closed in Aᵐ, and over a complete noetherian Tate ring every submodule of a finitely generated
module is closed (TauCeti.Huber.isClosed_of_isNoetherian). That deduction is made once, in
TauCeti.Huber.IsTateRing.exists_presentation_isStrictMap_isOpenMap; here strictness is
hypothesised, exactly as restrictedMvPowerSeriesSubmoduleMap_range_eq_ker hypothesises it, so
that this statement carries no hypothesis on A beyond the ambient ones.
Remark 8.29. Over a complete noetherian Tate ring A, the comparison map
M ⊗[A] A⟨T₁, …, Tₖ⟩ → M⟨T₁, …, Tₖ⟩ is bijective for every finitely generated A-module M
"endowed with its canonical topology (Proposition 6.18(1))" — Mathlib's module topology,
IsModuleTopology A M, which every complete first-countable module topology on M is
(TauCeti.Huber.IsTateRing.isModuleTopology).
This is Wedhorn's argument as he gives it: choose a presentation Aⁿ →[u] Aᵐ →[p] M → 0 with u
strict and p open — TauCeti.Huber.IsTateRing.exists_presentation_isStrictMap_isOpenMap, which
is where A being Tate, noetherian and complete is spent — and apply the two presentation-level
halves, restrictedMvPowerSeriesBaseChange_injective_of_presentation and
restrictedMvPowerSeriesBaseChange_surjective_of_presentation. Openness of p is passed to the
latter as the filter inequality it consumes, and strictness of u to the former as the openness
at 0 of u.rangeRestrict, read off through
LinearMap.isStrictMap_iff_isOpenQuotientMap_rangeRestrict.
No completeness or separation of M is assumed: the presentation is open because the module
topology is the quotient topology along Aᵐ ↠ M, and strict because its relations have closed
range in Aᵐ. ContinuousAdd M appears among the hypotheses only because M⟨T₁, …, Tₖ⟩ is a
submodule under it; it follows from IsModuleTopology A M (IsModuleTopology.toContinuousAdd),
which instance search cannot use since A does not occur in the goal.
Remark 8.29, packaged: M ⊗[A] A⟨T₁, …, Tₖ⟩ ≃ₗ[A] M⟨T₁, …, Tₖ⟩ for a finite module M
with its module topology over a complete noetherian Tate ring. This is the form the Layer 4.1
consequences consume; restrictedMvPowerSeriesBaseChange_bijective is the content.
Equations
Instances For
restrictedMvPowerSeriesBaseChangeEquiv is the comparison map.