Commit 2024-11-15 10:09 6ae3e986

View on Github →

refactor(RingTheory): generalize cotangent complex for arbitrary extensions (#18684)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Extension.lean

added theorem Algebra.Extension.Cotangent.ext

added def Algebra.Extension.Cotangent.map

added theorem Algebra.Extension.Cotangent.map_comp

added theorem Algebra.Extension.Cotangent.map_id

added theorem Algebra.Extension.Cotangent.map_mk

added def Algebra.Extension.Cotangent.mk

added theorem Algebra.Extension.Cotangent.mk_surjective

added def Algebra.Extension.Cotangent.of

added theorem Algebra.Extension.Cotangent.of_add

added theorem Algebra.Extension.Cotangent.of_val

added theorem Algebra.Extension.Cotangent.of_zero

added theorem Algebra.Extension.Cotangent.smul_eq_zero_of_mem

added def Algebra.Extension.Cotangent.val

added theorem Algebra.Extension.Cotangent.val_add

added theorem Algebra.Extension.Cotangent.val_mk

added theorem Algebra.Extension.Cotangent.val_of

added theorem Algebra.Extension.Cotangent.val_smul'''

added theorem Algebra.Extension.Cotangent.val_smul''

added theorem Algebra.Extension.Cotangent.val_smul'

added theorem Algebra.Extension.Cotangent.val_smul

added theorem Algebra.Extension.Cotangent.val_sub

added theorem Algebra.Extension.Cotangent.val_zero

added def Algebra.Extension.Cotangent

added theorem Algebra.Extension.Hom.comp_id

added theorem Algebra.Extension.Hom.id_comp

added def Algebra.Extension.Hom.toAlgHom

added theorem Algebra.Extension.Hom.toAlgHom_apply

added theorem Algebra.Extension.Hom.toAlgHom_id

added structure Algebra.Extension.Hom

added theorem Algebra.Extension.algebraMap_surjective

added def Algebra.Extension.baseChange

added def Algebra.Extension.localization

added def Algebra.Extension.ofSurjective

added def Algebra.Extension.self

added theorem Algebra.Extension.σ_injective

added theorem Algebra.Extension.σ_smul

added structure Algebra.Extension

Modified Mathlib/RingTheory/Generators.lean

deleted theorem Algebra.Generators.Cotangent.ext

deleted def Algebra.Generators.Cotangent.map

deleted theorem Algebra.Generators.Cotangent.map_comp

deleted theorem Algebra.Generators.Cotangent.map_id

deleted theorem Algebra.Generators.Cotangent.map_mk

deleted def Algebra.Generators.Cotangent.mk

deleted theorem Algebra.Generators.Cotangent.mk_surjective

deleted def Algebra.Generators.Cotangent.of

deleted theorem Algebra.Generators.Cotangent.of_add

deleted theorem Algebra.Generators.Cotangent.of_val

deleted theorem Algebra.Generators.Cotangent.of_zero

deleted theorem Algebra.Generators.Cotangent.smul_eq_zero_of_mem

deleted def Algebra.Generators.Cotangent.val

deleted theorem Algebra.Generators.Cotangent.val_add

deleted theorem Algebra.Generators.Cotangent.val_mk

deleted theorem Algebra.Generators.Cotangent.val_of

deleted theorem Algebra.Generators.Cotangent.val_smul'''

deleted theorem Algebra.Generators.Cotangent.val_smul''

deleted theorem Algebra.Generators.Cotangent.val_smul'

deleted theorem Algebra.Generators.Cotangent.val_smul

deleted theorem Algebra.Generators.Cotangent.val_sub

deleted theorem Algebra.Generators.Cotangent.val_zero

deleted def Algebra.Generators.Cotangent

added def Algebra.Generators.Hom.toExtensionHom

added theorem Algebra.Generators.Hom.toExtensionHom_comp

added theorem Algebra.Generators.Hom.toExtensionHom_id

added def Algebra.Generators.toExtension

Modified Mathlib/RingTheory/Kaehler/CotangentComplex.lean

added theorem Algebra.Extension.Cotangent.map_sub_map

added def Algebra.Extension.CotangentSpace.map

added theorem Algebra.Extension.CotangentSpace.map_comp

added theorem Algebra.Extension.CotangentSpace.map_comp_apply

added theorem Algebra.Extension.CotangentSpace.map_comp_cotangentComplex

added theorem Algebra.Extension.CotangentSpace.map_cotangentComplex

added theorem Algebra.Extension.CotangentSpace.map_id

added theorem Algebra.Extension.CotangentSpace.map_sub_map

added theorem Algebra.Extension.CotangentSpace.map_tmul

added def Algebra.Extension.H1Cotangent.map

added theorem Algebra.Extension.H1Cotangent.map_comp

added theorem Algebra.Extension.H1Cotangent.map_eq

added theorem Algebra.Extension.H1Cotangent.map_id

added theorem Algebra.Extension.H1Cotangent.val_add

added theorem Algebra.Extension.H1Cotangent.val_smul

added theorem Algebra.Extension.H1Cotangent.val_zero

added def Algebra.Extension.H1Cotangent

added def Algebra.Extension.Hom.sub

added def Algebra.Extension.Hom.subToKer

added theorem Algebra.Extension.Hom.sub_aux

added theorem Algebra.Extension.Hom.sub_one_tmul

added theorem Algebra.Extension.Hom.sub_tmul

added def Algebra.Extension.cotangentComplex

added theorem Algebra.Extension.cotangentComplex_mk

added theorem Algebra.Extension.exact_cotangentComplex_toKaehler

added def Algebra.Extension.h1Cotangentι

added theorem Algebra.Extension.h1Cotangentι_ext

added theorem Algebra.Extension.h1Cotangentι_injective

added theorem Algebra.Extension.subsingleton_h1Cotangent

added theorem Algebra.Extension.toKaehler_surjective

deleted theorem Algebra.Generators.Cotangent.map_sub_map

deleted def Algebra.Generators.CotangentSpace.map

deleted theorem Algebra.Generators.CotangentSpace.map_comp

deleted theorem Algebra.Generators.CotangentSpace.map_comp_apply

deleted theorem Algebra.Generators.CotangentSpace.map_comp_cotangentComplex

deleted theorem Algebra.Generators.CotangentSpace.map_cotangentComplex

deleted theorem Algebra.Generators.CotangentSpace.map_id

deleted theorem Algebra.Generators.CotangentSpace.map_sub_map

deleted theorem Algebra.Generators.CotangentSpace.map_tmul

deleted theorem Algebra.Generators.CotangentSpace.repr_map

modified def Algebra.Generators.H1Cotangent.equiv

deleted def Algebra.Generators.H1Cotangent.map

deleted theorem Algebra.Generators.H1Cotangent.map_comp

deleted theorem Algebra.Generators.H1Cotangent.map_eq

deleted theorem Algebra.Generators.H1Cotangent.map_id

deleted theorem Algebra.Generators.H1Cotangent.val_add

deleted theorem Algebra.Generators.H1Cotangent.val_smul

deleted theorem Algebra.Generators.H1Cotangent.val_zero

deleted def Algebra.Generators.H1Cotangent

deleted def Algebra.Generators.Hom.sub

deleted def Algebra.Generators.Hom.subToKer

deleted theorem Algebra.Generators.Hom.sub_aux

deleted theorem Algebra.Generators.Hom.sub_one_tmul

deleted theorem Algebra.Generators.Hom.sub_tmul

deleted def Algebra.Generators.cotangentComplex

deleted theorem Algebra.Generators.cotangentComplex_mk

modified def Algebra.Generators.cotangentSpaceBasis

modified theorem Algebra.Generators.cotangentSpaceBasis_apply

deleted theorem Algebra.Generators.exact_cotangentComplex_toKaehler

deleted def Algebra.Generators.h1Cotangentι

deleted theorem Algebra.Generators.h1Cotangentι_ext

deleted theorem Algebra.Generators.h1Cotangentι_injective

added theorem Algebra.Generators.repr_CotangentSpaceMap

deleted theorem Algebra.Generators.subsingleton_h1Cotangent

deleted theorem Algebra.Generators.toKaehler_cotangentSpaceBasis

deleted theorem Algebra.Generators.toKaehler_surjective

Modified Mathlib/RingTheory/Smooth/Kaehler.lean