Module

OpenSubgroupFundamentalGroup.lean

Nyll.EtaleFundamentalGroups.GaloisCovers.OpenSubgroupFundamentalGroup

3 declarations indexed from sourceView source ↗

Module documentation

Actual finite étale covers for arbitrary open subgroups

The quotient action of an arbitrary open subgroup is realized by a connected object, with no normality assumption and no restriction on the fiber universe. For a scheme this gives a pointed connected finite étale cover whose fundamental group is the specified subgroup. The inclusion is the actual homomorphism induced by the covering morphism.

Imports5

Nyll.EtaleFundamentalGroups.GaloisCategories.ConnectedActions
Nyll.EtaleFundamentalGroups.GaloisCategories.Functoriality
Nyll.EtaleFundamentalGroups.GeometricFiber.PointedCover
Nyll.EtaleFundamentalGroups.FiniteEtale.Connected
Mathlib.CategoryTheory.Galois.Equivalence

Imported by4

theorem

exists_connected_object_point_stabilizer_eq

L33 ↗

CategoryTheory.PreGaloisCategory.exists_connected_object_point_stabilizer_eq

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory
namespace CategoryTheory.PreGaloisCategory
universe u₁ u₂ w
variable {C : Type u₁} [Category.{u₂} C] [GaloisCategory C]

Lean source · statement

theorem exists_connected_object_point_stabilizer_eq
    (F : C ⥤ FintypeCat.{u₁}) [FiberFunctor F]
    (U : OpenSubgroup (Aut F)) :
    ∃ (X : C) (_ : IsConnected X) (x : F.obj X),
      MulAction.stabilizer (Aut F) x = (U : Subgroup (Aut F))

theorem

exists_connected_object_point_stabilizer_eq_any_universe

L67 ↗

CategoryTheory.PreGaloisCategory.exists_connected_object_point_stabilizer_eq_any_universe

Documentation

Every open subgroup is the stabilizer of a point of a connected object, even when the fiber functor and its source category have different universes.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory
namespace CategoryTheory.PreGaloisCategory
universe u₁ u₂ w
variable {C : Type u₁} [Category.{u₂} C] [GaloisCategory C]

Lean source · statement

theorem exists_connected_object_point_stabilizer_eq_any_universe
    (F : C ⥤ FintypeCat.{w}) [FiberFunctor F]
    (U : OpenSubgroup (Aut F)) :
    ∃ (X : C) (_ : IsConnected X) (x : F.obj X),
      MulAction.stabilizer (Aut F) x = (U : Subgroup (Aut F))

theorem

exists_connectedCover_lift_fundamentalGroup_equiv_openSubgroup

L114 ↗

AlgebraicGeometry.FiniteEtale.exists_connectedCover_lift_fundamentalGroup_equiv_openSubgroup

Documentation

Every open subgroup is the fundamental group of an actual connected finite étale cover. The equivalence identifies subgroup inclusion with the actual homomorphism on fundamental groups induced by the covering map.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory
universe u
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
variable {S : Scheme.{u}} [ConnectedSpace S]
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω]

Lean source · statement

theorem exists_connectedCover_lift_fundamentalGroup_equiv_openSubgroup
    (xi : Spec (.of Ω) ⟶ S) (U : OpenSubgroup π₁ᵉᵗ(xi)) :
    ∃ (A : FiniteEtale S) (_ : ConnectedSpace A.left)
      (xi' : Spec (.of Ω) ⟶ A.left) (hxi : xi' ≫ A.hom = xi)
      (e : π₁ᵉᵗ(xi') ≃ₜ* U),
      ∀ a : π₁ᵉᵗ(xi'), (e a : π₁ᵉᵗ(xi)) =
        hxi ▸ fundamentalGroupHom A.hom xi' a

Module documentation

Actual finite étale covers for arbitrary open subgroups

Declarations

exists_connected_object_point_stabilizer_eq

exists_connected_object_point_stabilizer_eq_any_universe

exists_connectedCover_lift_fundamentalGroup_equiv_openSubgroup