Theorems · Theorem · algebraic geometry

AlgebraicGeometry.ExistsHomHomCompEqCompAux.exists_index

∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] {S X : AlgebraicGeometry.Scheme}
  {D : CategoryTheory.Functor I AlgebraicGeometry.Scheme} {t : D ⟶ (CategoryTheory.Functor.const I).obj S} {f : X ⟶ S}
  [∀ (i : I), CompactSpace ↥(D.obj i)] [CategoryTheory.IsCofiltered I]
  [∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)]
  (A : AlgebraicGeometry.ExistsHomHomCompEqCompAux D t f),
  ∃ i' hii',
    ⇑(CategoryTheory.CategoryStruct.comp (D.map hii') (CategoryTheory.Limits.pullback.lift A.a A.b ⋯)) ⁻¹'
        (↑(AlgebraicGeometry.Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X))ᶜ =
      ∅

Defined in

Mathlib.AlgebraicGeometry.AffineTransitionLimit

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCompactSpaceCategoryTheory.IsCofilteredAlgebraicGeometry.IsAffineHom