Theorems · Definition · algebraic geometry

PresheafOfModules.Derivation.d

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} →
          {F : CategoryTheory.Functor C D} →
            {R : CategoryTheory.Functor Dᵒᵖ CommRingCat} →
              {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} →
                {φ : S ⟶ F.op.comp R} → M.Derivation φ → {X : Dᵒᵖ} → ↑(R.obj X) →+ ↑(M.obj X)

the underlying additive map R.obj X →+ M.obj X of a derivation

Defined in

Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf

Cited by

10 results in Mathlib

Foundations

Depth 28 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Category