Documentation

DerivedAlgGeo.AlgebraicGeometry.Duality.Serre.Categorical

Geometric comparison for Serre duality #

This file relates abstract Serre duality on the bounded coherent derived category of a smooth proper scheme to the existing sheaf-level bilinear duality data.

Main definitions #

Main results #

Implementation notes #

GeometricSerreData.serre reuses the canonical abstract Serre root. The scalar compatibility of the additive Ext comparison and the derived twist's restriction to sheaves are supplied; the resulting derived duality and its naturality are transported along the specified functor isomorphism. Hom-finiteness follows from sheaf Ext-finiteness, that transport, and the standard t-structure. No geometric inhabitant or derived tensor functor is constructed here. CategoryTheory.SerreFunctor.SerreFunctorData is the abstract API, and AlgebraicGeometry.Duality.Serre.BilinearData is the sheaf presentation.

A sheaf-level AlgebraicGeometry.Duality.Serre.BilinearData.TrivialCanonical does not identify the derived twist functor with identity; the dimension-two consequences below state that functor-level natural isomorphism explicitly.

References #

Tags #

Serre duality, bounded derived category, coherent sheaves, Ext comparison.

source
noncomputable def AlgebraicGeometry.Duality.Serre.extSpaceAddEquiv {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {n : ℕ} {K : SmoothProperVariety.CanonicalSheafData k X n} (S : BilinearData K) (E F : Coh X) (i : ℕ) :
↑(S.extSpace E F i) ≃+ CategoryTheory.Abelian.Ext E F i

Convert the supplied additive-group isomorphism to an additive equivalence. Its scalar compatibility is separately supplied by GeometricSerreData.extComparison_scalar.

Equations
Instances For
    source
    noncomputable def AlgebraicGeometry.Duality.Serre.sheafComparison {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {n : ℕ} {K : SmoothProperVariety.CanonicalSheafData k X n} (S : BilinearData K) (T : CategoryTheory.Functor (DerivedCategory.SchemeBoundedCoherentDerivedCategory X) (DerivedCategory.SchemeBoundedCoherentDerivedCategory X)) (hscalar : ∀ (E F : Coh X) (j : ℕ) (r : k) (x : ↑(S.extSpace E F j)), (extSpaceAddEquiv S E F j) (r • x) = r • (extSpaceAddEquiv S E F j) x) (hTwist : (E : Coh X) → T.obj ((DerivedCategory.boundedSingleFunctor (Coh X)).obj E) ≅ (DerivedCategory.boundedSingleFunctor (Coh X)).obj (S.canonicalTwist E)) (eta : (A B' : DerivedCategory.SchemeBoundedCoherentDerivedCategory X) → Module.Dual k (A ⟶ B') ≃ₗ[k] B' ⟶ (T.comp (CategoryTheory.shiftFunctor (DerivedCategory.SchemeBoundedCoherentDerivedCategory X) ↑n)).obj A) (E F : Coh X) (i : ℕ) (hi : i ≤ n) :
    Module.Dual k ↑(S.extSpace E F i) ≃ₗ[k] ↑(S.extSpace F (S.canonicalTwist E) (n - i))

    Transport a derived Serre pairing into the realized Ext coordinates. Agreement with the sheaf duality pairing is the separate GeometricSerreData.compat field.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      structure AlgebraicGeometry.Duality.Serre.GeometricSerreData {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {n : ℕ} (K : SmoothProperVariety.CanonicalSheafData k X n) :
      Type (u + 2)

      Abstract Serre duality on the bounded coherent derived category, together with its geometric twist and sheaf-level comparison in degrees i ≤ n.

      No inhabitant is constructed here. The specified twist's Serre duality and bounded Hom-finiteness are derived from these fields below.

      Instances For
        source
        noncomputable def AlgebraicGeometry.Duality.Serre.GeometricSerreData.toSerreFunctorData {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {n : ℕ} {K : SmoothProperVariety.CanonicalSheafData k X n} (G : GeometricSerreData K) :
        CategoryTheory.SerreFunctor.SerreFunctorData k (DerivedCategory.SchemeBoundedCoherentDerivedCategory X)

        Transport the abstract Serre functor to the specified geometric twist.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def AlgebraicGeometry.Duality.Serre.GeometricSerreData.serreDuality {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {n : ℕ} {K : SmoothProperVariety.CanonicalSheafData k X n} (G : GeometricSerreData K) (A B : DerivedCategory.SchemeBoundedCoherentDerivedCategory X) :
          Module.Dual k (A ⟶ B) ≃ₗ[k] B ⟶ (G.canonicalTwistFunctor.comp (CategoryTheory.shiftFunctor (DerivedCategory.SchemeBoundedCoherentDerivedCategory X) ↑n)).obj A

          Derived Serre duality for the specified twist, obtained from G.serre.

          Equations
          Instances For
            source
            theorem AlgebraicGeometry.Duality.Serre.GeometricSerreData.finrank_eq_from_abstract {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {n : ℕ} {K : SmoothProperVariety.CanonicalSheafData k X n} (G : GeometricSerreData K) (E F : Coh X) (i : ℕ) (hi : i ≤ n) :
            Module.finrank k ↑(G.bilinear.extSpace E F i) = Module.finrank k ↑(G.bilinear.extSpace F (G.bilinear.canonicalTwist E) (n - i))

            Recover the sheaf-level finrank identity from the abstract Serre pairing and the explicit Ext, twist, and sheaf comparison maps. No global Hom-finiteness input is needed.

            source
            theorem AlgebraicGeometry.Duality.Serre.GeometricSerreData.hom_finite_bounded {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {n : ℕ} {K : SmoothProperVariety.CanonicalSheafData k X n} (G : GeometricSerreData K) :
            CategoryTheory.Triangulated.HomFiniteBounded k (DerivedCategory.SchemeBoundedCoherentDerivedCategory X)

            The sheaf Ext comparison and Serre duality bound the derived Hom support, so the bounded coherent derived category has finite-dimensional Hom spaces with finite shift support.

            source
            noncomputable def AlgebraicGeometry.Duality.Serre.GeometricSerreData.serreIsoShift {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {n : ℕ} {K : SmoothProperVariety.CanonicalSheafData k X n} (G : GeometricSerreData K) (hT : G.canonicalTwistFunctor ≅ CategoryTheory.Functor.id (DerivedCategory.SchemeBoundedCoherentDerivedCategory X)) :
            G.toSerreFunctorData.S ≅ CategoryTheory.shiftFunctor (DerivedCategory.SchemeBoundedCoherentDerivedCategory X) ↑n

            Whisker the twist trivialization by the dimension shift, then remove the identity functor with the left unitor. The sheaf-level AlgebraicGeometry.Duality.Serre.BilinearData.TrivialCanonical does not supply this natural isomorphism.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              noncomputable def AlgebraicGeometry.Duality.Serre.GeometricSerreData.selfHomShiftTwoDual {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {n : ℕ} {K : SmoothProperVariety.CanonicalSheafData k X n} (G : GeometricSerreData K) (hn : n = 2) (hT : G.canonicalTwistFunctor ≅ CategoryTheory.Functor.id (DerivedCategory.SchemeBoundedCoherentDerivedCategory X)) (E : DerivedCategory.SchemeBoundedCoherentDerivedCategory X) :
              (E ⟶ (CategoryTheory.shiftFunctor (DerivedCategory.SchemeBoundedCoherentDerivedCategory X) 2).obj E) ≃ₗ[k] Module.Dual k (E ⟶ E)

              Specialize the Serre pairing to an object paired with itself and transport along the twist trivialization. Reverse the resulting equivalence so that the degree-two self-Hom can be computed from the endomorphism space.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                theorem AlgebraicGeometry.Duality.Serre.GeometricSerreData.nonempty_hom_shift_two_linearEquiv_of_nonempty_end_linearEquiv {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {n : ℕ} {K : SmoothProperVariety.CanonicalSheafData k X n} (G : GeometricSerreData K) (hn : n = 2) (hT : G.canonicalTwistFunctor ≅ CategoryTheory.Functor.id (DerivedCategory.SchemeBoundedCoherentDerivedCategory X)) (E : DerivedCategory.SchemeBoundedCoherentDerivedCategory X) (hEnd : Nonempty ((E ⟶ E) ≃ₗ[k] k)) :
                Nonempty ((E ⟶ (CategoryTheory.shiftFunctor (DerivedCategory.SchemeBoundedCoherentDerivedCategory X) 2).obj E) ≃ₗ[k] k)

                Compose the degree-two Serre equivalence with the dual of the endomorphism equivalence and the self-duality of the base field. This supplies the degree-two clause of AlgebraicGeometry.K3Surface.SphericalExtProfile under a derived twist trivialization; the profile itself keeps its independent fields.

                source
                theorem AlgebraicGeometry.Duality.Serre.GeometricSerreData.chiHom_symm_of_trivialTwist {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {n : ℕ} {K : SmoothProperVariety.CanonicalSheafData k X n} (G : GeometricSerreData K) (hn : n = 2) (hT : G.canonicalTwistFunctor ≅ CategoryTheory.Functor.id (DerivedCategory.SchemeBoundedCoherentDerivedCategory X)) (A B : DerivedCategory.SchemeBoundedCoherentDerivedCategory X) :
                CategoryTheory.Triangulated.chiHom k (DerivedCategory.SchemeBoundedCoherentDerivedCategory X) A B = CategoryTheory.Triangulated.chiHom k (DerivedCategory.SchemeBoundedCoherentDerivedCategory X) B A

                In dimension two a naturally trivial derived canonical twist makes the Hom-built Euler form symmetric. Bounded Hom support comes from the supplied geometric data.

                source
                theorem AlgebraicGeometry.Duality.Serre.GeometricSerreData.chiHom_boundedSingleFunctor_obj_eq_eulerChar {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {n : ℕ} {K : SmoothProperVariety.CanonicalSheafData k X n} (G : GeometricSerreData K) (E F : Coh X) :
                CategoryTheory.Triangulated.chiHom k (DerivedCategory.SchemeBoundedCoherentDerivedCategory X) ((DerivedCategory.boundedSingleFunctor (Coh X)).obj E) ((DerivedCategory.boundedSingleFunctor (Coh X)).obj F) = G.bilinear.eulerChar E F

                The Hom-built Euler form on embedded coherent sheaves equals the sheaf-level Euler characteristic supplied by the bilinear data. The derived Serre pairing and the sheaf restriction kill shifts above the dimension.

                source
                theorem AlgebraicGeometry.Duality.Serre.GeometricSerreData.chiHom_self_eq_of_trivialCanonical {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {n : ℕ} {K : SmoothProperVariety.CanonicalSheafData k X n} (G : GeometricSerreData K) (hn : n = 2) (T : G.bilinear.TrivialCanonical) (E : Coh X) :
                CategoryTheory.Triangulated.chiHom k (DerivedCategory.SchemeBoundedCoherentDerivedCategory X) ((DerivedCategory.boundedSingleFunctor (Coh X)).obj E) ((DerivedCategory.boundedSingleFunctor (Coh X)).obj E) = 2 * ↑(Module.finrank k ↑(G.bilinear.extSpace E E 0)) - ↑(Module.finrank k ↑(G.bilinear.extSpace E E 1))

                Transfer the existing sheaf-level AlgebraicGeometry.Duality.Serre.BilinearData.surface_selfEuler_eq calculation to the Hom-built Euler form on the bounded derived category. The sheaf-level trivial-canonical datum suffices for this numerical statement.