Commit 2024-07-12 09:29 8ba988d4

View on Github →

feat(RingTheory/AdicCompletion): comparison with tensor product (#14358) We construct the natural map AdicCompletion I R ⊗[R] M →ₗ[AdicCompletion I R] AdicCompletion I M for any R-module M and ideal I and show that it is an isomorphism for M = R^n and surjective if M is a finite R-module.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/SMulWithZero.lean

added theorem Pi.single_apply_smul

Created Mathlib/LinearAlgebra/TensorProduct/Pi.lean

added theorem TensorProduct.piScalarRightHom_tmul

added def TensorProduct.piScalarRightInv

added theorem TensorProduct.piScalarRight_apply

added theorem TensorProduct.piScalarRight_symm_single

Modified Mathlib/LinearAlgebra/TensorProduct/Prod.lean

Created Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean

added def AdicCompletion.ofTensorProduct

added def AdicCompletion.ofTensorProductBil

added theorem AdicCompletion.ofTensorProduct_bijective_of_pi_of_fintype

added theorem AdicCompletion.ofTensorProduct_naturality

added theorem AdicCompletion.ofTensorProduct_surjective_of_fg

added theorem AdicCompletion.ofTensorProduct_tmul