Theorems · Inductive type · algebraic geometry

AlgebraicGeometry.Scheme.Cover.LocallyDirected

{P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  {X : AlgebraicGeometry.Scheme} →
    (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) →
      [CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] → Type (max (max u u_1) v_1)

A directed P-cover of a scheme X is a cover 𝒰 with an ordering on the indices and compatible transition maps 𝒰ᵢ ⟶ 𝒰ⱼ for i ≤ j such that every x : 𝒰ᵢ ×[X] 𝒰ⱼ comes from some 𝒰ₖ for a k ≤ i and k ≤ j.

Defined in

Mathlib.AlgebraicGeometry.Cover.Directed

Cited by

63 results in Mathlib

Foundations

Depth 105 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Category