Module

AffineTransitionCharts.lean

Nyll.SchemeTheory.FiniteEtale.AffineTransitionCharts

4 declarations indexed from sourceView source ↗

Module documentation

Finite-etale chart models at a common inverse-system stage

The inverse images of an affine open at an original stage form an actual affine inverse system. Descend each finite-etale chart cover through its global-sections colimit, then use a finite cofiltered wide cospan to put all models over the same stage. Native pullback composition preserves every recovery isomorphism and the pulled-back opens still cover that stage.

Imports4

Nyll.SchemeTheory.FiniteEtale.AffineTransitionModel
Mathlib.AlgebraicGeometry.AffineTransitionLimit
Mathlib.CategoryTheory.Filtered.Basic
Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Imported by2

instance

finiteEtaleHasPullbacksAlongChart

L30 ↗

AlgebraicGeometry.FiniteEtale.finiteEtaleHasPullbacksAlongChart

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.FiniteEtale

Lean source · statement

instance finiteEtaleHasPullbacksAlongChart
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f

instance

finiteEtaleStableUnderBaseChangeAlongChart

L36 ↗

AlgebraicGeometry.FiniteEtale.finiteEtaleStableUnderBaseChangeAlongChart

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.FiniteEtale
local instance finiteEtaleHasPullbacksAlongChart
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩

Lean source · statement

instance finiteEtaleStableUnderBaseChangeAlongChart
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f

theorem

exists_affine_chart_model

L51 ↗

AlgebraicGeometry.FiniteEtale.exists_affine_chart_model

Documentation

A cover of the inverse image of an affine stage open descends along that open's actual tail diagram, with its native recovery map.

Source context 8 commands

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

noncomputable section
universe u v
open CategoryTheory Limits TopologicalSpace
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleHasPullbacksAlongChart
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongChart
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩
variable {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)]
include hc

Lean source · statement

theorem exists_affine_chart_model (i : I) (U : (D.obj i).Opens) (hU : IsAffineOpen U)
    (X : FiniteEtale (opensCone D c i U).pt) :
    ∃ (j : Over i) (Xⱼ : FiniteEtale ((opensDiagram D i U).obj j)),
      Nonempty ((FiniteEtale.pullback ((opensCone D c i U).π.app j)).obj Xⱼ ≅ X)

theorem

exists_common_stage_affine_chart_models

L63 ↗

AlgebraicGeometry.FiniteEtale.exists_common_stage_affine_chart_models

Documentation

Finite-etale covers on the limit charts of a finite affine stage cover have actual finite-etale models on one common stage cover. Every recovery is along the original restricted cone projection.

Source context 8 commands

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

noncomputable section
universe u v
open CategoryTheory Limits TopologicalSpace
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleHasPullbacksAlongChart
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongChart
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩
variable {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)]
include hc

Lean source · full declaration

theorem exists_common_stage_affine_chart_models
    (i : I) {K : Type v} [Finite K]
    (U : K → (D.obj i).Opens) (hcover : IsOpenCover U)
    (hU : ∀ k : K, IsAffineOpen (U k))
    (X : ∀ k : K, FiniteEtale (opensCone D c i (U k)).pt) :
    ∃ (j : I) (hji : j ⟶ i),
      IsOpenCover (fun k : K ↦ D.map hji ⁻¹ᵁ U k) ∧
      ∃ Xⱼ : ∀ k : K, FiniteEtale ((opensDiagram D i (U k)).obj (Over.mk hji)),
        ∀ k : K, Nonempty
          ((FiniteEtale.pullback ((opensCone D c i (U k)).π.app (Over.mk hji))).obj
            (Xⱼ k) ≅ X k) := by
  classical
  choose j Xj hj using fun k : K ↦ exists_affine_chart_model D c hc i (U k) (hU k) (X k)
  obtain ⟨l, hli, hlj, hcomp⟩ := IsCofiltered.wideCospan (fun k : K ↦ (j k).hom)
  let α (k : K) : Over.mk hli ⟶ j k := Over.homMk (hlj k) (hcomp k)
  let Y (k : K) : FiniteEtale ((opensDiagram D i (U k)).obj (Over.mk hli)) :=
    (FiniteEtale.pullback ((opensDiagram D i (U k)).map (α k))).obj (Xj k)
  refine ⟨l, hli, hcover.comap (D.map hli).base.hom, Y, ?_⟩
  intro k
  let p := (opensCone D c i (U k)).π.app (Over.mk hli)
  let q := (opensDiagram D i (U k)).map (α k)
  let r := (opensCone D c i (U k)).π.app (j k)
  have hpq : p ≫ q = r := (opensCone D c i (U k)).w (α k)
  let e₁ : FiniteEtale.pullback (p ≫ q) ≅
      FiniteEtale.pullback q ⋙ FiniteEtale.pullback p :=
    MorphismProperty.Over.pullbackComp
      (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) (Q := ⊤) p q
  let e₂ : FiniteEtale.pullback (p ≫ q) ≅ FiniteEtale.pullback r :=
    MorphismProperty.Over.pullbackCongr
      (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) (Q := ⊤) hpq
  exact ⟨(e₁.app (Xj k)).symm ≪≫ e₂.app (Xj k) ≪≫ (hj k).some⟩

Module documentation

Finite-etale chart models at a common inverse-system stage

Declarations

finiteEtaleHasPullbacksAlongChart

finiteEtaleStableUnderBaseChangeAlongChart

exists_affine_chart_model

exists_common_stage_affine_chart_models