Module

AutomorphismProfiniteCompletion.lean

Nyll.EtaleFundamentalGroups.GaloisCategories.AutomorphismProfiniteCompletion

16 declarations indexed from sourceView source ↗

Module documentation

The profinite completion of a topological group

This file proves Stacks Project, Tag 0BMU: the automorphism group of the forgetful functor on finite continuous actions of a topological group is its profinite completion.

Imports5

Mathlib.CategoryTheory.Action.Concrete
Mathlib.CategoryTheory.Action.Continuous
Mathlib.CategoryTheory.Galois.IsFundamentalgroup
Mathlib.Topology.Category.FinTopCat
Nyll.ClassFieldTheory.LocalClassFieldTheory.Infinite.ProfiniteCompletion

Imported by1

Nyll.EtaleFundamentalGroups.GaloisCategories.All

instance

carrierMulAction

L35 ↗

CategoryTheory.FiniteContinuousAction.carrierMulAction

Source context 7 commands

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

universe u v
noncomputable section
open CategoryTheory Topology
open scoped FintypeCatDiscrete PreGaloisCategory
namespace CategoryTheory
namespace FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

instance carrierMulAction
    (X : ContAction FintypeCat.{u} G) :
    MulAction G
      ((forget₂ (ContAction FintypeCat.{u} G) FintypeCat).obj X)

instance

carrierContinuousSMul

L41 ↗

CategoryTheory.FiniteContinuousAction.carrierContinuousSMul

Source context 7 commands

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

universe u v
noncomputable section
open CategoryTheory Topology
open scoped FintypeCatDiscrete PreGaloisCategory
namespace CategoryTheory
namespace FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

instance carrierContinuousSMul
    (X : ContAction FintypeCat.{u} G) :
    ContinuousSMul G
      ((forget₂ (ContAction FintypeCat.{u} G) FintypeCat).obj X)

instance

naturalSMul

L49 ↗

CategoryTheory.FiniteContinuousAction.naturalSMul

Source context 7 commands

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

universe u v
noncomputable section
open CategoryTheory Topology
open scoped FintypeCatDiscrete PreGaloisCategory
namespace CategoryTheory
namespace FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · full declaration

instance naturalSMul :
    PreGaloisCategory.IsNaturalSMul
      (forget₂ (ContAction FintypeCat.{u} G) FintypeCat) G where
  naturality g {X Y} f x := by
    change
      ConcreteCategory.hom (InducedCategory.Hom.hom f).hom
          (ConcreteCategory.hom (X.obj.ρ g) x) =
        ConcreteCategory.hom (Y.obj.ρ g)
          (ConcreteCategory.hom (InducedCategory.Hom.hom f).hom x)
    simpa only [FintypeCat.comp_apply] using
      ConcreteCategory.congr_hom ((InducedCategory.Hom.hom f).comm g) x

theorem

continuous_of_isOpen_ker

L61 ↗

CategoryTheory.FiniteContinuousAction.continuous_of_isOpen_ker

Source context 7 commands

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

universe u v
noncomputable section
open CategoryTheory Topology
open scoped FintypeCatDiscrete PreGaloisCategory
namespace CategoryTheory
namespace FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem continuous_of_isOpen_ker
    {H : Type u} [Group H] [TopologicalSpace H] [DiscreteTopology H]
    (f : G →* H) (hf : IsOpen (f.ker : Set G)) :
    Continuous f

theorem

canonicalHom_continuous

L74 ↗

CategoryTheory.FiniteContinuousAction.canonicalHom_continuous

Source context 7 commands

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

universe u v
noncomputable section
open CategoryTheory Topology
open scoped FintypeCatDiscrete PreGaloisCategory
namespace CategoryTheory
namespace FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem canonicalHom_continuous :
    Continuous
      (PreGaloisCategory.toAut
        (forget₂ (ContAction FintypeCat.{u} G) FintypeCat) G)

theorem

actionKernel_isOpen

L115 ↗

CategoryTheory.FiniteContinuousAction.actionKernel_isOpen

Source context 8 commands

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

universe u v
noncomputable section
open CategoryTheory Topology
open scoped FintypeCatDiscrete PreGaloisCategory
namespace CategoryTheory
namespace FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [IsTopologicalGroup G] in

Lean source · statement

theorem actionKernel_isOpen
    (X : ContAction FintypeCat.{u} G) :
    IsOpen
      ((MulAction.toPermHom G
        ((forget₂ (ContAction FintypeCat.{u} G) FintypeCat).obj X)).ker :
          Set G)

theorem

quotient_continuousSMul

L146 ↗

CategoryTheory.FiniteContinuousAction.quotient_continuousSMul

Source context 7 commands

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

universe u v
noncomputable section
open CategoryTheory Topology
open scoped FintypeCatDiscrete PreGaloisCategory
namespace CategoryTheory
namespace FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem quotient_continuousSMul
    (K : Subgroup G) [K.Normal]
    [TopologicalSpace (G ⧸ K)] [DiscreteTopology (G ⧸ K)]
    (hK : IsOpen (K : Set G)) :
    ContinuousSMul G (G ⧸ K)

theorem

exists_canonicalHom_eq_on_finite

L172 ↗

CategoryTheory.FiniteContinuousAction.exists_canonicalHom_eq_on_finite

Source context 7 commands

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

