Documentation

Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf

The presheaf of differentials of a presheaf of modules #

In this file, we define the type M.Derivation φ of derivations with values in a presheaf of R-modules M relative to a morphism of φ : S ⟶ F.op ⋙ R of presheaves of commutative rings over categories C and D that are related by a functor F : C ⥤ D. We formalize the notion of universal derivation.

Geometrically, if f : X ⟶ S is a morphisms of schemes (or more generally a morphism of commutative ringed spaces), we would like to apply these definitions in the case where F is the pullback functors from open subsets of S to open subsets of X and φ is the morphism $O_S ⟶ f_* O_X$.

In order to prove that there exists a universal derivation, the target of which shall be called the presheaf of relative differentials of φ, we first study the case where F is the identity functor. In this case where we have a morphism of presheaves of commutative rings φ' : S' ⟶ R, we construct a derivation DifferentialsConstruction.derivation' which is universal. Then, the general case (TODO) shall be obtained by observing that derivations for S ⟶ F.op ⋙ R identify to derivations for S' ⟶ R where S' is the pullback by F of the presheaf of commutative rings S (the data is the same: it suffices to show that the two vanishing conditions d_app are equivalent).

Given a morphism of presheaves of commutative rings φ : S ⟶ F.op ⋙ R, this is the type of relative φ-derivation of a presheaf of R-modules M.

  • d : {X : Dᵒᵖ} → (R.obj X) →+ (M.obj X)

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

  • d_mul : ∀ {X : Dᵒᵖ} (a b : (R.obj X)), self.d (a * b) = a self.d b + b self.d a
  • d_map : ∀ {X Y : Dᵒᵖ} (f : X Y) (x : (R.obj X)), self.d ((R.map f) x) = (M.map f).hom (self.d x)
  • d_app : ∀ {X : Cᵒᵖ} (a : (S.obj X)), self.d ((φ.app X) a) = 0
Instances For
    theorem PresheafOfModules.Derivation.ext {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst✝¹ : 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} {x y : M.Derivation φ} (d : @PresheafOfModules.Derivation.d C inst✝ D inst✝¹ S F R M φ x = @PresheafOfModules.Derivation.d C inst✝ D inst✝¹ S F R M φ y) :
    x = y
    theorem PresheafOfModules.Derivation.congr_d {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} {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} {φ : S F.op.comp R} {d d' : M.Derivation φ} (h : d = d') {X : Dᵒᵖ} (b : (R.obj X)) :
    d.d b = d'.d b

    The postcomposition of a derivation by a morphism of presheaves of modules.

    Equations
    • d.postcomp f = { d := fun {X : Dᵒᵖ} => (f.app X).hom.toAddMonoidHom.comp d.d, d_mul := , d_map := , d_app := }
    Instances For
      @[simp]
      theorem PresheafOfModules.Derivation.postcomp_d_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} {M N : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} {φ : S F.op.comp R} (d : M.Derivation φ) (f : M N) {X✝ : Dᵒᵖ} (a✝ : (R.obj X✝)) :
      (d.postcomp f).d a✝ = (f.app X✝).hom (d.d a✝)

      The universal property that a derivation d : M.Derivation φ must satisfy so that the presheaf of modules M can be considered as the presheaf of (relative) differentials of a presheaf of commutative rings φ : S ⟶ F.op ⋙ R.

      Instances For

        The property that there exists a universal derivation for a morphism of presheaves of commutative rings S ⟶ F.op ⋙ R.

        Instances
          @[reducible, inline]

          Given a morphism of presheaves of commutative rings φ : S ⟶ R, this is the type of relative φ-derivation of a presheaf of R-modules M.

          Equations
          • M.Derivation' φ' = M.Derivation φ'
          Instances For
            @[simp]
            theorem PresheafOfModules.Derivation'.d_app {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S' R : CategoryTheory.Functor Dᵒᵖ CommRingCat} {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} {φ' : S' R} (d : M.Derivation' φ') {X : Dᵒᵖ} (a : (S'.obj X)) :
            d.d ((φ'.app X) a) = 0
            noncomputable def PresheafOfModules.Derivation'.app {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S' R : CategoryTheory.Functor Dᵒᵖ CommRingCat} {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} {φ' : S' R} (d : M.Derivation' φ') (X : Dᵒᵖ) :
            (M.obj X).Derivation (φ'.app X)

            The derivation relative to the morphism of commutative rings φ'.app X induced by a derivation relative to a morphism of presheaves of commutative rings.

            Equations
            Instances For
              @[simp]
              theorem PresheafOfModules.Derivation'.app_apply {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S' R : CategoryTheory.Functor Dᵒᵖ CommRingCat} {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} {φ' : S' R} (d : M.Derivation' φ') {X : Dᵒᵖ} (b : (R.obj X)) :
              (d.app X).d b = d.d b
              def PresheafOfModules.Derivation'.mk {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S' R : CategoryTheory.Functor Dᵒᵖ CommRingCat} {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} {φ' : S' R} (d : (X : Dᵒᵖ) → (M.obj X).Derivation (φ'.app X)) (d_map : ∀ ⦃X Y : Dᵒᵖ⦄ (f : X Y) (x : (R.obj X)), (d Y).d ((R.map f) x) = (M.map f).hom ((d X).d x)) :
              M.Derivation' φ'

              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.

              Equations
              Instances For
                @[simp]
                theorem PresheafOfModules.Derivation'.mk_app {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S' R : CategoryTheory.Functor Dᵒᵖ CommRingCat} {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} {φ' : S' R} (d : (X : Dᵒᵖ) → (M.obj X).Derivation (φ'.app X)) (d_map : ∀ ⦃X Y : Dᵒᵖ⦄ (f : X Y) (x : (R.obj X)), (d Y).d ((R.map f) x) = (M.map f).hom ((d X).d x)) (X : Dᵒᵖ) :

                Constructor for Derivation.Universal in the case F is the identity functor.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

                  The presheaf of relative differentials of a morphism of presheaves of commutative rings.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For

                    The derivation Derivation' φ' is universal.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For