Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_X

∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme)
  [inst : P.IsStableUnderBaseChange] [inst_1 : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P]
  {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X)
  (f : W ⟶ X) [inst_2 : W.Over S] [inst_3 : X.Over S] [inst_4 : AlgebraicGeometry.Scheme.Cover.Over S 𝒰]
  [inst_5 : AlgebraicGeometry.Scheme.Hom.IsOver f S] {Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  [inst_6 : Q.HasOfPostcompProperty Q] [inst_7 : Q.IsStableUnderBaseChange] [inst_8 : Q.IsStableUnderComposition]
  (hX : Q (X ↘ S)) (hW : Q (W ↘ S)) (hQ : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)) (x : 𝒰.I₀),
  (AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp S 𝒰 f hX hW hQ).X x =
    (CategoryTheory.Limits.pullback (AlgebraicGeometry.Scheme.Hom.asOverProp f S)
        (AlgebraicGeometry.Scheme.Hom.asOverProp (𝒰.f x) S)).left

Defined in

Mathlib.AlgebraicGeometry.Cover.Over

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.MorphismProperty.IsStableUnderBaseChangeAlgebraicGeometry.Scheme.IsJointlySurjectivePreservingAlgebraicGeometry.Scheme.OverAlgebraicGeometry.Scheme.OverAlgebraicGeometry.Scheme.Cover.OverAlgebraicGeometry.Scheme.Hom.IsOverCategoryTheory.MorphismProperty.HasOfPostcompPropertyCategoryTheory.MorphismProperty.IsStableUnderBaseChangeCategoryTheory.MorphismProperty.IsStableUnderComposition