Functorial resolutions for arbitrary derived pullback

This file isolates the concrete resolution data sufficient to construct left-derived pullback along a scheme morphism. A PullbackAcyclicResolution f consists of a functorial replacement of every complex, a componentwise quasi-isomorphism from the replacement to the original complex, and a proof that pullback followed by localization inverts quasi-isomorphisms between the replacements.

The resulting functor on the derived categories is constructed by the universal property of localization. The comparison with ordinary pullback is then proved to have Mathlib's left-derived universal property; it is not stored as an additional assumption.

K-flat resolutions are intended to provide the main geometric inhabitants of this interface. Keeping the condition in terms of the exact functor that must invert quasi-isomorphisms also permits narrower supported constructions.

structure AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.PullbackAcyclicResolution {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) : Type (u + 1)

A functorial resolution on which pullback along f preserves quasi-isomorphisms.

The comparison points from the resolution to the original complex, as for a K-flat replacement. The last field is the operational acyclicity condition: after resolving, ordinary pullback descends through the source derived localization.

• resolution : CategoryTheory.Functor (CochainComplex (CategoryTheory.Over.left U).Modules ℤ) (CochainComplex (CategoryTheory.Over.left U).Modules ℤ)

  Functorial replacement of complexes on the source of pullback.

• comparison : self.resolution ⟶ CategoryTheory.Functor.id (CochainComplex (CategoryTheory.Over.left U).Modules ℤ)

  Comparison from the replacement to the original complex.

• comparison_quasiIso (K : CochainComplex (CategoryTheory.Over.left U).Modules ℤ) : HomologicalComplex.quasiIso (CategoryTheory.Over.left U).Modules (ComplexShape.up ℤ) (self.comparison.app K)

  Every comparison component is a quasi-isomorphism.

• pullback_inverts : (HomologicalComplex.quasiIso (CategoryTheory.Over.left U).Modules (ComplexShape.up ℤ)).IsInvertedBy (self.resolution.comp ((complexPullback f).comp (SchemeDerivedCategory.Q (CategoryTheory.Over.left T))))

  Pullback of resolved complexes sends every quasi-isomorphism to an isomorphism after localization on the target scheme.

• resolved_comparison_isIso (K : CochainComplex (CategoryTheory.Over.left U).Modules ℤ) : CategoryTheory.IsIso (((complexPullback f).comp (SchemeDerivedCategory.Q (CategoryTheory.Over.left T))).map (self.comparison.app (self.resolution.obj K)))

  Pulling back the comparison of an already resolved complex gives an isomorphism after target localization. This is the idempotence condition on the acyclic replacement that makes the comparison universal.

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

For exact pullback, the identity functor on complexes is already a pullback-acyclic resolution. This is the normalization case against which genuinely derived resolutions can be compared.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.PullbackAcyclicResolution.derivedFunctor {S : Scheme} {T U : SchemeBaseChange S} {f : T ⟶ U} (R : PullbackAcyclicResolution f) : CategoryTheory.Functor U.DerivedFiber T.DerivedFiber

The functor on derived categories obtained by resolving, pulling back, and using the universal property of localization.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.PullbackAcyclicResolution.derivedFactors {S : Scheme} {T U : SchemeBaseChange S} {f : T ⟶ U} (R : PullbackAcyclicResolution f) : (SchemeDerivedCategory.Q (CategoryTheory.Over.left U)).comp R.derivedFunctor ≅ R.resolution.comp ((complexPullback f).comp (SchemeDerivedCategory.Q (CategoryTheory.Over.left T)))

The localization factorization for resolved pullback.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.PullbackAcyclicResolution.localizationComparison {S : Scheme} {T U : SchemeBaseChange S} {f : T ⟶ U} (R : PullbackAcyclicResolution f) : R.resolution.comp (SchemeDerivedCategory.Q (CategoryTheory.Over.left U)) ≅ SchemeDerivedCategory.Q (CategoryTheory.Over.left U)

A resolution becomes naturally isomorphic to the identity after source localization.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.PullbackAcyclicResolution.counit {S : Scheme} {T U : SchemeBaseChange S} {f : T ⟶ U} (R : PullbackAcyclicResolution f) : (SchemeDerivedCategory.Q (CategoryTheory.Over.left U)).comp R.derivedFunctor ⟶ (complexPullback f).comp (SchemeDerivedCategory.Q (CategoryTheory.Over.left T))

The comparison from resolved derived pullback to ordinary pullback.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.PullbackAcyclicResolution.outerComparisonIso {S : Scheme} {T U : SchemeBaseChange S} {f : T ⟶ U} (R : PullbackAcyclicResolution f) : R.resolution.comp (R.resolution.comp (AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.PullbackAcyclicResolution.ordinaryPullback✝ f)) ≅ R.resolution.comp (AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.PullbackAcyclicResolution.ordinaryPullback✝ f)

