Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.Cover.sigma

{P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  {S : AlgebraicGeometry.Scheme} →
    [AlgebraicGeometry.IsZariskiLocalAtSource P] →
      [UnivLE.{v, u}] →
        AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) S →
          AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) S

If 𝒰 is a cover of S, this is the single object cover where the covering object is the disjoint union.

Defined in

Mathlib.AlgebraicGeometry.Cover.Sigma

Cited by

12 results in Mathlib

Foundations

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

Assumes

AlgebraicGeometry.IsZariskiLocalAtSourceUnivLE