Pullback of universally-gluable relative-perfect complexes

This file records the first object-level base-change layer for the relative-perfect moduli problem. A RelativePerfectPullback is not a proposition asserting preservation: it contains an actual left-derived pullback, the actual functor between the full categories of universally gluable relative-perfect complexes, and a natural isomorphism identifying the underlying functors.

The identity and composite constructions make these witnesses reusable in a future pseudofunctor on the big Zariski site. The arbitrary pullback field has Mathlib's left-derived universal property, so a K-flat construction can inhabit it without changing this API. This file does not yet construct those K-flat resolutions or prove preservation along every scheme morphism.

Main definitions

• RelativePerfectPullback: an actual lift of left-derived pullback to the universally-gluable relative-perfect loci.
• RelativePerfectPullback.identity: the canonical identity lift.
• RelativePerfectPullback.comp: composition relative to an actual ambient compositor.
• RelativePerfectPullback.compExact: the canonical exact composite.
• RelativePerfectPullback.congr: transport along equality of base-change morphisms.

Implementation notes

The ambient left-derived pullback is stored with the lift. The comparison is oriented from the lifted functor to ambient derived pullback so composition follows the contravariant order of scheme pullback.

noncomputable def AlgebraicGeometry.relativePerfectForget {S : Scheme} (T : DerivedCategory.Families.SchemeBaseChange S) : CategoryTheory.Functor (SchemeUniversallyGluableCategory (CategoryTheory.Over.hom T)) T.DerivedFiber

Forget a universally-gluable relative-perfect object to the ambient scheme-derived category.

Equations

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

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

An actual lift of left-derived pullback to universally-gluable relative-perfect complexes.

The functor is the preservation theorem: its codomain ensures that every pulled-back object remains pseudo-coherent, of finite Tor amplitude, and universally gluable. comparison prevents an unrelated functor from being presented as geometric pullback.

• ambient : DerivedCategory.Families.SchemeBaseChange.LeftDerivedPullback f

  The actual ambient left-derived pullback and its universal property.

• functor : CategoryTheory.Functor (SchemeUniversallyGluableCategory (CategoryTheory.Over.hom U)) (SchemeUniversallyGluableCategory (CategoryTheory.Over.hom T))

  Pullback on the actual universally-gluable relative-perfect loci.

• comparison : self.functor.comp (relativePerfectForget T) ≅ (relativePerfectForget U).comp self.ambient.functor

  Forgetting the lifted functor agrees naturally with ambient derived pullback.

noncomputable def AlgebraicGeometry.RelativePerfectPullback.identity {S : Scheme} (T : DerivedCategory.Families.SchemeBaseChange S) : RelativePerfectPullback (CategoryTheory.CategoryStruct.id T)

The identity base change has the canonical relative-perfect pullback. The underlying functor is the identity on the full relative-perfect locus; the comparison uses the proved unit isomorphism for derived pullback.

Equations

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

noncomputable def AlgebraicGeometry.RelativePerfectPullback.comp {S : Scheme} {T U V : DerivedCategory.Families.SchemeBaseChange S} {f : T ⟶ U} {g : U ⟶ V} (hf : RelativePerfectPullback f) (hg : RelativePerfectPullback g) (hfg : DerivedCategory.Families.SchemeBaseChange.LeftDerivedPullback (CategoryTheory.CategoryStruct.comp f g)) (ambientComp : hg.ambient.functor.comp hf.ambient.functor ≅ hfg.functor) : RelativePerfectPullback (CategoryTheory.CategoryStruct.comp f g)

Compose relative-perfect pullbacks in the contravariant order dictated by scheme pullback. For f : T ⟶ U and g : U ⟶ V, objects over V are first pulled back along g and then along f.

Equations

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

noncomputable def AlgebraicGeometry.RelativePerfectPullback.compExact {S : Scheme} {T U V : DerivedCategory.Families.SchemeBaseChange S} {f : T ⟶ U} {g : U ⟶ V} [DerivedCategory.Families.SchemeBaseChange.IsExactPullback f] [DerivedCategory.Families.SchemeBaseChange.IsExactPullback g] (hf : RelativePerfectPullback f) (hg : RelativePerfectPullback g) : RelativePerfectPullback (CategoryTheory.CategoryStruct.comp f g)

Compose two relative-perfect pullbacks when both ordinary pullbacks are exact. Uniqueness of left-derived functors compares their stored ambient functors with the repository's exact derived pullbacks.

Equations

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

def AlgebraicGeometry.RelativePerfectPullback.congr {S : Scheme} {T U : DerivedCategory.Families.SchemeBaseChange S} {f g : T ⟶ U} (P : RelativePerfectPullback f) (h : f = g) : RelativePerfectPullback g

Transport a relative-perfect pullback lift along equality of the underlying scheme base-change morphisms.

Equations

• P.congr h = h ▸ P