AlgebraicGeometry.FiniteEtale.exists_inverse_limit_stage_gluing_relations
All diagonal and triple gluing relations descend together from actual recovered local charts to one later stage.
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_stage_gluing_relations
{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) (𝒰 : (D.obj i).OpenCover) [Finite 𝒰.I₀]
(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 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)
[∀ a : 𝒰.I₀, QuasiCompact (V (a, a)).hom]
[∀ a : 𝒰.I₀, LocallyOfFiniteType (V (a, a)).hom]
[∀ a b d' : 𝒰.I₀, QuasiCompact (relativeTriple 𝒰 A V d a b d').hom]
[∀ a b d' : 𝒰.I₀, LocallyOfFiniteType (relativeTriple 𝒰 A V d a b d').hom]
(Z : Scheme.{u})
(h : ∀ a : 𝒰.I₀, (relativeRecoveryFunctor (c.π.app i)).obj (A a) ⟶ Z)
[hmono : ∀ a : 𝒰.I₀, Mono (h a)]
(hrec : ∀ a b : 𝒰.I₀,
(relativeRecoveryFunctor (c.π.app i)).map (t a b) ≫
(relativeRecoveryFunctor (c.π.app i)).map (d b a) ≫ h b =
(relativeRecoveryFunctor (c.π.app i)).map (d a b) ≫ h a) :
∃ (j : I) (hji : j ⟶ i),
(∀ a : 𝒰.I₀, (Over.pullback (D.map hji)).map (t a a) =
𝟙 ((Over.pullback (D.map hji)).obj (V (a, a)))) ∧
(∀ a b d' : 𝒰.I₀,
(Over.pullback (D.map hji)).map
(relativeTripleTransition 𝒰 A V d y ℓ hV t ht a b d' ≫
relativeTripleTransition 𝒰 A V d y ℓ hV t ht b d' a ≫
relativeTripleTransition 𝒰 A V d y ℓ hV t ht d' a b) =
𝟙 ((Over.pullback (D.map hji)).obj (relativeTriple 𝒰 A V d a b d')))