`A⟨T₁, …, Tₖ⟩` is faithfully flat over a complete noetherian Tate ring #

Wedhorn's Lemma 8.31(1): for a complete noetherian Tate ring A, the ring of restricted power series A⟨T₁, …, Tₖ⟩ is faithfully flat over A.

Flatness is Remark 8.29 applied to the ideals of A: for an ideal I, the comparison maps identify I ⊗[A] A⟨T⟩ → A ⊗[A] A⟨T⟩ with the coefficientwise inclusion I⟨T⟩ → A⟨T⟩, which is injective, and Mathlib's Module.Flat.iff_rTensor_injective asks for nothing more. Faithfulness is the prime {∑ aᵥ Tᵛ | a₀ ∈ 𝔭} Wedhorn writes down: the constant coefficient is a ring homomorphism A⟨T⟩ → A retracting A → A⟨T⟩, so every prime of A is the contraction of a prime of A⟨T⟩, and Module.FaithfullyFlat.of_comap_surjective concludes.

Main results #

TauCeti.Huber.flat_restrictedMvPowerSeriesSubring: A⟨T₁, …, Tₖ⟩ is flat over A.
TauCeti.Huber.faithfullyFlat_restrictedMvPowerSeriesSubring: it is faithfully flat.

Implementation notes #

For an ideal I of A, Remark 8.29 (restrictedMvPowerSeriesBaseChange_bijective) is applied to I with its subspace topology: I is closed (isClosed_of_isNoetherian), hence complete, hence carries the module topology (IsTateRing.isModuleTopology). Faithfulness goes through Module.FaithfullyFlat.of_comap_surjective, with the constant coefficient MvPowerSeries.constantCoeff ∘ restrictedMvPowerSeriesSubringVal as the ring homomorphism whose comap sections Spec (A⟨T⟩) → Spec A.