AlgebraicGeometry.FiniteEtale.exists_galoisCover_point_pullback_fundamentalGroup_equiv_comap_openNormal
An open normal subgroup at the target is represented by a Galois cover whose pointed pullback has fundamental group equal to its inverse image.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
variable {X Y : Scheme.{u}} [ConnectedSpace X] [ConnectedSpace Y]
variable {Omega : Type u} [Field Omega] [IsSepClosed Omega]Lean source · statement
theorem exists_galoisCover_point_pullback_fundamentalGroup_equiv_comap_openNormal
(f : X ⟶ Y) (xi : Spec (.of Omega) ⟶ X)
(U : OpenNormalSubgroup π₁ᵉᵗ(xi ≫ f)) :
∃ (A : FiniteEtale Y) (_ : IsGalois A)
(x : (fiber (xi ≫ f)).obj A),
MulAction.stabilizer π₁ᵉᵗ(xi ≫ f) x =
(U : Subgroup π₁ᵉᵗ(xi ≫ f)) ∧
Nonempty
(π₁ᵉᵗ(pullbackLiftOfFiberPoint f xi A x) ≃ₜ*
ProCGroups.OpenNormalSubgroup.comap
(fundamentalGroupHom f xi).toMonoidHom
(fundamentalGroupHom f xi).continuous_toFun U)