Theorems · Definition · algebraic geometry

AlgebraicGeometry.isLimitOpensCone

{I : Type u} →
  [inst : CategoryTheory.Category.{u, u} I] →
    (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme) →
      (c : CategoryTheory.Limits.Cone D) →
        CategoryTheory.Limits.IsLimit c →
          [CategoryTheory.IsCofiltered I] →
            (i : I) → (U : (D.obj i).Opens) → CategoryTheory.Limits.IsLimit (AlgebraicGeometry.opensCone D c i U)

Given a diagram { Dᵢ }_{i ∈ I} of schemes and an open U ⊆ Dᵢ, the preimage of U ⊆ Dᵢ under the map lim Dᵢ ⟶ Dᵢ is the limit of { Dⱼᵢ⁻¹ U }_{j ≤ i}.

Defined in

Mathlib.AlgebraicGeometry.AffineTransitionLimit

Cited by

8 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.IsCofiltered