map_cotangentComplex — Mathlib

English

Compatibility between cotangentSpace.map and cotangentComplex: map f composed with cotangentComplex equals cotangentComplex after applying map f with base-change.

Русский

Совместимость между map и cotangentComplex: отображение через f, применённое к cotangentComplex, равно cotangentComplex после применения map f и базового изменения.

LaTeX

$$$\\operatorname{CotangentSpace}.map(f) \\circ \\cotangentComplex = \\cotangentComplex.\\restrictScalars S \\circ \\Cotangent.map f$$$

Lean4

theorem map_cotangentComplex (f : Hom P P') (x) :
    CotangentSpace.map f (P.cotangentComplex x) = P'.cotangentComplex (.map f x) :=
  by
  obtain ⟨x, rfl⟩ := Cotangent.mk_surjective x
  rw [cotangentComplex_mk, map_tmul, map_one, Cotangent.map_mk, cotangentComplex_mk]

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