Topological exactness of the Laurent cover

For a complete Hausdorff strongly noetherian Tate ring A, the augmented sequence for the Laurent cover |f| ≤ 1, |f| ≥ 1 is strictly exact. The augmentation is a closed embedding, so the topology on A agrees with the equalizer topology inherited from the product of the two coordinate rings. The difference of restrictions is an open quotient map onto the coordinate ring of the overlap.

These are the topological statements needed to interpret Laurent-cover gluing in topological rings. Algebraic exactness is supplied by laurentCover_exact; the open mapping theorem over a Tate ring supplies strictness. The T0Space assumption implies Hausdorffness for these uniform additive groups.

References

• T. Wedhorn, Adic Spaces, Lemma 8.33 and Remark 8.20.
• L. Henkel, An Open Mapping Theorem for rings which have a zero sequence of units, arXiv:1407.5647.

theorem TauCeti.ValuationSpectrum.isClosedEmbedding_laurentCover {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [CompleteSpace A] [T0Space A] [Huber.IsTateRing A] [Huber.IsStronglyNoetherian A] (P : Huber.PairOfDefinition A) (f : A) (S₁ : Type u_2) (S₂ : Type u_3) [CommRing S₁] [Algebra A S₁] [IsLocalization.Away 1 S₁] [CommRing S₂] [Algebra A S₂] [IsLocalization.Away f S₂] (hden₂ : P.HasDenominatorPower {1} f S₂) : Topology.IsClosedEmbedding ⇑((P.toCompletionLoc {f, 1} 1 S₁ ⋯).prod (P.toCompletionLoc {1} f S₂ hden₂))

The augmentation for a Laurent cover is a closed embedding. In particular, the topology on A is the subspace topology on the equalizer of the two restrictions to the overlap.

theorem TauCeti.ValuationSpectrum.isOpenQuotientMap_laurentCover {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [CompleteSpace A] [T0Space A] [Huber.IsTateRing A] [Huber.IsStronglyNoetherian A] (P : Huber.PairOfDefinition A) (f : A) (S₁ : Type u_2) [CommRing S₁] [Algebra A S₁] [IsLocalization.Away 1 S₁] (S₂ : Type u_3) [CommRing S₂] [Algebra A S₂] [IsLocalization.Away f S₂] (hden₂ : P.HasDenominatorPower {1} f S₂) (S₁₂ : Type u_4) [CommRing S₁₂] [Algebra A S₁₂] [IsLocalization.Away (1 * f) S₁₂] : IsOpenQuotientMap ⇑((P.restrictionRingHom {f, 1} 1 S₁ ⋯ {f * f, f, 1} (1 * f) S₁₂ ⋯ f ⋯ ⋯).toAddMonoidHom.comp (AddMonoidHom.fst (UniformSpace.Completion S₁) (UniformSpace.Completion S₂)) - (P.restrictionRingHom {1} f S₂ hden₂ {f * f, f, 1} (1 * f) S₁₂ ⋯ 1 ⋯ ⋯).toAddMonoidHom.comp (AddMonoidHom.snd (UniformSpace.Completion S₁) (UniformSpace.Completion S₂)))

The difference of the two restrictions in a Laurent cover is an open quotient map. Thus the topology on the overlap ring agrees with the quotient topology from the product of the two coordinate rings.