Commit 2025-01-08 16:06 60ae2db3

View on Github →

feat(RingTheory/Smooth): calculate H¹(L) via formally smooth extensions (#20471)

Estimated changes

Modified Mathlib/RingTheory/Extension.lean

added def Algebra.Extension.infinitesimal

added theorem Algebra.Extension.ker_infinitesimal

added def Algebra.Extension.toInfinitesimal

Modified Mathlib/RingTheory/Ideal/Cotangent.lean

added theorem Ideal.comap_cotangentIdeal

added theorem Ideal.mk_mem_cotangentIdeal

added theorem Ideal.range_cotangentToQuotientSquare

deleted theorem Ideal.to_quotient_square_range

Modified Mathlib/RingTheory/Kaehler/CotangentComplex.lean

added def Algebra.Extension.H1Cotangent.equiv

Modified Mathlib/RingTheory/Smooth/Kaehler.lean

added theorem Algebra.Extension.Cotangent.map_toInfinitesimal_bijective

added theorem Algebra.Extension.CotangentSpace.map_toInfinitesimal_bijective

added def Algebra.Extension.H1Cotangent.equivOfFormallySmooth

added theorem Algebra.Extension.H1Cotangent.map_toInfinitesimal_bijective

added def Algebra.Extension.equivH1CotangentOfFormallySmooth

added def Algebra.Extension.homInfinitesimal