Commit 2025-01-20 11:48 30e9b28a

View on Github →

feat(RingTheory): H¹(L) under localization (#20591)

Estimated changes

Modified Mathlib/RingTheory/Etale/Basic.lean

added def RingHom.FormallyEtale

added theorem RingHom.formallyEtale_algebraMap

Modified Mathlib/RingTheory/Etale/Kaehler.lean

added def Algebra.Extension.tensorCotangent

added def Algebra.Extension.tensorCotangentInvFun

added theorem Algebra.Extension.tensorCotangentInvFun_smul_mk

added def Algebra.Extension.tensorCotangentSpace

added def Algebra.Extension.tensorH1Cotangent

added def Algebra.Extension.tensorH1CotangentOfIsLocalization

added theorem Algebra.Extension.tensorH1CotangentOfIsLocalization_toLinearMap

added theorem KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale_symm_D_algebraMap

Modified Mathlib/RingTheory/Extension.lean

added def Algebra.Extension.Hom.mapKer

Modified Mathlib/RingTheory/Smooth/Kaehler.lean

added theorem Algebra.Extension.H1Cotangent.equivOfFormallySmooth_apply

added theorem Algebra.Extension.H1Cotangent.equivOfFormallySmooth_symm

added theorem Algebra.Extension.H1Cotangent.equivOfFormallySmooth_toLinearMap