structure
L29 ↗FibreH0Family
CoherentBaseChange.FibreH0Family
A compatible family of local two-term models for degree-zero fibre dimensions.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory Opposite
universe u
namespace CoherentBaseChangeLean source · full declaration
structure FibreH0Family (T : Scheme.{u}) where
/-- The two-term model on each affine open of the scheme. -/
G : ∀ (U : T.Opens), IsAffineOpen U → TwoTermComplex.{u, u} Γ(T, U)
/-- The degree-zero fibre dimension assigned to each point of the scheme. -/
h0 : T → ℕ
/-- Each local model computes the assigned dimension at every point of its affine open. -/
hglue : ∀ (U : T.Opens) (hU : IsAffineOpen U) (t : U),
h0 t = (G U hU).fibreH0 (hU.primeIdealOf t)