EtaleFundamentalGroups.exists_finiteIntermediateField_overlap_transitions
Actual recovered overlap transitions descend together to one finite coefficient stage, retaining both structure maps and the recovery equation.
Source context 13 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory Limits Opposite AlgebraicGeometry
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L] [Algebra.IsAlgebraic k L]
variable (S : Scheme.{u}) [QuasiSeparatedSpace S] (f : S ⟶ Spec (CommRingCat.of k))
variable (𝒰 : S.OpenCover) [Finite 𝒰.I₀] [∀ i : 𝒰.I₀, IsAffine (𝒰.X i)]
variable (M : ∀ i : 𝒰.I₀, Over (𝒰.X i)) [∀ i : 𝒰.I₀, IsFiniteEtale (M i).hom]
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)
local notation "φ" => Spec.map (CommRingCat.ofHom (algebraMap k L))
local notation "A" => (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)))Lean source · statement
theorem exists_finiteIntermediateField_overlap_transitions :
∃ 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),
∀ 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 (A ij) (p ij ≫ f)).π.app (op s) ≫ g ij =
recoveredCoefficientTransition k L S f 𝒰 M Z e ij.1 ij.2 ≫
(constantFieldInverseLimitCone k L (A (ij.2, ij.1))
(p (ij.2, ij.1) ≫ f)).π.app (op s)