Affine derived families over a fixed affine morphism

For a fixed affine morphism Spec R ⟶ Spec B, a test B-algebra A does not carry the family directly. Its total space has coordinate ring the pushout R ⊗_B A, and hence is the scheme pullback Spec R ×_{Spec B} Spec A.

This file makes that geometry explicit. It constructs the coordinate-ring base-change functor on Under B, proves that its spectra form the required pullback squares, and reindexes the geometric affine moduli-groupoid pseudofunctor along this functor. The result is the correctly indexed affine substrate for the relative-perfect and universally-gluable restriction.

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineFamilyCoordinateRingFunctor {B : CommRingCat} (X : CategoryTheory.Under B) : CategoryTheory.Functor (CategoryTheory.Under B) CommRingCat

For X : B ⟶ R, send a test B-algebra A to the coordinate ring of the affine base change Spec R ×_{Spec B} Spec A.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.affineFamilyCoordinateRingFunctor X = (CategoryTheory.Under.pushout X.hom).comp (CategoryTheory.Under.forget X.right)

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.DerivedCategory.Dqc.AffineFamilyCoordinateRing {B : CommRingCat} (X A : CategoryTheory.Under B) : CommRingCat

The coordinate ring of the affine family obtained from X over a test B-algebra A.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.AffineFamilyCoordinateRing X A = (AlgebraicGeometry.DerivedCategory.Dqc.affineFamilyCoordinateRingFunctor X).obj A

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineFamilyToTestScheme {B : CommRingCat} (X A : CategoryTheory.Under B) : Spec (AffineFamilyCoordinateRing X A) ⟶ Spec A.right

The projection from the affine base-changed total space to the test scheme.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.affineFamilyToTestScheme X A = AlgebraicGeometry.Spec.map (CategoryTheory.Limits.pushout.inl A.hom X.hom)

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineFamilyToTotalSpace {B : CommRingCat} (X A : CategoryTheory.Under B) : Spec (AffineFamilyCoordinateRing X A) ⟶ Spec X.right

The projection from the affine base-changed total space to the original total space.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.affineFamilyToTotalSpace X A = AlgebraicGeometry.Spec.map (CategoryTheory.Limits.pushout.inr A.hom X.hom)

theorem AlgebraicGeometry.DerivedCategory.Dqc.affineFamily_isPullback {B : CommRingCat} (X A : CategoryTheory.Under B) : CategoryTheory.IsPullback (affineFamilyToTestScheme X A) (affineFamilyToTotalSpace X A) (Spec.map A.hom) (Spec.map X.hom)

The spectra used by the affine family construction form the actual scheme pullback square over Spec B.

@[reducible, inline]

abbrev AlgebraicGeometry.DerivedCategory.Dqc.AffineFamilyBoundedAboveProjectiveModuliFiber {B : CommRingCat} (X A : CategoryTheory.Under B) : Type (u + 1)

The groupoid of geometric bounded-above projective complexes on the affine base-changed total space.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineFamilyBoundedAboveProjectivePullback {B : CommRingCat} (X : CategoryTheory.Under B) {A A' : CategoryTheory.Under B} (f : A ⟶ A') : CategoryTheory.Functor (AffineFamilyBoundedAboveProjectiveModuliFiber X A) (AffineFamilyBoundedAboveProjectiveModuliFiber X A')

Pullback of affine derived families along a morphism of test B-algebras.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineFamilyBoundedAboveProjectivePseudofunctor {B : CommRingCat} (X : CategoryTheory.Under B) : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete (CategoryTheory.Under B)) CategoryTheory.Cat

The affine geometric moduli-groupoid pseudofunctor, reindexed over test B-algebras by forming the actual affine base-changed total space.

Equations

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

theorem AlgebraicGeometry.DerivedCategory.Dqc.affineFamilyBoundedAboveProjectivePseudofunctor_map_toFunctor {B : CommRingCat} (X : CategoryTheory.Under B) {A A' : CategoryTheory.Under B} (f : A ⟶ A') : ((affineFamilyBoundedAboveProjectivePseudofunctor X).map { as := f }).toFunctor = affineFamilyBoundedAboveProjectivePullback X f

A transition in the reindexed family pseudofunctor is the concrete arbitrary affine derived pullback along the induced map of pushout rings.

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineFamilyBoundedAboveProjectiveModuliForget {B : CommRingCat} (X A : CategoryTheory.Under B) : CategoryTheory.Functor (AffineFamilyBoundedAboveProjectiveModuliFiber X A) (SchemeQuasicoherentDerivedCategory (Spec (AffineFamilyCoordinateRing X A)))

Forget an affine family moduli groupoid to the honest Dqc category of its base-changed total space.

Equations

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