Module

OpenNormalFundamentalGroup.lean

Nyll.EtaleFundamentalGroups.GaloisCovers.OpenNormalFundamentalGroup

2 declarations indexed from sourceView source ↗

Module documentation

Fundamental groups of covers attached to open normal subgroups

An open normal subgroup of an étale fundamental group is represented by a finite étale Galois cover. Choosing the point above the original geometric point identifies the fundamental group of the cover with that subgroup as a topological group.

Imports3

Nyll.EtaleFundamentalGroups.GaloisCovers.OpenNormalUniverse
Nyll.EtaleFundamentalGroups.GeometricFiber.PointedCover
Mathlib.GroupTheory.Index

Imported by2

theorem

exists_galoisCover_lift_fundamentalGroup_equiv_openNormal_compatible

L35 ↗

AlgebraicGeometry.FiniteEtale.exists_galoisCover_lift_fundamentalGroup_equiv_openNormal_compatible

Documentation

Every open normal subgroup of an étale fundamental group is the fundamental group of a finite étale Galois cover at a point above the chosen base point.

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 {S : Scheme.{u}} [ConnectedSpace S]
variable {Omega : Type u} [Field Omega] [IsSepClosed Omega]

Lean source · statement

theorem exists_galoisCover_lift_fundamentalGroup_equiv_openNormal_compatible
    (xi : Spec (.of Omega) ⟶ S)
    (U : OpenNormalSubgroup π₁ᵉᵗ(xi)) :
    ∃ (A : FiniteEtale S) (_ : IsGalois A)
      (xi' : Spec (.of Omega) ⟶ A.left) (hxi : xi' ≫ A.hom = xi)
      (e : π₁ᵉᵗ(xi') ≃ₜ* U),
      Nat.card ((fiber xi).obj A) = U.toSubgroup.index ∧
      ∀ a : π₁ᵉᵗ(xi'), (e a : π₁ᵉᵗ(xi)) =
        hxi ▸ fundamentalGroupHom A.hom xi' a

theorem

exists_galoisCover_lift_fundamentalGroup_equiv_openNormal

L83 ↗

AlgebraicGeometry.FiniteEtale.exists_galoisCover_lift_fundamentalGroup_equiv_openNormal