Commit 2026-02-26 15:32 94298b7e

feat(Algebra/Category/Ring): equalizers of pushout maps of tensor product inclusions (#29960) This PR defines a ring map S →ₗ[R] S ⊗[R] S : s ↦ (s ⊗ₜ[R] 1) - (1 ⊗ₜ[R] s) for an R-algebra S, and show that its kernel is exactly (the image of) R if S is faithfully flat over R. Changes:

• TensorProduct.AlgebraTensorModule.distribBaseChange: Origianlly takes M and N, where M is an R-module with an additional instance IsScalarTower R A M. This is unnecessary, so I changed the M and N into N and Q, now both of which are merely modules over R. Main results :
• Add compatibility of Algebra.TensorProduct.includeLeft (or Algebra.TensorProduct.includeRight) with TensorProduct.AlgebraTensorModule.distribBaseChange and LinearMap.lTensor
• Define Algebra.TensorProduct.includeLeftSubRight, which is the R-linear map S →ₗ[R] S ⊗[R] S sending s : S to (s ⊗ₜ[R] 1) - (1 ⊗ₜ[R] s).
• Algebra.isEffective_of_faithfullyFlat: the pair algebraMap : R → S and includeLeftSubRight R S : S → S ⊗[R] S is exact if S is a faithfully flat R-algebra.