Nyll.SchemeTheory.FiniteEtale.AffineTransitionLocalModel

theorem

opensCone_isPullback

AlgebraicGeometry.opensCone_isPullback

Documentation

Each restricted cone map is the actual base change of the original cone projection along the corresponding open immersion.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
open CategoryTheory Limits TopologicalSpace
namespace AlgebraicGeometry

Lean source · statement

theorem opensCone_isPullback
    {I : Type u} [Category.{u} I] (D : I ⥤ Scheme.{u}) (c : Cone D)
    (i : I) (U : (D.obj i).Opens) (j : Over i) :
    IsPullback ((opensCone D c i U).π.app j) (c.π.app i ⁻¹ᵁ U).ι
      (D.map j.hom ⁻¹ᵁ U).ι (c.π.app j.left)

theorem

exists_common_stage_recovered_local_models

L46 ↗

AlgebraicGeometry.FiniteEtale.exists_common_stage_recovered_local_models

Documentation

A finite-etale cover of the limit has recovered local models on one actual later finite affine cover, with every chart square proved cartesian.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
open CategoryTheory Limits TopologicalSpace
namespace AlgebraicGeometry
namespace FiniteEtale

Lean source · full declaration

theorem exists_common_stage_recovered_local_models
    {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) {K : Type v} [Finite K]
    (U : K → (D.obj i).Opens) (hcover : IsOpenCover U)
    (hU : ∀ k : K, IsAffineOpen (U k)) (X : FiniteEtale c.pt) :
    ∃ (j : I) (hji : j ⟶ i),
      IsOpenCover (fun k : K ↦ D.map hji ⁻¹ᵁ U k) ∧
      ∃ M : ∀ k : K, FiniteEtale ((opensDiagram D i (U k)).obj (Over.mk hji)),
        ∀ k : K,
          IsPullback ((opensCone D c i (U k)).π.app (Over.mk hji))
            (c.π.app i ⁻¹ᵁ U k).ι (D.map hji ⁻¹ᵁ U k).ι (c.π.app j) ∧
          Nonempty
            ((FiniteEtale.pullback ((opensCone D c i (U k)).π.app (Over.mk hji))).obj
                (M k) ≅
              (FiniteEtale.pullback (c.π.app i ⁻¹ᵁ U k).ι).obj X) := by
  let XU (k : K) : FiniteEtale (opensCone D c i (U k)).pt :=
    (FiniteEtale.pullback (c.π.app i ⁻¹ᵁ U k).ι).obj X
  obtain ⟨j, hji, hV, M, hM⟩ :=
    exists_common_stage_affine_chart_models D c hc i U hcover hU XU
  exact ⟨j, hji, hV, M, fun k ↦
    ⟨opensCone_isPullback D c i (U k) (Over.mk hji), hM k⟩⟩

AffineTransitionLocalModel.lean

Module documentation

Recovered local models of an actual finite-etale cover

opensCone_isPullback

exists_common_stage_recovered_local_models

Module documentation

Recovered local models of an actual finite-etale cover

Declarations

opensCone_isPullback

exists_common_stage_recovered_local_models