Base change of a topological module to the completed ring

Let A be a commutative topological ring with a compatible uniformity and M a topological A-module with a compatible uniformity. For each m : M the continuous linear map a ↦ a • m extends to the separated completions, giving  → M̂. These maps are A-bilinear in (â, m) and define the canonical map

UniformSpace.Completion.ofTensorProduct A M : Completion A ⊗[A] M →ₗ[A] Completion M,

sending a ⊗ m to the image of a • m for a ∈ A. It is the topological analogue of Mathlib's AdicCompletion.ofTensorProduct. For finite modules over a Huber ring with a noetherian ring of definition it is bijective (TauCeti.Huber.PairOfDefinition.ofTensorProduct_bijective).

No completeness, separation or finiteness is assumed here.

noncomputable def UniformSpace.Completion.ofTensorProduct (A : Type u_1) [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] (M : Type u_2) [AddCommGroup M] [Module A M] [UniformSpace M] [IsUniformAddGroup M] [ContinuousSMul A M] [UniformContinuousConstSMul A M] : TensorProduct A (Completion A) M →ₗ[A] Completion M

The canonical map  ⊗[A] M → M̂ from the base change of M to the completion of A into the completion of M: it sends â ⊗ m to the value at â of the completion of a ↦ a • m.

theorem UniformSpace.Completion.ofTensorProduct_tmul {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] {M : Type u_2} [AddCommGroup M] [Module A M] [UniformSpace M] [IsUniformAddGroup M] [ContinuousSMul A M] [UniformContinuousConstSMul A M] (a : Completion A) (m : M) : (ofTensorProduct A M) (a ⊗ₜ[A] m) = (ContinuousLinearMap.toSpanSingleton A m).completion a

On a pure tensor â ⊗ m, the canonical map is the completion of a ↦ a • m, evaluated at â.

@[simp]

theorem UniformSpace.Completion.ofTensorProduct_coe_tmul {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] {M : Type u_2} [AddCommGroup M] [Module A M] [UniformSpace M] [IsUniformAddGroup M] [ContinuousSMul A M] [UniformContinuousConstSMul A M] (a : A) (m : M) : (ofTensorProduct A M) (↑a ⊗ₜ[A] m) = ↑(a • m)

The canonical map sends a ⊗ m, for a ∈ A, to the image of a • m in the completion.

theorem UniformSpace.Completion.continuous_ofTensorProduct_tmul {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] {M : Type u_2} [AddCommGroup M] [Module A M] [UniformSpace M] [IsUniformAddGroup M] [ContinuousSMul A M] [UniformContinuousConstSMul A M] (m : M) : Continuous fun (a : Completion A) => (ofTensorProduct A M) (a ⊗ₜ[A] m)

For fixed m, the canonical map is continuous in the completed scalar.