English
A nonempty finite G-set with a transitive action is connected.
Русский
Непустое конечное G-множество с резольвентно-транситивным действием является связным.
LaTeX
$$$\\text{If } X \\neq \\varnothing \\text{ and } \\text{MulAction.G-invariant action is transitive, then } IsConnected X$$$
Lean4
/-- A nonempty `G`-set with transitive `G`-action is connected. -/
theorem isConnected_of_transitive (X : FintypeCat) [MulAction G X] [MulAction.IsPretransitive G X] [h : Nonempty X] :
IsConnected (Action.FintypeCat.ofMulAction G X)
where
notInitial := not_initial_of_inhabited (Action.forget _ _) h.some
noTrivialComponent Y i hm
hni := by
/- We show that the induced inclusion `i.hom` of finite sets is surjective, using the
transitivity of the `G`-action. -/
obtain ⟨(y : Y.V)⟩ := (not_initial_iff_fiber_nonempty (Action.forget _ _) Y).mp hni
have : IsIso i.hom :=
by
refine (ConcreteCategory.isIso_iff_bijective i.hom).mpr ⟨?_, fun x' ↦ ?_⟩
· haveI : Mono i.hom := map_mono (forget₂ _ _) i
exact ConcreteCategory.injective_of_mono_of_preservesPullback i.hom
· letI x : X := i.hom y
obtain ⟨σ, hσ⟩ := MulAction.exists_smul_eq G x x'
use σ • y
change (Y.ρ σ ≫ i.hom) y = x'
rw [i.comm, FintypeCat.comp_apply]
exact hσ
apply isIso_of_reflects_iso i (Action.forget _ _)
