Derived coherence for exact scheme pullback

The identity and composition isomorphisms for exact pullback descend through the derived-category localization. This supplies the unit and composition isomorphisms for the contravariant assignment sending a scheme base change to its derived category of module sheaves.

This file does not yet prove the triangle and pentagon coherence equations for those isomorphisms, characterize exactness geometrically, construct a left-derived functor for nonexact pullback, or restrict the construction to bounded coherent or perfect complexes.

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.complexPullbackIdLocalized {S : Scheme} (T : SchemeBaseChange S) : (complexPullback (CategoryTheory.CategoryStruct.id T)).comp (SchemeDerivedCategory.Q (CategoryTheory.Over.left T)) ≅ SchemeDerivedCategory.Q (CategoryTheory.Over.left T)

The complex-level identity isomorphism, followed by localization.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.derivedPullbackId {S : Scheme} (T : SchemeBaseChange S) : derivedPullback (CategoryTheory.CategoryStruct.id T) ≅ CategoryTheory.Functor.id T.DerivedFiber

Exact derived pullback along an identity is naturally isomorphic to the identity functor.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.complexPullbackCompLocalized {S : Scheme} {T U V : SchemeBaseChange S} (f : T ⟶ U) (g : U ⟶ V) [IsExactPullback f] : ((complexPullback g).comp (SchemeDerivedCategory.Q (CategoryTheory.Over.left U))).comp (derivedPullback f) ≅ (complexPullback (CategoryTheory.CategoryStruct.comp f g)).comp (SchemeDerivedCategory.Q (CategoryTheory.Over.left T))

The complex-level composition isomorphism, followed by localization.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.derivedPullbackComp {S : Scheme} {T U V : SchemeBaseChange S} (f : T ⟶ U) (g : U ⟶ V) [IsExactPullback f] [IsExactPullback g] : (derivedPullback g).comp (derivedPullback f) ≅ derivedPullback (CategoryTheory.CategoryStruct.comp f g)

The composite of two exact derived pullbacks is naturally isomorphic to derived pullback along the composite scheme morphism.

Equations

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

@[simp]

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.derivedPullK₀_id {S : Scheme} (T : SchemeBaseChange S) : derivedPullK₀ (CategoryTheory.CategoryStruct.id T) = AddMonoidHom.id (CategoryTheory.Triangulated.K₀ T.DerivedFiber)

@[simp]

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.derivedPullK₀_comp {S : Scheme} {T U V : SchemeBaseChange S} (f : T ⟶ U) (g : U ⟶ V) [IsExactPullback f] [IsExactPullback g] : derivedPullK₀ (CategoryTheory.CategoryStruct.comp f g) = (derivedPullK₀ f).comp (derivedPullK₀ g)