app — Mathlib

English

Given a presheaf M and a morphism φ' of presheaves of rings, the app construction defines for each X ∈ Dᵒᵖ a derivation on M.obj X with target φ'.app X by taking d X as the underlying derivation.

Русский

Для пресшефa M и отображения φ' между пресшепами колец, определение app присваивает каждому X ∈ Dᵒᵖ вывод на модуле M.obj X с целью φ'.app X, задаваемый компонентом d X.

LaTeX

$$$\text{app}(d)(X) := (M.obj X).Derivation (\phi'.app X) \; \text{ with underlying map } b \mapsto d.d b$$$

Lean4

/-- The derivation relative to the morphism of commutative rings `φ'.app X` induced by
a derivation relative to a morphism of presheaves of commutative rings. -/
noncomputable def app (d : M.Derivation' φ') (X : Dᵒᵖ) : (M.obj X).Derivation (φ'.app X) :=
  ModuleCat.Derivation.mk (fun b ↦ d.d b)

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