AlgebraicGeometry.Scheme.Cover.exists_relativePullbackGlue_recovery_iso
The native pullback of the glued model is isomorphic over the new base to the scheme covered by the actual recovered local models.
Source context 15 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.Scheme.Cover
variable {S T L : 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 (ℓ : ∀ 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)))Lean source · statement
theorem exists_relativePullbackGlue_recovery_iso
(q : (relativeGlueDataOfPullbackEquations 𝒰 A V d y ℓ hV t ht ψ hdiag hcycle).glued ⟶ T)
(hq : ∀ i : 𝒰.I₀,
(relativeGlueDataOfPullbackEquations 𝒰 A V d y ℓ hV t ht ψ hdiag hcycle).ι i ≫ q =
((Over.pullback ψ).obj (A i)).hom)
(ρ : L ⟶ T) (χ : L ⟶ S) (hχ : χ = ρ ≫ ψ)
(Z : Over L)
(h : ∀ i : 𝒰.I₀, (Over.pullback χ).obj (A i) ⟶ Z)
[∀ i : 𝒰.I₀, IsOpenImmersion (h i).left]
(hcover : ∀ z : Z.left, ∃ (i : 𝒰.I₀) (a : ((Over.pullback χ).obj (A i)).left),
(h i).left a = z)
(hoverlap : ∀ i j : 𝒰.I₀,
IsPullback ((Over.pullback χ).map (d i j)).left
((Over.pullback χ).map (t i j ≫ d j i)).left (h i).left (h j).left) :
Nonempty ((Over.pullback ρ).obj (Over.mk q) ≅ Z)