NYLL
Module

RecoveredStageRecovery.lean

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

Module documentation

Recovered Stage Recovery

The actual recovered finite-stage charts form an open cover of the input scheme.

Imports4
Imported by2

Declarations

def

recoveredStageChartCover

L84 ↗
EtaleFundamentalGroups.recoveredStageChartCover
Documentation

The actual recovered finite-stage charts form an open cover of the input scheme.

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
def recoveredStageChartCover : Z.left.OpenCover
theorem

recoveredStageChartMap_isOpenImmersion

L93 ↗
EtaleFundamentalGroups.recoveredStageChartMap_isOpenImmersion
Documentation

The recovered finite-stage chart maps are open immersions.

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 recoveredStageChartMap_isOpenImmersion (i : 𝒰.I₀) :
    IsOpenImmersion (recoveredStageChartMap k L S f 𝒰 M Z e s i)
theorem

recoveredStageTransition_isPullback

L100 ↗
EtaleFundamentalGroups.recoveredStageTransition_isPullback
Documentation

The actual pulled-back finite-stage overlaps are the intersections of the recovered finite-stage charts in the input 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_isPullback (i j : 𝒰.I₀) :
    IsPullback ((Over.pullback ψ).map (dE i j)).left
      ((Over.pullback ψ).map (recoveredStageTransition k L S f 𝒰 M s g hgC i j ≫ dE j i)).left
      (recoveredStageChartMap k L S f 𝒰 M Z e s i)
      (recoveredStageChartMap k L S f 𝒰 M Z e s j)
theorem

coefficientModelMap_stage_naturality

L141 ↗
EtaleFundamentalGroups.coefficientModelMap_stage_naturality
Documentation

The actual coefficient cone maps commute with the coefficient extension of a map to the base scheme.

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 coefficientModelMap_stage_naturality (Y : Scheme.{u}) (b : Y ⟶ S) :
    (constantFieldInverseLimitCone k L Y (b ≫ f)).π.app (op s) ≫
      coefficientModelMap φE f b =
    coefficientModelMap φL f b ≫ (constantFieldInverseLimitCone k L S f).π.app (op s)
theorem

recoveredCoefficientChartMap_structure

L165 ↗
EtaleFundamentalGroups.recoveredCoefficientChartMap_structure
Documentation

The original recovered coefficient chart has its actual map to the extended base.

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 recoveredCoefficientChartMap_structure (i : 𝒰.I₀) :
    recoveredCoefficientChartMap k L S f 𝒰 M Z e i ≫ Z.hom =
      coefficientModelMap φL f (a i)
def

recoveredFiniteStageChartInclusion

L190 ↗
EtaleFundamentalGroups.recoveredFiniteStageChartInclusion
Documentation

The chart inclusion of the actually glued scheme, retaining its coefficient structure.

Source context 31 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))
variable (q : (recoveredFiniteStageGlueData k L S f 𝒰 M Z e s g hgC hgS hgR).glued ⟶
  pullback (Spec.map (CommRingCat.ofHom
    (algebraMap k (IntermediateField.adjoin k (s : Set L))))) f)
variable (hq : ∀ 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 hgC hgS hgR).ι i)
    ((constantFieldOpenCover k (IntermediateField.adjoin k (s : Set L)) S f 𝒰).f i) q)
local notation "Dg" => recoveredFiniteStageGlueData k L S f 𝒰 M Z e s g hgC hgS hgR
Lean source · statement
def recoveredFiniteStageChartInclusion (i : 𝒰.I₀) :
    AE i ⟶ Over.mk (q ≫ pullback.fst φE f)
def

recoveredFiniteStagePullbackCover

L201 ↗
EtaleFundamentalGroups.recoveredFiniteStagePullbackCover
Documentation

The coefficient pullback of the actual glued model is covered by the coefficient pullbacks of its original chart inclusions.

Source context 31 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))
variable (q : (recoveredFiniteStageGlueData k L S f 𝒰 M Z e s g hgC hgS hgR).glued ⟶
  pullback (Spec.map (CommRingCat.ofHom
    (algebraMap k (IntermediateField.adjoin k (s : Set L))))) f)
variable (hq : ∀ 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 hgC hgS hgR).ι i)
    ((constantFieldOpenCover k (IntermediateField.adjoin k (s : Set L)) S f 𝒰).f i) q)
local notation "Dg" => recoveredFiniteStageGlueData k L S f 𝒰 M Z e s g hgC hgS hgR
Lean source · statement
def recoveredFiniteStagePullbackCover :
    (pullback (q ≫ pullback.fst φE f) ψ).OpenCover
theorem

recoveredFiniteStagePullbackCover_isPullback

L213 ↗
EtaleFundamentalGroups.recoveredFiniteStagePullbackCover_isPullback
Documentation

The coefficient-pulled-back gluing overlaps are the actual overlaps of the coefficient-pulled-back glued model.

