Documentation

TauCeti.AlgebraicGeometry.Modules.Differentials.Rational

Regular differentials inside rational differentials #

On an integral scheme over Spec R, a differential section has a rational value in Ω[k(X)⁄R]: take its generic germ and use the stalk comparison for relative differentials. The value of d a is d of the rational function represented by a, and rational values commute with restriction to nonempty open subsets.

If the differential sheaf is invertible, these maps are injective. Moreover, a rational differential is regular on an open subset precisely when it comes from the differential stalk at every point of that subset. In particular these results apply to schemes smooth of relative dimension one, over an arbitrary commutative base ring. This realizes the differential line bundle as local lattices in its rational differential space, the input to comparing it with a divisor sheaf and with the canonical bundle defined using Weil differentials.

References #

The generic-stalk identification uses Scheme.relativeDifferentialsStalkEquiv; the regularity criterion uses InvertibleSheaf.mem_range_genericPoint_germ_iff.

source
noncomputable def TauCeti.AlgebraicGeometry.relativeDifferentialsGenericStalkEquiv (R : Type u) [CommRing R] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧R)] [AlgebraicGeometry.IsIntegral X] :
↑((AlgebraicGeometry.Scheme.relativeDifferentials R X).presheaf.stalk (genericPoint ↥X)) ≃ₗ[↑X.functionField] Ω[↑X.functionField⁄R]

The generic stalk of the differential sheaf, identified with the differentials of the function field. Both base-algebra structures are given by the generic germ of the base-ring map.

