English
If X is a connected G-set, then the action is pretransitive: for any x in X, the G-orbit of x is a transitive subobject generating X.
Русский
Если X связано, то действие G является пред-транситивным: орбита любого x порождает X как подобъект.
LaTeX
$$$\\text{X connected }\\Rightarrow \\text{MulAction.IsPretransitive } G\\ X.V$$$
Lean4
/-- The `G`-action on a connected finite `G`-set is transitive. -/
theorem pretransitive_of_isConnected (X : Action FintypeCat G) [IsConnected X] : MulAction.IsPretransitive G X.V where
exists_smul_eq x
y := by
/- We show that the `G`-orbit of `x` is a non-initial subobject of `X` and hence by
connectedness, the orbit equals `X.V`. -/
let T : Set X.V := MulAction.orbit G x
have : Fintype T := Fintype.ofFinite T
letI : MulAction G (FintypeCat.of T) := inferInstanceAs <| MulAction G ↑(MulAction.orbit G x)
let T' : Action FintypeCat G := Action.FintypeCat.ofMulAction G (FintypeCat.of T)
let i : T' ⟶ X := ⟨Subtype.val, fun _ ↦ rfl⟩
have : Mono i := ConcreteCategory.mono_of_injective _ (Subtype.val_injective)
have : IsIso i := by
apply IsConnected.noTrivialComponent T' i
apply (not_initial_iff_fiber_nonempty (Action.forget _ _) T').mpr
exact Set.Nonempty.coe_sort (MulAction.nonempty_orbit x)
have hb : Function.Bijective i.hom :=
by
apply (ConcreteCategory.isIso_iff_bijective i.hom).mp
exact map_isIso (forget₂ _ FintypeCat) i
obtain ⟨⟨y', ⟨g, (hg : g • x = y')⟩⟩, (hy' : y' = y)⟩ := hb.surjective y
use g
exact hg.trans hy'
