Skip to content

Commit 9a8dc7a

Browse files
chrisflavchrisflav
committed
feat(CategoryTheory/Galois): finite G-sets are a PreGaloisCategory (#9879)
We show that the category of finite `G`-sets is a `PreGaloisCategory` and the forgetful functor to finite sets is a `FibreFunctor`.
1 parent d1054e1 commit 9a8dc7a

4 files changed

Lines changed: 122 additions & 0 deletions

File tree

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1050,6 +1050,7 @@ import Mathlib.CategoryTheory.Functor.InvIsos
10501050
import Mathlib.CategoryTheory.Functor.ReflectsIso
10511051
import Mathlib.CategoryTheory.Functor.Trifunctor
10521052
import Mathlib.CategoryTheory.Galois.Basic
1053+
import Mathlib.CategoryTheory.Galois.Examples
10531054
import Mathlib.CategoryTheory.Generator
10541055
import Mathlib.CategoryTheory.GlueData
10551056
import Mathlib.CategoryTheory.GradedObject

‎Mathlib/CategoryTheory/Galois/Examples.lean‎

Lines changed: 103 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,103 @@
1+
/-
2+
Copyright (c) 2024 Christian Merten. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Christian Merten
5+
-/
6+
import Mathlib.CategoryTheory.Galois.Basic
7+
import Mathlib.RepresentationTheory.Action.Basic
8+
import Mathlib.RepresentationTheory.Action.Limits
9+
import Mathlib.CategoryTheory.Limits.FintypeCat
10+
import Mathlib.CategoryTheory.Limits.Shapes.Types
11+
import Mathlib.Logic.Equiv.TransferInstance
12+
13+
/-!
14+
# Examples of Galois categories and fibre functors
15+
16+
We show that for a group `G` the category of finite `G`-sets is a `PreGaloisCategory` and that the
17+
forgetful functor to `FintypeCat` is a `FibreFunctor`.
18+
19+
## Todo
20+
21+
* Characterize connected objects in the category of finite `G`-sets as those with transitive
22+
`G`-action
23+
24+
-/
25+
26+
universe u v w
27+
28+
namespace CategoryTheory
29+
30+
namespace FintypeCat
31+
32+
open Limits Functor PreGaloisCategory
33+
34+
/-- Complement of the image of a morphism `f : X ⟶ Y` in `FintypeCat`. -/
35+
noncomputable def imageComplement {X Y : FintypeCat.{u}} (f : X ⟶ Y) :
36+
FintypeCat.{u} := by
37+
haveI : Fintype (↑(Set.range f)ᶜ) := Fintype.ofFinite _
38+
exact FintypeCat.of (↑(Set.range f)ᶜ)
39+
40+
/-- The inclusion from the complement of the image of `f : X ⟶ Y` into `Y`. -/
41+
def imageComplementIncl {X Y : FintypeCat.{u}}
42+
(f : X ⟶ Y) : imageComplement f ⟶ Y :=
43+
Subtype.val
44+
45+
variable (G : Type u) [Group G]
46+
47+
/-- Given `f : X ⟶ Y` for `X Y : Action FintypeCat (MonCat.of G)`, the complement of the image
48+
of `f` has a natural `G`-action. -/
49+
noncomputable def Action.imageComplement {X Y : Action FintypeCat (MonCat.of G)}
50+
(f : X ⟶ Y) : Action FintypeCat (MonCat.of G) where
51+
V := FintypeCat.imageComplement f.hom
52+
ρ := MonCat.ofHom <| {
53+
toFun := fun g y ↦ Subtype.mk (Y.ρ g y.val) <| by
54+
intro ⟨x, h⟩
55+
apply y.property
56+
use X.ρ g⁻¹ x
57+
calc (X.ρ g⁻¹ ≫ f.hom) x
58+
= (Y.ρ g⁻¹ * Y.ρ g) y.val := by rw [f.comm, FintypeCat.comp_apply, h]; rfl
59+
_ = y.val := by rw [← map_mul, mul_left_inv, Action.ρ_one, FintypeCat.id_apply]
60+
map_one' := by simp only [Action.ρ_one]; rfl
61+
map_mul' := fun g h ↦ FintypeCat.hom_ext _ _ <| fun y ↦ Subtype.ext <| by
62+
exact congrFun (MonoidHom.map_mul Y.ρ g h) y.val
63+
}
64+
65+
/-- The inclusion from the complement of the image of `f : X ⟶ Y` into `Y`. -/
66+
def Action.imageComplementIncl {X Y : Action FintypeCat (MonCat.of G)} (f : X ⟶ Y) :
67+
Action.imageComplement G f ⟶ Y where
68+
hom := FintypeCat.imageComplementIncl f.hom
69+
comm _ := rfl
70+
71+
instance {X Y : Action FintypeCat (MonCat.of G)} (f : X ⟶ Y) :
72+
Mono (Action.imageComplementIncl G f) := by
73+
apply Functor.mono_of_mono_map (forget _)
74+
apply ConcreteCategory.mono_of_injective
75+
exact Subtype.val_injective
76+
77+
/-- The category of finite sets has quotients by finite groups in arbitrary universes. -/
78+
instance [Finite G] : HasColimitsOfShape (SingleObj G) FintypeCat.{w} := by
79+
obtain ⟨G', hg, hf, ⟨e⟩⟩ := Finite.exists_type_zero_nonempty_mulEquiv G
80+
exact Limits.hasColimitsOfShape_of_equivalence e.toSingleObjEquiv.symm
81+
82+
noncomputable instance : PreservesFiniteLimits (forget (Action FintypeCat (MonCat.of G))) := by
83+
show PreservesFiniteLimits (Action.forget FintypeCat _ ⋙ FintypeCat.incl)
84+
apply compPreservesFiniteLimits
85+
86+
/-- The category of finite `G`-sets is a `PreGaloisCategory`. -/
87+
instance : PreGaloisCategory (Action FintypeCat (MonCat.of G)) where
88+
hasQuotientsByFiniteGroups G _ _ := inferInstance
89+
monoInducesIsoOnDirectSummand {X Y} i h :=
90+
⟨Action.imageComplement G i, Action.imageComplementIncl G i,
91+
⟨isColimitOfReflects (Action.forget _ _ ⋙ FintypeCat.incl) <|
92+
(isColimitMapCoconeBinaryCofanEquiv (forget _) i _).symm
93+
(Types.isCoprodOfMono ((forget _).map i))⟩⟩
94+
95+
/-- The forgetful functor from finite `G`-sets to sets is a `FibreFunctor`. -/
96+
noncomputable instance : FibreFunctor (Action.forget FintypeCat (MonCat.of G)) where
97+
preservesFiniteCoproducts := ⟨fun _ _ ↦ inferInstance⟩
98+
preservesQuotientsByFiniteGroups _ _ _ := inferInstance
99+
reflectsIsos := ⟨fun f (h : IsIso f.hom) => inferInstance⟩
100+
101+
end FintypeCat
102+
103+
end CategoryTheory

‎Mathlib/CategoryTheory/SingleObj.lean‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Yury Kudryashov
55
-/
66
import Mathlib.CategoryTheory.Endomorphism
7+
import Mathlib.CategoryTheory.FinCategory
78
import Mathlib.CategoryTheory.Category.Cat
89
import Mathlib.Algebra.Category.MonCat.Basic
910
import Mathlib.Combinatorics.Quiver.SingleObj
@@ -78,6 +79,10 @@ theorem comp_as_mul {x y z : SingleObj M} (f : x ⟶ y) (g : y ⟶ z) : f ≫ g
7879
rfl
7980
#align category_theory.single_obj.comp_as_mul CategoryTheory.SingleObj.comp_as_mul
8081

82+
/-- If `M` is finite and in universe zero, then `SingleObj M` is a `FinCategory`. -/
83+
instance finCategoryOfFintype (M : Type) [Fintype M] [Monoid M] : FinCategory (SingleObj M)
84+
where
85+
8186
/-- Groupoid structure on `SingleObj M`.
8287
8388
See <https://stacks.math.columbia.edu/tag/0019>.

‎Mathlib/Logic/Equiv/TransferInstance.lean‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -740,3 +740,16 @@ end R
740740
end Instances
741741

742742
end Equiv
743+
744+
namespace Finite
745+
746+
attribute [-instance] Fin.instMulFin
747+
748+
/-- Any finite group in universe `u` is equivalent to some finite group in universe `0`. -/
749+
lemma exists_type_zero_nonempty_mulEquiv (G : Type u) [Group G] [Finite G] :
750+
∃ (G' : Type) (_ : Group G') (_ : Fintype G'), Nonempty (G ≃* G') := by
751+
obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin G
752+
letI groupH : Group (Fin n) := Equiv.group e.symm
753+
exact ⟨Fin n, inferInstance, inferInstance, ⟨MulEquiv.symm <| Equiv.mulEquiv e.symm⟩⟩
754+
755+
end Finite

0 commit comments

Comments
 (0)