relativeDifferentials'_map_d — Mathlib

English

A variant of the map compatibility for relative Kaehler differentials; explicit equality of KaehlerDifferential.map applied to morphisms and R.map f.

Русский

Вариант совместимости отображения KaehlerDifferential для относительных дифференциалов; явное равенство отображения KaehlerDifferential.apply к morphism и R.map f.

LaTeX

$$$\mathrm{LinearMap}.coerce\_d( ((relativeDifferentials' φ').map f) )\; x = \mathrm{KaehlerDifferential.d}(R.map f x)$$$

Lean4

@[simp]
theorem relativeDifferentials'_map_d {X Y : Dᵒᵖ} (f : X ⟶ Y) (x : R.obj X) :
    DFunLike.coe (α := CommRingCat.KaehlerDifferential (φ'.app X)) (β := fun _ ↦
        CommRingCat.KaehlerDifferential (φ'.app Y))
        (ModuleCat.Hom.hom (R := ↑(R.obj X)) ((relativeDifferentials' φ').map f))
        (CommRingCat.KaehlerDifferential.d x) =
      CommRingCat.KaehlerDifferential.d (R.map f x) :=
  CommRingCat.KaehlerDifferential.map_d (φ'.naturality f) _

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