theorem MulAction.IsTransitive.of_mulEquiv {H : Type u_1} [Group H] {K : Type u_2} [Group K] {X : Type u_3} [MulAction H X] {Y : Type u_4} [MulAction K Y] (eH : H ≃* K) (eX : X ≃ Y) (hcompat : ∀ (g : H) (x : X), eX (g • x) = eH g • eX x) (h : IsTransitive H X) : IsTransitive K Y

Transport transitivity across a compatible equivalence of acting groups and underlying sets.

theorem MulAction.isTransitive_iff_of_mulEquiv {H : Type u_1} [Group H] {K : Type u_2} [Group K] {X : Type u_3} [MulAction H X] {Y : Type u_4} [MulAction K Y] (eH : H ≃* K) (eX : X ≃ Y) (hcompat : ∀ (g : H) (x : X), eX (g • x) = eH g • eX x) : IsTransitive H X ↔ IsTransitive K Y

Transitivity is invariant under a compatible equivalence of acting groups and underlying sets.

theorem CategoryTheory.Functor.isTransitive_iff_comp_of_isEquivalence {C : Type u_1} [Groupoid C] {D : Type u_2} [Groupoid D] (F : Functor C D) [F.IsEquivalence] (T : Functor D (Type v)) : T.IsTransitive ↔ (F.comp T).IsTransitive

Restriction along an equivalence of groupoids preserves and reflects transitivity of set-valued functors.

theorem restrictionAlongSkeleton_isEquivalence {G : Type u₁} [CategoryTheory.Groupoid G] {B : Type u₂} [CategoryTheory.Groupoid B] {ι : CategoryTheory.Functor G B} (hι : CategoryTheory.IsSkeletonOf B G ι) : ((CategoryTheory.Functor.whiskeringLeft G B (Type v)).obj ι).IsEquivalence

Remark 3.6.6: restriction along a skeleton inclusion ι : G ⥤ B identifies B-sets with G-sets by making precomposition with ι an equivalence of functor categories.

theorem isTransitive_iff_comp_of_isSkeletonOf {G : Type u₁} [CategoryTheory.Groupoid G] {B : Type u₂} [CategoryTheory.Groupoid B] {ι : CategoryTheory.Functor G B} (hι : CategoryTheory.IsSkeletonOf B G ι) (T : CategoryTheory.Functor B (Type v)) : T.IsTransitive ↔ (ι.comp T).IsTransitive

Restriction along a skeleton inclusion preserves and reflects transitivity of groupoid actions on sets.