English
If a is a base point with pretransitivity, then the action on s ∩ g·s is pretransitive.
Русский
Если a базовая точка с предпереходностью, то действие на s ∩ g·s также предпереходно.
LaTeX
$$$\text{isPretransitive}\big(\mathrm{fixingSubgroup}(M,s\cap g\cdot s),\mathrm{ofFixingSubgroup}(M,s\cap g\cdot s)\big)$$$
Lean4
/-- A pretransitivity criterion. -/
theorem isPretransitive_ofFixingSubgroup_inter (hs : IsPretransitive (fixingSubgroup M s) (ofFixingSubgroup M s))
{g : M} (ha : s ∪ g • s ≠ ⊤) : IsPretransitive (fixingSubgroup M (s ∩ g • s)) (ofFixingSubgroup M (s ∩ g • s)) :=
by
rw [Ne, Set.top_eq_univ, ← Set.compl_empty_iff, ← Ne, ← Set.nonempty_iff_ne_empty] at ha
obtain ⟨a, ha⟩ := ha
rw [Set.compl_union] at ha
have ha' : a ∈ (s ∩ g • s)ᶜ := by
rw [Set.compl_inter]
exact Set.mem_union_left _ ha.1
rw [MulAction.isPretransitive_iff_base (⟨a, ha'⟩ : ofFixingSubgroup M (s ∩ g • s))]
rintro ⟨x, hx⟩
rw [mem_ofFixingSubgroup_iff, Set.mem_inter_iff, not_and_or] at hx
rcases hx with hx | hx
· obtain ⟨⟨k, hk⟩, hkax⟩ := hs.exists_smul_eq ⟨a, ha.1⟩ ⟨x, hx⟩
use ⟨k, fun ⟨y, hy⟩ ↦ hk ⟨y, hy.1⟩⟩
rwa [Subtype.ext_iff] at hkax ⊢
· have hg'x : g⁻¹ • x ∈ ofFixingSubgroup M s := mt Set.mem_smul_set_iff_inv_smul_mem.mpr hx
have hg'a : g⁻¹ • a ∈ ofFixingSubgroup M s := mt Set.mem_smul_set_iff_inv_smul_mem.mpr ha.2
obtain ⟨⟨k, hk⟩, hkax⟩ := hs.exists_smul_eq ⟨g⁻¹ • a, hg'a⟩ ⟨g⁻¹ • x, hg'x⟩
use ⟨g * k * g⁻¹, ?_⟩
· simp only [← SetLike.coe_eq_coe] at hkax ⊢
rwa [SetLike.val_smul, Subgroup.mk_smul, eq_inv_smul_iff, smul_smul, smul_smul] at hkax
· rw [mem_fixingSubgroup_iff] at hk ⊢
intro y hy
rw [mul_smul, mul_smul, smul_eq_iff_eq_inv_smul g]
exact hk _ (Set.mem_smul_set_iff_inv_smul_mem.mp hy.2)
