AlgebraicGeometry.FiniteEtale.exists_inverse_limit_open_stage_iso_family
Isomorphisms over finitely many compact stage opens descend to actual isomorphisms at one common later stage, retaining each recovery equation.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
open CategoryTheory Limits TopologicalSpace
namespace AlgebraicGeometry.FiniteEtaleLean source · statement
theorem exists_inverse_limit_open_stage_iso_family
{I : Type u} [Category.{u} I] [IsCofiltered I]
(D : I ⥤ Scheme.{u}) (c : Cone D) (hc : IsLimit c)
[∀ {i j : I} (h : i ⟶ j), IsAffineHom (D.map h)]
[∀ i : I, QuasiSeparatedSpace (D.obj i)]
(i : I) {K : Type v} [Finite K]
(U : K → (D.obj i).Opens)
(hU : ∀ k : K, IsCompact (U k : Set (D.obj i)))
(t : Over i)
(A B : ∀ k : K, FiniteEtale ((opensDiagram D i (U k)).obj t))
(a : ∀ k : K,
(FiniteEtale.pullback ((opensCone D c i (U k)).π.app t)).obj (A k) ≅
(FiniteEtale.pullback ((opensCone D c i (U k)).π.app t)).obj (B k)) :
∃ (s : Over i) (hst : s ⟶ t)
(b : ∀ k : K,
(FiniteEtale.pullback ((opensDiagram D i (U k)).map hst)).obj (A k) ≅
(FiniteEtale.pullback ((opensDiagram D i (U k)).map hst)).obj (B k)),
∀ k : K,
(inverseLimitPullbackComparison (opensDiagram D i (U k))
(opensCone D c i (U k)) hst).hom.app (A k) ≫
(FiniteEtale.pullback ((opensCone D c i (U k)).π.app s)).map (b k).hom =
(a k).hom ≫
(inverseLimitPullbackComparison (opensDiagram D i (U k))
(opensCone D c i (U k)) hst).hom.app (B k)