Commit 2026-03-03 17:54 dab97168

View on Github →

feat(RingTheory): I / I ^ 2 commutes with flat base change (#35544) Towards smooth descends along faithfully flat ring maps. From Pi1.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Quotient.lean

added theorem TensorProduct.AlgebraTensorModule.tensorQuotientEquiv_apply_tmul

added theorem TensorProduct.AlgebraTensorModule.tensorQuotientEquiv_symm_apply_mk_tmul

Modified Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean

added theorem TensorProduct.AlgebraTensorModule.range_lTensor_idealMap

Modified Mathlib/RingTheory/Ideal/Cotangent.lean

added def Ideal.Cotangent.lift

added theorem Ideal.Cotangent.lift_comp_toCotangent

added theorem Ideal.Cotangent.lift_surjective_iff

added theorem Ideal.Cotangent.lift_toCotangent

added theorem Ideal.cotangentToQuotientSquare_injective

Created Mathlib/RingTheory/Ideal/CotangentBaseChange.lean

added def Ideal.tensorCotangentEquiv

added theorem Ideal.tensorCotangentEquiv_tmul

added def Ideal.tensorCotangentHom

added theorem Ideal.tensorCotangentHom_injective_of_flat

added theorem Ideal.tensorCotangentHom_surjective

added theorem Ideal.tensorCotangentHom_tmul

Modified Mathlib/RingTheory/Ideal/Maps.lean

added theorem Algebra.idealMap_mul

Modified Mathlib/RingTheory/TensorProduct/Quotient.lean

added theorem Algebra.TensorProduct.tensorQuotientEquiv_apply_tmul

added theorem Algebra.TensorProduct.tensorQuotientEquiv_symm_apply_tmul