Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.Cover.pullbackHom

{P : CategoryTheory.MorphismProperty 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) →
            (i : 𝒰.toPreZeroHypercover.1) →
              [inst_2 : ∀ (x : 𝒰.I₀), CategoryTheory.Limits.HasPullback f (𝒰.f x)] →
                (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i

The family of morphisms from the pullback cover to the original cover.

Defined in

Mathlib.AlgebraicGeometry.Cover.MorphismProperty

Cited by

32 results in Mathlib

Foundations

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

Assumes

CategoryTheory.MorphismProperty.IsStableUnderBaseChangeAlgebraicGeometry.Scheme.IsJointlySurjectivePreservingCategoryTheory.Limits.HasPullback