The two ways of comparing a double resolution with a single resolution: first compare the outer resolution.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.PullbackAcyclicResolution.innerComparisonIso {S : Scheme} {T U : SchemeBaseChange S} {f : T ⟶ U} (R : PullbackAcyclicResolution f) : R.resolution.comp (R.resolution.comp (AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.PullbackAcyclicResolution.ordinaryPullback✝ f)) ≅ R.resolution.comp (AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.PullbackAcyclicResolution.ordinaryPullback✝ f)

The two ways of comparing a double resolution with a single resolution: first map the inner comparison through the outer resolution.

Equations

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

instance AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.PullbackAcyclicResolution.counit_app_resolution_isIso {S : Scheme} {T U : SchemeBaseChange S} {f : T ⟶ U} (R : PullbackAcyclicResolution f) (K : CochainComplex (CategoryTheory.Over.left U).Modules ℤ) : CategoryTheory.IsIso (R.counit.app (R.resolution.obj K))

The comparison defining resolved derived pullback is invertible on an already resolved complex.

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.PullbackAcyclicResolution.whiskeredLift {S : Scheme} {T U : SchemeBaseChange S} {f : T ⟶ U} (R : PullbackAcyclicResolution f) (G : CategoryTheory.Functor U.DerivedFiber T.DerivedFiber) (β : (SchemeDerivedCategory.Q (CategoryTheory.Over.left U)).comp G ⟶ AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.PullbackAcyclicResolution.ordinaryPullback✝ f) : (SchemeDerivedCategory.Q (CategoryTheory.Over.left U)).comp G ⟶ (SchemeDerivedCategory.Q (CategoryTheory.Over.left U)).comp R.derivedFunctor

The lift before descending it through source localization. Its middle two factors compare the two canonical maps from a double resolution to a single resolution.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.PullbackAcyclicResolution.lift {S : Scheme} {T U : SchemeBaseChange S} {f : T ⟶ U} (R : PullbackAcyclicResolution f) (G : CategoryTheory.Functor U.DerivedFiber T.DerivedFiber) (β : (SchemeDerivedCategory.Q (CategoryTheory.Over.left U)).comp G ⟶ AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.PullbackAcyclicResolution.ordinaryPullback✝ f) : G ⟶ R.derivedFunctor

The universal lift induced by a pullback-acyclic resolution.

Equations

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

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.PullbackAcyclicResolution.whiskerLeft_lift {S : Scheme} {T U : SchemeBaseChange S} {f : T ⟶ U} (R : PullbackAcyclicResolution f) (G : CategoryTheory.Functor U.DerivedFiber T.DerivedFiber) (β : (SchemeDerivedCategory.Q (CategoryTheory.Over.left U)).comp G ⟶ AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.PullbackAcyclicResolution.ordinaryPullback✝ f) : (SchemeDerivedCategory.Q (CategoryTheory.Over.left U)).whiskerLeft (R.lift G β) = R.whiskeredLift G β

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.PullbackAcyclicResolution.whiskerLeft_lift_assoc {S : Scheme} {T U : SchemeBaseChange S} {f : T ⟶ U} (R : PullbackAcyclicResolution f) (G : CategoryTheory.Functor U.DerivedFiber T.DerivedFiber) (β : (SchemeDerivedCategory.Q (CategoryTheory.Over.left U)).comp G ⟶ AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.PullbackAcyclicResolution.ordinaryPullback✝ f) {Z : CategoryTheory.Functor (CochainComplex (CategoryTheory.Over.left U).Modules ℤ) T.DerivedFiber} (h : (SchemeDerivedCategory.Q (CategoryTheory.Over.left U)).comp R.derivedFunctor ⟶ Z) : CategoryTheory.CategoryStruct.comp ((SchemeDerivedCategory.Q (CategoryTheory.Over.left U)).whiskerLeft (R.lift G β)) h = CategoryTheory.CategoryStruct.comp (R.whiskeredLift G β) h

@[simp]

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.PullbackAcyclicResolution.whiskeredLift_fac {S : Scheme} {T U : SchemeBaseChange S} {f : T ⟶ U} (R : PullbackAcyclicResolution f) (G : CategoryTheory.Functor U.DerivedFiber T.DerivedFiber) (β : (SchemeDerivedCategory.Q (CategoryTheory.Over.left U)).comp G ⟶ AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.PullbackAcyclicResolution.ordinaryPullback✝ f) : CategoryTheory.CategoryStruct.comp (R.whiskeredLift G β) R.counit = β