Source context 31 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))
variable (q : (recoveredFiniteStageGlueData k L S f 𝒰 M Z e s g hgC hgS hgR).glued ⟶
  pullback (Spec.map (CommRingCat.ofHom
    (algebraMap k (IntermediateField.adjoin k (s : Set L))))) f)
variable (hq : ∀ 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 hgC hgS hgR).ι i)
    ((constantFieldOpenCover k (IntermediateField.adjoin k (s : Set L)) S f 𝒰).f i) q)
local notation "Dg" => recoveredFiniteStageGlueData k L S f 𝒰 M Z e s g hgC hgS hgR
Lean source · statement
theorem recoveredFiniteStagePullbackCover_isPullback (i j : 𝒰.I₀) :
    IsPullback ((Over.pullback ψ).map (dE i j)).left
      ((Over.pullback ψ).map (recoveredStageTransition k L S f 𝒰 M s g hgC i j ≫ dE j i)).left
      ((Over.pullback ψ).map
        (recoveredFiniteStageChartInclusion k L S f 𝒰 M Z e s g hgC hgS hgR q hq i)).left
      ((Over.pullback ψ).map
        (recoveredFiniteStageChartInclusion k L S f 𝒰 M Z e s g hgC hgS hgR q hq j)).left
theorem

exists_recoveredFiniteStageGlueData_coefficient_iso

L226 ↗
EtaleFundamentalGroups.exists_recoveredFiniteStageGlueData_coefficient_iso
Documentation

The coefficient extension of the actually glued finite-stage scheme recovers the original scheme, with equality on every actual local chart.

Source context 31 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))
variable (q : (recoveredFiniteStageGlueData k L S f 𝒰 M Z e s g hgC hgS hgR).glued ⟶
  pullback (Spec.map (CommRingCat.ofHom
    (algebraMap k (IntermediateField.adjoin k (s : Set L))))) f)
variable (hq : ∀ 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 hgC hgS hgR).ι i)
    ((constantFieldOpenCover k (IntermediateField.adjoin k (s : Set L)) S f 𝒰).f i) q)
local notation "Dg" => recoveredFiniteStageGlueData k L S f 𝒰 M Z e s g hgC hgS hgR
Lean source · statement
theorem exists_recoveredFiniteStageGlueData_coefficient_iso :
    ∃ eL : pullback (q ≫ pullback.fst φE f) ψ ≅ Z.left,
      ∀ i : 𝒰.I₀,
        ((Over.pullback ψ).map
          (recoveredFiniteStageChartInclusion k L S f 𝒰 M Z e s g hgC hgS hgR q hq i)).left ≫
            eL.hom = recoveredStageChartMap k L S f 𝒰 M Z e s i
def

recoveredFiniteStageBaseMap

L255 ↗
EtaleFundamentalGroups.recoveredFiniteStageBaseMap
Documentation

The coefficient pullback of the glued model has its actual structural map to the original extended base.

Source context 31 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))
variable (q : (recoveredFiniteStageGlueData k L S f 𝒰 M Z e s g hgC hgS hgR).glued ⟶
  pullback (Spec.map (CommRingCat.ofHom
    (algebraMap k (IntermediateField.adjoin k (s : Set L))))) f)
variable (hq : ∀ 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 hgC hgS hgR).ι i)
    ((constantFieldOpenCover k (IntermediateField.adjoin k (s : Set L)) S f 𝒰).f i) q)
local notation "Dg" => recoveredFiniteStageGlueData k L S f 𝒰 M Z e s g hgC hgS hgR
Lean source · statement
def recoveredFiniteStageBaseMap : pullback (q ≫ pullback.fst φE f) ψ ⟶ pullback φL f
theorem

recoveredFiniteStageBaseMap_stage

L263 ↗
EtaleFundamentalGroups.recoveredFiniteStageBaseMap_stage
Source context 31 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))
variable (q : (recoveredFiniteStageGlueData k L S f 𝒰 M Z e s g hgC hgS hgR).glued ⟶
  pullback (Spec.map (CommRingCat.ofHom
    (algebraMap k (IntermediateField.adjoin k (s : Set L))))) f)
variable (hq : ∀ 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 hgC hgS hgR).ι i)
    ((constantFieldOpenCover k (IntermediateField.adjoin k (s : Set L)) S f 𝒰).f i) q)
local notation "Dg" => recoveredFiniteStageGlueData k L S f 𝒰 M Z e s g hgC hgS hgR
Lean source · statement
theorem recoveredFiniteStageBaseMap_stage :
    recoveredFiniteStageBaseMap k L S f 𝒰 M Z e s g hgC hgS hgR q ≫
      (constantFieldInverseLimitCone k L S f).π.app (op s) =
    pullback.fst (q ≫ pullback.fst φE f) ψ ≫ q
theorem

