Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.Cover.overEquiv_generate_toPresieveOver_eq_ofArrows

∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {S : AlgebraicGeometry.Scheme}
  [inst : P.IsStableUnderBaseChange] {X : CategoryTheory.Over S}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X.left)
  [inst_1 : AlgebraicGeometry.Scheme.Cover.Over S 𝒰],
  (CategoryTheory.Sieve.overEquiv X) (CategoryTheory.Sieve.generate 𝒰.toPresieveOver) =
    CategoryTheory.Sieve.ofArrows 𝒰.X 𝒰.f

Defined in

Mathlib.AlgebraicGeometry.Sites.Small

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.MorphismProperty.IsStableUnderBaseChangeAlgebraicGeometry.Scheme.Cover.Over