Commit 2023-10-05 09:03 e640058c

View on Github →

feat: Right exactness of tensor product of modules (#6447)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Exact.lean

added theorem Function.Exact.comp_eq_zero

added theorem Function.Exact.linearMap_comp_eq_zero

added theorem Function.Exact.linearMap_ker_eq

added def Function.Exact

added theorem Function.LinearMap.exact_iff

Modified Mathlib/LinearAlgebra/TensorProduct.lean

added theorem LinearMap.comm_comp_lTensor_comp_comm_eq

added theorem LinearMap.comm_comp_rTensor_comp_comm_eq

added theorem TensorProduct.lift_comp_comm_eq

added theorem TensorProduct.map_comp_comm_eq

Created Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean

added theorem LinearMap.exact_map_mkQ_range

added theorem LinearMap.exact_subtype_ker_map

added theorem LinearMap.exact_subtype_mkQ

added theorem TensorProduct.map_ker

added theorem TensorProduct.map_surjective

added def lTensor.inverse

added theorem lTensor.inverse_apply

added theorem lTensor.inverse_comp_lTensor

added def lTensor.inverse_of_rightInverse

added theorem lTensor.inverse_of_rightInverse_apply

added theorem lTensor.inverse_of_rightInverse_comp_lTensor

added def lTensor.linearEquiv_of_rightInverse

added theorem lTensor.surjective

added def lTensor.toFun

added theorem lTensor_exact

added theorem lTensor_mkQ

added theorem le_comap_range_lTensor

added theorem le_comap_range_rTensor

added def rTensor.inverse

added theorem rTensor.inverse_apply

added theorem rTensor.inverse_comp_rTensor

added def rTensor.inverse_of_rightInverse

added theorem rTensor.inverse_of_rightInverse_apply

added theorem rTensor.inverse_of_rightInverse_comp_rTensor

added def rTensor.linearEquiv_of_rightInverse

added theorem rTensor.surjective

added def rTensor.toFun

added theorem rTensor_exact

added theorem rTensor_mkQ

Modified docs/references.bib