Tannaka duality for G-sets

A monoid G can be read off from the category Action (Type u) G of G-sets together with the forgetful functor Action.forget (Type u) G to types: the monoid of natural endomorphisms of that functor is G itself, so its automorphism group is the unit group Gˣ, which for a group G is G again.

The proof is the usual one. A natural endomorphism η is determined by its value s at the identity of the left regular G-set Action.leftRegular G, because for every G-set A and every point x of A the orbit map a ↦ a • x is a map of G-sets out of the left regular one, and naturality against it forces η to act as x ↦ s • x.

The last statements below transport this along an equivalence: a functor C ⥤ Type u that factors as an equivalence onto G-sets followed by the forgetful functor has endomorphism monoid G and automorphism group Gˣ. This is the form the classification of covering spaces consumes, with C the covering spaces of a based space and G its fundamental group.

No finiteness enters, so this is not Mathlib's CategoryTheory.PreGaloisCategory picture: there a fibre functor takes values in FintypeCat and CategoryTheory.PreGaloisCategory.IsFundamentalGroup asks for a compact topological group, which for a discrete G means a finite one.

Main declarations

• TauCeti.toEndForgetAction: the monoid map sending g : G to the natural endomorphism of the forgetful functor acting by g, with TauCeti.toEndForgetAction_app_apply computing it.
• CategoryTheory.Action.leftRegularHom: the orbit map of a point of a G-set, as a map of G-sets out of the left regular G-set.
• TauCeti.end_forgetAction_app_apply: a natural endomorphism of the forgetful functor acts on every G-set by the element of G it produces at the identity of the left regular G-set.
• TauCeti.endForgetActionMulEquiv: Tannaka duality for G-sets: G is the monoid of natural endomorphisms of the forgetful functor.
• TauCeti.unitsAutForgetActionMulEquiv: the automorphism form, over a monoid: the automorphism group of the forgetful functor is Gˣ.
• TauCeti.autForgetActionMulEquiv: its specialisation to a group G, where the automorphism group is G itself.
• TauCeti.endCompForgetActionMulEquiv, TauCeti.unitsAutCompForgetActionMulEquiv and TauCeti.autCompForgetActionMulEquiv: all three forms transported along an equivalence C ⥤ Action (Type u) G.

References

The argument is the standard Tannaka reconstruction of a group from its permutation representations; see for instance Lenstra, Galois theory for schemes, Section 3, where the same naturality-against-orbit-maps computation identifies the automorphism group of a fibre functor. Mathlib's Mathlib/RepresentationTheory/Tannaka.lean proves the linear analogue for finite groups, a different statement sharing no proof with this one.

def TauCeti.toEndForgetAction (G : Type u) [Monoid G] : G →* CategoryTheory.End (Action.forget (Type u) G)

Acting by g : G on every G-set is a natural endomorphism of the forgetful functor from G-sets to types; this is the resulting monoid map G →* End (Action.forget (Type u) G).

Equations

• TauCeti.toEndForgetAction G = { toFun := fun (g : G) => { app := fun (A : Action (Type ?u.1) G) => A.ρ g, naturality := ⋯ }, map_one' := ⋯, map_mul' := ⋯ }

theorem TauCeti.toEndForgetAction_app_apply {G : Type u} [Monoid G] (g : G) (A : Action (Type u) G) (x : CategoryTheory.ToType A) : (CategoryTheory.ConcreteCategory.hom (((toEndForgetAction G) g).app A)) x = g • x

The computation rule for TauCeti.toEndForgetAction.

This is not a simp lemma: the type of NatTrans.app puts (Action.forget (Type u) G).obj A in the coercion of the left-hand side, and simp rewrites that to A.V by Action.forget_obj, so the left-hand side here is not in simp-normal form.

theorem TauCeti.toEndForgetAction_app_leftRegular_one {G : Type u} [Monoid G] (g : G) : (CategoryTheory.ConcreteCategory.hom (((toEndForgetAction G) g).app (Action.leftRegular G))) 1 = g

The value of TauCeti.toEndForgetAction G g at the identity of the left regular G-set; not a simp lemma, for the reason given at TauCeti.toEndForgetAction_app_apply.

