NYLL
Module

OpenNormal.lean

Nyll.EtaleFundamentalGroups.GaloisCovers.OpenNormal
4 declarations indexed from sourceView source ↗

Module documentation

Galois objects attached to open normal subgroups

This file packages the normal-subgroup part of the fundamental equivalence between a Galois category and finite continuous actions of its fundamental group.

Imports4
Imported by2

Declarations

def

quotientRightIso

L31 ↗
CategoryTheory.PreGaloisCategory.quotientRightIso
Source context 6 commands

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

noncomputable section
open CategoryTheory
namespace CategoryTheory.PreGaloisCategory
universe u₁ u₂
variable {C : Type u₁} [Category.{u₂} C] [GaloisCategory C]
variable (F : C ⥤ FintypeCat.{u₁}) [FiberFunctor F]
Lean source · full declaration
def quotientRightIso
    (N : Subgroup (Aut F)) [N.Normal]
    [Fintype (Aut F ⧸ N)] (g : Aut F) :
    (Aut F ⧸ₐ N) ≅ (Aut F ⧸ₐ N) where
  hom := Action.FintypeCat.toEndHom N g
  inv := Action.FintypeCat.toEndHom N g⁻¹
  hom_inv_id := by
    apply Action.hom_ext
    ext q
    induction q using Quotient.inductionOn with
    | _ q =>
        change (⟦q * g⁻¹ * (g⁻¹)⁻¹⟧ : Aut F ⧸ N) = ⟦q⟧
        simp
  inv_hom_id := by
    apply Action.hom_ext
    ext q
    induction q using Quotient.inductionOn with
    | _ q =>
        change (⟦q * g * g⁻¹⟧ : Aut F ⧸ N) = ⟦q⟧
        simp
theorem

isGalois_of_fiber_iso_quotient_openNormal

L54 ↗
CategoryTheory.PreGaloisCategory.isGalois_of_fiber_iso_quotient_openNormal
Documentation

An object whose canonical fundamental-group action is an open-normal quotient is a Galois object.

Source context 6 commands

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

noncomputable section
open CategoryTheory
namespace CategoryTheory.PreGaloisCategory
universe u₁ u₂
variable {C : Type u₁} [Category.{u₂} C] [GaloisCategory C]
variable (F : C ⥤ FintypeCat.{u₁}) [FiberFunctor F]
Lean source · statement
theorem isGalois_of_fiber_iso_quotient_openNormal
    (U : OpenNormalSubgroup (Aut F)) (X : C)
    (e : (functorToAction F).obj X ≅
      Aut F ⧸ₐ (U : Subgroup (Aut F))) :
    IsGalois X
theorem

exists_galois_object_fiber_iso_quotient

L119 ↗
CategoryTheory.PreGaloisCategory.exists_galois_object_fiber_iso_quotient
Documentation

Every open normal subgroup of the fundamental group of a Galois category is represented by a Galois object whose fiber is the corresponding quotient action.

Source context 6 commands

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

noncomputable section
open CategoryTheory
namespace CategoryTheory.PreGaloisCategory
universe u₁ u₂
variable {C : Type u₁} [Category.{u₂} C] [GaloisCategory C]
variable (F : C ⥤ FintypeCat.{u₁}) [FiberFunctor F]
Lean source · full declaration
theorem exists_galois_object_fiber_iso_quotient
    (U : OpenNormalSubgroup (Aut F)) :
    ∃ (X : C) (hX : IsGalois X),
      letI := hX
      Nonempty ((functorToAction F).obj X ≅
        Aut F ⧸ₐ (U : Subgroup (Aut F))) := by
  let : Fintype (Aut F ⧸ (U : Subgroup (Aut F))) :=
    Fintype.ofFinite _
  let V : OpenSubgroup (Aut F) := U.toOpenSubgroup
  obtain ⟨X, ⟨e⟩⟩ :=
    exists_lift_of_quotient_openSubgroup (F := F) V
  have hX : IsGalois X :=
    isGalois_of_fiber_iso_quotient_openNormal F U X e
  exact ⟨X, hX, ⟨e⟩⟩
theorem

exists_galois_object_point_stabilizer_eq

L137 ↗
CategoryTheory.PreGaloisCategory.exists_galois_object_point_stabilizer_eq
Documentation

Every open normal subgroup is the stabilizer of a point on the fiber of a Galois object. The point is the inverse image of the identity coset under the quotient-action presentation of the fiber.

Source context 6 commands

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

noncomputable section
open CategoryTheory
namespace CategoryTheory.PreGaloisCategory
universe u₁ u₂
variable {C : Type u₁} [Category.{u₂} C] [GaloisCategory C]
variable (F : C ⥤ FintypeCat.{u₁}) [FiberFunctor F]
Lean source · statement
theorem exists_galois_object_point_stabilizer_eq
    (U : OpenNormalSubgroup (Aut F)) :
    ∃ (X : C) (_ : IsGalois X) (x : F.obj X),
      MulAction.stabilizer (Aut F) x = (U : Subgroup (Aut F))

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.