isUniversal' — Mathlib

Lean4
/-- The derivation `Derivation' φ'` is universal. -/
noncomputable def isUniversal' : (derivation' φ').Universal :=
  Derivation'.Universal.mk
    (fun {M'} d' ↦
      { app := fun X ↦ (d'.app X).desc
        naturality := fun {X Y} f ↦
          CommRingCat.KaehlerDifferential.ext
            (fun b ↦ by
              dsimp
              rw [ModuleCat.Derivation.desc_d, Derivation'.app_apply]
              erw [relativeDifferentials'_map_d φ' f]
              simp) })
    (fun {M'} d' ↦ by
      ext X b
      apply ModuleCat.Derivation.desc_d)
    (fun {M} α β h ↦ by
      ext1 X
      exact CommRingCat.KaehlerDifferential.ext (Derivation.congr_d h))
Похожие утверждения