AlgebraicGeometry.FiniteEtale.arithmetic_exactSequence_of_isSepClosure
The arithmetic short exact sequence over a separable closure. Both maps are the actual continuous maps on geometric fiber automorphism groups.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtaleLean source · full declaration
theorem arithmetic_exactSequence_of_isSepClosure
(k L : Type u) [Field k] [Field L] [Algebra k L] [IsSepClosure k L]
(X : Scheme.{u}) [CompactSpace X] [QuasiSeparatedSpace X]
(f : X ⟶ Spec (.of k))
[ConnectedSpace ↑(Limits.pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f)]
{Ω : Type u} [Field Ω] [IsSepClosed Ω]
(xi : Spec (.of Ω) ⟶ Limits.pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f) :
let geometric := fundamentalGroupHom (Limits.pullback.snd _ f) xi
let arithmetic := arithmeticFundamentalGroupHom k L f (xi ≫ Limits.pullback.snd _ f)
Function.Injective geometric ∧ Function.Surjective arithmetic ∧
arithmetic.toMonoidHom.ker = geometric.toMonoidHom.range := by
let : IsSepClosed L := IsSepClosure.sep_closed k
let : ConnectedSpace X := connectedSpace_of_connected_constantField k L f
refine ⟨fundamentalGroupHom_injective_of_separable_constant_extension k L X f xi,
arithmeticFundamentalGroupHom_surjective_of_connected_constantField k L L f
(xi ≫ Limits.pullback.snd _ f), ?_⟩
exact (arithmeticFundamentalGroupHom_ker k L f (xi ≫ Limits.pullback.snd _ f)).trans
(fundamentalGroupHom_constantField_ker_eq_range k L f xi)