comm₁₂_single — Mathlib

English

The image of a single generator r is sent to the corresponding differential in the cotangent extension.

Русский

Изображение одного генератора r переходит в соответствующий дифференциал в касательном расширении.

LaTeX

$$$hom_1 pres (Finsupp.single r 1) = Extension.Cotangent.mk\\langle pres.relation r, \\dots \\rangle$$$

Lean4

theorem comm₁₂_single (r : σ) :
    pres.toExtension.cotangentComplex (hom₁ pres (Finsupp.single r 1)) =
      pres.cotangentSpaceBasis.repr.symm ((differentialsRelations pres).relation r) :=
  by
  simp only [hom₁, Finsupp.linearCombination_single, one_smul, differentialsRelations, Basis.repr_symm_apply,
    Extension.cotangentComplex_mk]
  exact pres.cotangentSpaceBasis.repr.injective (by ext; simp)

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