Theorems · Theorem · algebraic geometry

AlgebraicGeometry.ExistsHomHomCompEqCompAux.exists_eq

∀ {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}
  [inst_1 : ∀ (i : I), CompactSpace ↥(D.obj i)] [AlgebraicGeometry.LocallyOfFiniteType f]
  [inst_3 : CategoryTheory.IsCofiltered I] [inst_4 : ∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)]
  (A : AlgebraicGeometry.ExistsHomHomCompEqCompAux D t f) [∀ (i : I), AlgebraicGeometry.IsAffineHom (A.c.π.app i)]
  (j : A.𝒰D.I₀),
  ∃ k hki',
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ (D.map hki') A.𝒰D).f j)
        (CategoryTheory.CategoryStruct.comp (D.map (CategoryTheory.CategoryStruct.comp hki' A.hii')) A.a) =
      CategoryTheory.CategoryStruct.comp ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ (D.map hki') A.𝒰D).f j)
        (CategoryTheory.CategoryStruct.comp (D.map (CategoryTheory.CategoryStruct.comp hki' A.hii')) A.b)

Defined in

Mathlib.AlgebraicGeometry.AffineTransitionLimit

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCompactSpaceAlgebraicGeometry.LocallyOfFiniteTypeCategoryTheory.IsCofilteredAlgebraicGeometry.IsAffineHomAlgebraicGeometry.IsAffineHom