Connected G-sets are the transitive ones

An object of a category is connected in the sense of CategoryTheory.PreGaloisCategory.IsConnected when it is not initial and admits no nontrivial subobject. This file identifies that condition for G-sets: an object of Action (Type u) G is connected exactly when it is nonempty and G acts transitively on it, which is TauCeti.isTransitiveAction.

Mathlib proves the same statement for finite G-sets in CategoryTheory.Action.isConnected_iff_transitive, but that proof runs through the fibre functor of the Galois category Action FintypeCat G, machinery unavailable here: Action (Type u) G has objects with infinite underlying type and is not a Galois category. The argument is instead run directly, over the two facts about the forgetful functor Action (Type u) G ⥤ Type u that replace it: it preserves and reflects monomorphisms, and a G-set is initial exactly when its underlying type is empty.

Both facts are Mathlib's, once the concrete-category forgetful functor of Action (Type u) G is known to preserve and reflect the empty colimit; that is what the two instances below record, and with them CategoryTheory.Concrete.initial_iff_empty_of_preserves_of_reflects applies verbatim to G-sets.

Main declarations

• TauCeti.mono_action_iff_injective: a map of G-sets is a monomorphism exactly when it is injective.
• TauCeti.isConnected_action_iff_isTransitiveAction: a G-set is connected exactly when it is transitive.

instance TauCeti.preservesColimit_empty_forget_action {G : Type v} [Monoid G] : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty (Action (Type u) G)) (CategoryTheory.forget (Action (Type u) G))

The concrete-category forgetful functor of Action (Type u) G preserves initial objects: it is the composite of Action.forget, which preserves all colimits of shape Discrete PEmpty, with the forgetful functor of Type u.

instance TauCeti.reflectsColimit_empty_forget_action {G : Type v} [Monoid G] : CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Functor.empty (Action (Type u) G)) (CategoryTheory.forget (Action (Type u) G))

The concrete-category forgetful functor of Action (Type u) G reflects initial objects.

@[simp]

theorem TauCeti.mono_action_iff_injective {G : Type v} [Monoid G] {A B : Action (Type u) G} (f : A ⟶ B) : CategoryTheory.Mono f ↔ Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f.hom)

A map of G-sets is a monomorphism exactly when the underlying map of types is injective. Both directions come from the forgetful functor to types, which preserves and reflects finite limits and hence monomorphisms.

@[simp]

theorem TauCeti.isConnected_action_iff_isTransitiveAction {G : Type v} [Monoid G] (A : Action (Type u) G) : CategoryTheory.PreGaloisCategory.IsConnected A ↔ isTransitiveAction G A

A G-set is connected exactly when it is transitive, that is, exactly when its underlying type is nonempty and G acts transitively on it.