Commit 2025-02-23 16:13 7a329d59

View on Github →

feat(RingTheory/Cotangent): liftBaseChange is injective for localizations (#21037) This will be used to show a representation independent characterization of standard smoothness.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Module/LocalizedModule/Basic.lean

added theorem IsLocalizedModule.injective_of_map_eq

added theorem IsLocalizedModule.injective_of_map_zero

Created Mathlib/RingTheory/CotangentLocalizationAway.lean

added def Algebra.Generators.compLocalizationAwayAlgHom

added theorem Algebra.Generators.compLocalizationAwayAlgHom_X_inl

added theorem Algebra.Generators.compLocalizationAwayAlgHom_relation_eq_zero

added theorem Algebra.Generators.compLocalizationAwayAlgHom_toAlgHom_toComp

added theorem Algebra.Generators.comp_localizationAway_ker

added theorem Algebra.Generators.liftBaseChange_injective_of_isLocalizationAway

added theorem Algebra.Generators.sq_ker_comp_le_ker_compLocalizationAwayAlgHom

Modified Mathlib/RingTheory/Generators.lean

added def Algebra.Generators.kerCompPreimage

added theorem Algebra.Generators.ker_comp_eq_sup

added theorem Algebra.Generators.map_ofComp_ker

added theorem Algebra.Generators.ofComp_kerCompPreimage

added theorem Algebra.Generators.toAlgHom_ofComp_rename

added theorem Algebra.Generators.toAlgHom_ofComp_surjective

Modified Mathlib/RingTheory/Kaehler/JacobiZariski.lean

deleted theorem Algebra.Generators.Cotangent.map_ofComp_ker

deleted def Algebra.Generators.kerCompPreimage

deleted theorem Algebra.Generators.ofComp_kerCompPreimage

Modified Mathlib/RingTheory/Presentation.lean

added theorem Algebra.Generators.ker_localizationAway