Transitive G-sets

A G-set, in the categorical sense of an object of Action (Type u) G, is transitive when it is nonempty and G acts transitively on its underlying type. This file records that condition as an ObjectProperty, shows it is closed under isomorphisms, and names the resulting full subcategory.

The action referred to is the one Action.instMulAction puts on the underlying type ToType A, so both conjuncts are read through that instance rather than through A.ρ. Following Mathlib's convention, MulAction.IsPretransitive allows the empty set, so nonemptiness is a genuine extra condition and is imposed separately.

The property is named TauCeti.isTransitiveAction rather than being placed in a TauCeti.Action namespace: Action is a Mathlib type, and scripts/lint-dot-notation.py rejects a Mathlib type's namespace nested inside namespace TauCeti, because dot notation on that type then fails to elaborate.

Main declarations

• TauCeti.isTransitiveAction: the property of being a transitive G-set.
• TauCeti.isTransitiveAction_iff: its two conjuncts.
• TauCeti.smul_eq_ρ_apply: the scalar multiplication both conjuncts refer to is evaluation of the representation.
• TauCeti.TransitiveAction: transitive G-sets as a full subcategory of all G-sets, with TauCeti.TransitiveAction.mk, TauCeti.TransitiveAction.forget, TauCeti.TransitiveAction.isTransitiveAction and TauCeti.TransitiveAction.fullyFaithfulForget.

def TauCeti.isTransitiveAction (G : Type v) [Monoid G] : CategoryTheory.ObjectProperty (Action (Type u) G)

A G-set is transitive when G acts pretransitively on it and it is nonempty.

Equations

• TauCeti.isTransitiveAction G A = (MulAction.IsPretransitive G (CategoryTheory.ToType A) ∧ Nonempty (CategoryTheory.ToType A))

theorem TauCeti.smul_eq_ρ_apply {G : Type v} [Monoid G] (A : Action (Type u) G) (g : G) (x : CategoryTheory.ToType A) : g • x = (CategoryTheory.ConcreteCategory.hom (A.ρ g)) x

The scalar multiplication that Action.instMulAction puts on the underlying type of a G-set is evaluation of its representation.

instance TauCeti.instIsClosedUnderIsomorphismsActionTypeIsTransitiveAction (G : Type v) [Monoid G] : (isTransitiveAction G).IsClosedUnderIsomorphisms

Transitivity of a G-set is preserved by isomorphisms of G-sets: an isomorphism is an equivariant bijection on underlying types.

@[simp]

theorem TauCeti.isTransitiveAction_iff {G : Type v} [Monoid G] (A : Action (Type u) G) : isTransitiveAction G A ↔ MulAction.IsPretransitive G (CategoryTheory.ToType A) ∧ Nonempty (CategoryTheory.ToType A)

Membership in the transitivity property of G-sets.

@[reducible, inline]

abbrev TauCeti.TransitiveAction (G : Type v) [Monoid G] : Type (max v (u_1 + 1))

Transitive G-sets, as a full subcategory of all G-sets.

Equations

• TauCeti.TransitiveAction G = (TauCeti.isTransitiveAction G).FullSubcategory

@[reducible, inline]

abbrev TauCeti.TransitiveAction.forget (G : Type v) [Monoid G] : CategoryTheory.Functor (TransitiveAction G) (Action (Type u) G)

The fully faithful inclusion of transitive G-sets into all G-sets.

Equations

• TauCeti.TransitiveAction.forget G = (TauCeti.isTransitiveAction G).ι

def TauCeti.TransitiveAction.fullyFaithfulForget (G : Type v) [Monoid G] : (forget G).FullyFaithful

The inclusion of transitive G-sets into all G-sets is fully faithful.

Equations

• TauCeti.TransitiveAction.fullyFaithfulForget G = (TauCeti.isTransitiveAction G).fullyFaithfulι

def TauCeti.TransitiveAction.mk {G : Type v} [Monoid G] (A : Action (Type u) G) (hA : TauCeti.isTransitiveAction G A) : TransitiveAction G

Construct a transitive G-set from a G-set and a proof of transitivity.

Equations

• TauCeti.TransitiveAction.mk A hA = { obj := A, property := hA }

theorem TauCeti.TransitiveAction.isTransitiveAction {G : Type v} [Monoid G] (A : TransitiveAction G) : TauCeti.isTransitiveAction G A.obj

The underlying G-set of a transitive G-set is transitive.