English
The presheaf of relative Kaehler differentials is defined, at each X ∈ Dᵒᵖ, to be the Kaehler differential of φ'.app X, with maps induced by φ'.naturality; i.e., levels defined by the Kaehler differentials functorial in X.
Русский
Пресшеф модуля относительных каэлеровых производных задаётся на каждом X ∈ Dᵒᵖ как Kaehler-дифференциал φ'.app X, а отображения задаются натуральностью φ'.naturality.
LaTeX
$$$\text{relativeDifferentials'} X = \mathrm{KaehlerDifferential}(\phi'.app X)$ and\; (\text{map } f) = \mathrm{KaehlerDifferential.map}(g' := R.map f)(\phi'.naturality f)$$$
Lean4
/-- Constructor for `Derivation.Universal` in the case `F` is the identity functor. -/
def mk {d : M.Derivation' φ'} (desc : ∀ {M' : PresheafOfModules (R ⋙ forget₂ _ _)} (_ : M'.Derivation' φ'), M ⟶ M')
(fac : ∀ {M' : PresheafOfModules (R ⋙ forget₂ _ _)} (d' : M'.Derivation' φ'), d.postcomp (desc d') = d')
(postcomp_injective :
∀ {M' : PresheafOfModules (R ⋙ forget₂ _ _)} (α β : M ⟶ M'), d.postcomp α = d.postcomp β → α = β) :
d.Universal where
desc := desc
fac := fac
postcomp_injective := postcomp_injective
