Adic completion as tensor product

In this file we examine properties of the natural map

AdicCompletion I R ⊗[R] M →ₗ[AdicCompletion I R] AdicCompletion I M.

We show (in the AdicCompletion namespace):

• ofTensorProduct_bijective_of_pi_of_fintype: it is an isomorphism if M = R^n.
• ofTensorProduct_surjective_of_finite: it is surjective, if M is a finite R-module.
• ofTensorProduct_bijective_of_finite_of_isNoetherian: it is an isomorphism if R is Noetherian and M is a finite R-module.

As a corollary we obtain

• flat_of_isNoetherian: the adic completion of a Noetherian ring R is R-flat.

TODO

• Show that ofTensorProduct is an isomorphism for any finite free R-module over an arbitrary ring. This is mostly composing with the isomorphism to R^n and checking that a diagram commutes.

noncomputable def AdicCompletion.ofTensorProduct {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] : TensorProduct R (AdicCompletion I R) M →ₗ[AdicCompletion I R] AdicCompletion I M

The natural AdicCompletion I R-linear map from AdicCompletion I R ⊗[R] M to the adic completion of M.

Equations

• AdicCompletion.ofTensorProduct I M = TensorProduct.AlgebraTensorModule.lift (AdicCompletion.ofTensorProductBil✝ I M)

@[simp]

theorem AdicCompletion.ofTensorProduct_tmul {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] (r : AdicCompletion I R) (x : M) : (ofTensorProduct I M) (r ⊗ₜ[R] x) = r • (of I M) x

theorem AdicCompletion.ofTensorProduct_naturality {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) : map I f ∘ₗ ofTensorProduct I M = ofTensorProduct I N ∘ₗ TensorProduct.AlgebraTensorModule.map LinearMap.id f

ofTensorProduct is functorial in M.

noncomputable def AdicCompletion.ofTensorProductEquivOfPiFintype {R : Type u_1} [CommRing R] (I : Ideal R) (ι : Type u_4) [Fintype ι] [DecidableEq ι] : TensorProduct R (AdicCompletion I R) (ι → R) ≃ₗ[AdicCompletion I R] AdicCompletion I (ι → R)

ofTensorProduct as an equiv in the case of M = R^ι where ι is finite.

Equations

• AdicCompletion.ofTensorProductEquivOfPiFintype I ι = LinearEquiv.ofLinear (AdicCompletion.ofTensorProduct I (ι → R)) ↑(AdicCompletion.ofTensorProductInvOfPiFintype✝ I ι) ⋯ ⋯

theorem AdicCompletion.ofTensorProduct_bijective_of_pi_of_fintype {R : Type u_1} [CommRing R] (I : Ideal R) (ι : Type u_4) [Finite ι] : Function.Bijective ⇑(ofTensorProduct I (ι → R))

If M = R^ι, ofTensorProduct is bijective.

theorem AdicCompletion.ofTensorProduct_surjective_of_finite {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] [Module.Finite R M] : Function.Surjective ⇑(ofTensorProduct I M)

If M is a finite R-module, then the canonical map AdicCompletion I R ⊗[R] M →ₗ AdicCompletion I M is surjective.

Noetherian case

Suppose R is Noetherian. Then we show that the canonical map AdicCompletion I R ⊗[R] M →ₗ[AdicCompletion I R] AdicCompletion I M is an isomorphism for every finite R-module M.

The strategy is the following: Choose a surjection f : (ι → R) →ₗ[R] M and consider the following commutative diagram:

 AdicCompletion I R ⊗[R] ker f -→ AdicCompletion I R ⊗[R] (ι → R) -→ AdicCompletion I R ⊗[R] M -→ 0
               |                             |                                 |                  |
               ↓                             ↓                                 ↓                  ↓
    AdicCompletion I (ker f) ------→ AdicCompletion I (ι → R) -------→ AdicCompletion I M ------→ 0

