AlgebraicGeometry.FiniteEtale.fundamentalGroupHom_constantField_range_normal
The geometric fundamental group has normal image after extension to a separable closure with connected base change.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory Limits CategoryTheory.PreGaloisCategory
universe u
namespace AlgebraicGeometry.FiniteEtaleLean source · statement
theorem fundamentalGroupHom_constantField_range_normal
(k L : Type u) [Field k] [Field L] [Algebra k L]
[Algebra.IsSeparable k L] [IsSepClosed 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) :
(fundamentalGroupHom (Limits.pullback.snd _ f) xi).toMonoidHom.range.Normal