instSubsingletonUniversal — Mathlib

English

There is a universal construction for Derivation' in the relative differential setting, giving a universal property with a desc, fac, and postcomp_injective data, linking all derivations and morphisms consistently.

Русский

Существует универсальная конструкция для Derivation' в относительных дифференциалах, задающая универсальное свойство через данные desc, fac и postcomp_injective, связывая все деривации и морфизмы согласованно.

LaTeX

$$$\\text{mk}: \\{\\text{desc}, \\text{fac}, \\text{postcomp_injective}\\} \\to (\\text{Universal } d)$$$

Lean4

instance : Subsingleton d.Universal where
  allEq h₁
    h₂ :=
    by
    suffices
      ∀ {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)} (d' : M'.Derivation φ), h₁.desc d' = h₂.desc d'
      by
      cases h₁
      cases h₂
      simp only [Universal.mk.injEq]
      ext : 2
      apply this
    intro M' d'
    apply h₁.postcomp_injective
    simp

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