Completion of a finite module over a Huber ring is base change to the completed ring

Let A be a Huber ring with a pair of definition (A₀, I) such that A₀ is noetherian, Â its completion and M a finitely generated A-module with its natural topology. The canonical map  ⊗[A] M → M̂ (UniformSpace.Completion.ofTensorProduct) is bijective, and it is a homeomorphism when  ⊗[A] M carries its natural Â-module topology (Huber, A generalization of formal schemes and rigid analytic varieties, Lemma 2.3(iii)). Neither A nor M is assumed complete or Hausdorff: for A = ℤ with the p-adic topology and M = ℤ ⧸ ℓ with ℓ ≠ p prime, M is indiscrete and both sides vanish.

This is the identification of the completed Čech complexes of finite modules with the Čech complexes of their base changes, used in Huber's sheafiness theorem for rings with a noetherian ring of definition.

Implementation notes

Choose a surjection q : Aⁿ → M with kernel K. Identifying the completion of Aⁿ with Âⁿ (AbstractCompletion.pi), completion of the open surjection q is an open surjection ψ : Âⁿ → M̂ whose kernel is the closure of the image of K (AddMonoidHom.surjective_completion, AddMonoidHom.ker_completion). On the other side, Âⁿ → Â ⊗[A] M is surjective and kills the Â-submodule spanned by K. The ring of definition of Â is noetherian (TauCeti.Huber.PairOfDefinition.isNoetherianRing_completion) and Â is complete, so every Â-submodule of Âⁿ is closed (TauCeti.Huber.PairOfDefinition.isClosed_of_isNoetherianRing); in particular the closure of the image of K lies in its Â-span, which gives injectivity.

Main results

• TauCeti.Huber.PairOfDefinition.ofTensorProduct_bijective:  ⊗[A] M → M̂ is bijective.
• TauCeti.Huber.PairOfDefinition.isHomeomorph_ofTensorProduct: it is a homeomorphism for the natural Â-module topology on  ⊗[A] M.
• TauCeti.Huber.PairOfDefinition.ofTensorProductEquiv: the resulting A-linear equivalence.

References

• R. Huber, A generalization of formal schemes and rigid analytic varieties, Math. Z. 217 (1994), §2, Lemma 2.3(iii) and its proof.

A presentation q : Aⁿ → M and the two maps out of Âⁿ

theorem TauCeti.Huber.PairOfDefinition.ofTensorProduct_bijective {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] {M : Type u_2} [AddCommGroup M] [Module A M] [Module.Finite A M] [UniformSpace M] [IsUniformAddGroup M] [IsModuleTopology A M] [UniformContinuousConstSMul A M] (P : PairOfDefinition A) [IsNoetherianRing ↥P.ringOfDefinition] : Function.Bijective ⇑(UniformSpace.Completion.ofTensorProduct A M)

Completion of a finite module is base change to the completed ring (Huber, Lemma 2.3(iii)). If A is a Huber ring with a noetherian ring of definition and M is a finitely generated A-module with its natural topology, the canonical map  ⊗[A] M → M̂ is bijective.

theorem TauCeti.Huber.PairOfDefinition.isHomeomorph_ofTensorProduct {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] {M : Type u_2} [AddCommGroup M] [Module A M] [Module.Finite A M] [UniformSpace M] [IsUniformAddGroup M] [IsModuleTopology A M] [UniformContinuousConstSMul A M] (P : PairOfDefinition A) [IsNoetherianRing ↥P.ringOfDefinition] [TopologicalSpace (TensorProduct A (UniformSpace.Completion A) M)] [IsModuleTopology (UniformSpace.Completion A) (TensorProduct A (UniformSpace.Completion A) M)] : IsHomeomorph ⇑(UniformSpace.Completion.ofTensorProduct A M)

The comparison  ⊗[A] M → M̂ is a homeomorphism for the natural Â-module topology on  ⊗[A] M, if A is a Huber ring with a noetherian ring of definition and M is a finitely generated A-module with its natural topology (Huber, Lemma 2.3(iii)).

noncomputable def TauCeti.Huber.PairOfDefinition.ofTensorProductEquiv {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] {M : Type u_2} [AddCommGroup M] [Module A M] [Module.Finite A M] [UniformSpace M] [IsUniformAddGroup M] [IsModuleTopology A M] [UniformContinuousConstSMul A M] (P : PairOfDefinition A) [IsNoetherianRing ↥P.ringOfDefinition] : TensorProduct A (UniformSpace.Completion A) M ≃ₗ[A] UniformSpace.Completion M

The A-linear equivalence  ⊗[A] M ≃ M̂ given by the canonical map, for a finitely generated module M over a Huber ring with a noetherian ring of definition.

@[simp]

theorem TauCeti.Huber.PairOfDefinition.ofTensorProductEquiv_apply {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] {M : Type u_2} [AddCommGroup M] [Module A M] [Module.Finite A M] [UniformSpace M] [IsUniformAddGroup M] [IsModuleTopology A M] [UniformContinuousConstSMul A M] (P : PairOfDefinition A) [IsNoetherianRing ↥P.ringOfDefinition] (t : TensorProduct A (UniformSpace.Completion A) M) : P.ofTensorProductEquiv t = (UniformSpace.Completion.ofTensorProduct A M) t

The equivalence ofTensorProductEquiv is the canonical map.

@[simp]

theorem TauCeti.Huber.PairOfDefinition.ofTensorProductEquiv_symm_coe {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] {M : Type u_2} [AddCommGroup M] [Module A M] [Module.Finite A M] [UniformSpace M] [IsUniformAddGroup M] [IsModuleTopology A M] [UniformContinuousConstSMul A M] (P : PairOfDefinition A) [IsNoetherianRing ↥P.ringOfDefinition] (m : M) : P.ofTensorProductEquiv.symm ↑m = 1 ⊗ₜ[A] m

The inverse of ofTensorProductEquiv sends the image of m : M in M̂ to 1 ⊗ m.