exact_cotangentComplex_toKaehler — Mathlib

English

The first cotangent homology H1Cotangent is the kernel of the cotangent complex map, giving a canonical abelian group structure to cotangent data.

Русский

Первая котантогенная группа H1Cotangent есть ядро котантного комплекса, задающее абелеву группу котант-данных.

LaTeX

$$$\\mathrm{H1Cotangent}(P) = \\ker(P.cotangentComplex)$$$

Lean4

theorem exact_cotangentComplex_toKaehler : Function.Exact P.cotangentComplex P.toKaehler :=
  exact_kerCotangentToTensor_mapBaseChange _ _ _ P.algebraMap_surjective

Похожие утверждения