AlgebraicGeometry.FiniteEtale.exists_relativePullbackGlue_finiteEtale
Gluing the actual pulled-back finite-etale local models produces an actual finite-etale morphism, compatible with every native chart map.
Source context 18 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory Limits
open AlgebraicGeometry.Scheme.Cover
namespace AlgebraicGeometry.FiniteEtale
variable {S T : Scheme.{u}} (𝒰 : S.OpenCover)
variable (A : 𝒰.I₀ → Over S) (V : 𝒰.I₀ × 𝒰.I₀ → Over S)
variable (d : ∀ i j : 𝒰.I₀, V (i, j) ⟶ A i)
variable (y : ∀ i : 𝒰.I₀, (A i).left ⟶ 𝒰.X i)
variable (hy : ∀ i : 𝒰.I₀, y i ≫ 𝒰.f i = (A i).hom)
variable (ℓ : ∀ i j : 𝒰.I₀, (V (i, j)).left ⟶ 𝒰.X j)
variable (hV : ∀ i j : 𝒰.I₀, IsPullback (d i j).left (ℓ i j) (y i ≫ 𝒰.f i) (𝒰.f j))
variable (t : ∀ i j : 𝒰.I₀, V (i, j) ⟶ V (j, i))
variable (ht : ∀ i j : 𝒰.I₀, (t i j).left ≫ (d j i).left ≫ y j = ℓ i j)
variable (ψ : T ⟶ S)
variable (hdiag : ∀ i : 𝒰.I₀,
(Over.pullback ψ).map (t i i) = 𝟙 ((Over.pullback ψ).obj (V (i, i))))
variable (hcycle : ∀ i j k : 𝒰.I₀,
(Over.pullback ψ).map
(relativeTripleTransition 𝒰 A V d y ℓ hV t ht i j k ≫
relativeTripleTransition 𝒰 A V d y ℓ hV t ht j k i ≫
relativeTripleTransition 𝒰 A V d y ℓ hV t ht k i j) =
𝟙 ((Over.pullback ψ).obj (relativeTriple 𝒰 A V d i j k)))
include hy inLean source · statement
theorem exists_relativePullbackGlue_finiteEtale [∀ i : 𝒰.I₀, IsFiniteEtale (y i)] :
∃ q : (relativeGlueDataOfPullbackEquations 𝒰 A V d y ℓ hV t ht ψ hdiag hcycle).glued ⟶ T,
IsFiniteEtale q ∧ ∀ i : 𝒰.I₀,
(relativeGlueDataOfPullbackEquations 𝒰 A V d y ℓ hV t ht ψ hdiag hcycle).ι i ≫ q =
((Over.pullback ψ).obj (A i)).hom