Residue-field fibers of a scheme-indexed categorical family

For a scheme base change T ⟶ S and a point x : T, Mathlib constructs the canonical morphism Spec κ(x) ⟶ T. This file regards its composite with T ⟶ S as an object of Over S, then evaluates a client-supplied SchemeTriangulatedFiberFamily S there. The family's contravariant pseudofunctor supplies categorical and Grothendieck-group restriction to the residue fiber.

The residue-field schemes and morphisms are genuine geometric objects. The triangulated categories and pullback functors remain client data: no derived category, derived base-change theorem, geometric slicing witness, relative HN structure, openness, boundedness, moduli construction, or Theorem 22.2 conclusion is asserted.

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.residue {S : Scheme} (T : SchemeBaseChange S) (x : ↥(CategoryTheory.Over.left T)) : SchemeBaseChange S

The residue-field base change of T ⟶ S at a point of T.

Equations

• T.residue x = CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Over.left T).fromSpecResidueField x) (CategoryTheory.Over.hom T))

@[simp]

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.residue_left {S : Scheme} (T : SchemeBaseChange S) (x : ↥(CategoryTheory.Over.left T)) : CategoryTheory.Over.left (T.residue x) = Spec ((CategoryTheory.Over.left T).residueField x)

@[simp]

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.residue_hom {S : Scheme} (T : SchemeBaseChange S) (x : ↥(CategoryTheory.Over.left T)) : CategoryTheory.Over.hom (T.residue x) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Over.left T).fromSpecResidueField x) (CategoryTheory.Over.hom T)

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.residueTo {S : Scheme} (T : SchemeBaseChange S) (x : ↥(CategoryTheory.Over.left T)) : T.residue x ⟶ T

The canonical morphism from a residue-field base change to the original scheme over S.

Equations

• T.residueTo x = CategoryTheory.Over.homMk ((CategoryTheory.Over.left T).fromSpecResidueField x) ⋯

@[simp]

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.residueTo_left {S : Scheme} (T : SchemeBaseChange S) (x : ↥(CategoryTheory.Over.left T)) : CategoryTheory.Over.Hom.left (T.residueTo x) = (CategoryTheory.Over.left T).fromSpecResidueField x

@[reducible, inline]

abbrev AlgebraicGeometry.DerivedCategory.Families.SchemeTriangulatedFiberFamily.ResidueFiber {S : Scheme} (F : SchemeTriangulatedFiberFamily S) (T : SchemeBaseChange S) (x : ↥(CategoryTheory.Over.left T)) : Type w

The triangulated residue fiber over a point of a scheme base change.

Equations

• F.ResidueFiber T x = CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F (T.residue x)

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.DerivedCategory.Families.SchemeTriangulatedFiberFamily.pullToResidue {S : Scheme} (F : SchemeTriangulatedFiberFamily S) (T : SchemeBaseChange S) (x : ↥(CategoryTheory.Over.left T)) : CategoryTheory.Functor (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) (F.ResidueFiber T x)

Restriction from the category over T to its residue fiber at x.

Equations

• F.pullToResidue T x = CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.pull F (T.residueTo x)

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.DerivedCategory.Families.SchemeTriangulatedFiberFamily.pullK₀ToResidue {S : Scheme} (F : SchemeTriangulatedFiberFamily S) (T : SchemeBaseChange S) (x : ↥(CategoryTheory.Over.left T)) : CategoryTheory.Triangulated.K₀ (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) →+ CategoryTheory.Triangulated.K₀ (F.ResidueFiber T x)

Pullback on Grothendieck groups from T to its residue fiber.

Equations

• F.pullK₀ToResidue T x = CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.pullK₀ F (T.residueTo x)

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeTriangulatedFiberFamily.pullK₀ToResidue_of {S : Scheme} (F : SchemeTriangulatedFiberFamily S) (T : SchemeBaseChange S) (x : ↥(CategoryTheory.Over.left T)) (E : CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) : (F.pullK₀ToResidue T x) (CategoryTheory.Triangulated.K₀.of (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) E) = CategoryTheory.Triangulated.K₀.of (F.ResidueFiber T x) ((F.pullToResidue T x).obj E)