cotangentComplexAux_zero_iff — Mathlib

English

Let P be a finite σ PreSubmersivePresentation and x ∈ P.ker. The cotangentComplexAux at Cotangent.mk x vanishes if and only if, for every i ∈ σ, the evaluation (aeval P.val) (pderiv (P.map i) x.val) equals 0.

Русский

Пусть P — пред-subмёрсивное представление с конечным σ и x ∈ P.ker. Касательный комплекс_aux в Cotangent.mk x равен нулю тогда и только тогда, когда для каждого i ∈ σ значение (aeval P.val) (pderiv (P.map i) x.val) равно нулю.

LaTeX

$$$P.cotangentComplexAux (Cotangent.mk x) = 0 \\iff (\\forall i : σ, (\\mathrm{aeval} P.val) (\\mathrm{pderiv} (P.map i) x.val) = 0)$$$

Lean4

theorem cotangentComplexAux_zero_iff [Finite σ] {P : PreSubmersivePresentation R S ι σ} (x : P.ker) :
    P.cotangentComplexAux (Cotangent.mk x) = 0 ↔ ∀ i : σ, (aeval P.val) (pderiv (P.map i) x.val) = 0 :=
  by
  rw [funext_iff]
  simp_rw [cotangentComplexAux_apply, Pi.zero_apply]

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