Equations
Instances For
    source
    noncomputable def TauCeti.AlgebraicGeometry.rationalDifferential (R : Type u) [CommRing R] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧R)] [AlgebraicGeometry.IsIntegral X] (U : X.Opens) [Nonempty ↥↑U] :
    ↑((AlgebraicGeometry.Scheme.relativeDifferentials R X).presheaf.obj (Opposite.op U)) →ₗ[↑(X.presheaf.obj (Opposite.op U))] Ω[↑X.functionField⁄R]

    The rational value of a differential section over a nonempty open subset.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem TauCeti.AlgebraicGeometry.rationalDifferential_apply (R : Type u) [CommRing R] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧R)] [AlgebraicGeometry.IsIntegral X] (U : X.Opens) [Nonempty ↥↑U] (s : ↑((AlgebraicGeometry.Scheme.relativeDifferentials R X).presheaf.obj (Opposite.op U))) :
      (rationalDifferential R U) s = (relativeDifferentialsGenericStalkEquiv R) ((CategoryTheory.ConcreteCategory.hom ((AlgebraicGeometry.Scheme.relativeDifferentials R X).presheaf.germ U (genericPoint ↥X) ⋯)) s)

      The rational value is the differential's generic germ under the stalk comparison. This is not a simp lemma: computation rules preserve rationalDifferential as the normal form.

      source
      @[simp]
      theorem TauCeti.AlgebraicGeometry.rationalDifferential_d (R : Type u) [CommRing R] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧R)] [AlgebraicGeometry.IsIntegral X] (U : X.Opens) [Nonempty ↥↑U] (a : ↑(X.presheaf.obj (Opposite.op U))) :
      (rationalDifferential R U) ((AlgebraicGeometry.Scheme.universalDerivation R X).d a) = (KaehlerDifferential.D R ↑X.functionField) ((CategoryTheory.ConcreteCategory.hom (X.germToFunctionField U)) a)

      The rational value of d a is the differential of the rational function represented by a.

      source
      @[simp]
      theorem TauCeti.AlgebraicGeometry.rationalDifferential_map (R : Type u) [CommRing R] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧R)] [AlgebraicGeometry.IsIntegral X] {U V : X.Opens} [Nonempty ↥↑U] [Nonempty ↥↑V] (i : U ⟶ V) (s : ↑((AlgebraicGeometry.Scheme.relativeDifferentials R X).presheaf.obj (Opposite.op V))) :
      (rationalDifferential R U) ((CategoryTheory.ConcreteCategory.hom ((AlgebraicGeometry.Scheme.relativeDifferentials R X).presheaf.map i.op)) s) = (rationalDifferential R V) s

      Restriction to a nonempty open subset preserves the rational value of a differential.

      source
      noncomputable def TauCeti.AlgebraicGeometry.rationalDifferentialStalk (R : Type u) [CommRing R] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧R)] [AlgebraicGeometry.IsIntegral X] (x : ↥X) :
      ↑((AlgebraicGeometry.Scheme.relativeDifferentials R X).presheaf.stalk x) →ₗ[↑(X.presheaf.stalk x)] Ω[↑X.functionField⁄R]

      The map from a differential stalk to rational differentials, induced by specialization to the generic stalk, linear for the local-ring action through its map to the function field.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem TauCeti.AlgebraicGeometry.rationalDifferentialStalk_apply (R : Type u) [CommRing R] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧R)] [AlgebraicGeometry.IsIntegral X] (x : ↥X) (s : ↑((AlgebraicGeometry.Scheme.relativeDifferentials R X).presheaf.stalk x)) :
        (rationalDifferentialStalk R x) s = (relativeDifferentialsGenericStalkEquiv R) ((CategoryTheory.ConcreteCategory.hom ((AlgebraicGeometry.Scheme.relativeDifferentials R X).presheaf.stalkSpecializes ⋯)) s)

        The local rational value is specialization to the generic stalk under the stalk comparison. This is not a simp lemma: computation rules preserve rationalDifferentialStalk as the normal form.

        source
        @[simp]
        theorem TauCeti.AlgebraicGeometry.rationalDifferentialStalk_germ (R : Type u) [CommRing R] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧R)] [AlgebraicGeometry.IsIntegral X] {U : X.Opens} [Nonempty ↥↑U] (x : ↥X) (hx : x ∈ U) (s : ↑((AlgebraicGeometry.Scheme.relativeDifferentials R X).presheaf.obj (Opposite.op U))) :
        (rationalDifferentialStalk R x) ((CategoryTheory.ConcreteCategory.hom ((AlgebraicGeometry.Scheme.relativeDifferentials R X).presheaf.germ U x hx)) s) = (rationalDifferential R U) s

        Passing from a differential section through any stalk gives its rational value.

        source
        @[simp]
        theorem TauCeti.AlgebraicGeometry.rationalDifferentialStalk_symm_D (R : Type u) [CommRing R] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧R)] [AlgebraicGeometry.IsIntegral X] (x : ↥X) (a : ↑(X.presheaf.stalk x)) :
        (rationalDifferentialStalk R x) ((AlgebraicGeometry.Scheme.relativeDifferentialsStalkEquiv R X x).symm ((KaehlerDifferential.D R ↑(X.presheaf.stalk x)) a)) = (KaehlerDifferential.D R ↑X.functionField) ((algebraMap ↑(X.presheaf.stalk x) ↑X.functionField) a)

        The local rational-differential map sends the local differential of a to the differential of its image in the function field.

        source
        theorem TauCeti.AlgebraicGeometry.rationalDifferential_injective (R : Type u) [CommRing R] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧R)] [AlgebraicGeometry.IsIntegral X] [SheafOfModules.isInvertible X (AlgebraicGeometry.Scheme.relativeDifferentials R X)] (U : X.Opens) [Nonempty ↥↑U] :
        Function.Injective ⇑(rationalDifferential R U)

        A differential section is determined by its rational value when the differential sheaf is invertible, in particular on a scheme smooth of relative dimension one.

        source
        @[simp]
        theorem TauCeti.AlgebraicGeometry.rationalDifferential_eq_zero_iff (R : Type u) [CommRing R] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧R)] [AlgebraicGeometry.IsIntegral X] [SheafOfModules.isInvertible X (AlgebraicGeometry.Scheme.relativeDifferentials R X)] (U : X.Opens) [Nonempty ↥↑U] (s : ↑((AlgebraicGeometry.Scheme.relativeDifferentials R X).presheaf.obj (Opposite.op U))) :
        (rationalDifferential R U) s = 0 ↔ s = 0

        A differential section with zero rational value is zero when the differential sheaf is invertible.

        source
        theorem TauCeti.AlgebraicGeometry.mem_range_rationalDifferential_iff (R : Type u) [CommRing R] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧R)] [AlgebraicGeometry.IsIntegral X] [SheafOfModules.isInvertible X (AlgebraicGeometry.Scheme.relativeDifferentials R X)] (U : X.Opens) [Nonempty ↥↑U] (ω : Ω[↑X.functionField⁄R]) :
        ω ∈ Set.range ⇑(rationalDifferential R U) ↔ ∀ x ∈ U, ω ∈ Set.range ⇑(rationalDifferentialStalk R x)

        A rational differential is regular on a nonempty open subset exactly when it comes from all the differential stalks there, provided the differential sheaf is invertible.