The separated completed rational-localization Čech complex

Complete the terms of the rational-localization Čech complex for their natural additive uniformities. Continuity of the algebraic maps gives continuous maps on the separated completions, using Mathlib’s AddMonoidHom.completion on TauCeti.cechLocalizationAugmentation and TauCeti.cechLocalizationDifferential. Their values on the dense algebraic terms characterize them, and consecutive maps compose to zero.

These are the maps of the separated completion of the topologised algebraic Čech complex. For M = B they give the maps of Huber's analytic Čech complex; 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. This construction does not assert exactness: that requires strictness of the algebraic complex, in addition to its algebraic exactness. The construction here allows non-Hausdorff uncompleted terms and does not assume noetherianity, completeness of the coefficient ring, or finite generation of the module.

References

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

@[reducible, inline]

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

The separated completion of the degree-p term of the rational-localization Čech complex, for the product of the natural module topologies on its faces.

noncomputable def TauCeti.Huber.NoetherianCech.completedDifferential {B : Type u_1} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] {ι : Type u_2} (f : ι → B) (P : PairOfDefinition B) (M : Type u_3) [AddCommGroup M] [Module B M] (hf : Ideal.span (Set.range f) = ⊤) [LinearOrder ι] (p : ℕ) : completedTerm f P M hf p →+ completedTerm f P M hf (p + 1)

The differential of the separated completed rational-localization Čech complex.

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

The completed differential is continuous.

@[simp]

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

The completed differential agrees with the algebraic differential on the dense algebraic term.

theorem TauCeti.Huber.NoetherianCech.completedDifferential_comp_differential {B : Type u_1} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] {ι : Type u_2} (f : ι → B) (P : PairOfDefinition B) (M : Type u_3) [AddCommGroup M] [Module B M] (hf : Ideal.span (Set.range f) = ⊤) [LinearOrder ι] (p : ℕ) : (completedDifferential f P M hf (p + 1)).comp (completedDifferential f P M hf p) = 0

Two consecutive differentials of the completed complex compose to zero.

noncomputable def TauCeti.Huber.NoetherianCech.completedAugmentation {B : Type u_1} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] {ι : Type u_2} (f : ι → B) (P : PairOfDefinition B) (M : Type u_3) [AddCommGroup M] [Module B M] (hf : Ideal.span (Set.range f) = ⊤) [UniformSpace M] [IsUniformAddGroup M] [IsModuleTopology B M] : UniformSpace.Completion M →+ completedTerm f P M hf 0

The augmentation from the separated completion of M to the degree-zero completed term.

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

The completed augmentation is continuous.

@[simp]

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

The completed augmentation agrees with the algebraic augmentation on the original module.

theorem TauCeti.Huber.NoetherianCech.completedDifferential_comp_augmentation {B : Type u_1} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] {ι : Type u_2} (f : ι → B) (P : PairOfDefinition B) (M : Type u_3) [AddCommGroup M] [Module B M] (hf : Ideal.span (Set.range f) = ⊤) [UniformSpace M] [IsUniformAddGroup M] [IsModuleTopology B M] [LinearOrder ι] : (completedDifferential f P M hf 0).comp (completedAugmentation f P M hf) = 0

The completed augmentation followed by the first completed differential is zero.