recoveredFiniteStageBaseMap_coefficient

L270 ↗
EtaleFundamentalGroups.recoveredFiniteStageBaseMap_coefficient
Source context 31 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))
variable (q : (recoveredFiniteStageGlueData k L S f 𝒰 M Z e s g hgC hgS hgR).glued ⟶
  pullback (Spec.map (CommRingCat.ofHom
    (algebraMap k (IntermediateField.adjoin k (s : Set L))))) f)
variable (hq : ∀ 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 hgC hgS hgR).ι i)
    ((constantFieldOpenCover k (IntermediateField.adjoin k (s : Set L)) S f 𝒰).f i) q)
local notation "Dg" => recoveredFiniteStageGlueData k L S f 𝒰 M Z e s g hgC hgS hgR
Lean source · statement
theorem recoveredFiniteStageBaseMap_coefficient :
    recoveredFiniteStageBaseMap k L S f 𝒰 M Z e s g hgC hgS hgR q ≫ pullback.fst φL f =
      pullback.snd (q ≫ pullback.fst φE f) ψ
theorem

recoveredFiniteStageBaseMap_isPullback

L277 ↗
EtaleFundamentalGroups.recoveredFiniteStageBaseMap_isPullback
Documentation

The coefficient pullback is also the actual pullback along the finite-stage projection of the base scheme.

Source context 31 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))
variable (q : (recoveredFiniteStageGlueData k L S f 𝒰 M Z e s g hgC hgS hgR).glued ⟶
  pullback (Spec.map (CommRingCat.ofHom
    (algebraMap k (IntermediateField.adjoin k (s : Set L))))) f)
variable (hq : ∀ 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 hgC hgS hgR).ι i)
    ((constantFieldOpenCover k (IntermediateField.adjoin k (s : Set L)) S f 𝒰).f i) q)
local notation "Dg" => recoveredFiniteStageGlueData k L S f 𝒰 M Z e s g hgC hgS hgR
Lean source · statement
theorem recoveredFiniteStageBaseMap_isPullback :
    IsPullback (recoveredFiniteStageBaseMap k L S f 𝒰 M Z e s g hgC hgS hgR q)
      (pullback.fst (q ≫ pullback.fst φE f) ψ)
      ((constantFieldInverseLimitCone k L S f).π.app (op s)) q
theorem

recoveredFiniteStageChartInclusion_baseMap

L289 ↗
EtaleFundamentalGroups.recoveredFiniteStageChartInclusion_baseMap
Documentation

Every recovered chart respects the actual base structural map of the coefficient-pulled-back glued model.

Source context 31 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))
variable (q : (recoveredFiniteStageGlueData k L S f 𝒰 M Z e s g hgC hgS hgR).glued ⟶
  pullback (Spec.map (CommRingCat.ofHom
    (algebraMap k (IntermediateField.adjoin k (s : Set L))))) f)
variable (hq : ∀ 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 hgC hgS hgR).ι i)
    ((constantFieldOpenCover k (IntermediateField.adjoin k (s : Set L)) S f 𝒰).f i) q)
local notation "Dg" => recoveredFiniteStageGlueData k L S f 𝒰 M Z e s g hgC hgS hgR
Lean source · statement
theorem recoveredFiniteStageChartInclusion_baseMap (i : 𝒰.I₀) :
    ((Over.pullback ψ).map
      (recoveredFiniteStageChartInclusion k L S f 𝒰 M Z e s g hgC hgS hgR q hq i)).left ≫
        recoveredFiniteStageBaseMap k L S f 𝒰 M Z e s g hgC hgS hgR q =
      recoveredStageChartMap k L S f 𝒰 M Z e s i ≫ Z.hom
theorem

nonempty_recoveredFiniteStageGlueData_over_iso

L325 ↗
EtaleFundamentalGroups.nonempty_recoveredFiniteStageGlueData_over_iso
Documentation

The actual finite-stage glued scheme recovers the original object over the extended base, not only its underlying scheme.

Source context 32 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))
variable (q : (recoveredFiniteStageGlueData k L S f 𝒰 M Z e s g hgC hgS hgR).glued ⟶
  pullback (Spec.map (CommRingCat.ofHom
    (algebraMap k (IntermediateField.adjoin k (s : Set L))))) f)
variable (hq : ∀ 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 hgC hgS hgR).ι i)
    ((constantFieldOpenCover k (IntermediateField.adjoin k (s : Set L)) S f 𝒰).f i) q)
local notation "Dg" => recoveredFiniteStageGlueData k L S f 𝒰 M Z e s g hgC hgS hgR
include hq in
Lean source · statement
theorem nonempty_recoveredFiniteStageGlueData_over_iso :
    Nonempty ((Over.pullback ((constantFieldInverseLimitCone k L S f).π.app (op s))).obj
      (Over.mk q) ≅ Z)

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