feat(CategoryTheory/Galois): equivalence to ContAction (#24563)

Author: chrisflav

Mathlib.lean

@@ -2037,6 +2037,7 @@ import Mathlib.CategoryTheory.Functor.TwoSquare
 import Mathlib.CategoryTheory.Galois.Action
 import Mathlib.CategoryTheory.Galois.Basic
 import Mathlib.CategoryTheory.Galois.Decomposition
+import Mathlib.CategoryTheory.Galois.Equivalence
 import Mathlib.CategoryTheory.Galois.EssSurj
 import Mathlib.CategoryTheory.Galois.Examples
 import Mathlib.CategoryTheory.Galois.Full

Mathlib/CategoryTheory/Galois/Basic.lean

@@ -26,6 +26,9 @@ the definitions in Lenstras notes (see below for a reference).
 * `IsConnected`       : an object of a category is connected if it is not initial
                         and does not have non-trivial subobjects
 
+Any fiber functor `F` induces an equivalence with the category of finite, discrete `Aut F`-types.
+This is proven in `Mathlib.CategoryTheory.Galois.Equivalence`.
+
 ## Implementation details
 
 We mostly follow Def 3.1 in Lenstras notes. In axiom (G3)
@@ -170,7 +173,7 @@ section
 
 /-- If `F` is a fiber functor and `E` is an equivalence between categories of finite types,
 then `F ⋙ E` is again a fiber functor. -/
-lemma comp_right (E : FintypeCat.{w} ⥤ FintypeCat.{t}) [E.IsEquivalence] :
+instance comp_right (E : FintypeCat.{w} ⥤ FintypeCat.{t}) [E.IsEquivalence] :
     FiberFunctor (F ⋙ E) where
   preservesQuotientsByFiniteGroups _ := comp_preservesColimitsOfShape F E
 

Mathlib/CategoryTheory/Galois/Equivalence.lean

@@ -0,0 +1,90 @@
+/-
+Copyright (c) 2025 Christian Merten. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Merten
+-/
+import Mathlib.CategoryTheory.Galois.EssSurj
+import Mathlib.CategoryTheory.Action.Continuous
+import Mathlib.Topology.Category.FinTopCat
+
+/-!
+# Fiber functors induce an equivalence of categories
+
+Let `C` be a Galois category with fiber functor `F`.
+
+In this file we conclude that the induced functor from `C` to the category of finite,
+discrete `Aut F`-sets is an equivalence of categories.
+-/
+
+universe u₂ u₁ w
+
+open CategoryTheory
+
+namespace CategoryTheory
+
+variable {C : Type u₁} [Category.{u₂} C] {F : C ⥤ FintypeCat.{w}}
+
+namespace PreGaloisCategory
+
+variable [GaloisCategory C] [FiberFunctor F]
+
+open scoped FintypeCatDiscrete
+
+variable (F) in
+/-- The induced functor from `C` to the category of finite, discrete `Aut F`-sets. -/
+@[simps! obj_obj map]
+def functorToContAction : C ⥤ ContAction FintypeCat (Aut F) :=
+  ObjectProperty.lift _ (functorToAction F) (fun X ↦ continuousSMul_aut_fiber F X)
+
+instance : (functorToContAction F).Faithful :=
+  inferInstanceAs <| (ObjectProperty.lift _ _ _).Faithful
+
+instance : (functorToContAction F).Full :=
+  inferInstanceAs <| (ObjectProperty.lift _ _ _).Full
+
+instance {F : C ⥤ FintypeCat.{u₁}} [FiberFunctor F] : (functorToContAction F).EssSurj where
+  mem_essImage X := by
+    have : ContinuousSMul (Aut F) X.obj.V.carrier := X.2
+    obtain ⟨A, ⟨i⟩⟩ := exists_lift_of_continuous (F := F) X
+    exact ⟨A, ⟨ObjectProperty.isoMk _ i⟩⟩
+
+instance : (functorToContAction F).EssSurj := by
+  let F' : C ⥤ FintypeCat.{u₁} := F ⋙ FintypeCat.uSwitch.{w, u₁}
+  letI : FiberFunctor F' := FiberFunctor.comp_right _
+  have : (functorToContAction F').EssSurj := inferInstance
+  let f : Aut F ≃ₜ* Aut F' :=
+    (autEquivAutWhiskerRight F (FintypeCat.uSwitchEquivalence.{w, u₁}).fullyFaithfulFunctor)
+  let equiv : ContAction FintypeCat.{u₁} (Aut F') ≌ ContAction FintypeCat.{w} (Aut F) :=
+    (FintypeCat.uSwitchEquivalence.{u₁, w}.mapContAction (Aut F')
+       (fun X ↦ by
+          rw [Action.isContinuous_def]
+          show Continuous ((fun p ↦ (FintypeCat.uSwitchEquiv X.obj.V).symm p) ∘
+              (fun p : Aut F' × _ ↦ (X.obj.ρ p.1) p.2) ∘
+              (fun p : Aut F' × _ ↦ (p.1, FintypeCat.uSwitchEquiv _ p.2)))
+          have : Continuous (fun p : Aut F' × _ ↦ (X.obj.ρ p.1) p.2) := X.2.1
+          fun_prop)
+       (fun X ↦ by
+          rw [Action.isContinuous_def]
+          show Continuous ((fun p ↦ (FintypeCat.uSwitchEquiv X.obj.V).symm p) ∘
+              (fun p : Aut F' × _ ↦ (X.obj.ρ p.1) p.2) ∘
+              (fun p : Aut F' × _ ↦ (p.1, FintypeCat.uSwitchEquiv _ p.2)))
+          have : Continuous (fun p : Aut F' × _ ↦ (X.obj.ρ p.1) p.2) := X.2.1
+          fun_prop)).trans <|
+      ContAction.resEquiv _ f
+  have : functorToContAction F ≅ functorToContAction F' ⋙ equiv.functor :=
+    NatIso.ofComponents
+      (fun X ↦ ObjectProperty.isoMk _ (Action.mkIso (FintypeCat.uSwitchEquivalence.unitIso.app _)
+      (fun g ↦ FintypeCat.uSwitchEquivalence.unitIso.hom.naturality (g.hom.app X))))
+      (fun f ↦ by
+        ext : 2
+        exact FintypeCat.uSwitchEquivalence.unitIso.hom.naturality (F.map f))
+  exact Functor.essSurj_of_iso this.symm
+
+/-- Any fiber functor `F` induces an equivalence of categories with the category of finite and
+discrete `Aut F`-sets. -/
+@[stacks 0BN4]
+instance : (functorToContAction F).IsEquivalence where
+
+end PreGaloisCategory
+
+end CategoryTheory

Mathlib/CategoryTheory/Galois/Topology.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Christian Merten
 -/
 import Mathlib.CategoryTheory.Galois.Prorepresentability
+import Mathlib.Topology.Algebra.ContinuousMonoidHom
 import Mathlib.Topology.Algebra.Group.Basic
 
 /-!
@@ -118,6 +119,27 @@ instance continuousSMul_aut_fiber (X : C) : ContinuousSMul (Aut F) (F.obj X) whe
     show Continuous (g ∘ h)
     fun_prop
 
+/-- If `G` is a functor of categories of finite types, the induced map `Aut F → Aut (F ⋙ G)` is
+continuous. -/
+lemma continuous_mapAut_whiskeringRight (G : FintypeCat.{w} ⥤ FintypeCat.{v}) :
+    Continuous (((whiskeringRight _ _ _).obj G).mapAut F) := by
+  rw [Topology.IsInducing.continuous_iff (autEmbedding_isClosedEmbedding _).isInducing,
+    continuous_pi_iff]
+  intro X
+  show Continuous fun a ↦ G.mapAut (F.obj X) (autEmbedding F a X)
+  fun_prop
+
+/-- If `G` is a fully faithful functor of categories finite types, this is the automorphism of
+topological groups `Aut F ≃ Aut (F ⋙ G)`. -/
+noncomputable def autEquivAutWhiskerRight {G : FintypeCat.{w} ⥤ FintypeCat.{v}}
+    (h : G.FullyFaithful) :
+    Aut F ≃ₜ* Aut (F ⋙ G) where
+  __ := (h.whiskeringRight C).autMulEquivOfFullyFaithful F
+  continuous_toFun := continuous_mapAut_whiskeringRight F G
+  continuous_invFun := Continuous.continuous_symm_of_equiv_compact_to_t2
+    (f := ((h.whiskeringRight C).autMulEquivOfFullyFaithful F).toEquiv)
+    (continuous_mapAut_whiskeringRight F G)
+
 variable [GaloisCategory C] [FiberFunctor F]
 
 /--

Mathlib/Topology/Category/FinTopCat.lean

@@ -66,3 +66,18 @@ instance (X : FinTopCat) : Fintype ((forget₂ FinTopCat TopCat).obj X) :=
   X.fintype
 
 end FinTopCat
+
+namespace FintypeCatDiscrete
+
+/-- Scoped topological space instance on objects of the category of finite types, assigning
+the discrete topology. -/
+scoped instance (X : FintypeCat) : TopologicalSpace X := ⊥
+scoped instance (X : FintypeCat) : DiscreteTopology X := ⟨rfl⟩
+
+/-- The forgetful functor from finite types to topological spaces, forgetting discreteness.
+This is a scoped instance. -/
+scoped instance : HasForget₂ FintypeCat TopCat where
+  forget₂.obj X := TopCat.of X
+  forget₂.map f := TopCat.ofHom ⟨f, continuous_of_discreteTopology⟩
+
+end FintypeCatDiscrete