The relative-perfect presheaf on the big Zariski site over a base

This file places the universally-gluable relative-perfect moduli problem on the correctly oriented site Over S with the topology Scheme.zariskiTopology.over S. Its transition data uses actual left-derived pullback and an actual lift to the universally-gluable relative-perfect loci.

RelativePerfectBigZariskiStack adds Mathlib's effective descent condition. It is intentionally a structure rather than a theorem: constructing its isStack field requires effective descent for the complexes and their isomorphisms. Once supplied, the existing stack infrastructure immediately gives fully faithful morphism descent and effective object descent for every big-Zariski covering family.

Main definitions

• RelativePerfectBigZariskiPresheaf: the concrete relative-perfect pseudofunctor on Over S.
• RelativePerfectBigZariskiStack: the same pseudofunctor with effective big-Zariski descent.
• RelativePerfectBigZariskiStack.cechDescentEquivalence: the resulting equivalence with Čech descent data.

structure AlgebraicGeometry.RelativePerfectBigZariskiPresheaf (S : Scheme) : Type (u + 2)

The universally-gluable relative-perfect moduli presheaf on the big Zariski site of schemes over S.

Every transition contains an actual left-derived pullback and an actual lift to the relative-perfect locus. The final comparison identifies that lifted pullback with the pseudofunctor transition.

• presheaf : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete (DerivedCategory.Families.SchemeBaseChange S)ᵒᵖ) CategoryTheory.Cat

  The contravariant groupoid-valued pseudofunctor on schemes over S.

• fiberEquivalence (T : DerivedCategory.Families.SchemeBaseChange S) : ↑(self.presheaf.obj { as := Opposite.op T }) ≌ RelativePerfectModuliFiber T

  Identification of every fiber with the concrete core of universally-gluable relative-perfect complexes.

• pullback {T U : DerivedCategory.Families.SchemeBaseChange S} (f : T ⟶ U) : RelativePerfectPullback f

  The actual lifted left-derived pullback attached to every morphism of schemes over S.

• transitionComparison {T U : DerivedCategory.Families.SchemeBaseChange S} (f : T ⟶ U) : (self.fiberEquivalence U).functor.comp (self.pullback f).coreFunctor ≅ (self.presheaf.map f.op.toLoc).toFunctor.comp (self.fiberEquivalence T).functor

  The concrete lifted pullback agrees with the pseudofunctor transition.

instance AlgebraicGeometry.RelativePerfectBigZariskiPresheaf.fiber_isGroupoid {S : Scheme} (M : RelativePerfectBigZariskiPresheaf S) (T : CategoryTheory.LocallyDiscrete (DerivedCategory.Families.SchemeBaseChange S)ᵒᵖ) : CategoryTheory.IsGroupoid ↑(M.presheaf.obj T)

Every fiber of the big-Zariski relative-perfect presheaf is a groupoid.

noncomputable def AlgebraicGeometry.RelativePerfectBigZariskiPresheaf.ambientComparison {S : Scheme} (M : RelativePerfectBigZariskiPresheaf S) {T U : DerivedCategory.Families.SchemeBaseChange S} (f : T ⟶ U) : (M.fiberEquivalence U).functor.comp ((relativePerfectModuliForget U).comp (M.pullback f).ambient.functor) ≅ (M.presheaf.map f.op.toLoc).toFunctor.comp ((M.fiberEquivalence T).functor.comp (relativePerfectModuliForget T))

After forgetting to the ambient derived categories, a pseudofunctor transition is the stored arbitrary left-derived pullback.

Equations

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

noncomputable def AlgebraicGeometry.RelativePerfectBigZariskiPresheaf.exactAmbientComparison {S : Scheme} (M : RelativePerfectBigZariskiPresheaf S) {T U : DerivedCategory.Families.SchemeBaseChange S} (f : T ⟶ U) [DerivedCategory.Families.SchemeBaseChange.IsExactPullback f] : (M.fiberEquivalence U).functor.comp ((relativePerfectModuliForget U).comp (DerivedCategory.Families.SchemeBaseChange.derivedPullback f)) ≅ (M.presheaf.map f.op.toLoc).toFunctor.comp ((M.fiberEquivalence T).functor.comp (relativePerfectModuliForget T))

On an exact arrow, the ambient transition is the repository's exact derived pullback.

Equations

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

structure AlgebraicGeometry.RelativePerfectBigZariskiStack (S : Scheme) extends AlgebraicGeometry.RelativePerfectBigZariskiPresheaf S : Type (u + 2)

A universally-gluable relative-perfect presheaf with effective descent for the big Zariski topology over S.

• presheaf : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete (DerivedCategory.Families.SchemeBaseChange S)ᵒᵖ) CategoryTheory.Cat
• fiberEquivalence (T : DerivedCategory.Families.SchemeBaseChange S) : ↑(self.presheaf.obj { as := Opposite.op T }) ≌ RelativePerfectModuliFiber T
• pullback {T U : DerivedCategory.Families.SchemeBaseChange S} (f : T ⟶ U) : RelativePerfectPullback f
• transitionComparison {T U : DerivedCategory.Families.SchemeBaseChange S} (f : T ⟶ U) : (self.fiberEquivalence U).functor.comp (self.pullback f).coreFunctor ≅ (self.presheaf.map f.op.toLoc).toFunctor.comp (self.fiberEquivalence T).functor
• isStack : self.presheaf.IsStack (Scheme.zariskiTopology.over S)

  Effective descent for objects and morphisms.

def AlgebraicGeometry.RelativePerfectBigZariskiStack.toStackInGroupoids {S : Scheme} (M : RelativePerfectBigZariskiStack S) : CategoryTheory.StackInGroupoids (DerivedCategory.Families.SchemeBaseChange S) (Scheme.zariskiTopology.over S)

The stack in groupoids underlying a relative-perfect big-Zariski stack.

Equations

• M.toStackInGroupoids = { presheaf := M.presheaf, fiberIsGroupoid := ⋯, isStack := ⋯ }

noncomputable def AlgebraicGeometry.RelativePerfectBigZariskiStack.cechDescentEquivalence {S : Scheme} (M : RelativePerfectBigZariskiStack S) {T : DerivedCategory.Families.SchemeBaseChange S} (U : CategoryTheory.StackInGroupoids.Cover T) : ↑(M.toStackInGroupoids.presheaf.obj { as := Opposite.op T }) ≌ M.toStackInGroupoids.CechDescent U

Effective Čech descent for every big-Zariski cover over S.

Equations

• M.cechDescentEquivalence U = M.toStackInGroupoids.cechDescentEquivalence U

noncomputable def AlgebraicGeometry.RelativePerfectBigZariskiStack.fullyFaithfulToCechDescent {S : Scheme} (M : RelativePerfectBigZariskiStack S) {T : DerivedCategory.Families.SchemeBaseChange S} (U : CategoryTheory.StackInGroupoids.Cover T) : (M.toStackInGroupoids.toCechDescent U).FullyFaithful

Morphisms of relative-perfect complexes satisfy descent along every big-Zariski cover over S.

Equations

• M.fullyFaithfulToCechDescent U = M.toStackInGroupoids.fullyFaithfulToCechDescent U

theorem AlgebraicGeometry.RelativePerfectBigZariskiStack.essSurjToCechDescent {S : Scheme} (M : RelativePerfectBigZariskiStack S) {T : DerivedCategory.Families.SchemeBaseChange S} (U : CategoryTheory.StackInGroupoids.Cover T) : (M.toStackInGroupoids.toCechDescent U).EssSurj

Every compatible big-Zariski descent object is effective.