NYLL
Module

PurelyInseparableGluing.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.FiniteField.PurelyInseparableGluing
15 declarations indexed from sourceView source ↗

Module documentation

Gluing finite étale models across purely inseparable extensions

Imports8
Imported by3

Declarations

instance

gluingOverlapOver_etale

L61 ↗
EtaleFundamentalGroups.gluingOverlapOver_etale
Source context 9 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {X Y : Scheme.{u}} (ψ : Y ⟶ X) (𝒰 : X.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (Z : Over Y)
variable (e : ∀ i : 𝒰.I₀,
  (Over.pullback (pullback.fst (𝒰.f i) ψ)).obj (M i) ≅
    (Over.pullback (pullback.snd (𝒰.f i) ψ)).obj Z)
variable [hM : ∀ i : 𝒰.I₀, IsFiniteEtale (M i).hom]
Lean source · statement
instance gluingOverlapOver_etale (i j : 𝒰.I₀) : Etale (gluingOverlapOver 𝒰 M (i, j)).hom
def

descendedGluingTransition

L68 ↗
EtaleFundamentalGroups.descendedGluingTransition
Documentation

The unique transition recovered by fully faithful radicial pullback.

Source context 10 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {X Y : Scheme.{u}} (ψ : Y ⟶ X) (𝒰 : X.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (Z : Over Y)
variable (e : ∀ i : 𝒰.I₀,
  (Over.pullback (pullback.fst (𝒰.f i) ψ)).obj (M i) ≅
    (Over.pullback (pullback.snd (𝒰.f i) ψ)).obj Z)
variable [hM : ∀ i : 𝒰.I₀, IsFiniteEtale (M i).hom]
variable [IsIntegralHom ψ] [UniversallyInjective ψ] [Surjective ψ]
Lean source · statement
def descendedGluingTransition (i j : 𝒰.I₀) :
    gluingOverlapOver 𝒰 M (i, j) ⟶ gluingOverlapOver 𝒰 M (j, i)
theorem

descendedGluingTransition_recovery

L74 ↗
EtaleFundamentalGroups.descendedGluingTransition_recovery
Source context 10 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {X Y : Scheme.{u}} (ψ : Y ⟶ X) (𝒰 : X.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (Z : Over Y)
variable (e : ∀ i : 𝒰.I₀,
  (Over.pullback (pullback.fst (𝒰.f i) ψ)).obj (M i) ≅
    (Over.pullback (pullback.snd (𝒰.f i) ψ)).obj Z)
variable [hM : ∀ i : 𝒰.I₀, IsFiniteEtale (M i).hom]
variable [IsIntegralHom ψ] [UniversallyInjective ψ] [Surjective ψ]
Lean source · statement
theorem descendedGluingTransition_recovery (i j : 𝒰.I₀) :
    (Over.pullback ψ).map (descendedGluingTransition ψ 𝒰 M Z e i j) =
      recoveredPullbackTransition ψ 𝒰 M Z e i j
theorem

descendedGluingTransition_structure

L81 ↗
EtaleFundamentalGroups.descendedGluingTransition_structure
Source context 10 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {X Y : Scheme.{u}} (ψ : Y ⟶ X) (𝒰 : X.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (Z : Over Y)
variable (e : ∀ i : 𝒰.I₀,
  (Over.pullback (pullback.fst (𝒰.f i) ψ)).obj (M i) ≅
    (Over.pullback (pullback.snd (𝒰.f i) ψ)).obj Z)
variable [hM : ∀ i : 𝒰.I₀, IsFiniteEtale (M i).hom]
variable [IsIntegralHom ψ] [UniversallyInjective ψ] [Surjective ψ]
Lean source · statement
theorem descendedGluingTransition_structure (i j : 𝒰.I₀) :
    (descendedGluingTransition ψ 𝒰 M Z e i j).left ≫
      (gluingOverlapFirst 𝒰 M j i).left ≫ (M j).hom =
        pullback.snd ((M i).hom ≫ 𝒰.f i) (𝒰.f j)
theorem

descendedGluingTransition_chartMap

L93 ↗
EtaleFundamentalGroups.descendedGluingTransition_chartMap
Source context 10 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {X Y : Scheme.{u}} (ψ : Y ⟶ X) (𝒰 : X.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (Z : Over Y)
variable (e : ∀ i : 𝒰.I₀,
  (Over.pullback (pullback.fst (𝒰.f i) ψ)).obj (M i) ≅
    (Over.pullback (pullback.snd (𝒰.f i) ψ)).obj Z)
variable [hM : ∀ i : 𝒰.I₀, IsFiniteEtale (M i).hom]
variable [IsIntegralHom ψ] [UniversallyInjective ψ] [Surjective ψ]
Lean source · statement
theorem descendedGluingTransition_chartMap (i j : 𝒰.I₀) :
    ((Over.pullback ψ).map (descendedGluingTransition ψ 𝒰 M Z e i j)).left ≫
      ((Over.pullback ψ).map (gluingOverlapFirst 𝒰 M j i)).left ≫
        recoveredPullbackChartMap ψ 𝒰 M Z e j =
      ((Over.pullback ψ).map (gluingOverlapFirst 𝒰 M i j)).left ≫
        recoveredPullbackChartMap ψ 𝒰 M Z e i
instance

recoveredPullbackChartMap_mono

L102 ↗
EtaleFundamentalGroups.recoveredPullbackChartMap_mono
Source context 10 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {X Y : Scheme.{u}} (ψ : Y ⟶ X) (𝒰 : X.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (Z : Over Y)
variable (e : ∀ i : 𝒰.I₀,
  (Over.pullback (pullback.fst (𝒰.f i) ψ)).obj (M i) ≅
    (Over.pullback (pullback.snd (𝒰.f i) ψ)).obj Z)
variable [hM : ∀ i : 𝒰.I₀, IsFiniteEtale (M i).hom]
variable [IsIntegralHom ψ] [UniversallyInjective ψ] [Surjective ψ]
Lean source · statement
instance recoveredPullbackChartMap_mono (i : 𝒰.I₀) :
    Mono (recoveredPullbackChartMap ψ 𝒰 M Z e i)
theorem

gluingRecoveryFunctor_overlap_injective

L108 ↗
EtaleFundamentalGroups.gluingRecoveryFunctor_overlap_injective
Documentation

Recovery is injective on maps into each actual separated étale overlap.

Source context 11 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {X Y : Scheme.{u}} (ψ : Y ⟶ X) (𝒰 : X.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (Z : Over Y)
variable (e : ∀ i : 𝒰.I₀,
  (Over.pullback (pullback.fst (𝒰.f i) ψ)).obj (M i) ≅
    (Over.pullback (pullback.snd (𝒰.f i) ψ)).obj Z)
variable [hM : ∀ i : 𝒰.I₀, IsFiniteEtale (M i).hom]
variable [IsIntegralHom ψ] [UniversallyInjective ψ] [Surjective ψ]
local instance recoveredPullbackChartMap_mono (i : 𝒰.I₀) :
    Mono (recoveredPullbackChartMap ψ 𝒰 M Z e i) := by
  have := recoveredPullbackChartMap_isOpenImmersion ψ 𝒰 M Z e i
  infer_instance
Lean source · statement
theorem gluingRecoveryFunctor_overlap_injective (T : Over X) (i j : 𝒰.I₀) :
    Function.Injective ((gluingRecoveryFunctor ψ).map
      (X := T) (Y := gluingOverlapOver 𝒰 M (i, j)))
def

radicialLocalModelGlueData

L121 ↗
EtaleFundamentalGroups.radicialLocalModelGlueData
Documentation

Gluing data for the local models and their descended transitions.

Source context 11 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {X Y : Scheme.{u}} (ψ : Y ⟶ X) (𝒰 : X.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (Z : Over Y)
variable (e : ∀ i : 𝒰.I₀,
  (Over.pullback (pullback.fst (𝒰.f i) ψ)).obj (M i) ≅
    (Over.pullback (pullback.snd (𝒰.f i) ψ)).obj Z)
variable [hM : ∀ i : 𝒰.I₀, IsFiniteEtale (M i).hom]
variable [IsIntegralHom ψ] [UniversallyInjective ψ] [Surjective ψ]
local instance recoveredPullbackChartMap_mono (i : 𝒰.I₀) :
    Mono (recoveredPullbackChartMap ψ 𝒰 M Z e i) := by
  have := recoveredPullbackChartMap_isOpenImmersion ψ 𝒰 M Z e i
  infer_instance
Lean source · statement
def radicialLocalModelGlueData : Scheme.GlueData.{u}
theorem

exists_finiteEtale_radicialLocalModelGlueData

L131 ↗
EtaleFundamentalGroups.exists_finiteEtale_radicialLocalModelGlueData
Source context 12 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {X Y : Scheme.{u}} (ψ : Y ⟶ X) (𝒰 : X.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (Z : Over Y)
variable (e : ∀ i : 𝒰.I₀,
  (Over.pullback (pullback.fst (𝒰.f i) ψ)).obj (M i) ≅
    (Over.pullback (pullback.snd (𝒰.f i) ψ)).obj Z)
variable [hM : ∀ i : 𝒰.I₀, IsFiniteEtale (M i).hom]
variable [IsIntegralHom ψ] [UniversallyInjective ψ] [Surjective ψ]
local instance recoveredPullbackChartMap_mono (i : 𝒰.I₀) :
    Mono (recoveredPullbackChartMap ψ 𝒰 M Z e i) := by
  have := recoveredPullbackChartMap_isOpenImmersion ψ 𝒰 M Z e i
  infer_instance
include hM in
Lean source · statement
theorem exists_finiteEtale_radicialLocalModelGlueData :
    ∃ q : (radicialLocalModelGlueData ψ 𝒰 M Z e).glued ⟶ X,
      IsFiniteEtale q ∧ ∀ i : 𝒰.I₀,
        IsPullback (M i).hom ((radicialLocalModelGlueData ψ 𝒰 M Z e).ι i) (𝒰.f i) q
theorem

descendedGluingTransition_isPullback

L146 ↗
EtaleFundamentalGroups.descendedGluingTransition_isPullback
Documentation

The recovered raw overlap is the intersection of the two recovered charts.

Source context 11 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {X Y : Scheme.{u}} (ψ : Y ⟶ X) (𝒰 : X.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (Z : Over Y)
variable (e : ∀ i : 𝒰.I₀,
  (Over.pullback (pullback.fst (𝒰.f i) ψ)).obj (M i) ≅
    (Over.pullback (pullback.snd (𝒰.f i) ψ)).obj Z)
variable [hM : ∀ i : 𝒰.I₀, IsFiniteEtale (M i).hom]
variable [IsIntegralHom ψ] [UniversallyInjective ψ] [Surjective ψ]
local instance recoveredPullbackChartMap_mono (i : 𝒰.I₀) :
    Mono (recoveredPullbackChartMap ψ 𝒰 M Z e i) := by
  have := recoveredPullbackChartMap_isOpenImmersion ψ 𝒰 M Z e i
  infer_instance
Lean source · statement
theorem descendedGluingTransition_isPullback (i j : 𝒰.I₀) :
    IsPullback ((Over.pullback ψ).map (gluingOverlapFirst 𝒰 M i j)).left
      ((Over.pullback ψ).map
        (descendedGluingTransition ψ 𝒰 M Z e i j ≫ gluingOverlapFirst 𝒰 M j i)).left
      (recoveredPullbackChartMap ψ 𝒰 M Z e i)
      (recoveredPullbackChartMap ψ 𝒰 M Z e j)
def

radicialGluedChartInclusion

L177 ↗
EtaleFundamentalGroups.radicialGluedChartInclusion
Documentation

The inclusion of a local model into the glued relative scheme.

Source context 13 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {X Y : Scheme.{u}} (ψ : Y ⟶ X) (𝒰 : X.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (Z : Over Y)
variable (e : ∀ i : 𝒰.I₀,
  (Over.pullback (pullback.fst (𝒰.f i) ψ)).obj (M i) ≅
    (Over.pullback (pullback.snd (𝒰.f i) ψ)).obj Z)
variable [hM : ∀ i : 𝒰.I₀, IsFiniteEtale (M i).hom]
variable [IsIntegralHom ψ] [UniversallyInjective ψ] [Surjective ψ]
local instance recoveredPullbackChartMap_mono (i : 𝒰.I₀) :
    Mono (recoveredPullbackChartMap ψ 𝒰 M Z e i) := by
  have := recoveredPullbackChartMap_isOpenImmersion ψ 𝒰 M Z e i
  infer_instance
variable (q : (radicialLocalModelGlueData ψ 𝒰 M Z e).glued ⟶ X)
variable (hq : ∀ i : 𝒰.I₀,
  IsPullback (M i).hom ((radicialLocalModelGlueData ψ 𝒰 M Z e).ι i) (𝒰.f i) q)
Lean source · statement
def radicialGluedChartInclusion (i : 𝒰.I₀) : gluingLocalOver 𝒰 M i ⟶ Over.mk q
def

radicialGluedPullbackCover

L181 ↗
EtaleFundamentalGroups.radicialGluedPullbackCover
Documentation

The open cover of the glued scheme after coefficient pullback.

Source context 13 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {X Y : Scheme.{u}} (ψ : Y ⟶ X) (𝒰 : X.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (Z : Over Y)
variable (e : ∀ i : 𝒰.I₀,
  (Over.pullback (pullback.fst (𝒰.f i) ψ)).obj (M i) ≅
    (Over.pullback (pullback.snd (𝒰.f i) ψ)).obj Z)
variable [hM : ∀ i : 𝒰.I₀, IsFiniteEtale (M i).hom]
variable [IsIntegralHom ψ] [UniversallyInjective ψ] [Surjective ψ]
local instance recoveredPullbackChartMap_mono (i : 𝒰.I₀) :
    Mono (recoveredPullbackChartMap ψ 𝒰 M Z e i) := by
  have := recoveredPullbackChartMap_isOpenImmersion ψ 𝒰 M Z e i
  infer_instance
variable (q : (radicialLocalModelGlueData ψ 𝒰 M Z e).glued ⟶ X)
variable (hq : ∀ i : 𝒰.I₀,
  IsPullback (M i).hom ((radicialLocalModelGlueData ψ 𝒰 M Z e).ι i) (𝒰.f i) q)
Lean source · statement
def radicialGluedPullbackCover : ((Over.pullback ψ).obj (Over.mk q)).left.OpenCover
theorem

radicialGluedPullbackCover_isPullback

L188 ↗
EtaleFundamentalGroups.radicialGluedPullbackCover_isPullback
Source context 13 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {X Y : Scheme.{u}} (ψ : Y ⟶ X) (𝒰 : X.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (Z : Over Y)
variable (e : ∀ i : 𝒰.I₀,
  (Over.pullback (pullback.fst (𝒰.f i) ψ)).obj (M i) ≅
    (Over.pullback (pullback.snd (𝒰.f i) ψ)).obj Z)
variable [hM : ∀ i : 𝒰.I₀, IsFiniteEtale (M i).hom]
variable [IsIntegralHom ψ] [UniversallyInjective ψ] [Surjective ψ]
local instance recoveredPullbackChartMap_mono (i : 𝒰.I₀) :
    Mono (recoveredPullbackChartMap ψ 𝒰 M Z e i) := by
  have := recoveredPullbackChartMap_isOpenImmersion ψ 𝒰 M Z e i
  infer_instance
variable (q : (radicialLocalModelGlueData ψ 𝒰 M Z e).glued ⟶ X)
variable (hq : ∀ i : 𝒰.I₀,
  IsPullback (M i).hom ((radicialLocalModelGlueData ψ 𝒰 M Z e).ι i) (𝒰.f i) q)
Lean source · statement
theorem radicialGluedPullbackCover_isPullback (i j : 𝒰.I₀) :
    IsPullback ((Over.pullback ψ).map (gluingOverlapFirst 𝒰 M i j)).left
      ((Over.pullback ψ).map
        (descendedGluingTransition ψ 𝒰 M Z e i j ≫ gluingOverlapFirst 𝒰 M j i)).left
      ((Over.pullback ψ).map (radicialGluedChartInclusion ψ 𝒰 M Z e q hq i)).left
      ((Over.pullback ψ).map (radicialGluedChartInclusion ψ 𝒰 M Z e q hq j)).left
theorem

nonempty_radicialGluedPullback_iso

L203 ↗
EtaleFundamentalGroups.nonempty_radicialGluedPullback_iso
Source context 14 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {X Y : Scheme.{u}} (ψ : Y ⟶ X) (𝒰 : X.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (Z : Over Y)
variable (e : ∀ i : 𝒰.I₀,
  (Over.pullback (pullback.fst (𝒰.f i) ψ)).obj (M i) ≅
    (Over.pullback (pullback.snd (𝒰.f i) ψ)).obj Z)
variable [hM : ∀ i : 𝒰.I₀, IsFiniteEtale (M i).hom]
variable [IsIntegralHom ψ] [UniversallyInjective ψ] [Surjective ψ]
local instance recoveredPullbackChartMap_mono (i : 𝒰.I₀) :
    Mono (recoveredPullbackChartMap ψ 𝒰 M Z e i) := by
  have := recoveredPullbackChartMap_isOpenImmersion ψ 𝒰 M Z e i
  infer_instance
variable (q : (radicialLocalModelGlueData ψ 𝒰 M Z e).glued ⟶ X)
variable (hq : ∀ i : 𝒰.I₀,
  IsPullback (M i).hom ((radicialLocalModelGlueData ψ 𝒰 M Z e).ι i) (𝒰.f i) q)
include hq in
Lean source · statement
theorem nonempty_radicialGluedPullback_iso :
    Nonempty ((Over.pullback ψ).obj (Over.mk q) ≅ Z)
theorem

exists_finiteEtale_model_of_local_models

L230 ↗
EtaleFundamentalGroups.exists_finiteEtale_model_of_local_models
Documentation

Actual finite étale local models with actual recovery glue to a global model along a universal homeomorphism.

Source context 14 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable {X Y : Scheme.{u}} (ψ : Y ⟶ X) (𝒰 : X.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (Z : Over Y)
variable (e : ∀ i : 𝒰.I₀,
  (Over.pullback (pullback.fst (𝒰.f i) ψ)).obj (M i) ≅
    (Over.pullback (pullback.snd (𝒰.f i) ψ)).obj Z)
variable [hM : ∀ i : 𝒰.I₀, IsFiniteEtale (M i).hom]
variable [IsIntegralHom ψ] [UniversallyInjective ψ] [Surjective ψ]
local instance recoveredPullbackChartMap_mono (i : 𝒰.I₀) :
    Mono (recoveredPullbackChartMap ψ 𝒰 M Z e i) := by
  have := recoveredPullbackChartMap_isOpenImmersion ψ 𝒰 M Z e i
  infer_instance
variable (q : (radicialLocalModelGlueData ψ 𝒰 M Z e).glued ⟶ X)
variable (hq : ∀ i : 𝒰.I₀,
  IsPullback (M i).hom ((radicialLocalModelGlueData ψ 𝒰 M Z e).ι i) (𝒰.f i) q)
include hM e in
Lean source · statement
theorem exists_finiteEtale_model_of_local_models :
    ∃ N : FiniteEtale X,
      Nonempty ((Over.pullback ψ).obj ((FiniteEtale.forget X).obj N) ≅ Z)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.