Commit 2025-03-10 17:36 fb20f2eb

View on Github →

feat(LocalRing/Module): fg flat module over a local ring is free (#20460) Show that if M is a flat module over a local ring, then every family that is linearly independent over the residue field is also linearly independent over the local ring. As a consequence, if M is moreover finite, then M is free.

Estimated changes

Modified Mathlib/Algebra/Module/Equiv/Defs.lean

added theorem LinearEquiv.toLinearMap_eq_coe

Modified Mathlib/Algebra/Module/Submodule/Map.lean

added theorem Submodule.comap_coe_toLinearMap

added theorem Submodule.map_coe_toLinearMap

Modified Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean

added def Finsupp.addSingleEquiv

added theorem Finsupp.linearCombination_comp_addSingleEquiv

Modified Mathlib/LinearAlgebra/LinearIndependent/Defs.lean

added theorem linearIndependent_add_smul_iff

Modified Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean

added theorem LinearMap.ker_tensorProductMk

Modified Mathlib/RingTheory/Flat/EquationalCriterion.lean

Modified Mathlib/RingTheory/LocalRing/Module.lean

added theorem Module.IsLocalRing.linearIndependent_of_flat

modified theorem Module.free_of_flat_of_isLocalRing

Modified Mathlib/RingTheory/TensorProduct/Basic.lean

added theorem Submodule.map_range_rTensor_subtype_lid