relativeDifferentials' — Mathlib

English

For X, Y ∈ Dᵒᵖ and f: X ⟶ Y, the differential map commutes with R.map f, i.e., map_d of Kaehler differentials aligns with R.map f.

Русский

Для X, Y ∈ Dᵒᵖ и f: X ⟶ Y диагональная карта дифференциала коммутирует с R.map f.

LaTeX

$$$\mathrm{KaehlerDifferential.map}(φ'.naturality f) = \mathrm{KaehlerDifferential.d}(R.map f x)$$$

Lean4

/-- The presheaf of relative differentials of a morphism of presheaves of
commutative rings. -/
@[simps -isSimp]
noncomputable def relativeDifferentials' : PresheafOfModules.{u} (R ⋙ forget₂ _ _)
    where
  obj
    X :=
    CommRingCat.KaehlerDifferential
      (φ'.app X)
        -- Have to hint `g' := R.map f` below, or it gets unfolded weirdly.

  map
    f :=
    CommRingCat.KaehlerDifferential.map (g' := R.map f)
      (φ'.naturality f)
        -- Without `dsimp`, `ext` doesn't pick up the right lemmas.

  map_id _ := by dsimp; ext; simp
  map_comp _ _ := by dsimp; ext; simp

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