Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.Cover.mkOfCovers

{X : AlgebraicGeometry.Scheme} →
  {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
    (J : Type u_1) →
      (obj : J → AlgebraicGeometry.Scheme) →
        (map : (j : J) → obj j ⟶ X) →
          (∀ (x : ↥X), ∃ j y, (map j) y = x) →
            autoParam (∀ (j : J), P (map j)) AlgebraicGeometry.Scheme.Cover.mkOfCovers._auto_1 →
              AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X

Given a family of schemes with morphisms to X satisfying P that jointly cover X, Cover.mkOfCovers is an associated P-cover of X.

Defined in

Mathlib.AlgebraicGeometry.Cover.MorphismProperty

Cited by

5 results in Mathlib

Foundations

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