def CategoryTheory.Action.leftRegularHom {G : Type u} [Monoid G] {A : Action (Type u) G} (x : ToType A) : Action.leftRegular G ⟶ A

The orbit map a ↦ a • x of a point x of a G-set A, as a map of G-sets from the left regular G-set to A.

Equations

• CategoryTheory.Action.leftRegularHom x = { hom := TypeCat.ofHom fun (a : G) => a • x, comm := ⋯ }

@[simp]

theorem CategoryTheory.Action.leftRegularHom_hom_apply {G : Type u} [Monoid G] {A : Action (Type u) G} (x : ToType A) (a : G) : (ConcreteCategory.hom (leftRegularHom x).hom) a = a • x

theorem TauCeti.end_forgetAction_app_apply {G : Type u} [Monoid G] (η : CategoryTheory.End (Action.forget (Type u) G)) {s : G} (hs : (CategoryTheory.ConcreteCategory.hom (η.app (Action.leftRegular G))) 1 = s) (A : Action (Type u) G) (x : CategoryTheory.ToType A) : (CategoryTheory.ConcreteCategory.hom (η.app A)) x = s • x

A natural endomorphism of the forgetful functor from G-sets to types acts on every G-set as the element of G it produces at the identity of the left regular G-set: naturality against the orbit map CategoryTheory.Action.leftRegularHom leaves it no other choice.

theorem TauCeti.toEndForgetAction_bijective (G : Type u) [Monoid G] : Function.Bijective ⇑(toEndForgetAction G)

Acting by the elements of G exhausts the natural endomorphisms of the forgetful functor, and does so without repetition: evaluation at the identity of the left regular G-set inverts TauCeti.toEndForgetAction, by TauCeti.end_forgetAction_app_apply.

noncomputable def TauCeti.endForgetActionMulEquiv (G : Type u) [Monoid G] : G ≃* CategoryTheory.End (Action.forget (Type u) G)

Tannaka duality for G-sets. A monoid G is the monoid of natural endomorphisms of the forgetful functor from G-sets to types.

Equations

• TauCeti.endForgetActionMulEquiv G = MulEquiv.ofBijective (TauCeti.toEndForgetAction G) ⋯

@[simp]

theorem TauCeti.endForgetActionMulEquiv_apply {G : Type u} [Monoid G] (g : G) : (endForgetActionMulEquiv G) g = (toEndForgetAction G) g

@[simp]

theorem TauCeti.endForgetActionMulEquiv_symm_apply_eq {G : Type u} [Monoid G] (η : CategoryTheory.End (Action.forget (Type u) G)) (g : G) : (endForgetActionMulEquiv G).symm η = g ↔ (CategoryTheory.ConcreteCategory.hom (η.app (Action.leftRegular G))) 1 = g

The inverse Tannaka equivalence is characterized by evaluation at the identity of the left regular G-set.

noncomputable def TauCeti.unitsAutForgetActionMulEquiv (G : Type u) [Monoid G] : Gˣ ≃* CategoryTheory.Aut (Action.forget (Type u) G)

Tannaka duality for G-sets, automorphism form: the automorphism group of the forgetful functor from G-sets to types is the group of units of the monoid G.

An automorphism is an invertible endomorphism, so this is the endomorphism form TauCeti.endForgetActionMulEquiv on units.

Equations

• TauCeti.unitsAutForgetActionMulEquiv G = (Units.mapEquiv (TauCeti.endForgetActionMulEquiv G)).trans (CategoryTheory.Aut.unitsEndEquivAut (Action.forget (Type ?u.1) G))

theorem TauCeti.unitsAutForgetActionMulEquiv_hom_app_apply {G : Type u} [Monoid G] (g : Gˣ) (A : Action (Type u) G) (x : CategoryTheory.ToType A) : (CategoryTheory.ConcreteCategory.hom (((unitsAutForgetActionMulEquiv G) g).hom.app A)) x = ↑g • x

The automorphism attached to a unit g acts by g; not a simp lemma, for the reason given at TauCeti.toEndForgetAction_app_apply.

