Coherence for exact pullback on scheme-derived fibers

Exact pullback of module sheaves is closed under identity morphisms and composition. This file records those instances and lifts Mathlib's coherent identity and composition isomorphisms for module pullback to cochain complexes. Consequently the derived pullback functors from Families.ExactPullback are available for identities and composites without additional exactness hypotheses.

This is still a deliberately strict boundary: no identity or composition isomorphism is asserted after localization to derived categories, no pseudofunctor coherence is proved there, and exactness is not deduced from flatness. Those constructions belong to later milestones.

instance AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.isExactPullbackId {S : Scheme} (T : SchemeBaseChange S) : IsExactPullback (CategoryTheory.CategoryStruct.id T)

Pullback along an identity morphism is exact.

instance AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.isExactPullbackComp {S : Scheme} {T U V : SchemeBaseChange S} (f : T ⟶ U) (g : U ⟶ V) [IsExactPullback f] [IsExactPullback g] : IsExactPullback (CategoryTheory.CategoryStruct.comp f g)

A composite of exact pullbacks is exact.

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.complexPullbackId {S : Scheme} (T : SchemeBaseChange S) : complexPullback (CategoryTheory.CategoryStruct.id T) ≅ CategoryTheory.Functor.id (CochainComplex (CategoryTheory.Over.left T).Modules ℤ)

Degreewise pullback along an identity is naturally isomorphic to the identity functor on cochain complexes.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.complexPullbackComp {S : Scheme} {T U V : SchemeBaseChange S} (f : T ⟶ U) (g : U ⟶ V) : (complexPullback g).comp (complexPullback f) ≅ complexPullback (CategoryTheory.CategoryStruct.comp f g)

Degreewise pullback along a composite is naturally isomorphic to the composite of the two degreewise pullbacks.

Equations

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

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.identityDerivedPullback {S : Scheme} (T : SchemeBaseChange S) : CategoryTheory.Functor T.DerivedFiber T.DerivedFiber

The derived pullback functor attached to an identity morphism.

Equations

• T.identityDerivedPullback = AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.derivedPullback (CategoryTheory.CategoryStruct.id T)

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.compositeDerivedPullback {S : Scheme} {T U V : SchemeBaseChange S} (f : T ⟶ U) (g : U ⟶ V) [IsExactPullback f] [IsExactPullback g] : CategoryTheory.Functor V.DerivedFiber T.DerivedFiber

The derived pullback functor attached to a composite of exact pullbacks.

Equations

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