δ_eq — Mathlib

English

δ is independent of the choice of presentation in a refined setting; the δ map remains the same under varying P and Q data through the same equivalences.

Русский

δ не зависит от выбранной презентации в более точной настройке; отображение δ сохраняется при изменении данных P и Q через те же эквивалентности.

LaTeX

$$$δ Q P = δ Q P'$$$

Lean4

theorem δ_eq (x : Q.toExtension.H1Cotangent) (y) (hy : Extension.Cotangent.map (ofComp Q P).toExtensionHom y = x.1) (z)
    (hz :
      (Extension.CotangentSpace.map (toComp Q P).toExtensionHom).liftBaseChange T z =
        (Q.comp P).toExtension.cotangentComplex y) :
    δ Q P x = P.toExtension.toKaehler.baseChange T z :=
  by
  simp only [δ]
  apply SnakeLemma.δ_eq
  exacts [hy, hz]

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