Documentation

DerivedAlgGeo.AlgebraicGeometry.DerivedCategory.Families.ExactPullbackDqc

Quasi-coherent cohomology under exact scheme pullback #

An exact pullback commutes with cohomology. Ordinary pullback preserves quasi-coherent module sheaves along every scheme morphism, so the exact derived pullback preserves the quasi-coherent-cohomology locus. Flat pullback is an unconditional geometric specialization because flatness supplies exactness.

This proves the exact and flat cases of the derived preservation obligation. Arbitrary nonexact pullback still needs a derived comparison; its cohomology need not be the ordinary pullback of the source cohomology sheaf.

Main definitions #

Main results #

Implementation notes #

The generic exact-functor homology isomorphism compares target cohomology to ordinary pullback of source cohomology. The scheme-module theorem supplies quasi-coherence of the latter, and isomorphism closure supplies the former.

References #

The exact homology comparison is in the repository's Algebra/Homology/DerivedCategory/Homology.lean; ordinary quasi-coherent pullback is in AlgebraicGeometry/Modules/Quasicoherent/Pullback.lean.

Tags #

derived pullback, quasi-coherent cohomology, exact pullback, flat pullback

source
theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.derivedPullback_preservesQuasicoherentCohomology {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsExactPullback f] (E : Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left U)) :
Dqc.schemeQuasicoherentCohomology (CategoryTheory.Over.left T) ((derivedPullback f).obj E.obj)

Exact derived pullback preserves quasi-coherent cohomology. The exact homology comparison reduces this to ordinary quasi-coherent pullback.

source
noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.exactDqcLeftDerivedPullback {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsExactPullback f] :
DqcLeftDerivedPullback f

The proof-backed quasi-coherent left-derived pullback in the exact case.

Equations
Instances For
    source
    noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.flatDqcLeftDerivedPullback {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [Flat (CategoryTheory.Over.Hom.left f)] :
    DqcLeftDerivedPullback f

    Flat pullback preserves quasi-coherent cohomology without a caller-supplied exactness or preservation witness.

    Equations
    Instances For