subsingleton_h1Cotangent — Mathlib

English

The first cotangent space H1Cotangent is a Subsingleton (i.e., trivial) if and only if the cotangent map cotangentComplex is injective.

Русский

Первое когнатное пространство H1Cotangent является тривиальным тогда и только тогда, когда отображение cotangentComplex инъективно.

LaTeX

$$$(\\text{Subsingleton } P.H1Cotangent) \\iff (\\text{Function.Injective } P.cotangentComplex)$$$

Lean4

theorem subsingleton_h1Cotangent (P : Extension R S) :
    Subsingleton P.H1Cotangent ↔ Function.Injective P.cotangentComplex :=
  by
  delta Extension.H1Cotangent
  rw [← LinearMap.ker_eq_bot, Submodule.eq_bot_iff, subsingleton_iff_forall_eq 0, Subtype.forall']
  simp only [Subtype.ext_iff, Submodule.coe_zero]

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