Commit 2024-11-11 17:09 c9d1bd64

View on Github →

feat: tensoring a localization with itself does nothing (#18744) IsLocalization.tensorSelfAlgEquiv: If A is a localization of a commutative ring R, then A ⊗[R] A is canonically isomorphic to A as A-algebras via multiplication. To construct the isomorphism we introduce a stronger version of Algebra.TensorProduct.lmul'. Also add some easy theorem (linearMap_compatibleSMul) and defs (distribBaseChange, LinearEquiv.baseChange) and protect IsLocalization.map_smul.

Estimated changes

Modified Mathlib/Algebra/Algebra/Bilinear.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Basic.lean

added def TensorProduct.equivOfCompatibleSMul

added def TensorProduct.mapOfCompatibleSMul'

added def TensorProduct.mapOfCompatibleSMul

added theorem TensorProduct.mapOfCompatibleSMul_surjective

added theorem TensorProduct.mapOfCompatibleSMul_tmul

Modified Mathlib/LinearAlgebra/TensorProduct/Tower.lean

modified def TensorProduct.AlgebraTensorModule.cancelBaseChange

added def TensorProduct.AlgebraTensorModule.distribBaseChange

Modified Mathlib/RingTheory/Localization/BaseChange.lean

added theorem IsLocalization.bijective_linearMap_mul'

added theorem IsLocalization.tensorProduct_compatibleSMul

Modified Mathlib/RingTheory/Localization/Basic.lean

added theorem IsLocalization.linearMap_compatibleSMul

Modified Mathlib/RingTheory/Localization/Defs.lean

deleted theorem IsLocalization.map_smul

Modified Mathlib/RingTheory/TensorProduct/Basic.lean

added def Algebra.TensorProduct.lmul''

modified def Algebra.TensorProduct.lmul'

added def Algebra.TensorProduct.lmulEquiv

added def LinearEquiv.baseChange