Commit 2024-06-04 09:13 992a28ce

View on Github →

feat: the equational criterion for flatness (#12666) We prove the equational criterion for flatness. As a consequence, every homomorphism from a finitely presented module to a flat module factors through a finite free module.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Module/FinitePresentation.lean

added theorem Module.FinitePresentation.equiv_quotient

Modified Mathlib/LinearAlgebra/TensorProduct/Vanishing.lean

Created Mathlib/RingTheory/Flat/EquationalCriterion.lean

added theorem Module.Flat.exists_factorization_of_apply_eq_zero

added theorem Module.Flat.exists_factorization_of_apply_eq_zero_of_free

added theorem Module.Flat.exists_factorization_of_comp_eq_zero_of_free

added theorem Module.Flat.exists_factorization_of_isFinitelyPresented

added theorem Module.Flat.iff_forall_exists_factorization

added theorem Module.Flat.iff_forall_isTrivialRelation

added theorem Module.Flat.isTrivialRelation_of_sum_smul_eq_zero

added theorem Module.Flat.of_forall_exists_factorization

added theorem Module.Flat.of_forall_isTrivialRelation

added theorem Module.Flat.tfae_equational_criterion

added theorem Module.isTrivialRelation_iff_vanishesTrivially

added theorem Module.sum_smul_eq_zero_of_isTrivialRelation