The vertical maps are given by ofTensorProduct. By the previous section we know that the second vertical map is an isomorphism. Since R is Noetherian, ker f is finitely-generated, so again by the previous section the first vertical map is surjective.

Moreover, both rows are exact by right-exactness of the tensor product and exactness of adic completions over Noetherian rings. Hence we conclude by the 5-lemma.

theorem AdicCompletion.ofTensorProduct_bijective_of_finite_of_isNoetherian {R : Type u} [CommRing R] (I : Ideal R) (M : Type u) [AddCommGroup M] [Module R M] [IsNoetherianRing R] [Module.Finite R M] : Function.Bijective ⇑(ofTensorProduct I M)

If R is a Noetherian ring and M is a finite R-module, then the natural map given by AdicCompletion.ofTensorProduct is an isomorphism.

noncomputable def AdicCompletion.ofTensorProductEquivOfFiniteNoetherian {R : Type u} [CommRing R] (I : Ideal R) (M : Type u) [AddCommGroup M] [Module R M] [IsNoetherianRing R] [Module.Finite R M] : TensorProduct R (AdicCompletion I R) M ≃ₗ[AdicCompletion I R] AdicCompletion I M

ofTensorProduct packaged as linear equiv if M is a finite R-module and R is Noetherian.

Equations

• AdicCompletion.ofTensorProductEquivOfFiniteNoetherian I M = LinearEquiv.ofBijective (AdicCompletion.ofTensorProduct I M) ⋯

theorem AdicCompletion.coe_ofTensorProductEquivOfFiniteNoetherian {R : Type u} [CommRing R] (I : Ideal R) (M : Type u) [AddCommGroup M] [Module R M] [IsNoetherianRing R] [Module.Finite R M] : ↑(ofTensorProductEquivOfFiniteNoetherian I M) = ofTensorProduct I M

@[simp]

theorem AdicCompletion.ofTensorProductEquivOfFiniteNoetherian_apply {R : Type u} [CommRing R] (I : Ideal R) (M : Type u) [AddCommGroup M] [Module R M] [IsNoetherianRing R] [Module.Finite R M] (x : TensorProduct R (AdicCompletion I R) M) : (ofTensorProductEquivOfFiniteNoetherian I M) x = (ofTensorProduct I M) x

@[simp]

theorem AdicCompletion.ofTensorProductEquivOfFiniteNoetherian_symm_of {R : Type u} [CommRing R] (I : Ideal R) (M : Type u) [AddCommGroup M] [Module R M] [IsNoetherianRing R] [Module.Finite R M] (x : M) : (ofTensorProductEquivOfFiniteNoetherian I M).symm ((of I M) x) = 1 ⊗ₜ[R] x

theorem AdicCompletion.tensor_map_id_left_eq_map {R : Type u} [CommRing R] (I : Ideal R) [IsNoetherianRing R] {M : Type u} [AddCommGroup M] [Module R M] {N : Type u} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) [Module.Finite R M] [Module.Finite R N] : TensorProduct.AlgebraTensorModule.map LinearMap.id f = ↑(ofTensorProductEquivOfFiniteNoetherian I N).symm ∘ₗ map I f ∘ₗ ↑(ofTensorProductEquivOfFiniteNoetherian I M)

theorem AdicCompletion.tensor_map_id_left_injective_of_injective {R : Type u} [CommRing R] (I : Ideal R) [IsNoetherianRing R] {M : Type u} [AddCommGroup M] [Module R M] {N : Type u} [AddCommGroup N] [Module R N] {f : M →ₗ[R] N} [Module.Finite R M] [Module.Finite R N] (hf : Function.Injective ⇑f) : Function.Injective ⇑(TensorProduct.AlgebraTensorModule.map LinearMap.id f)

instance AdicCompletion.flat_of_isNoetherian {R : Type u} [CommRing R] (I : Ideal R) [IsNoetherianRing R] : Module.Flat R (AdicCompletion I R)

Adic completion of a Noetherian ring R is flat over R.