English
IsPreprimitive is invariant under conjugation of the fixing-subgroup by the stabilizer.
Русский
Предпримитивность сохранится при сопряжении фиксационной подгруппы стабилизаторoм.
LaTeX
$$IsPreprimitive (fixingSubgroup G s) (ofFixingSubgroup G s) ≃ IsPreprimitive (fixingSubgroup G (g • s)) (ofFixingSubgroup G (g • s))$$
Lean4
/-- An action is preprimitive iff it is `1`-preprimitive -/
@[to_additive]
theorem is_one_preprimitive_iff : IsMultiplyPreprimitive M α 1 ↔ IsPreprimitive M α :=
by
constructor
· intro H1
rw [← isPreprimitive_of_fixingSubgroup_empty_iff]
apply H1.isPreprimitive_ofFixingSubgroup (by simp)
· intro h
rw [isMultiplyPreprimitive_iff]
constructor
· exact is_one_pretransitive_iff.mpr h.toIsPretransitive
· intro s hs
suffices s = ∅ by rwa [this, isPreprimitive_of_fixingSubgroup_empty_iff]
rw [← Set.encard_eq_zero]
suffices s.encard ≠ (⊤ : ℕ∞) by
obtain ⟨m, hm⟩ := ENat.ne_top_iff_exists.mp this
rw [← hm, ← Nat.cast_one, ← ENat.coe_add, Nat.cast_inj, Nat.add_eq_right] at hs
simp [← hm, hs]
exact fun h ↦ by simp [h] at hs
