English
A pretransitive structure on Fin n ↪ α corresponds to pretransitive action on G.
Русский
Предтранситивная структура на Fin n ↪ α эквивалентна предтранситивному действию на G.
LaTeX
$$IsMultiplyPretransitive G α n ↔ IsPretransitive G (Fin n ↪ α)$$
Lean4
/-- A pretransitive action is `n.succ-`preprimitive iff
the action of stabilizers is `n`-preprimitive. -/
@[to_additive]
theorem isMultiplyPreprimitive_succ_iff_ofStabilizer [IsPretransitive M α] {n : ℕ} (hn : 1 ≤ n) {a : α} :
IsMultiplyPreprimitive M α n.succ ↔ IsMultiplyPreprimitive (stabilizer M a) (SubMulAction.ofStabilizer M a) n :=
by
constructor
· apply isMultiplyPreprimitive_ofStabilizer
· intro H
rw [isMultiplyPreprimitive_iff]
constructor
· exact ofStabilizer.isMultiplyPretransitive.mpr H.isMultiplyPretransitive
· intro s hs
have : ∃ b : α, b ∈ s := by
rw [← Set.nonempty_def, Set.nonempty_iff_ne_empty]
intro h
apply not_lt.mpr hn
rw [h, Set.encard_empty, zero_add, ← Nat.cast_one, Nat.cast_inj, Nat.succ_inj] at hs
simp only [← hs, zero_lt_one]
obtain ⟨b, hb⟩ := this
obtain ⟨g, hg : g • b = a⟩ := exists_smul_eq M b a
rw [isPreprimitive_ofFixingSubgroup_conj_iff (g := g)]
set s' := g • s with hs'
let t : Set (SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s'
have hst : s' = insert a (Subtype.val '' t) := by
ext x
constructor
· intro hxs
by_cases hxa : x = a
· simp [hxa]
· exact Set.mem_insert_of_mem _ ⟨⟨x, hxa⟩, by simp only [t, Set.mem_preimage]; exact hxs, rfl⟩
· rw [Set.mem_insert_iff]
rintro (⟨rfl⟩ | ⟨y, hy, rfl⟩)
· simpa [s', ← hg]
· simpa only using hy
rw [hst, isPreprimitive_fixingSubgroup_insert_iff]
apply IsMultiplyPreprimitive.isPreprimitive_ofFixingSubgroup _ n
apply ENat.add_left_injective_of_ne_top ENat.one_ne_top
simp only
rw [← Nat.cast_one, ← Nat.cast_add, ← hs]
apply congr_arg₂ _ _ rfl
rw [show s = g⁻¹ • s' from by simp [hs'], ← Set.image_smul, (MulAction.injective g⁻¹).encard_image, hst]
rw [Set.encard_insert_of_notMem, Subtype.coe_injective.encard_image, ENat.coe_one]
exact notMem_val_image M t
