Commit 2024-07-31 08:12 9c47f211

View on Github →

feat(RingTheory/Kaehler): Cotangent complex associated to an embedding into affine space. (#14859)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Exact.lean

added theorem Function.Exact.inl_snd

added theorem Function.Exact.inr_fst

Modified Mathlib/LinearAlgebra/Dual.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Basis.lean

added def Basis.baseChange

added theorem Basis.baseChange_apply

added theorem Basis.baseChange_repr_tmul

modified theorem Basis.tensorProduct_apply'

modified theorem Basis.tensorProduct_apply

modified theorem Basis.tensorProduct_repr_tmul_apply

Modified Mathlib/LinearAlgebra/TensorProduct/Matrix.lean

Modified Mathlib/RingTheory/Generators.lean

added theorem Algebra.Generators.Cotangent.map_comp

added theorem Algebra.Generators.Cotangent.map_id

added theorem Algebra.Generators.Cotangent.val_sub

added theorem Algebra.Generators.Hom.toAlgHom_comp_apply

added theorem Algebra.Generators.Hom.toAlgHom_id

added theorem Algebra.Generators.Hom.toAlgHom_monomial

Created Mathlib/RingTheory/Kaehler/CotangentComplex.lean

added theorem Algebra.Generators.Cotangent.map_sub_map

added def Algebra.Generators.CotangentSpace.map

added theorem Algebra.Generators.CotangentSpace.map_comp

added theorem Algebra.Generators.CotangentSpace.map_comp_apply

added theorem Algebra.Generators.CotangentSpace.map_comp_cotangentComplex

added theorem Algebra.Generators.CotangentSpace.map_cotangentComplex

added theorem Algebra.Generators.CotangentSpace.map_id

added theorem Algebra.Generators.CotangentSpace.map_sub_map

added theorem Algebra.Generators.CotangentSpace.map_tmul

added theorem Algebra.Generators.CotangentSpace.repr_map

added def Algebra.Generators.Hom.sub

added def Algebra.Generators.Hom.subToKer

added theorem Algebra.Generators.Hom.sub_aux

added theorem Algebra.Generators.Hom.sub_one_tmul

added theorem Algebra.Generators.Hom.sub_tmul

added def Algebra.Generators.cotangentComplex

added theorem Algebra.Generators.cotangentComplex_mk

added def Algebra.Generators.cotangentSpaceBasis

added theorem Algebra.Generators.cotangentSpaceBasis_apply

added theorem Algebra.Generators.cotangentSpaceBasis_repr_one_tmul

added theorem Algebra.Generators.cotangentSpaceBasis_repr_tmul

added theorem Algebra.Generators.exact_cotangentComplex_toKaehler

added theorem Algebra.Generators.toKaehler_cotangentSpaceBasis

added theorem Algebra.Generators.toKaehler_surjective