Commit 2024-12-28 11:04 161c83c3

View on Github →

feat(RingTheory): Jacobi-Zariski sequence (#19067)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Module/Presentation/Differentials.lean

Modified Mathlib/Data/Finsupp/Basic.lean

added theorem Finsupp.prod_sumElim

modified def Finsupp.sumElim

Modified Mathlib/RingTheory/Generators.lean

added theorem Algebra.Generators.map_toComp_ker

added theorem Algebra.Generators.ofComp_toAlgHom_monomial_sumElim

added theorem Algebra.Generators.toComp_toAlgHom

added theorem Algebra.Generators.toComp_toAlgHom_monomial

Modified Mathlib/RingTheory/Kaehler/CotangentComplex.lean

added theorem Algebra.Generators.toKaehler_cotangentSpaceBasis

Created Mathlib/RingTheory/Kaehler/JacobiZariski.lean

added theorem Algebra.Generators.Cotangent.exact

added theorem Algebra.Generators.Cotangent.map_ofComp_ker

added theorem Algebra.Generators.Cotangent.surjective_map_ofComp

added def Algebra.Generators.CotangentSpace.compEquiv

added theorem Algebra.Generators.CotangentSpace.compEquiv_symm_inr

added theorem Algebra.Generators.CotangentSpace.compEquiv_symm_zero

added theorem Algebra.Generators.CotangentSpace.exact

added theorem Algebra.Generators.CotangentSpace.fst_compEquiv

added theorem Algebra.Generators.CotangentSpace.fst_compEquiv_apply

added theorem Algebra.Generators.CotangentSpace.map_ofComp_surjective

added theorem Algebra.Generators.CotangentSpace.map_toComp_injective

added theorem Algebra.Generators.H1Cotangent.exact_map_δ'

added theorem Algebra.Generators.H1Cotangent.exact_map_δ

added theorem Algebra.Generators.H1Cotangent.exact_δ_map

added theorem Algebra.Generators.H1Cotangent.map_comp_cotangentComplex_baseChange

added def Algebra.Generators.H1Cotangent.δ

added def Algebra.Generators.H1Cotangent.δAux

added theorem Algebra.Generators.H1Cotangent.δAux_C

added theorem Algebra.Generators.H1Cotangent.δAux_X

added theorem Algebra.Generators.H1Cotangent.δAux_monomial

added theorem Algebra.Generators.H1Cotangent.δAux_mul

added theorem Algebra.Generators.H1Cotangent.δAux_ofComp

added theorem Algebra.Generators.H1Cotangent.δAux_toAlgHom

added theorem Algebra.Generators.H1Cotangent.δ_comp_equiv

added theorem Algebra.Generators.H1Cotangent.δ_eq

added theorem Algebra.Generators.H1Cotangent.δ_eq_δ

added theorem Algebra.Generators.H1Cotangent.δ_eq_δAux

added theorem Algebra.Generators.H1Cotangent.δ_map

added def Algebra.Generators.kerCompPreimage

added theorem Algebra.Generators.ofComp_kerCompPreimage

added theorem Algebra.H1Cotangent.exact_map_δ

added theorem Algebra.H1Cotangent.exact_δ_mapBaseChange

added def Algebra.H1Cotangent.δ