Documentation

DerivedAlgGeo.AlgebraicGeometry.DerivedCategory.Families.FlatPullbackResolution

The identity resolution for flat pullback #

Flat morphisms have exact pullback on module sheaves, so their derived pullback needs no nontrivial replacement: the identity functor on complexes is a pullback-acyclic resolution. This file connects the geometric flatness theorem with the resolution-based arbitrary derived-pullback construction.

The resulting functor is canonically isomorphic to the existing exact derived pullback. This supplies a normalization test for later K-flat resolutions along genuinely non-flat morphisms.

source
noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.PullbackAcyclicResolution.ofFlat {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [Flat (CategoryTheory.Over.Hom.left f)] :
PullbackAcyclicResolution f

A flat scheme morphism has the identity pullback-acyclic resolution.

Equations
Instances For
    source
    noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.PullbackAcyclicResolution.flatComparison {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [Flat (CategoryTheory.Over.Hom.left f)] :
    (ofFlat f).derivedFunctor ≅ derivedPullback f

    Resolution-derived pullback along a flat morphism agrees canonically with exact derived pullback.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.PullbackAcyclicResolution.flatComparison_hom_counit {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [Flat (CategoryTheory.Over.Hom.left f)] :
      CategoryTheory.CategoryStruct.comp ((SchemeDerivedCategory.Q (CategoryTheory.Over.left U)).whiskerLeft (flatComparison f).hom) (derivedPullbackFactors f).hom = (ofFlat f).counit

      The flat comparison respects the displayed transformations to ordinary degreewise pullback.

      source
      theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.PullbackAcyclicResolution.flatComparison_hom_counit_assoc {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [Flat (CategoryTheory.Over.Hom.left f)] {Z : CategoryTheory.Functor (CochainComplex (CategoryTheory.Over.left U).Modules ℤ) T.DerivedFiber} (h : (complexPullback f).comp (SchemeDerivedCategory.Q (CategoryTheory.Over.left T)) ⟶ Z) :
      CategoryTheory.CategoryStruct.comp ((SchemeDerivedCategory.Q (CategoryTheory.Over.left U)).whiskerLeft (flatComparison f).hom) (CategoryTheory.CategoryStruct.comp (derivedPullbackFactors f).hom h) = CategoryTheory.CategoryStruct.comp (ofFlat f).counit h

      The flat comparison respects the displayed transformations to ordinary degreewise pullback.