isPretransitive_of_surjective — Mathlib

English

If toAut F G is surjective, then G acts pretransitively on fibers over every connected object X.

Русский

Если toAut F G сюръективен, тогда G действует прeтранситивно на волокнах над любым связанным объектом X.

LaTeX

$$$\text{Surjective}(toAut\,F\,G)\Rightarrow\forall X\,[IsConnected(X)]:\ MulAction.IsPretransitive G (F(X))$$$

Lean4

/-- If `toAut F G` is surjective, then `G` acts transitively on the fibers of connected objects.
For a converse see `toAut_surjective`. -/
theorem isPretransitive_of_surjective (h : Function.Surjective (toAut F G)) (X : C) [IsConnected X] :
    MulAction.IsPretransitive G (F.obj X) where
  exists_smul_eq x
    y := by
    obtain ⟨t, ht⟩ := MulAction.exists_smul_eq (Aut F) x y
    obtain ⟨g, rfl⟩ := h t
    exact ⟨g, ht⟩

Похожие утверждения