H1Cotangent — Mathlib

English

Isomorphism class of H1Cotangent does not depend on the choice of presentation; i.e. isomorphic algebras give isomorphic H1Cotangent spaces.

Русский

Класс изоморфности H1Cotangent не зависит от выбора презентации; тождественные алгебры дают изоморфные пространства H1Cotangent.

LaTeX

$$equiv (P P') : P.toExtension.H1Cotangent ≃ₗ[S] P'.toExtension.H1Cotangent$$

Lean4

/-- `H¹(L_{S/R})`, the first homology of the (naive) cotangent complex of `S` over `R`. -/
abbrev H1Cotangent : Type _ :=
  (Generators.self R S).toExtension.H1Cotangent

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