English
If Hk is IsMultiplyPretransitive G α k and s ⊆ α with s.ncard = k, then (fixingSubgroup G s).index · (|α| − k)! = |α|!.
Русский
Если Hk = IsMultiplyPretransitive G α k и s ⊆ α с |s| = k, то индекс фиксирующей подгруппы умноженный на (|α| − k)! равен |α|!.
LaTeX
$$$IsMultiplyPretransitive\ G\ α\ k \rightarrow (fixingSubgroup\ G\ s).index \cdot (|α| - k)!.factorial = |α|!.factorial$$$
Lean4
/-- For a multiply pretransitive action, computes the index
of the fixing_subgroup of a subset of adequate cardinality -/
theorem index_of_fixingSubgroup_mul [Finite α] {k : ℕ} (Hk : IsMultiplyPretransitive G α k) {s : Set α}
(hs : s.ncard = k) : (fixingSubgroup G s).index * (Nat.card α - k).factorial = (Nat.card α).factorial := by
induction k generalizing G α with
| zero =>
rw [Set.ncard_eq_zero] at hs
simp [hs]
| succ k
hrec =>
have hGX : IsPretransitive G α := by
rw [← is_one_pretransitive_iff]
apply isMultiplyPretransitive_of_le (n := k + 1)
· rw [Nat.succ_le_succ_iff]; apply Nat.zero_le
· rw [← hs, ← Set.ncard_univ]
exact ncard_le_ncard s.subset_univ finite_univ
have : s.Nonempty := by
rw [← Set.ncard_pos, hs]
exact succ_pos k
obtain ⟨a, has⟩ := this
let t : Set (SubMulAction.ofStabilizer G a) := Subtype.val ⁻¹' s
have hat : Subtype.val '' t = s \ { a } :=
by
rw [Set.image_preimage_eq_inter_range]
simp only [Subtype.range_coe_subtype]
rw [Set.diff_eq_compl_inter, Set.inter_comm]
congr
have hat' : s = insert a (Subtype.val '' t) := by rw [hat, Set.insert_diff_singleton, Set.insert_eq_of_mem has]
have hfs := SubMulAction.fixingSubgroup_of_insert a t
rw [← hat'] at hfs
rw [hfs, Subgroup.index_map,
(MonoidHom.ker_eq_bot_iff (stabilizer G a).subtype).mpr
(by simp only [Subgroup.coe_subtype, Subtype.coe_injective])]
simp only [sup_bot_eq, Subgroup.range_subtype]
have htcard : t.ncard = k :=
by
rw [← Nat.succ_inj, Nat.succ_eq_add_one, Nat.succ_eq_add_one, ← hs, hat', eq_comm]
suffices ¬a ∈ (Subtype.val '' t) by
convert Set.ncard_insert_of_notMem this ?_
rw [Set.ncard_image_of_injective _ Subtype.coe_injective]
apply Set.toFinite
intro h
obtain ⟨⟨b, hb⟩, _, hb'⟩ := h
apply hb
simp only [← hb', Set.mem_singleton_iff]
suffices (fixingSubgroup (stabilizer G a) t).index * (Nat.card α - 1 - k).factorial = (Nat.card α - 1).factorial
by
rw [add_comm k, Nat.mul_right_comm, ← Nat.sub_sub, this, mul_comm, index_stabilizer_of_transitive G a]
exact Nat.mul_factorial_pred (card_ne_zero.mpr ⟨⟨a⟩, inferInstance⟩)
convert hrec (ofStabilizer.isMultiplyPretransitive.mp Hk) htcard
all_goals { rw [nat_card_ofStabilizer_eq G a]
}