@[simp]

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.PullbackAcyclicResolution.whiskeredLift_fac_assoc {S : Scheme} {T U : SchemeBaseChange S} {f : T ⟶ U} (R : PullbackAcyclicResolution f) (G : CategoryTheory.Functor U.DerivedFiber T.DerivedFiber) (β : (SchemeDerivedCategory.Q (CategoryTheory.Over.left U)).comp G ⟶ AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.PullbackAcyclicResolution.ordinaryPullback✝ 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 (R.whiskeredLift G β) (CategoryTheory.CategoryStruct.comp R.counit h) = CategoryTheory.CategoryStruct.comp β h

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.PullbackAcyclicResolution.lift_fac {S : Scheme} {T U : SchemeBaseChange S} {f : T ⟶ U} (R : PullbackAcyclicResolution f) (G : CategoryTheory.Functor U.DerivedFiber T.DerivedFiber) (β : (SchemeDerivedCategory.Q (CategoryTheory.Over.left U)).comp G ⟶ AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.PullbackAcyclicResolution.ordinaryPullback✝ f) : CategoryTheory.CategoryStruct.comp ((SchemeDerivedCategory.Q (CategoryTheory.Over.left U)).whiskerLeft (R.lift G β)) R.counit = β

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.PullbackAcyclicResolution.lift_fac_assoc {S : Scheme} {T U : SchemeBaseChange S} {f : T ⟶ U} (R : PullbackAcyclicResolution f) (G : CategoryTheory.Functor U.DerivedFiber T.DerivedFiber) (β : (SchemeDerivedCategory.Q (CategoryTheory.Over.left U)).comp G ⟶ AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.PullbackAcyclicResolution.ordinaryPullback✝ 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 (R.lift G β)) (CategoryTheory.CategoryStruct.comp R.counit h) = CategoryTheory.CategoryStruct.comp β h

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.PullbackAcyclicResolution.counit_hom_ext {S : Scheme} {T U : SchemeBaseChange S} {f : T ⟶ U} (R : PullbackAcyclicResolution f) (G : CategoryTheory.Functor U.DerivedFiber T.DerivedFiber) (γ₁ γ₂ : G ⟶ R.derivedFunctor) (hγ : CategoryTheory.CategoryStruct.comp ((SchemeDerivedCategory.Q (CategoryTheory.Over.left U)).whiskerLeft γ₁) R.counit = CategoryTheory.CategoryStruct.comp ((SchemeDerivedCategory.Q (CategoryTheory.Over.left U)).whiskerLeft γ₂) R.counit) : γ₁ = γ₂

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.PullbackAcyclicResolution.isLeftDerived {S : Scheme} {T U : SchemeBaseChange S} {f : T ⟶ U} (R : PullbackAcyclicResolution f) : R.derivedFunctor.IsLeftDerivedFunctor R.counit (HomologicalComplex.quasiIso (CategoryTheory.Over.left U).Modules (ComplexShape.up ℤ))

A pullback-acyclic resolution constructs the genuine left-derived pullback universal property.

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.PullbackAcyclicResolution.toLeftDerivedPullback {S : Scheme} {T U : SchemeBaseChange S} {f : T ⟶ U} (R : PullbackAcyclicResolution f) : LeftDerivedPullback f

Package a functorial pullback-acyclic resolution as the arbitrary left-derived pullback interface used by the relative-perfect moduli theory.

Equations

• R.toLeftDerivedPullback = { functor := R.derivedFunctor, counit := R.counit, isLeftDerived := ⋯ }

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.PullbackAcyclicResolution.exactComparison {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsExactPullback f] : (ofExact f).derivedFunctor ≅ derivedPullback f

The functor obtained from the identity resolution for exact pullback is canonically isomorphic to Mathlib's exact derived functor.

Equations

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

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.PullbackAcyclicResolution.exactComparison_hom_counit {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsExactPullback f] : CategoryTheory.CategoryStruct.comp ((SchemeDerivedCategory.Q (CategoryTheory.Over.left U)).whiskerLeft (exactComparison f).hom) (derivedPullbackFactors f).hom = (ofExact f).counit

The exact comparison intertwines the two transformations to ordinary degreewise pullback.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.PullbackAcyclicResolution.exactComparison_hom_counit_assoc {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsExactPullback 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 (exactComparison f).hom) (CategoryTheory.CategoryStruct.comp (derivedPullbackFactors f).hom h) = CategoryTheory.CategoryStruct.comp (ofExact f).counit h

The exact comparison intertwines the two transformations to ordinary degreewise pullback.