AlgebraicGeometry.FiniteEtale.exists_inverse_limit_stage_map_eq
Two morphisms of finite-etale covers whose native pullbacks to the limit agree have equal native pullbacks at a later original stage.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtaleLean source · statement
theorem exists_inverse_limit_stage_map_eq
{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) {A B : FiniteEtale (D.obj i)} (a b : A ⟶ B)
(hab : (FiniteEtale.pullback (c.π.app i)).map a =
(FiniteEtale.pullback (c.π.app i)).map b) :
∃ (j : I) (hji : j ⟶ i),
(FiniteEtale.pullback (D.map hji)).map a =
(FiniteEtale.pullback (D.map hji)).map b