theorem TauCeti.unitsAutForgetActionMulEquiv_inv_app_apply {G : Type u} [Monoid G] (g : Gˣ) (A : Action (Type u) G) (x : CategoryTheory.ToType A) : (CategoryTheory.ConcreteCategory.hom (((unitsAutForgetActionMulEquiv G) g).inv.app A)) x = ↑g⁻¹ • x

The inverse of the automorphism attached to a unit g acts by g⁻¹; not a simp lemma, for the reason given at TauCeti.toEndForgetAction_app_apply.

@[simp]

theorem TauCeti.unitsAutForgetActionMulEquiv_symm_apply_eq {G : Type u} [Monoid G] (η : CategoryTheory.Aut (Action.forget (Type u) G)) (g : Gˣ) : (unitsAutForgetActionMulEquiv G).symm η = g ↔ (CategoryTheory.ConcreteCategory.hom (η.hom.app (Action.leftRegular G))) 1 = ↑g

The inverse of the automorphism form of Tannaka duality is characterized by evaluating the forward natural transformation at the identity of the left regular G-set.

noncomputable def TauCeti.endCompForgetActionMulEquiv (G : Type u) [Monoid G] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (e : CategoryTheory.Functor C (Action (Type u) G)) [e.IsEquivalence] : G ≃* CategoryTheory.End (e.comp (Action.forget (Type u) G))

Tannaka duality transported along an equivalence: if a functor e from a category C to G-sets is an equivalence, then G is the monoid of natural endomorphisms of the composite functor C ⥤ Type u.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.endCompForgetActionMulEquiv_app_apply {G : Type u} [Monoid G] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (e : CategoryTheory.Functor C (Action (Type u) G)) [e.IsEquivalence] (g : G) (p : C) (x : CategoryTheory.ToType (e.obj p)) : (CategoryTheory.ConcreteCategory.hom (((endCompForgetActionMulEquiv G e) g).app p)) x = g • x

The value of a transported natural endomorphism on a point of a fibre.

This is not a simp lemma: simp rewrites the composite (e ⋙ Action.forget (Type u) G).obj p appearing in the type of x to (Action.forget (Type u) G).obj (e.obj p), so the left-hand side here is not in simp-normal form.

noncomputable def TauCeti.unitsAutCompForgetActionMulEquiv (G : Type u) [Monoid G] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (e : CategoryTheory.Functor C (Action (Type u) G)) [e.IsEquivalence] : Gˣ ≃* CategoryTheory.Aut (e.comp (Action.forget (Type u) G))

The automorphism form of Tannaka duality, transported along an equivalence: if a functor e from a category C to G-sets is an equivalence, then Gˣ is the automorphism group of the composite C ⥤ Type u.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.unitsAutCompForgetActionMulEquiv_hom_app_apply {G : Type u} [Monoid G] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (e : CategoryTheory.Functor C (Action (Type u) G)) [e.IsEquivalence] (g : Gˣ) (p : C) (x : CategoryTheory.ToType (e.obj p)) : (CategoryTheory.ConcreteCategory.hom (((unitsAutCompForgetActionMulEquiv G e) g).hom.app p)) x = ↑g • x

The value of a transported natural automorphism on a point of a fibre; not a simp lemma, for the reason given at TauCeti.endCompForgetActionMulEquiv_app_apply.

theorem TauCeti.unitsAutCompForgetActionMulEquiv_inv_app_apply {G : Type u} [Monoid G] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (e : CategoryTheory.Functor C (Action (Type u) G)) [e.IsEquivalence] (g : Gˣ) (p : C) (x : CategoryTheory.ToType (e.obj p)) : (CategoryTheory.ConcreteCategory.hom (((unitsAutCompForgetActionMulEquiv G e) g).inv.app p)) x = ↑g⁻¹ • x

The inverse of a transported natural automorphism acts by the inverse unit on every fibre; not a simp lemma, for the reason given at TauCeti.endCompForgetActionMulEquiv_app_apply.

noncomputable def TauCeti.autForgetActionMulEquiv (G : Type u) [Group G] : G ≃* CategoryTheory.Aut (Action.forget (Type u) G)

Tannaka duality for G-sets, group form: a group G is the automorphism group of the forgetful functor from G-sets to types. This is the monoid form TauCeti.unitsAutForgetActionMulEquiv read through the identification toUnits of a group with its group of units.

