Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.Cover.pullbackCoverOver_f

∀ {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] (x : 𝒰.I₀),
  (AlgebraicGeometry.Scheme.Cover.pullbackCoverOver S 𝒰 f).f x =
    CategoryTheory.Over.Hom.left
      (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Hom.asOver f S)
        (AlgebraicGeometry.Scheme.Hom.asOver (𝒰.f x) S))

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.IsOver