English
Construction of the universal object for Derivation.Universal in the case when F is the identity functor, providing a data structure (desc, fac, postcomp_injective) giving a universal derivation.
Русский
Построение универсального объекта для Derivation.Universal в случае, когда F — тождественный функтор, с данными (desc, fac, postcomp_injective) задающими универсальное свойство деривации.
LaTeX
$$$\text{Universal.mk} \; (d\;:{\text{M.Derivation' } φ'}) \; (desc) (fac) (postcomp\_injective) : \text{Derivation.Universal } d$$$
Lean4
/-- Given a morphism of presheaves of commutative rings `φ'`, this is the
in derivation `M.Derivation' φ'` that is given by a compatible family of derivations
with values in the modules `M.obj X` for all `X`. -/
def mk (d_map : ∀ ⦃X Y : Dᵒᵖ⦄ (f : X ⟶ Y) (x : R.obj X), (d Y).d ((R.map f) x) = (M.map f) ((d X).d x)) :
M.Derivation' φ' where d {X} := AddMonoidHom.mk' (d X).d (by simp)
