The universal property of a universal derivation of presheaves

Mathlib's PresheafOfModulesOfCommRing.Derivation.Universal records that a derivation d : M.Derivation φ, relative to a morphism of presheaves of commutative rings φ : S ⟶ F.op ⋙ R, is universal: every derivation d' into a presheaf of R-modules N factors as d.postcomp f for a unique morphism f : M ⟶ N. This file packages that universal property as a bijection (M ⟶ N) ≃ N.Derivation φ, natural in N, which is the form in which it is transported along adjunctions, for instance to sheaves of modules through sheafification.

Main declarations

• PresheafOfModulesOfCommRing.Derivation.postcomp_comp: postcomposing a derivation is functorial;
• PresheafOfModulesOfCommRing.Derivation.Universal.homEquiv: for a universal derivation d : M.Derivation φ, the bijection (M ⟶ N) ≃ N.Derivation φ sending f to d.postcomp f.

@[simp]

theorem PresheafOfModulesOfCommRing.Derivation.postcomp_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ CommRingCat} {φ : S ⟶ F.op.comp R} {M N P : PresheafOfModulesOfCommRing R} (d : M.Derivation φ) (f : M ⟶ N) (g : N ⟶ P) : d.postcomp (CategoryTheory.CategoryStruct.comp f g) = (d.postcomp f).postcomp g

Postcomposing a derivation with a composite of morphisms of presheaves of modules is postcomposing with each in turn.

noncomputable def PresheafOfModulesOfCommRing.Derivation.Universal.homEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ CommRingCat} {φ : S ⟶ F.op.comp R} {M : PresheafOfModulesOfCommRing R} {d : M.Derivation φ} (hd : d.Universal) (N : PresheafOfModulesOfCommRing R) : (M ⟶ N) ≃ N.Derivation φ

The universal property of a universal derivation d : M.Derivation φ: morphisms M ⟶ N of presheaves of modules correspond to derivations into N, by postcomposition with d.

Equations

• hd.homEquiv N = { toFun := fun (f : M ⟶ N) => d.postcomp f, invFun := fun (d' : N.Derivation φ) => hd.desc d', left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem PresheafOfModulesOfCommRing.Derivation.Universal.homEquiv_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ CommRingCat} {φ : S ⟶ F.op.comp R} {M N : PresheafOfModulesOfCommRing R} {d : M.Derivation φ} (hd : d.Universal) (f : M ⟶ N) : (hd.homEquiv N) f = d.postcomp f

The bijection of a universal derivation d sends a morphism f to d.postcomp f.

@[simp]

theorem PresheafOfModulesOfCommRing.Derivation.Universal.homEquiv_symm_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ CommRingCat} {φ : S ⟶ F.op.comp R} {M N : PresheafOfModulesOfCommRing R} {d : M.Derivation φ} (hd : d.Universal) (d' : N.Derivation φ) : (hd.homEquiv N).symm d' = hd.desc d'

The inverse bijection of a universal derivation is its descent map.