hom₁_single — Mathlib

English

The canonical map from the freely generated module to the extension cotangent module is well defined and interacts compatibly with the relations.

Русский

Каноническое отображение от свободно порожденного модуля к модулю касательной к расширению корректно взаимодействует с отношениями.

LaTeX

$$$\\text{hom}_1 : (\\sigma \\to_0 S) \\to_A pres.toExtension.Cotangent$ is a linear map compatible with presentation relations.$$

Lean4

theorem hom₁_single (r : σ) : hom₁ pres (Finsupp.single r 1) = Extension.Cotangent.mk ⟨pres.relation r, by simp⟩ := by
  simp [hom₁]

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