kerCotangentToTensor_toCotangent

Mathlib.RingTheory.Kaehler.Basic

URI: https://scilib.ai/kg/mathlib#KaehlerDifferential.kerCotangentToTensor_toCotangent

English

The kernel of cotangent to tensor at 1 is trivial under algebra map.

Русский

Ядро cotangent to tensor на единице тривиально при алгебраическом отображении.

LaTeX

$$$\\kerCotangentToTensor\\,R\\,A\\,B \\big(1\\big) = 0$$$

Lean4

@[simp]
theorem kerCotangentToTensor_toCotangent (x) : kerCotangentToTensor R A B (Ideal.toCotangent _ x) = 1 ⊗ₜ D _ _ x.1 :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru