Module

RecoveredFiniteStage.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.FiniteField.RecoveredFiniteStage

8 declarations indexed from sourceView source ↗

Module documentation

Recovered Finite Stage

The actually descended transition with its coefficient structure.

Imports4

Imported by2

def

recoveredStageTransition_structure

L103 ↗

EtaleFundamentalGroups.recoveredStageTransition_structure

Documentation

The descended transition respects the second actual base chart.

Source context 29 commands

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

noncomputable section
open CategoryTheory Limits Opposite AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]
variable (S : Scheme.{u}) (f : S ⟶ Spec (CommRingCat.of k)) (𝒰 : S.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (Z : Over (pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f))
variable (e : ∀ i : 𝒰.I₀,
  (Over.pullback (pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap k L)))
    (𝒰.f i ≫ f))).obj (M i) ≅
      (Over.pullback ((constantFieldOpenCover k L S f 𝒰).f i)).obj Z)
variable (s : Finset L)
local notation "φL" => Spec.map (CommRingCat.ofHom (algebraMap k L))
local notation "E" => IntermediateField.adjoin k (s : Set L)
local notation "φE" => Spec.map (CommRingCat.ofHom
  (algebraMap k (IntermediateField.adjoin k (s : Set L))))
local notation "ψ" => Spec.map (CommRingCat.ofHom
  (AlgHom.toRingHom (IntermediateField.val (IntermediateField.adjoin k (s : Set L)))))
local notation "𝒰E" => constantFieldOpenCover k (IntermediateField.adjoin k (s : Set L)) S f 𝒰
local notation "a" => (fun i : 𝒰.I₀ => Comma.hom (M i) ≫ 𝒰.f i)
local notation "V₀" => (fun ij : 𝒰.I₀ × 𝒰.I₀ =>
  pullback (Comma.hom (M (Prod.fst ij)) ≫ 𝒰.f (Prod.fst ij)) (𝒰.f (Prod.snd ij)))
local notation "p" => (fun ij : 𝒰.I₀ × 𝒰.I₀ =>
  pullback.fst (Comma.hom (M (Prod.fst ij)) ≫ 𝒰.f (Prod.fst ij)) (𝒰.f (Prod.snd ij)) ≫
    (Comma.hom (M (Prod.fst ij)) ≫ 𝒰.f (Prod.fst ij)))
local notation "AE" => (fun i : 𝒰.I₀ => coefficientLocalModelOver φE f (𝒰.f i) (Comma.hom (M i)))
local notation "VE" => (fun ij : 𝒰.I₀ × 𝒰.I₀ =>
  coefficientOverlapOver φE f (𝒰.f (Prod.fst ij)) (𝒰.f (Prod.snd ij)) (Comma.hom (M (Prod.fst ij))))
local notation "dE" => (fun i j : 𝒰.I₀ =>
  coefficientOverlapInclusion φE f (𝒰.f i) (𝒰.f j) (Comma.hom (M i)))
local notation "yE" => (fun i : 𝒰.I₀ =>
  coefficientLocalModelStructure φE f (𝒰.f i) (Comma.hom (M i)))
local notation "ℓE" => (fun i j : 𝒰.I₀ =>
  coefficientOverlapSecondMap φE f (𝒰.f i) (𝒰.f j) (Comma.hom (M i)))
local notation "hVE" => (fun i j : 𝒰.I₀ =>
  coefficientOverlap_isPullback φE f (𝒰.f i) (𝒰.f j) (Comma.hom (M i)))
variable (g : ∀ ij : 𝒰.I₀ × 𝒰.I₀, pullback (Spec.map (CommRingCat.ofHom (algebraMap k
  (IntermediateField.adjoin k (s : Set L))))) ((pullback.fst ((M ij.1).hom ≫ 𝒰.f ij.1) (𝒰.f ij.2)
  ≫ ((M ij.1).hom ≫ 𝒰.f ij.1)) ≫ f) ⟶
  pullback (Spec.map (CommRingCat.ofHom (algebraMap k (IntermediateField.adjoin k (s : Set L)))))
    ((pullback.fst ((M ij.2).hom ≫ 𝒰.f ij.2) (𝒰.f ij.1) ≫ ((M ij.2).hom ≫ 𝒰.f ij.2)) ≫ f))
variable (hgC : ∀ ij : 𝒰.I₀ × 𝒰.I₀,
  g ij ≫ pullback.fst (Spec.map (CommRingCat.ofHom (algebraMap k (IntermediateField.adjoin k (s :
    Set L))))) ((pullback.fst ((M ij.2).hom ≫ 𝒰.f ij.2) (𝒰.f ij.1) ≫ ((M ij.2).hom ≫ 𝒰.f ij.2)) ≫
    f) = pullback.fst (Spec.map (CommRingCat.ofHom (algebraMap k (IntermediateField.adjoin k (s :
    Set L))))) ((pullback.fst ((M ij.1).hom ≫ 𝒰.f ij.1) (𝒰.f ij.2) ≫ ((M ij.1).hom ≫ 𝒰.f ij.1)) ≫
    f))
variable (hgS : ∀ ij : 𝒰.I₀ × 𝒰.I₀,
  g ij ≫ pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap k (IntermediateField.adjoin k (s :
    Set L))))) ((pullback.fst ((M ij.2).hom ≫ 𝒰.f ij.2) (𝒰.f ij.1) ≫ ((M ij.2).hom ≫ 𝒰.f ij.2)) ≫
    f) ≫ (pullback.fst ((M ij.2).hom ≫ 𝒰.f ij.2) (𝒰.f ij.1) ≫ ((M ij.2).hom ≫ 𝒰.f ij.2)) =
    pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap k (IntermediateField.adjoin k (s : Set
      L))))) ((pullback.fst ((M ij.1).hom ≫ 𝒰.f ij.1) (𝒰.f ij.2) ≫ ((M ij.1).hom ≫ 𝒰.f ij.1)) ≫ f)
      ≫ (pullback.fst ((M ij.1).hom ≫ 𝒰.f ij.1) (𝒰.f ij.2) ≫ ((M ij.1).hom ≫ 𝒰.f ij.1)))
variable (hgR : ∀ ij : 𝒰.I₀ × 𝒰.I₀,
  (constantFieldInverseLimitCone k L (pullback ((M ij.1).hom ≫ 𝒰.f ij.1) (𝒰.f ij.2))
    ((pullback.fst ((M ij.1).hom ≫ 𝒰.f ij.1) (𝒰.f ij.2) ≫ ((M ij.1).hom ≫ 𝒰.f ij.1)) ≫ f)).π.app
    (op s) ≫ g ij =
    recoveredCoefficientTransition k L S f 𝒰 M Z e ij.1 ij.2 ≫
      (constantFieldInverseLimitCone k L (pullback ((M ij.2).hom ≫ 𝒰.f ij.2) (𝒰.f ij.1))
        ((pullback.fst ((M ij.2).hom ≫ 𝒰.f ij.2) (𝒰.f ij.1) ≫ ((M ij.2).hom ≫ 𝒰.f ij.2)) ≫
        f)).π.app (op s))
include hgS in

Lean source · statement

theorem recoveredStageTransition_structure (i j : 𝒰.I₀) :
    (recoveredStageTransition k L S f 𝒰 M s g hgC i j).left ≫
      (dE j i).left ≫ yE j = ℓE i j

theorem

recoveredStageTransition_chartMap

L122 ↗

EtaleFundamentalGroups.recoveredStageTransition_chartMap

Documentation

The descended transition recovers the original map to the given scheme.

Source context 29 commands

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

noncomputable section
open CategoryTheory Limits Opposite AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]
variable (S : Scheme.{u}) (f : S ⟶ Spec (CommRingCat.of k)) (𝒰 : S.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (Z : Over (pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f))
variable (e : ∀ i : 𝒰.I₀,
  (Over.pullback (pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap k L)))
    (𝒰.f i ≫ f))).obj (M i) ≅
      (Over.pullback ((constantFieldOpenCover k L S f 𝒰).f i)).obj Z)
variable (s : Finset L)
local notation "φL" => Spec.map (CommRingCat.ofHom (algebraMap k L))
local notation "E" => IntermediateField.adjoin k (s : Set L)
local notation "φE" => Spec.map (CommRingCat.ofHom
  (algebraMap k (IntermediateField.adjoin k (s : Set L))))
local notation "ψ" => Spec.map (CommRingCat.ofHom
  (AlgHom.toRingHom (IntermediateField.val (IntermediateField.adjoin k (s : Set L)))))
local notation "𝒰E" => constantFieldOpenCover k (IntermediateField.adjoin k (s : Set L)) S f 𝒰
local notation "a" => (fun i : 𝒰.I₀ => Comma.hom (M i) ≫ 𝒰.f i)
local notation "V₀" => (fun ij : 𝒰.I₀ × 𝒰.I₀ =>
  pullback (Comma.hom (M (Prod.fst ij)) ≫ 𝒰.f (Prod.fst ij)) (𝒰.f (Prod.snd ij)))
local notation "p" => (fun ij : 𝒰.I₀ × 𝒰.I₀ =>
  pullback.fst (Comma.hom (M (Prod.fst ij)) ≫ 𝒰.f (Prod.fst ij)) (𝒰.f (Prod.snd ij)) ≫
    (Comma.hom (M (Prod.fst ij)) ≫ 𝒰.f (Prod.fst ij)))
local notation "AE" => (fun i : 𝒰.I₀ => coefficientLocalModelOver φE f (𝒰.f i) (Comma.hom (M i)))
local notation "VE" => (fun ij : 𝒰.I₀ × 𝒰.I₀ =>
  coefficientOverlapOver φE f (𝒰.f (Prod.fst ij)) (𝒰.f (Prod.snd ij)) (Comma.hom (M (Prod.fst ij))))
local notation "dE" => (fun i j : 𝒰.I₀ =>
  coefficientOverlapInclusion φE f (𝒰.f i) (𝒰.f j) (Comma.hom (M i)))
local notation "yE" => (fun i : 𝒰.I₀ =>
  coefficientLocalModelStructure φE f (𝒰.f i) (Comma.hom (M i)))
local notation "ℓE" => (fun i j : 𝒰.I₀ =>
  coefficientOverlapSecondMap φE f (𝒰.f i) (𝒰.f j) (Comma.hom (M i)))
local notation "hVE" => (fun i j : 𝒰.I₀ =>
  coefficientOverlap_isPullback φE f (𝒰.f i) (𝒰.f j) (Comma.hom (M i)))
variable (g : ∀ ij : 𝒰.I₀ × 𝒰.I₀, pullback (Spec.map (CommRingCat.ofHom (algebraMap k
  (IntermediateField.adjoin k (s : Set L))))) ((pullback.fst ((M ij.1).hom ≫ 𝒰.f ij.1) (𝒰.f ij.2)
  ≫ ((M ij.1).hom ≫ 𝒰.f ij.1)) ≫ f) ⟶
  pullback (Spec.map (CommRingCat.ofHom (algebraMap k (IntermediateField.adjoin k (s : Set L)))))
    ((pullback.fst ((M ij.2).hom ≫ 𝒰.f ij.2) (𝒰.f ij.1) ≫ ((M ij.2).hom ≫ 𝒰.f ij.2)) ≫ f))
variable (hgC : ∀ ij : 𝒰.I₀ × 𝒰.I₀,
  g ij ≫ pullback.fst (Spec.map (CommRingCat.ofHom (algebraMap k (IntermediateField.adjoin k (s :
    Set L))))) ((pullback.fst ((M ij.2).hom ≫ 𝒰.f ij.2) (𝒰.f ij.1) ≫ ((M ij.2).hom ≫ 𝒰.f ij.2)) ≫
    f) = pullback.fst (Spec.map (CommRingCat.ofHom (algebraMap k (IntermediateField.adjoin k (s :
    Set L))))) ((pullback.fst ((M ij.1).hom ≫ 𝒰.f ij.1) (𝒰.f ij.2) ≫ ((M ij.1).hom ≫ 𝒰.f ij.1)) ≫
    f))
variable (hgS : ∀ ij : 𝒰.I₀ × 𝒰.I₀,
  g ij ≫ pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap k (IntermediateField.adjoin k (s :
    Set L))))) ((pullback.fst ((M ij.2).hom ≫ 𝒰.f ij.2) (𝒰.f ij.1) ≫ ((M ij.2).hom ≫ 𝒰.f ij.2)) ≫
    f) ≫ (pullback.fst ((M ij.2).hom ≫ 𝒰.f ij.2) (𝒰.f ij.1) ≫ ((M ij.2).hom ≫ 𝒰.f ij.2)) =
    pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap k (IntermediateField.adjoin k (s : Set
      L))))) ((pullback.fst ((M ij.1).hom ≫ 𝒰.f ij.1) (𝒰.f ij.2) ≫ ((M ij.1).hom ≫ 𝒰.f ij.1)) ≫ f)
      ≫ (pullback.fst ((M ij.1).hom ≫ 𝒰.f ij.1) (𝒰.f ij.2) ≫ ((M ij.1).hom ≫ 𝒰.f ij.1)))
variable (hgR : ∀ ij : 𝒰.I₀ × 𝒰.I₀,
  (constantFieldInverseLimitCone k L (pullback ((M ij.1).hom ≫ 𝒰.f ij.1) (𝒰.f ij.2))
    ((pullback.fst ((M ij.1).hom ≫ 𝒰.f ij.1) (𝒰.f ij.2) ≫ ((M ij.1).hom ≫ 𝒰.f ij.1)) ≫ f)).π.app
    (op s) ≫ g ij =
    recoveredCoefficientTransition k L S f 𝒰 M Z e ij.1 ij.2 ≫
      (constantFieldInverseLimitCone k L (pullback ((M ij.2).hom ≫ 𝒰.f ij.2) (𝒰.f ij.1))
        ((pullback.fst ((M ij.2).hom ≫ 𝒰.f ij.2) (𝒰.f ij.1) ≫ ((M ij.2).hom ≫ 𝒰.f ij.2)) ≫
        f)).π.app (op s))
include hgR in

Lean source · statement

theorem recoveredStageTransition_chartMap (i j : 𝒰.I₀) :
    (gluingRecoveryFunctor ψ).map (recoveredStageTransition k L S f 𝒰 M s g hgC i j) ≫
      (gluingRecoveryFunctor ψ).map (dE j i) ≫ recoveredStageChartMap k L S f 𝒰 M Z e s j =
    (gluingRecoveryFunctor ψ).map (dE i j) ≫ recoveredStageChartMap k L S f 𝒰 M Z e s i

def

recoveredFiniteStageGlueData_finiteEtale

L158 ↗

EtaleFundamentalGroups.recoveredFiniteStageGlueData_finiteEtale

Documentation

The actual finite-stage gluing data carry a finite étale structural map.

Source context 28 commands

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

noncomputable section
open CategoryTheory Limits Opposite AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]
variable (S : Scheme.{u}) (f : S ⟶ Spec (CommRingCat.of k)) (𝒰 : S.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (Z : Over (pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f))
variable (e : ∀ i : 𝒰.I₀,
  (Over.pullback (pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap k L)))
    (𝒰.f i ≫ f))).obj (M i) ≅
      (Over.pullback ((constantFieldOpenCover k L S f 𝒰).f i)).obj Z)
variable (s : Finset L)
local notation "φL" => Spec.map (CommRingCat.ofHom (algebraMap k L))
local notation "E" => IntermediateField.adjoin k (s : Set L)
local notation "φE" => Spec.map (CommRingCat.ofHom
  (algebraMap k (IntermediateField.adjoin k (s : Set L))))
local notation "ψ" => Spec.map (CommRingCat.ofHom
  (AlgHom.toRingHom (IntermediateField.val (IntermediateField.adjoin k (s : Set L)))))
local notation "𝒰E" => constantFieldOpenCover k (IntermediateField.adjoin k (s : Set L)) S f 𝒰
local notation "a" => (fun i : 𝒰.I₀ => Comma.hom (M i) ≫ 𝒰.f i)
local notation "V₀" => (fun ij : 𝒰.I₀ × 𝒰.I₀ =>
  pullback (Comma.hom (M (Prod.fst ij)) ≫ 𝒰.f (Prod.fst ij)) (𝒰.f (Prod.snd ij)))
local notation "p" => (fun ij : 𝒰.I₀ × 𝒰.I₀ =>
  pullback.fst (Comma.hom (M (Prod.fst ij)) ≫ 𝒰.f (Prod.fst ij)) (𝒰.f (Prod.snd ij)) ≫
    (Comma.hom (M (Prod.fst ij)) ≫ 𝒰.f (Prod.fst ij)))
local notation "AE" => (fun i : 𝒰.I₀ => coefficientLocalModelOver φE f (𝒰.f i) (Comma.hom (M i)))
local notation "VE" => (fun ij : 𝒰.I₀ × 𝒰.I₀ =>
  coefficientOverlapOver φE f (𝒰.f (Prod.fst ij)) (𝒰.f (Prod.snd ij)) (Comma.hom (M (Prod.fst ij))))
local notation "dE" => (fun i j : 𝒰.I₀ =>
  coefficientOverlapInclusion φE f (𝒰.f i) (𝒰.f j) (Comma.hom (M i)))
local notation "yE" => (fun i : 𝒰.I₀ =>
  coefficientLocalModelStructure φE f (𝒰.f i) (Comma.hom (M i)))
local notation "ℓE" => (fun i j : 𝒰.I₀ =>
  coefficientOverlapSecondMap φE f (𝒰.f i) (𝒰.f j) (Comma.hom (M i)))
local notation "hVE" => (fun i j : 𝒰.I₀ =>
  coefficientOverlap_isPullback φE f (𝒰.f i) (𝒰.f j) (Comma.hom (M i)))
variable (g : ∀ ij : 𝒰.I₀ × 𝒰.I₀, pullback (Spec.map (CommRingCat.ofHom (algebraMap k
  (IntermediateField.adjoin k (s : Set L))))) ((pullback.fst ((M ij.1).hom ≫ 𝒰.f ij.1) (𝒰.f ij.2)
  ≫ ((M ij.1).hom ≫ 𝒰.f ij.1)) ≫ f) ⟶
  pullback (Spec.map (CommRingCat.ofHom (algebraMap k (IntermediateField.adjoin k (s : Set L)))))
    ((pullback.fst ((M ij.2).hom ≫ 𝒰.f ij.2) (𝒰.f ij.1) ≫ ((M ij.2).hom ≫ 𝒰.f ij.2)) ≫ f))
variable (hgC : ∀ ij : 𝒰.I₀ × 𝒰.I₀,
  g ij ≫ pullback.fst (Spec.map (CommRingCat.ofHom (algebraMap k (IntermediateField.adjoin k (s :
    Set L))))) ((pullback.fst ((M ij.2).hom ≫ 𝒰.f ij.2) (𝒰.f ij.1) ≫ ((M ij.2).hom ≫ 𝒰.f ij.2)) ≫
    f) = pullback.fst (Spec.map (CommRingCat.ofHom (algebraMap k (IntermediateField.adjoin k (s :
    Set L))))) ((pullback.fst ((M ij.1).hom ≫ 𝒰.f ij.1) (𝒰.f ij.2) ≫ ((M ij.1).hom ≫ 𝒰.f ij.1)) ≫
    f))
variable (hgS : ∀ ij : 𝒰.I₀ × 𝒰.I₀,
  g ij ≫ pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap k (IntermediateField.adjoin k (s :
    Set L))))) ((pullback.fst ((M ij.2).hom ≫ 𝒰.f ij.2) (𝒰.f ij.1) ≫ ((M ij.2).hom ≫ 𝒰.f ij.2)) ≫
    f) ≫ (pullback.fst ((M ij.2).hom ≫ 𝒰.f ij.2) (𝒰.f ij.1) ≫ ((M ij.2).hom ≫ 𝒰.f ij.2)) =
    pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap k (IntermediateField.adjoin k (s : Set
      L))))) ((pullback.fst ((M ij.1).hom ≫ 𝒰.f ij.1) (𝒰.f ij.2) ≫ ((M ij.1).hom ≫ 𝒰.f ij.1)) ≫ f)
      ≫ (pullback.fst ((M ij.1).hom ≫ 𝒰.f ij.1) (𝒰.f ij.2) ≫ ((M ij.1).hom ≫ 𝒰.f ij.1)))
variable (hgR : ∀ ij : 𝒰.I₀ × 𝒰.I₀,
  (constantFieldInverseLimitCone k L (pullback ((M ij.1).hom ≫ 𝒰.f ij.1) (𝒰.f ij.2))
    ((pullback.fst ((M ij.1).hom ≫ 𝒰.f ij.1) (𝒰.f ij.2) ≫ ((M ij.1).hom ≫ 𝒰.f ij.1)) ≫ f)).π.app
    (op s) ≫ g ij =
    recoveredCoefficientTransition k L S f 𝒰 M Z e ij.1 ij.2 ≫
      (constantFieldInverseLimitCone k L (pullback ((M ij.2).hom ≫ 𝒰.f ij.2) (𝒰.f ij.1))
        ((pullback.fst ((M ij.2).hom ≫ 𝒰.f ij.2) (𝒰.f ij.1) ≫ ((M ij.2).hom ≫ 𝒰.f ij.2)) ≫
        f)).π.app (op s))

Lean source · statement

theorem recoveredFiniteStageGlueData_finiteEtale [∀ i : 𝒰.I₀, IsFiniteEtale (M i).hom] :
    ∃ q : (recoveredFiniteStageGlueData k L S f 𝒰 M Z e s g hgC hgS hgR).glued ⟶
        pullback φE f,
      IsFiniteEtale q ∧ ∀ i : 𝒰.I₀,
        IsPullback (yE i)
          ((recoveredFiniteStageGlueData k L S f 𝒰 M Z e s g hgC hgS hgR).ι i)
          ((𝒰E).f i) q

theorem

exists_finiteIntermediateField_recovered_glueData

L185 ↗

EtaleFundamentalGroups.exists_finiteIntermediateField_recovered_glueData

Documentation

The actual recovered finite family admits one finite coefficient stage with actual gluing data and a finite étale glued scheme. The descended transitions and their recovery equations are retained for global recovery.

Source context 28 commands

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

noncomputable section
open CategoryTheory Limits Opposite AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]
variable (S : Scheme.{u}) (f : S ⟶ Spec (CommRingCat.of k)) (𝒰 : S.OpenCover)
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i))
variable (Z : Over (pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f))
variable (e : ∀ i : 𝒰.I₀,
  (Over.pullback (pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap k L)))
    (𝒰.f i ≫ f))).obj (M i) ≅
      (Over.pullback ((constantFieldOpenCover k L S f 𝒰).f i)).obj Z)
variable (s : Finset L)
local notation "φL" => Spec.map (CommRingCat.ofHom (algebraMap k L))
local notation "E" => IntermediateField.adjoin k (s : Set L)
local notation "φE" => Spec.map (CommRingCat.ofHom
  (algebraMap k (IntermediateField.adjoin k (s : Set L))))
local notation "ψ" => Spec.map (CommRingCat.ofHom
  (AlgHom.toRingHom (IntermediateField.val (IntermediateField.adjoin k (s : Set L)))))
local notation "𝒰E" => constantFieldOpenCover k (IntermediateField.adjoin k (s : Set L)) S f 𝒰
local notation "a" => (fun i : 𝒰.I₀ => Comma.hom (M i) ≫ 𝒰.f i)
local notation "V₀" => (fun ij : 𝒰.I₀ × 𝒰.I₀ =>
  pullback (Comma.hom (M (Prod.fst ij)) ≫ 𝒰.f (Prod.fst ij)) (𝒰.f (Prod.snd ij)))
local notation "p" => (fun ij : 𝒰.I₀ × 𝒰.I₀ =>
  pullback.fst (Comma.hom (M (Prod.fst ij)) ≫ 𝒰.f (Prod.fst ij)) (𝒰.f (Prod.snd ij)) ≫
    (Comma.hom (M (Prod.fst ij)) ≫ 𝒰.f (Prod.fst ij)))
local notation "AE" => (fun i : 𝒰.I₀ => coefficientLocalModelOver φE f (𝒰.f i) (Comma.hom (M i)))
local notation "VE" => (fun ij : 𝒰.I₀ × 𝒰.I₀ =>
  coefficientOverlapOver φE f (𝒰.f (Prod.fst ij)) (𝒰.f (Prod.snd ij)) (Comma.hom (M (Prod.fst ij))))
local notation "dE" => (fun i j : 𝒰.I₀ =>
  coefficientOverlapInclusion φE f (𝒰.f i) (𝒰.f j) (Comma.hom (M i)))
local notation "yE" => (fun i : 𝒰.I₀ =>
  coefficientLocalModelStructure φE f (𝒰.f i) (Comma.hom (M i)))
local notation "ℓE" => (fun i j : 𝒰.I₀ =>
  coefficientOverlapSecondMap φE f (𝒰.f i) (𝒰.f j) (Comma.hom (M i)))
local notation "hVE" => (fun i j : 𝒰.I₀ =>
  coefficientOverlap_isPullback φE f (𝒰.f i) (𝒰.f j) (Comma.hom (M i)))
variable (g : ∀ ij : 𝒰.I₀ × 𝒰.I₀, pullback (Spec.map (CommRingCat.ofHom (algebraMap k
  (IntermediateField.adjoin k (s : Set L))))) ((pullback.fst ((M ij.1).hom ≫ 𝒰.f ij.1) (𝒰.f ij.2)
  ≫ ((M ij.1).hom ≫ 𝒰.f ij.1)) ≫ f) ⟶
  pullback (Spec.map (CommRingCat.ofHom (algebraMap k (IntermediateField.adjoin k (s : Set L)))))
    ((pullback.fst ((M ij.2).hom ≫ 𝒰.f ij.2) (𝒰.f ij.1) ≫ ((M ij.2).hom ≫ 𝒰.f ij.2)) ≫ f))
variable (hgC : ∀ ij : 𝒰.I₀ × 𝒰.I₀,
  g ij ≫ pullback.fst (Spec.map (CommRingCat.ofHom (algebraMap k (IntermediateField.adjoin k (s :
    Set L))))) ((pullback.fst ((M ij.2).hom ≫ 𝒰.f ij.2) (𝒰.f ij.1) ≫ ((M ij.2).hom ≫ 𝒰.f ij.2)) ≫
    f) = pullback.fst (Spec.map (CommRingCat.ofHom (algebraMap k (IntermediateField.adjoin k (s :
    Set L))))) ((pullback.fst ((M ij.1).hom ≫ 𝒰.f ij.1) (𝒰.f ij.2) ≫ ((M ij.1).hom ≫ 𝒰.f ij.1)) ≫
    f))
variable (hgS : ∀ ij : 𝒰.I₀ × 𝒰.I₀,
  g ij ≫ pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap k (IntermediateField.adjoin k (s :
    Set L))))) ((pullback.fst ((M ij.2).hom ≫ 𝒰.f ij.2) (𝒰.f ij.1) ≫ ((M ij.2).hom ≫ 𝒰.f ij.2)) ≫
    f) ≫ (pullback.fst ((M ij.2).hom ≫ 𝒰.f ij.2) (𝒰.f ij.1) ≫ ((M ij.2).hom ≫ 𝒰.f ij.2)) =
    pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap k (IntermediateField.adjoin k (s : Set
      L))))) ((pullback.fst ((M ij.1).hom ≫ 𝒰.f ij.1) (𝒰.f ij.2) ≫ ((M ij.1).hom ≫ 𝒰.f ij.1)) ≫ f)
      ≫ (pullback.fst ((M ij.1).hom ≫ 𝒰.f ij.1) (𝒰.f ij.2) ≫ ((M ij.1).hom ≫ 𝒰.f ij.1)))
variable (hgR : ∀ ij : 𝒰.I₀ × 𝒰.I₀,
  (constantFieldInverseLimitCone k L (pullback ((M ij.1).hom ≫ 𝒰.f ij.1) (𝒰.f ij.2))
    ((pullback.fst ((M ij.1).hom ≫ 𝒰.f ij.1) (𝒰.f ij.2) ≫ ((M ij.1).hom ≫ 𝒰.f ij.1)) ≫ f)).π.app
    (op s) ≫ g ij =
    recoveredCoefficientTransition k L S f 𝒰 M Z e ij.1 ij.2 ≫
      (constantFieldInverseLimitCone k L (pullback ((M ij.2).hom ≫ 𝒰.f ij.2) (𝒰.f ij.1))
        ((pullback.fst ((M ij.2).hom ≫ 𝒰.f ij.2) (𝒰.f ij.1) ≫ ((M ij.2).hom ≫ 𝒰.f ij.2)) ≫
        f)).π.app (op s))

Lean source · full declaration

theorem exists_finiteIntermediateField_recovered_glueData
    [Algebra.IsAlgebraic k L] [QuasiSeparatedSpace S]
    [Finite 𝒰.I₀] [∀ i : 𝒰.I₀, IsAffine (𝒰.X i)]
    [∀ i : 𝒰.I₀, IsFiniteEtale (M i).hom] :
    ∃ s₀ : Finset L, FiniteDimensional k (IntermediateField.adjoin k (s₀ : Set L)) ∧
      ∃ g₀ : ∀ ij : 𝒰.I₀ × 𝒰.I₀,
        pullback (Spec.map (CommRingCat.ofHom
          (algebraMap k (IntermediateField.adjoin k (s₀ : Set L))))) (p ij ≫ f) ⟶
        pullback (Spec.map (CommRingCat.ofHom
          (algebraMap k (IntermediateField.adjoin k (s₀ : Set L))))) (p (ij.2, ij.1) ≫ f),
      ∃ hg₀ : ∀ ij : 𝒰.I₀ × 𝒰.I₀,
        g₀ ij ≫ pullback.fst _ (p (ij.2, ij.1) ≫ f) = pullback.fst _ (p ij ≫ f) ∧
        g₀ ij ≫ pullback.snd _ (p (ij.2, ij.1) ≫ f) ≫ p (ij.2, ij.1) =
          pullback.snd _ (p ij ≫ f) ≫ p ij ∧
        (constantFieldInverseLimitCone k L (V₀ ij) (p ij ≫ f)).π.app (op s₀) ≫ g₀ ij =
          recoveredCoefficientTransition k L S f 𝒰 M Z e ij.1 ij.2 ≫
            (constantFieldInverseLimitCone k L (V₀ (ij.2, ij.1))
              (p (ij.2, ij.1) ≫ f)).π.app (op s₀),
      ∃ q : (recoveredFiniteStageGlueData k L S f 𝒰 M Z e s₀ g₀
          (fun ij => (hg₀ ij).1) (fun ij => (hg₀ ij).2.1) (fun ij => (hg₀ ij).2.2)).glued ⟶
        pullback (Spec.map (CommRingCat.ofHom
          (algebraMap k (IntermediateField.adjoin k (s₀ : Set L))))) f,
        IsFiniteEtale q ∧ ∀ i : 𝒰.I₀,
          IsPullback (coefficientLocalModelStructure (Spec.map (CommRingCat.ofHom
            (algebraMap k (IntermediateField.adjoin k (s₀ : Set L))))) f (𝒰.f i) (M i).hom)
            ((recoveredFiniteStageGlueData k L S f 𝒰 M Z e s₀ g₀
              (fun ij => (hg₀ ij).1) (fun ij => (hg₀ ij).2.1) (fun ij => (hg₀ ij).2.2)).ι i)
            ((constantFieldOpenCover k (IntermediateField.adjoin k (s₀ : Set L)) S f 𝒰).f i) q := by
  obtain ⟨s₀, hfin, g₀, hg₀⟩ :=
    exists_finiteIntermediateField_overlap_transitions k L S f 𝒰 M Z e
  refine ⟨s₀, hfin, g₀, hg₀, ?_⟩
  exact recoveredFiniteStageGlueData_finiteEtale k L S f 𝒰 M Z e s₀ g₀
    (fun ij => (hg₀ ij).1) (fun ij => (hg₀ ij).2.1) (fun ij => (hg₀ ij).2.2)

Module documentation

Recovered Finite Stage

Declarations