universe u v
noncomputable section
open CategoryTheory Topology
open scoped FintypeCatDiscrete PreGaloisCategory
namespace CategoryTheory
namespace FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem exists_canonicalHom_eq_on_finite
    {ι : Type v} [Finite ι]
    (X : ι → ContAction FintypeCat.{u} G)
    (σ : Aut
      (forget₂ (ContAction FintypeCat.{u} G) FintypeCat)) :
    ∃ g : G, ∀ i,
      (PreGaloisCategory.toAut
          (forget₂ (ContAction FintypeCat.{u} G) FintypeCat) G g).hom.app
          (X i) =
        σ.hom.app (X i)

theorem

canonicalHom_denseRange

L277 ↗

CategoryTheory.FiniteContinuousAction.canonicalHom_denseRange

Source context 7 commands

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

universe u v
noncomputable section
open CategoryTheory Topology
open scoped FintypeCatDiscrete PreGaloisCategory
namespace CategoryTheory
namespace FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem canonicalHom_denseRange :
    DenseRange
      (PreGaloisCategory.toAut
        (forget₂ (ContAction FintypeCat.{u} G) FintypeCat) G)

def

canonicalContinuousHom

L300 ↗

CategoryTheory.FiniteContinuousAction.canonicalContinuousHom

Source context 7 commands

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

universe u v
noncomputable section
open CategoryTheory Topology
open scoped FintypeCatDiscrete PreGaloisCategory
namespace CategoryTheory
namespace FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · full declaration

def canonicalContinuousHom :
    G →ₜ*
      Aut (forget₂ (ContAction FintypeCat.{u} G) FintypeCat) where
  toMonoidHom :=
    PreGaloisCategory.toAut
      (forget₂ (ContAction FintypeCat.{u} G) FintypeCat) G
  continuous_toFun := canonicalHom_continuous G

def

automorphismProfiniteGroup

L308 ↗

CategoryTheory.FiniteContinuousAction.automorphismProfiniteGroup

Source context 7 commands

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

universe u v
noncomputable section
open CategoryTheory Topology
open scoped FintypeCatDiscrete PreGaloisCategory
namespace CategoryTheory
namespace FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

def automorphismProfiniteGroup : ProfiniteGrp.{u + 1}

theorem

canonicalHom_preimage_cofinal

L312 ↗

CategoryTheory.FiniteContinuousAction.canonicalHom_preimage_cofinal

Source context 7 commands

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

universe u v
noncomputable section
open CategoryTheory Topology
open scoped FintypeCatDiscrete PreGaloisCategory
namespace CategoryTheory
namespace FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem canonicalHom_preimage_cofinal
    (H : LocalClassFieldTheory.OpenFiniteIndexNormalSubgroup G) :
    ∃ N : OpenNormalSubgroup
        (Aut (forget₂ (ContAction FintypeCat.{u} G) FintypeCat)),
      LocalClassFieldTheory.topologicalProfiniteCompletionPreimageIndex
          (automorphismProfiniteGroup G)
          (canonicalContinuousHom G) N ≤ H

theorem

canonicalLift_injective

L359 ↗

CategoryTheory.FiniteContinuousAction.canonicalLift_injective

Source context 7 commands

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

universe u v
noncomputable section
open CategoryTheory Topology
open scoped FintypeCatDiscrete PreGaloisCategory
namespace CategoryTheory
namespace FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem canonicalLift_injective :
    Function.Injective
      (LocalClassFieldTheory.topologicalProfiniteCompletionLift
        (automorphismProfiniteGroup G) (canonicalContinuousHom G))

theorem

canonicalLift_surjective

L433 ↗

CategoryTheory.FiniteContinuousAction.canonicalLift_surjective

Source context 7 commands

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

universe u v
noncomputable section
open CategoryTheory Topology
open scoped FintypeCatDiscrete PreGaloisCategory
namespace CategoryTheory
namespace FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem canonicalLift_surjective :
    Function.Surjective
      (LocalClassFieldTheory.topologicalProfiniteCompletionLift
        (automorphismProfiniteGroup G) (canonicalContinuousHom G))

def

profiniteCompletionEquivAutForget

L459 ↗

CategoryTheory.FiniteContinuousAction.profiniteCompletionEquivAutForget

Documentation

The automorphism group of the forgetful functor on finite continuous G-sets is canonically the profinite completion of G.

Source context 7 commands

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

universe u v
noncomputable section
open CategoryTheory Topology
open scoped FintypeCatDiscrete PreGaloisCategory
namespace CategoryTheory
namespace FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

def profiniteCompletionEquivAutForget :
    LocalClassFieldTheory.TopologicalProfiniteCompletion G ≃ₜ*
      Aut (forget₂ (ContAction FintypeCat.{u} G) FintypeCat)

theorem

profiniteCompletionEquivAutForget_apply_completionMap

L481 ↗

CategoryTheory.FiniteContinuousAction.profiniteCompletionEquivAutForget_apply_completionMap

Source context 7 commands

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

universe u v
noncomputable section
open CategoryTheory Topology
open scoped FintypeCatDiscrete PreGaloisCategory
namespace CategoryTheory
namespace FiniteContinuousAction
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem profiniteCompletionEquivAutForget_apply_completionMap
    (g : G) :
    profiniteCompletionEquivAutForget G
        (LocalClassFieldTheory.topologicalProfiniteCompletionMap G g) =
      PreGaloisCategory.toAut
        (forget₂ (ContAction FintypeCat.{u} G) FintypeCat) G g

Module documentation

The profinite completion of a topological group

Declarations