English
Let M act on α with an Iwasawa structure. If the action is quasiprimitive and N ⊲ M acts nontrivially on α, then the commutator subgroup [M,M] is contained in N.
Русский
Пусть M действует на α с структурой Айвасава. Если действие квазиприводимо, и N ⊲ M действует не тривиально на α, то коммутатор [M,M] лежит в N.
LaTeX
$$$[M,M] \le N$$$
Lean4
/-- The Iwasawa criterion : If a quasiprimitive action of a group G on X
has an Iwasawa structure, then any normal subgroup that acts nontrivially
contains the group of commutators. -/
theorem commutator_le (IwaS : IwasawaStructure M α) [IsQuasiPreprimitive M α] (N : Subgroup M) [nN : N.Normal]
(hNX : MulAction.fixedPoints N α ≠ .univ) : commutator M ≤ N :=
by
have is_transN := IsQuasiPreprimitive.isPretransitive_of_normal hNX
have ntα : Nontrivial α := nontrivial_of_fixedPoints_ne_univ hNX
obtain a : α := Nontrivial.to_nonempty.some
apply
nN.commutator_le_of_self_sup_commutative_eq_top ?_
(IwaS.is_comm a)
-- We have to prove that N ⊔ IwaS.T x = ⊤
rw [eq_top_iff, ← IwaS.is_generator, iSup_le_iff]
intro x
obtain ⟨g, rfl⟩ := MulAction.exists_smul_eq N a x
rw [Subgroup.smul_def, IwaS.is_conj g a]
rintro _ ⟨k, hk, rfl⟩
have hg' : ↑g ∈ N ⊔ IwaS.T a := Subgroup.mem_sup_left (Subtype.mem g)
have hk' : k ∈ N ⊔ IwaS.T a := Subgroup.mem_sup_right hk
exact (N ⊔ IwaS.T a).mul_mem ((N ⊔ IwaS.T a).mul_mem hg' hk') ((N ⊔ IwaS.T a).inv_mem hg')