Equations

• TauCeti.autForgetActionMulEquiv G = toUnits.trans (TauCeti.unitsAutForgetActionMulEquiv G)

theorem TauCeti.autForgetActionMulEquiv_apply {G : Type u} [Group G] (g : G) : (autForgetActionMulEquiv G) g = (unitsAutForgetActionMulEquiv G) (toUnits g)

The group form of Tannaka duality is the monoid form at the unit attached to g.

theorem TauCeti.autForgetActionMulEquiv_hom_app_apply {G : Type u} [Group G] (g : G) (A : Action (Type u) G) (x : CategoryTheory.ToType A) : (CategoryTheory.ConcreteCategory.hom (((autForgetActionMulEquiv G) g).hom.app A)) x = g • x

The automorphism attached to g acts by g; not a simp lemma, for the reason given at TauCeti.toEndForgetAction_app_apply.

theorem TauCeti.autForgetActionMulEquiv_inv_app_apply {G : Type u} [Group G] (g : G) (A : Action (Type u) G) (x : CategoryTheory.ToType A) : (CategoryTheory.ConcreteCategory.hom (((autForgetActionMulEquiv G) g).inv.app A)) x = g⁻¹ • x

The inverse of the automorphism associated to g acts by g⁻¹; not a simp lemma, for the reason given at TauCeti.toEndForgetAction_app_apply.

@[simp]

theorem TauCeti.autForgetActionMulEquiv_symm_apply_eq {G : Type u} [Group G] (η : CategoryTheory.Aut (Action.forget (Type u) G)) (g : G) : (autForgetActionMulEquiv G).symm η = g ↔ (CategoryTheory.ConcreteCategory.hom (η.hom.app (Action.leftRegular G))) 1 = g

The inverse Tannaka equivalence is characterized by evaluating the forward natural transformation at the identity of the left regular G-set.

noncomputable def TauCeti.autCompForgetActionMulEquiv (G : Type u) [Group G] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (e : CategoryTheory.Functor C (Action (Type u) G)) [e.IsEquivalence] : G ≃* CategoryTheory.Aut (e.comp (Action.forget (Type u) G))

Tannaka duality transported along an equivalence: if a functor e from a category C to G-sets is an equivalence, then the group G is the automorphism group of the composite C ⥤ Type u.

Equations

• TauCeti.autCompForgetActionMulEquiv G e = toUnits.trans (TauCeti.unitsAutCompForgetActionMulEquiv G e)

theorem TauCeti.autCompForgetActionMulEquiv_apply {G : Type u} [Group G] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (e : CategoryTheory.Functor C (Action (Type u) G)) [e.IsEquivalence] (g : G) : (autCompForgetActionMulEquiv G e) g = (unitsAutCompForgetActionMulEquiv G e) (toUnits g)

The transported group form of Tannaka duality is the transported monoid form at the unit attached to g.

theorem TauCeti.autCompForgetActionMulEquiv_hom_app_apply {G : Type u} [Group G] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (e : CategoryTheory.Functor C (Action (Type u) G)) [e.IsEquivalence] (g : G) (p : C) (x : CategoryTheory.ToType (e.obj p)) : (CategoryTheory.ConcreteCategory.hom (((autCompForgetActionMulEquiv G e) g).hom.app p)) x = g • x

The value of a transported natural automorphism on a point of a fibre; not a simp lemma, for the reason given at TauCeti.endCompForgetActionMulEquiv_app_apply.

theorem TauCeti.autCompForgetActionMulEquiv_inv_app_apply {G : Type u} [Group G] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (e : CategoryTheory.Functor C (Action (Type u) G)) [e.IsEquivalence] (g : G) (p : C) (x : CategoryTheory.ToType (e.obj p)) : (CategoryTheory.ConcreteCategory.hom (((autCompForgetActionMulEquiv G e) g).inv.app p)) x = g⁻¹ • x

The inverse of a transported natural automorphism acts by g⁻¹ on every fibre; not a simp lemma, for the reason given at TauCeti.endCompForgetActionMulEquiv_app_apply.