theorem
L31 ↗exists_eq_stage_family
AlgebraicGeometry.AffineTransitionHom.exists_eq_stage_family
Finitely many equalities of stage-model morphisms which hold over the actual limit already hold simultaneously after a single transition. The indexing family is allowed to be empty.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
open CategoryTheory Limits
namespace AlgebraicGeometry.AffineTransitionHomLean source · statement
theorem exists_eq_stage_family
{I : Type u} [Category.{u} I] [IsCofiltered I] {S : Scheme.{u}}
(D : I ⥤ Over S) (c : Cone D) (hc : IsLimit c)
[∀ {i j : I} (h : i ⟶ j), IsAffineHom (D.map h).left]
[∀ i : I, CompactSpace (D.obj i).left]
{K : Type v} [Finite K] (Y Z : K → Scheme.{u})
(f : ∀ k : K, Y k ⟶ S) (g : ∀ k : K, Z k ⟶ S)
[∀ k : K, QuasiCompact (f k)] [∀ k : K, LocallyOfFiniteType (g k)]
(i : I)
(a b : ∀ k : K, pullback (D.obj i).hom (f k) ⟶ pullback (D.obj i).hom (g k))
(ha : ∀ k : K, a k ≫ pullback.fst (D.obj i).hom (g k) =
pullback.fst (D.obj i).hom (f k))
(hb : ∀ k : K, b k ≫ pullback.fst (D.obj i).hom (g k) =
pullback.fst (D.obj i).hom (f k))
(hab : ∀ k : K, (cone D c (f k)).π.app i ≫ a k =
(cone D c (f k)).π.app i ≫ b k) :
∃ (j : I) (hji : j ⟶ i), ∀ k : K,
(diagram D (f k)).map hji ≫ a k = (diagram D (f k)).map hji ≫ b k