Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.Cover.intersectionOfLocallyDirected

{P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  {X : AlgebraicGeometry.Scheme} →
    (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) →
      [inst : CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] →
        [𝒰.LocallyDirected] →
          [P.IsStableUnderBaseChange] →
            [P.HasOfPostcompProperty P] →
              (i j : 𝒰.I₀) →
                AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P)
                  (CategoryTheory.Limits.pullback (𝒰.f i) (𝒰.f j))

If 𝒰 is a directed cover of X, this is the cover of 𝒰ᵢ ×[X] 𝒰ⱼ by {𝒰ₖ} where k ≤ i and k ≤ j.

Defined in

Mathlib.AlgebraicGeometry.Cover.Directed

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryAlgebraicGeometry.Scheme.Cover.LocallyDirectedCategoryTheory.MorphismProperty.IsStableUnderBaseChangeCategoryTheory.MorphismProperty.HasOfPostcompProperty