feat(CategoryTheory/Galois): definition and characterisation of Galoi…

…s objects (#10215)

Defines Galois objects in a Galois category in a fibre functor independent way, also gives an equivalent characterisation in terms of a fibre functor.

To allow for a definition that only depends on `C`, contrary to what was said earlier, we introduce a `GaloisCategory` typeclass extending `PreGaloisCategory` that additionally asserts the existence of a fibre functor.

Mathlib.lean

@@ -1064,6 +1064,7 @@ import Mathlib.CategoryTheory.Functor.ReflectsIso
 import Mathlib.CategoryTheory.Functor.Trifunctor
 import Mathlib.CategoryTheory.Galois.Basic
 import Mathlib.CategoryTheory.Galois.Examples
+import Mathlib.CategoryTheory.Galois.GaloisObjects
 import Mathlib.CategoryTheory.Generator
 import Mathlib.CategoryTheory.GlueData
 import Mathlib.CategoryTheory.GradedObject

Mathlib/CategoryTheory/Endomorphism.lean

@@ -5,6 +5,7 @@ Authors: Yury Kudryashov, Scott Morrison, Simon Hudon
 -/
 import Mathlib.Algebra.Group.Equiv.Basic
 import Mathlib.Algebra.Group.Units
+import Mathlib.Algebra.Group.Units.Hom
 import Mathlib.CategoryTheory.Groupoid
 import Mathlib.CategoryTheory.Opposites
 import Mathlib.GroupTheory.GroupAction.Defs
@@ -168,6 +169,10 @@ def unitsEndEquivAut : (End X)ˣ ≃* Aut X where
 set_option linter.uppercaseLean3 false in
 #align category_theory.Aut.units_End_equiv_Aut CategoryTheory.Aut.unitsEndEquivAut
 
+/-- The inclusion of `Aut X` to `End X` as a monoid homomorphism. -/
+@[simps!]
+def toEnd (X : C) : Aut X →* End X := (Units.coeHom (End X)).comp (Aut.unitsEndEquivAut X).symm
+
 /-- Isomorphisms induce isomorphisms of the automorphism group -/
 def autMulEquivOfIso {X Y : C} (h : X ≅ Y) : Aut X ≃* Aut Y where
   toFun x := ⟨h.inv ≫ x.hom ≫ h.hom, h.inv ≫ x.inv ≫ h.hom, _, _⟩

Mathlib/CategoryTheory/Galois/Basic.lean

@@ -22,6 +22,7 @@ the definitions in Lenstras notes (see below for a reference).
 
 * `PreGaloisCategory` : defining properties of Galois categories not involving a fibre functor
 * `FibreFunctor`      : a fibre functor from a PreGaloisCategory to `FintypeCat`
+* `GaloisCategory`    : a `PreGaloisCategory` that admits a `FibreFunctor`
 * `ConnectedObject`   : an object of a category that is not initial and has no non-trivial
                         subobjects
 
@@ -50,8 +51,8 @@ A category `C` is a PreGalois category if it satisfies all properties
 of a Galois category in the sense of SGA1 that do not involve a fibre functor.
 A Galois category should furthermore admit a fibre functor.
 
-We do not provide a typeclass `GaloisCategory`; users should
-assume `[PreGaloisCategory C] (F : C ⥤ FintypeCat) [FibreFunctor F]` instead.
+The only difference between `[PreGaloisCategory C] (F : C ⥤ FintypeCat) [FibreFunctor F]` and
+`[GaloisCategory C]` is that the former fixes one fibre functor `F`.
 -/
 
 /-- Definition of a (Pre)Galois category. Lenstra, Def 3.1, (G1)-(G3) -/
@@ -122,6 +123,9 @@ variable {C : Type u₁} [Category.{u₂, u₁} C] {F : C ⥤ FintypeCat.{w}} [P
 attribute [instance] preservesTerminalObjects preservesPullbacks preservesEpis
   preservesFiniteCoproducts reflectsIsos preservesQuotientsByFiniteGroups
 
+noncomputable instance : ReflectsLimitsOfShape (Discrete PEmpty.{1}) F :=
+  reflectsLimitsOfShapeOfReflectsIsomorphisms
+
 noncomputable instance : ReflectsColimitsOfShape (Discrete PEmpty.{1}) F :=
   reflectsColimitsOfShapeOfReflectsIsomorphisms
 
@@ -169,7 +173,7 @@ lemma not_initial_of_inhabited {X : C} (x : F.obj X) (h : IsInitial X) : False :
   ((initial_iff_fibre_empty F X).mp ⟨h⟩).false x
 
 /-- The fibre of a connected object is nonempty. -/
-lemma nonempty_fibre_of_connected (X : C) [ConnectedObject X] : Nonempty (F.obj X) := by
+instance nonempty_fibre_of_connected (X : C) [ConnectedObject X] : Nonempty (F.obj X) := by
   by_contra h
   have ⟨hin⟩ : Nonempty (IsInitial X) := (initial_iff_fibre_empty F X).mpr (not_nonempty_iff.mp h)
   exact ConnectedObject.notInitial hin
@@ -202,4 +206,29 @@ lemma evaluation_aut_injective_of_connected (A : C) [ConnectedObject A] (a : F.o
 
 end PreGaloisCategory
 
+/-- A `PreGaloisCategory` is a `GaloisCategory` if it admits a fibre functor. -/
+class GaloisCategory (C : Type u₁) [Category.{u₂, u₁} C]
+    extends PreGaloisCategory C : Prop where
+  hasFibreFunctor : ∃ F : C ⥤ FintypeCat.{u₂}, Nonempty (PreGaloisCategory.FibreFunctor F)
+
+namespace PreGaloisCategory
+
+variable {C : Type u₁} [Category.{u₂, u₁} C] [GaloisCategory C]
+
+/-- In a `GaloisCategory` the set of morphisms out of a connected object is finite. -/
+instance (A X : C) [ConnectedObject A] : Finite (A ⟶ X) := by
+  obtain ⟨F, ⟨hF⟩⟩ := @GaloisCategory.hasFibreFunctor C _ _
+  obtain ⟨a⟩ := nonempty_fibre_of_connected F A
+  apply Finite.of_injective (fun f ↦ F.map f a)
+  exact evaluationInjective_of_connected F A X a
+
+/-- In a `GaloisCategory` the set of automorphism of a connected object is finite. -/
+instance (A : C) [ConnectedObject A] : Finite (Aut A) := by
+  obtain ⟨F, ⟨hF⟩⟩ := @GaloisCategory.hasFibreFunctor C _ _
+  obtain ⟨a⟩ := nonempty_fibre_of_connected F A
+  apply Finite.of_injective (fun f ↦ F.map f.hom a)
+  exact evaluation_aut_injective_of_connected F A a
+
+end PreGaloisCategory
+
 end CategoryTheory

Mathlib/CategoryTheory/Galois/Examples.lean

@@ -98,6 +98,10 @@ noncomputable instance : FibreFunctor (Action.forget FintypeCat (MonCat.of G)) w
   preservesQuotientsByFiniteGroups _ _ _ := inferInstance
   reflectsIsos := ⟨fun f (h : IsIso f.hom) => inferInstance⟩
 
+/-- The category of finite `G`-sets is a `GaloisCategory`. -/
+instance : GaloisCategory (Action FintypeCat (MonCat.of G)) where
+  hasFibreFunctor := ⟨Action.forget FintypeCat (MonCat.of G), ⟨inferInstance⟩⟩
+
 end FintypeCat
 
 end CategoryTheory

Mathlib/CategoryTheory/Galois/GaloisObjects.lean

@@ -0,0 +1,100 @@
+/-
+Copyright (c) 2024 Christian Merten. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Merten
+-/
+import Mathlib.CategoryTheory.Galois.Basic
+import Mathlib.CategoryTheory.Limits.FintypeCat
+import Mathlib.CategoryTheory.Limits.Preserves.Limits
+import Mathlib.CategoryTheory.Limits.Shapes.SingleObj
+import Mathlib.Logic.Equiv.TransferInstance
+
+/-!
+# Galois objects in Galois categories
+
+We define when a connected object of a Galois category `C` is Galois in a fibre functor independent
+way and show equivalent characterisations.
+
+## Main definitions
+
+* `IsGalois` : Connected object `X` of `C` such that `X / Aut X` is terminal.
+
+## Main results
+
+* `galois_iff_pretransitive` : A connected object `X` is Galois if and only if `Aut X`
+                               acts transitively on `F.obj X` for a fibre functor `F`.
+
+-/
+universe u₁ u₂ v₁ v₂ v w
+
+namespace CategoryTheory
+
+namespace PreGaloisCategory
+
+open Limits Functor
+
+noncomputable instance {G : Type v} [Group G] [Finite G] :
+    PreservesColimitsOfShape (SingleObj G) FintypeCat.incl.{w} := by
+  choose G' hg hf e using Finite.exists_type_zero_nonempty_mulEquiv G
+  exact Limits.preservesColimitsOfShapeOfEquiv (Classical.choice e).toSingleObjEquiv.symm _
+
+/-- A connected object `X` of `C` is Galois if the quotient `X / Aut X` is terminal. -/
+class IsGalois {C : Type u₁} [Category.{u₂, u₁} C] [GaloisCategory C] (X : C)
+    extends ConnectedObject X : Prop where
+  quotientByAutTerminal : Nonempty (IsTerminal <| colimit <| SingleObj.functor <| Aut.toEnd X)
+
+variable {C : Type u₁} [Category.{u₂, u₁} C]
+
+/-- The natural action of `Aut X` on `F.obj X`. -/
+instance autMulFibre (F : C ⥤ FintypeCat.{w}) (X : C) : MulAction (Aut X) (F.obj X) where
+  smul σ a := F.map σ.hom a
+  one_smul a := by
+    show F.map (𝟙 X) a = a
+    simp only [map_id, FintypeCat.id_apply]
+  mul_smul g h a := by
+    show F.map (h.hom ≫ g.hom) a = (F.map h.hom ≫ F.map g.hom) a
+    simp only [map_comp, FintypeCat.comp_apply]
+
+variable [GaloisCategory C] (F : C ⥤ FintypeCat.{w}) [FibreFunctor F]
+
+/-- For a connected object `X` of `C`, the quotient `X / Aut X` is terminal if and only if
+the quotient `F.obj X / Aut X` has exactly one element. -/
+noncomputable def quotientByAutTerminalEquivUniqueQuotient
+    (X : C) [ConnectedObject X] :
+    IsTerminal (colimit <| SingleObj.functor <| Aut.toEnd X) ≃
+    Unique (MulAction.orbitRel.Quotient (Aut X) (F.obj X)) := by
+  let J : SingleObj (Aut X) ⥤ C := SingleObj.functor (Aut.toEnd X)
+  let e : (F ⋙ FintypeCat.incl).obj (colimit J) ≅ _ :=
+    preservesColimitIso (F ⋙ FintypeCat.incl) J ≪≫
+    (Equiv.toIso <| SingleObj.Types.colimitEquivQuotient (J ⋙ F ⋙ FintypeCat.incl))
+  apply Equiv.trans
+  apply (IsTerminal.isTerminalIffObj (F ⋙ FintypeCat.incl) _).trans
+    (isLimitEmptyConeEquiv _ (asEmptyCone _) (asEmptyCone _) e)
+  exact Types.isTerminalEquivUnique _
+
+lemma isGalois_iff_aux (X : C) [ConnectedObject X] :
+    IsGalois X ↔ Nonempty (IsTerminal <| colimit <| SingleObj.functor <| Aut.toEnd X) :=
+  ⟨fun h ↦ h.quotientByAutTerminal, fun h ↦ ⟨h⟩⟩
+
+/-- Given a fibre functor `F` and a connected object `X` of `C`. Then `X` is Galois if and only if
+the natural action of `Aut X` on `F.obj X` is transitive. -/
+theorem isGalois_iff_pretransitive (X : C) [ConnectedObject X] :
+    IsGalois X ↔ MulAction.IsPretransitive (Aut X) (F.obj X) := by
+  rw [isGalois_iff_aux, Equiv.nonempty_congr <| quotientByAutTerminalEquivUniqueQuotient F X]
+  exact (MulAction.pretransitive_iff_unique_quotient_of_nonempty (Aut X) (F.obj X)).symm
+
+/-- If `X` is Galois, the quotient `X / Aut X` is terminal.  -/
+noncomputable def isTerminalQuotientOfIsGalois (X : C) [IsGalois X] :
+    IsTerminal <| colimit <| SingleObj.functor <| Aut.toEnd X :=
+  Nonempty.some IsGalois.quotientByAutTerminal
+
+/-- If `X` is Galois, then the action of `Aut X` on `F.obj X` is
+transitive for every fibre functor `F`. -/
+instance isPretransitive_of_isGalois (X : C) [IsGalois X] :
+    MulAction.IsPretransitive (Aut X) (F.obj X) := by
+  rw [← isGalois_iff_pretransitive]
+  infer_instance
+
+end PreGaloisCategory
+
+end CategoryTheory

Mathlib/GroupTheory/GroupAction/Basic.lean

@@ -438,6 +438,23 @@ def orbitRel.Quotient : Type _ :=
 #align mul_action.orbit_rel.quotient MulAction.orbitRel.Quotient
 #align add_action.orbit_rel.quotient AddAction.orbitRel.Quotient
 
+/-- An action is pretransitive if and only if the quotient by `MulAction.orbitRel` is a
+subsingleton. -/
+theorem pretransitive_iff_subsingleton_quotient :
+    IsPretransitive G α ↔ Subsingleton (orbitRel.Quotient G α) := by
+  refine ⟨fun _ ↦ ⟨fun a b ↦ ?_⟩, fun _ ↦ ⟨fun a b ↦ ?_⟩⟩
+  · refine Quot.inductionOn a (fun x ↦ ?_)
+    exact Quot.inductionOn b (fun y ↦ Quot.sound <| exists_smul_eq G y x)
+  · have h : Quotient.mk (orbitRel G α) b = ⟦a⟧ := Subsingleton.elim _ _
+    exact Quotient.eq_rel.mp h
+
+/-- If `α` is non-empty, an action is pretransitive if and only if the quotient has exactly one
+element. -/
+theorem pretransitive_iff_unique_quotient_of_nonempty [Nonempty α] :
+    IsPretransitive G α ↔ Nonempty (Unique <| orbitRel.Quotient G α) := by
+  rw [unique_iff_subsingleton_and_nonempty, pretransitive_iff_subsingleton_quotient, iff_self_and]
+  exact fun _ ↦ (nonempty_quotient_iff _).mpr inferInstance
+
 variable {G α}
 
 /-- The orbit corresponding to an element of the quotient by `MulAction.orbitRel` -/