cotangentComplexAux_surjective — Mathlib

English

For finite σ, the map cotangentComplexAux is surjective.

Русский

Для конечного σ отображение cotangentComplexAux сюръективно.

LaTeX

$$For finite σ, $P.cotangentComplexAux$ is surjective.$$

Lean4

theorem cotangentComplexAux_surjective [Finite σ] : Function.Surjective P.cotangentComplexAux :=
  by
  rw [← LinearMap.range_eq_top, _root_.eq_top_iff, ← P.basisDeriv.span_eq, Submodule.span_le]
  rintro - ⟨i, rfl⟩
  use Cotangent.mk ⟨P.relation i, P.relation_mem_ker i⟩
  ext j
  rw [P.cotangentComplexAux_apply]
  simp

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