Commit 2026-04-08 17:43 ad537887

View on Github →

feat(RingTheory/Extension): naive cotangent complex commutes with flat base change (#35593) From Pi1.

Estimated changes

Modified Mathlib/RingTheory/Extension/Basic.lean

added def Algebra.Extension.Hom.ofAlgHom

added theorem Algebra.Extension.Hom.toAlgHom_ofAlgHom

added def Algebra.Extension.cotangentEquivCotangentKer

added theorem Algebra.Extension.ker_baseChange

Modified Mathlib/RingTheory/Extension/Cotangent/BaseChange.lean

added theorem Algebra.Extension.tensorCotangentOfFlat_tmul

added theorem Algebra.Extension.tensorH1CotangentOfFlat_tmul

added def Algebra.Extension.tensorToH1Cotangent

added theorem Algebra.Extension.tensorToH1Cotangent_bijective_of_flat

added theorem Algebra.Extension.tensorToH1Cotangent_tmul

added theorem Algebra.tensorH1CotangentOfFlat_tmul

Modified Mathlib/RingTheory/Extension/Cotangent/Basic.lean

added theorem Algebra.Extension.H1Cotangent.map_comp_apply

Modified Mathlib/RingTheory/Extension/Generators.lean

added theorem Algebra.Generators.baseChangeFromBaseChange_apply

added theorem Algebra.Generators.baseChangeToBaseChange_apply

modified def Algebra.Generators.comp

modified def Algebra.Generators.extendScalars

Modified Mathlib/RingTheory/Ideal/Cotangent.lean

added theorem Ideal.Cotangent.Ideal.mapCotangent_ker_of_surjective

added theorem Ideal.Cotangent.Ideal.mapCotangent_surjective_of_comap_eq

added theorem Ideal.Cotangent.IsLocalRing.CotangentSpace.map_eq_top_iff

added theorem Ideal.Cotangent.IsLocalRing.CotangentSpace.span_image_eq_top_iff

added theorem Ideal.Cotangent.IsLocalRing.finrank_cotangentSpace_eq_zero

added theorem Ideal.Cotangent.IsLocalRing.finrank_cotangentSpace_eq_zero_iff

added theorem Ideal.Cotangent.IsLocalRing.finrank_cotangentSpace_le_one_iff

added theorem Ideal.Cotangent.IsLocalRing.subsingleton_cotangentSpace_iff

added def Ideal.Cotangent.equivOfEq

added theorem Ideal.Cotangent.equivOfEq_symm

added theorem Ideal.Cotangent.equivOfEq_toCotangent

modified def Ideal.Cotangent.lift

modified theorem Ideal.Cotangent.lift_comp_toCotangent

modified theorem Ideal.Cotangent.lift_surjective_iff

modified theorem Ideal.Cotangent.lift_toCotangent

deleted theorem Ideal.mapCotangent_ker_of_surjective

deleted theorem Ideal.mapCotangent_surjective_of_comap_eq

deleted theorem IsLocalRing.CotangentSpace.map_eq_top_iff

deleted theorem IsLocalRing.CotangentSpace.span_image_eq_top_iff

deleted theorem IsLocalRing.finrank_cotangentSpace_eq_zero

deleted theorem IsLocalRing.finrank_cotangentSpace_eq_zero_iff

deleted theorem IsLocalRing.finrank_cotangentSpace_le_one_iff

deleted theorem IsLocalRing.subsingleton_cotangentSpace_iff