English
The G-action on a connected finite G-set is transitive in the sense of pretransitivity: the orbit of any point is the entire set.
Русский
Действие G на связном конечном G-множество транзитивно в смысле пред-транситивности: орбита любого элемента равна всему множеству.
LaTeX
$$$\\text{If } X \\text{ is connected, then } \\text{MulAction.IsPretransitive } G X.V$$$
Lean4
/-- Given `f : X ⟶ Y` for `X Y : Action FintypeCat G`, the complement of the image
of `f` has a natural `G`-action. -/
noncomputable def imageComplement {X Y : Action FintypeCat G} (f : X ⟶ Y) : Action FintypeCat G
where
V := FintypeCat.imageComplement f.hom
ρ :=
{ toFun := fun g y ↦
Subtype.mk (Y.ρ g y.val) <| by
intro ⟨x, h⟩
apply y.property
use X.ρ g⁻¹ x
calc
(X.ρ g⁻¹ ≫ f.hom) x = (Y.ρ g⁻¹ * Y.ρ g) y.val := by rw [f.comm, FintypeCat.comp_apply, h]; rfl
_ = y.val := by rw [← map_mul, inv_mul_cancel, Action.ρ_one, FintypeCat.id_apply]
map_one' := by simp only [map_one, End.one_def, FintypeCat.id_apply, Subtype.coe_eta]; rfl
map_mul' := by
intro g h
congr! 1 with ⟨x, hx⟩
apply Subtype.ext
simp only [map_mul, End.mul_def, FintypeCat.comp_apply]
rfl }
