Commit 2023-10-18 08:53 d2e0ba3e

View on Github →

feat (LinearAlgebra/TensorProduct/RightExactness): right exactness of tensor product for algebras (#7533) Prove right exactness of tensor product for algebras.

Algebra.TensorProduct.ker_map computes the kernel of Algebra.TensorProduct.map f g
Algebra.TensorProduct.lTensor_ker and Algebra.TensorProduct.rTensor_ker compute the kernels of Algebra.TensorProduct.map f id and Algebra.TensorProduct.map id g

Estimated changes

Modified Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean

added theorem Algebra.TensorProduct.lTensor_ker

added theorem Algebra.TensorProduct.map_ker

added theorem Algebra.TensorProduct.rTensor_ker

added theorem Ideal.map_includeLeft_eq

added theorem Ideal.map_includeRight_eq

deleted def lTensor.inverse_of_rightInverse

deleted def lTensor.toFun

deleted def rTensor.inverse_of_rightInverse

deleted def rTensor.toFun

Modified Mathlib/RingTheory/Ideal/Operations.lean

added theorem AlgHom.coe_ideal_map

added theorem AlgHom.coe_ker