English
If hs is a pretransitive structure, then the refined intersection setup is preprimitive.
Русский
Если hs образует пре-транситивную структуру, то пересечение дополнительно примитивно.
LaTeX
$$$\text{isPreprimitive}\big(\mathrm{fixingSubgroup}(M,s\cap g\cdot s),\mathrm{ofFixingSubgroup}(M,s\cap g\cdot s)\big)$$$
Lean4
/-- A primitivity criterion -/
theorem isPreprimitive_ofFixingSubgroup_inter [Finite α]
(hs : IsPreprimitive (fixingSubgroup M s) (ofFixingSubgroup M s)) {g : M} (ha : s ∪ g • s ≠ ⊤) :
IsPreprimitive (fixingSubgroup M (s ∩ g • s)) (ofFixingSubgroup M (s ∩ g • s)) :=
by
have := IsPretransitive.isPretransitive_ofFixingSubgroup_inter hs.toIsPretransitive ha
apply IsPreprimitive.of_card_lt (f := ofFixingSubgroup_of_inclusion M Set.inter_subset_left)
rw [show Nat.card (ofFixingSubgroup M (s ∩ g • s)) = (s ∩ g • s)ᶜ.ncard from Nat.card_coe_set_eq _,
Set.ncard_range_of_injective ofFixingSubgroup_of_inclusion_injective,
show Nat.card (ofFixingSubgroup M s) = sᶜ.ncard from Nat.card_coe_set_eq _, Set.compl_inter]
refine (Set.ncard_union_lt sᶜ.toFinite (g • s)ᶜ.toFinite ?_).trans_le ?_
· rwa [Set.disjoint_compl_right_iff_subset, Set.compl_subset_iff_union]
· rw [← Set.smul_set_compl, Set.ncard_smul_set, two_mul]
