Pseudofunctor laws for exact derived pullback

The complex-level pullback unit and associativity laws are inherited degreewise from Mathlib's module-sheaf pullback pseudofunctor. Localization then transports those laws to exact pullback on the concrete derived fibers. Equality congruence is lifted through the same localization so the laws have canonical, typed right-hand sides even when composition is only propositionally equal.

This file proves the left-unit, right-unit, and associativity (pentagon) laws for the exact derived pullback compositor. It does not yet prove compatibility of these isomorphisms with the triangulated shift, characterize exact pullback by a geometric flatness criterion, or construct nonexact left-derived pullback.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.complexPullback_associativity {S : Scheme} {T U V W : SchemeBaseChange S} (f : T ⟶ U) (g : U ⟶ V) (h : V ⟶ W) : CategoryTheory.CategoryStruct.comp (complexPullbackComp f (CategoryTheory.CategoryStruct.comp g h)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (complexPullbackComp g h).inv (complexPullback f)) (CategoryTheory.CategoryStruct.comp ((complexPullback h).associator (complexPullback g) (complexPullback f)).hom (CategoryTheory.CategoryStruct.comp ((complexPullback h).whiskerLeft (complexPullbackComp f g).hom) (complexPullbackComp (CategoryTheory.CategoryStruct.comp f g) h).hom))) = CategoryTheory.eqToHom ⋯

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.complexPullback_associativity_assoc {S : Scheme} {T U V W : SchemeBaseChange S} (f : T ⟶ U) (g : U ⟶ V) (h : V ⟶ W) {Z : CategoryTheory.Functor (CochainComplex (CategoryTheory.Over.left W).Modules ℤ) (CochainComplex (CategoryTheory.Over.left T).Modules ℤ)} (h✝ : complexPullback (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h) ⟶ Z) : CategoryTheory.CategoryStruct.comp (complexPullbackComp f (CategoryTheory.CategoryStruct.comp g h)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (complexPullbackComp g h).inv (complexPullback f)) (CategoryTheory.CategoryStruct.comp ((complexPullback h).associator (complexPullback g) (complexPullback f)).hom (CategoryTheory.CategoryStruct.comp ((complexPullback h).whiskerLeft (complexPullbackComp f g).hom) (CategoryTheory.CategoryStruct.comp (complexPullbackComp (CategoryTheory.CategoryStruct.comp f g) h).hom h✝)))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h✝

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.complexPullback_left_unitality {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) : CategoryTheory.CategoryStruct.comp (complexPullbackComp f (CategoryTheory.CategoryStruct.id U)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight U.complexPullbackId.hom (complexPullback f)) (complexPullback f).leftUnitor.hom) = CategoryTheory.eqToHom ⋯

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.complexPullback_left_unitality_assoc {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) {Z : CategoryTheory.Functor (CochainComplex (CategoryTheory.Over.left U).Modules ℤ) (CochainComplex (CategoryTheory.Over.left T).Modules ℤ)} (h : complexPullback f ⟶ Z) : CategoryTheory.CategoryStruct.comp (complexPullbackComp f (CategoryTheory.CategoryStruct.id U)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight U.complexPullbackId.hom (complexPullback f)) (CategoryTheory.CategoryStruct.comp (complexPullback f).leftUnitor.hom h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.complexPullback_right_unitality {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) : CategoryTheory.CategoryStruct.comp (complexPullbackComp (CategoryTheory.CategoryStruct.id T) f).inv (CategoryTheory.CategoryStruct.comp ((complexPullback f).whiskerLeft T.complexPullbackId.hom) (complexPullback f).rightUnitor.hom) = CategoryTheory.eqToHom ⋯

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.complexPullback_right_unitality_assoc {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) {Z : CategoryTheory.Functor (CochainComplex (CategoryTheory.Over.left U).Modules ℤ) (CochainComplex (CategoryTheory.Over.left T).Modules ℤ)} (h : complexPullback f ⟶ Z) : CategoryTheory.CategoryStruct.comp (complexPullbackComp (CategoryTheory.CategoryStruct.id T) f).inv (CategoryTheory.CategoryStruct.comp ((complexPullback f).whiskerLeft T.complexPullbackId.hom) (CategoryTheory.CategoryStruct.comp (complexPullback f).rightUnitor.hom h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.complexPullbackCongr {S : Scheme} {T U : SchemeBaseChange S} {f g : T ⟶ U} (h : f = g) : complexPullback f ≅ complexPullback g

Equality of scheme base-change morphisms induces a canonical isomorphism between their pullback functors on cochain complexes.

Equations

• AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.complexPullbackCongr h = h ▸ CategoryTheory.Iso.refl (AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.complexPullback f)

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.derivedPullbackCongr {S : Scheme} {T U : SchemeBaseChange S} {f g : T ⟶ U} [IsExactPullback f] [IsExactPullback g] (h : f = g) : derivedPullback f ≅ derivedPullback g

Equality of exact scheme base-change morphisms induces a canonical isomorphism between their derived pullback functors.

Equations

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

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.derivedPullback_left_unitality {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsExactPullback f] : CategoryTheory.CategoryStruct.comp (derivedPullbackComp f (CategoryTheory.CategoryStruct.id U)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight U.derivedPullbackId.hom (derivedPullback f)) (derivedPullback f).leftUnitor.hom) = (derivedPullbackCongr ⋯).hom

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.derivedPullback_left_unitality_assoc {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsExactPullback f] {Z : CategoryTheory.Functor U.DerivedFiber T.DerivedFiber} (h : derivedPullback f ⟶ Z) : CategoryTheory.CategoryStruct.comp (derivedPullbackComp f (CategoryTheory.CategoryStruct.id U)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight U.derivedPullbackId.hom (derivedPullback f)) (CategoryTheory.CategoryStruct.comp (derivedPullback f).leftUnitor.hom h)) = CategoryTheory.CategoryStruct.comp (derivedPullbackCongr ⋯).hom h

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.derivedPullback_right_unitality {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsExactPullback f] : CategoryTheory.CategoryStruct.comp (derivedPullbackComp (CategoryTheory.CategoryStruct.id T) f).inv (CategoryTheory.CategoryStruct.comp ((derivedPullback f).whiskerLeft T.derivedPullbackId.hom) (derivedPullback f).rightUnitor.hom) = (derivedPullbackCongr ⋯).hom

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.derivedPullback_right_unitality_assoc {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsExactPullback f] {Z : CategoryTheory.Functor U.DerivedFiber T.DerivedFiber} (h : derivedPullback f ⟶ Z) : CategoryTheory.CategoryStruct.comp (derivedPullbackComp (CategoryTheory.CategoryStruct.id T) f).inv (CategoryTheory.CategoryStruct.comp ((derivedPullback f).whiskerLeft T.derivedPullbackId.hom) (CategoryTheory.CategoryStruct.comp (derivedPullback f).rightUnitor.hom h)) = CategoryTheory.CategoryStruct.comp (derivedPullbackCongr ⋯).hom h

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.derivedPullback_associativity {S : Scheme} {T U V W : SchemeBaseChange S} (f : T ⟶ U) (g : U ⟶ V) (h : V ⟶ W) [IsExactPullback f] [IsExactPullback g] [IsExactPullback h] : CategoryTheory.CategoryStruct.comp (derivedPullbackComp f (CategoryTheory.CategoryStruct.comp g h)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (derivedPullbackComp g h).inv (derivedPullback f)) (CategoryTheory.CategoryStruct.comp ((derivedPullback h).associator (derivedPullback g) (derivedPullback f)).hom (CategoryTheory.CategoryStruct.comp ((derivedPullback h).whiskerLeft (derivedPullbackComp f g).hom) (derivedPullbackComp (CategoryTheory.CategoryStruct.comp f g) h).hom))) = (derivedPullbackCongr ⋯).hom

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.derivedPullback_associativity_assoc {S : Scheme} {T U V W : SchemeBaseChange S} (f : T ⟶ U) (g : U ⟶ V) (h : V ⟶ W) [IsExactPullback f] [IsExactPullback g] [IsExactPullback h] {Z : CategoryTheory.Functor W.DerivedFiber T.DerivedFiber} (h✝ : derivedPullback (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h) ⟶ Z) : CategoryTheory.CategoryStruct.comp (derivedPullbackComp f (CategoryTheory.CategoryStruct.comp g h)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (derivedPullbackComp g h).inv (derivedPullback f)) (CategoryTheory.CategoryStruct.comp ((derivedPullback h).associator (derivedPullback g) (derivedPullback f)).hom (CategoryTheory.CategoryStruct.comp ((derivedPullback h).whiskerLeft (derivedPullbackComp f g).hom) (CategoryTheory.CategoryStruct.comp (derivedPullbackComp (CategoryTheory.CategoryStruct.comp f g) h).hom h✝)))) = CategoryTheory.CategoryStruct.comp (derivedPullbackCongr ⋯).hom h✝