AlgebraicGeometry.FiniteEtale.exists_inverse_limit_model_of_recovered_charts
Actual recovered local charts produce a finite-etale model at a later original stage. Diagonal and triple laws are generated by eventual equality.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory Limits
open AlgebraicGeometry.Scheme.Cover
namespace AlgebraicGeometry.FiniteEtaleLean source · statement
theorem exists_inverse_limit_model_of_recovered_charts
{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, CompactSpace (D.obj i)] [∀ i : I, QuasiSeparatedSpace (D.obj i)]
(i : I) (𝒰 : (D.obj i).OpenCover.{u}) [Finite 𝒰.I₀]
[∀ a : 𝒰.I₀, CompactSpace (𝒰.X a)]
(A : 𝒰.I₀ → Over (D.obj i)) (V : 𝒰.I₀ × 𝒰.I₀ → Over (D.obj i))
(d : ∀ a b : 𝒰.I₀, V (a, b) ⟶ A a)
(y : ∀ a : 𝒰.I₀, (A a).left ⟶ 𝒰.X a)
[∀ a : 𝒰.I₀, IsFiniteEtale (y a)]
(hy : ∀ a : 𝒰.I₀, y a ≫ 𝒰.f a = (A a).hom)
(ℓ : ∀ a b : 𝒰.I₀, (V (a, b)).left ⟶ 𝒰.X b)
(hV : ∀ a b : 𝒰.I₀,
IsPullback (d a b).left (ℓ a b) (y a ≫ 𝒰.f a) (𝒰.f b))
(t : ∀ a b : 𝒰.I₀, V (a, b) ⟶ V (b, a))
(ht : ∀ a b : 𝒰.I₀, (t a b).left ≫ (d b a).left ≫ y b = ℓ a b)
(X : FiniteEtale c.pt)
(h : ∀ a : 𝒰.I₀,
(Over.pullback (c.π.app i)).obj (A a) ⟶ (FiniteEtale.forget c.pt).obj X)
[∀ a : 𝒰.I₀, IsOpenImmersion (h a).left]
(hcover : ∀ x : X.left, ∃ (a : 𝒰.I₀)
(z : ((Over.pullback (c.π.app i)).obj (A a)).left), (h a).left z = x)
(hoverlap : ∀ a b : 𝒰.I₀,
IsPullback ((Over.pullback (c.π.app i)).map (d a b)).left
((Over.pullback (c.π.app i)).map (t a b ≫ d b a)).left (h a).left (h b).left) :
∃ (j : I) (_ : j ⟶ i) (N : FiniteEtale (D.obj j)),
Nonempty ((FiniteEtale.pullback (c.π.app j)).obj N ≅ X)