Commit 2026-02-13 16:00 ca1d0aeb

View on Github →

feat(RingTheory): Algebra.FinitePresentation descends along faithfully flat algebras (#35254) From Pi1.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Finiteness.lean

added theorem TensorProduct.exists_sum_tmul_eq

Created Mathlib/RingTheory/Finiteness/Descent.lean

added theorem Algebra.FinitePresentation.of_finitePresentation_tensorProduct_of_faithfullyFlat

added theorem Algebra.FiniteType.of_finiteType_tensorProduct_of_faithfullyFlat

added theorem Ideal.FG.of_FG_map_of_faithfullyFlat

added theorem Module.Finite.of_finite_tensorProduct_of_faithfullyFlat

added theorem RingHom.Finite.codescendsAlong_faithfullyFlat

added theorem RingHom.FinitePresentation.codescendsAlong_faithfullyFlat

added theorem RingHom.FiniteType.codescendsAlong_faithfullyFlat

Modified Mathlib/RingTheory/TensorProduct/Maps.lean

added theorem Algebra.TensorProduct.Algebra.TensorProduct.commRight_symm_tmul

added theorem Algebra.TensorProduct.commRight_tmul