Continuity of the rational-localization Čech complex

The augmentation and differentials of the algebraic Čech complex are continuous for the natural module topologies over the uncompleted rational localizations. Consequently they extend to the separated completions of this topologised algebraic complex. These give the maps of Huber's analytic Čech complex for M = B; for finite M over a ring with a noetherian ring of definition, identifying the completed terms with Huber's terms requires a comparison not proved here. No finiteness, completeness or noetherian hypothesis is needed for continuity.

The topology on a face depends on its cardinality: deleting a vertex changes both the denominator and the numerator family. The restriction is continuous because multiplying the old numerators by the deleted vertex gives numerators for the larger face. The module restriction then follows by extending scalars on TauCeti.cechLocalizationRestriction using Mathlib’s LinearMap.extendScalarsOfIsLocalization.

References

• R. Huber, A generalization of formal schemes and rigid analytic varieties, Math. Z. 217 (1994), §2, the complexes (*) and (**) in the proof of Theorem 2.5, Case I.

theorem TauCeti.Huber.NoetherianCech.continuous_cechLocalizationRestriction_erase {B : Type u_1} [CommRing B] {ι : Type u_2} (f : ι → B) [TopologicalSpace B] [IsTopologicalRing B] (P : PairOfDefinition B) (hf : Ideal.span (Set.range f) = ⊤) (M : Type u_3) [AddCommGroup M] [Module B M] [DecidableEq ι] (p : ℕ) (S : Finset ι) (a : ↥S) : Continuous ⇑(cechLocalizationRestriction M f ⋯)

Restriction from a face with one vertex deleted is continuous for the natural topologies of uncompleted rational localizations.

theorem TauCeti.Huber.NoetherianCech.continuous_cechLocalizationAugmentation {B : Type u_1} [CommRing B] {ι : Type u_2} (f : ι → B) [TopologicalSpace B] [IsTopologicalRing B] (P : PairOfDefinition B) (hf : Ideal.span (Set.range f) = ⊤) (M : Type u_3) [AddCommGroup M] [Module B M] [TopologicalSpace M] [IsModuleTopology B M] : Continuous ⇑(cechLocalizationAugmentation M f)

The augmentation of the rational-localization Čech complex is continuous.

theorem TauCeti.Huber.NoetherianCech.continuous_cechLocalizationDifferential {B : Type u_1} [CommRing B] {ι : Type u_2} (f : ι → B) [TopologicalSpace B] [IsTopologicalRing B] (P : PairOfDefinition B) (hf : Ideal.span (Set.range f) = ⊤) (M : Type u_3) [AddCommGroup M] [Module B M] [LinearOrder ι] (p : ℕ) : Continuous ⇑(cechLocalizationDifferential M f p)

Every differential of the rational-localization Čech complex is continuous.