isMultiplyPreprimitive_ofStabilizer

English

If a primitive subgroup contains a swap, then it is the full permutation group.

Русский

Если примитивная подгруппа содержит своп, то она является полной группой перестановок.

LaTeX

$$G = ⊤$$

Lean4

/-- The action of `stabilizer M a` is one-less preprimitive -/
@[to_additive /-- The action of `stabilizer M a` is one-less preprimitive. -/
    ]
theorem isMultiplyPreprimitive_ofStabilizer [IsPretransitive M α] {n : ℕ} {a : α} [IsMultiplyPreprimitive M α n.succ] :
    IsMultiplyPreprimitive (stabilizer M a) (SubMulAction.ofStabilizer M a) n :=
  by
  rcases Nat.lt_or_ge n 1 with h0 | h1
  · rw [Nat.lt_one_iff] at h0
    rw [h0]
    apply is_zero_preprimitive
  rw [isMultiplyPreprimitive_iff]
  constructor
  · rw [← ofStabilizer.isMultiplyPretransitive]
    exact IsMultiplyPreprimitive.isMultiplyPretransitive M α n.succ
  · intro s hs
    have :
      IsPreprimitive ↥(fixingSubgroup M (insert a (Subtype.val '' s)))
        ↥(ofFixingSubgroup M (insert a (Subtype.val '' s))) :=
      by
      apply IsMultiplyPreprimitive.isPreprimitive_ofFixingSubgroup M n.succ
      rw [Set.encard_insert_of_notMem, Subtype.coe_injective.encard_image, hs, Nat.cast_succ]
      aesop
    exact IsPreprimitive.of_surjective ofFixingSubgroup_insert_map_bijective.surjective

Похожие утверждения