cotangentComplex_injective — Mathlib

English

The extended cotangent complex map is injective; i.e., the kernel is trivial.

Русский

Расширенное отображение касательного комплекса инъективно; ядро тривиально.

LaTeX

$$Injectivity of $P.toExtension.cotangentComplex$.$$

Lean4

theorem cotangentComplex_injective : Function.Injective P.toExtension.cotangentComplex :=
  by
  have := P.cotangentComplexAux_injective
  simp only [PreSubmersivePresentation.cotangentComplexAux, LinearMap.coe_comp, LinearEquiv.coe_coe] at this
  exact Function.Injective.of_comp (Function.Injective.of_comp <| Function.Injective.of_comp this)

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