D

Mathlib.Algebra.Category.ModuleCat.Differentials.Basic

URI: https://scilib.ai/kg/mathlib#CommRingCat.KaehlerDifferential.D

Lean4

/-- The (universal) derivation in `(KaehlerDifferential f).Derivation f`
when `f : A ⟶ B` is a morphism in the category `CommRingCat`. -/
noncomputable def D : (KaehlerDifferential f).Derivation f :=
  letI := f.hom.toAlgebra
  ModuleCat.Derivation.mk (fun b ↦ _root_.KaehlerDifferential.D A B b) (by simp) (by simp)
    (_root_.KaehlerDifferential.D A B).map_algebraMap

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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