Theorem: commutator_le_iwasawa (Jordan/Iwasawa.lean)

State before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_qprim : IsQuasipreprimitive M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
hNX : MulAction.fixedPoints (↥N) α ≠ ⊤
⊢ commutator M ≤ N
Tactic:
have is_transN := is_qprim.pretransitive_of_normal nN hNX
State after:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_qprim : IsQuasipreprimitive M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
hNX : MulAction.fixedPoints (↥N) α ≠ ⊤
is_transN : MulAction.IsPretransitive (↥N) α
⊢ commutator M ≤ N

State before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_qprim : IsQuasipreprimitive M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
hNX : MulAction.fixedPoints (↥N) α ≠ ⊤
is_transN : MulAction.IsPretransitive (↥N) α
⊢ commutator M ≤ N
Tactic:
have ntα : Nontrivial α := isnontrivial_of_nontrivial_action hNX
State after:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_qprim : IsQuasipreprimitive M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
hNX : MulAction.fixedPoints (↥N) α ≠ ⊤
is_transN : MulAction.IsPretransitive (↥N) α
ntα : Nontrivial α
⊢ commutator M ≤ N

State before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_qprim : IsQuasipreprimitive M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
hNX : MulAction.fixedPoints (↥N) α ≠ ⊤
is_transN : MulAction.IsPretransitive (↥N) α
ntα : Nontrivial α
⊢ commutator M ≤ N
Tactic:
obtain a : α := Nontrivial.to_nonempty.some
State after:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_qprim : IsQuasipreprimitive M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
hNX : MulAction.fixedPoints (↥N) α ≠ ⊤
is_transN : MulAction.IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
⊢ commutator M ≤ N

State before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_qprim : IsQuasipreprimitive M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
hNX : MulAction.fixedPoints (↥N) α ≠ ⊤
is_transN : MulAction.IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
⊢ commutator M ≤ N
Tactic:
refine' contains_commutators_of N nN (IwaS.T a) _ (IwaS.is_comm a)
State after:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_qprim : IsQuasipreprimitive M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
hNX : MulAction.fixedPoints (↥N) α ≠ ⊤
is_transN : MulAction.IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
⊢ N ⊔ IwaS.T a = ⊤

State before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_qprim : IsQuasipreprimitive M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
hNX : MulAction.fixedPoints (↥N) α ≠ ⊤
is_transN : MulAction.IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
⊢ N ⊔ IwaS.T a = ⊤
Tactic:
rw [eq_top_iff, ← IwaS.is_generator, iSup_le_iff]
State after:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_qprim : IsQuasipreprimitive M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
hNX : MulAction.fixedPoints (↥N) α ≠ ⊤
is_transN : MulAction.IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
⊢ ∀ (i : α), IwaS.T i ≤ N ⊔ IwaS.T a

State before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_qprim : IsQuasipreprimitive M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
hNX : MulAction.fixedPoints (↥N) α ≠ ⊤
is_transN : MulAction.IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
⊢ ∀ (i : α), IwaS.T i ≤ N ⊔ IwaS.T a
Tactic:
intro x
State after:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_qprim : IsQuasipreprimitive M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
hNX : MulAction.fixedPoints (↥N) α ≠ ⊤
is_transN : MulAction.IsPretransitive (↥N) α
ntα : Nontrivial α
a x : α
⊢ IwaS.T x ≤ N ⊔ IwaS.T a

State before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_qprim : IsQuasipreprimitive M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
hNX : MulAction.fixedPoints (↥N) α ≠ ⊤
is_transN : MulAction.IsPretransitive (↥N) α
ntα : Nontrivial α
a x : α
⊢ IwaS.T x ≤ N ⊔ IwaS.T a
Tactic:
obtain ⟨g, rfl⟩ := MulAction.exists_smul_eq N a x
State after:
case intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_qprim : IsQuasipreprimitive M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
hNX : MulAction.fixedPoints (↥N) α ≠ ⊤
is_transN : MulAction.IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
g : ↥N
⊢ IwaS.T (g • a) ≤ N ⊔ IwaS.T a

State before:
case intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_qprim : IsQuasipreprimitive M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
hNX : MulAction.fixedPoints (↥N) α ≠ ⊤
is_transN : MulAction.IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
g : ↥N
⊢ IwaS.T (g • a) ≤ N ⊔ IwaS.T a
Tactic:
rw [Subgroup.smul_def, IwaS.is_conj g a]
State after:
case intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_qprim : IsQuasipreprimitive M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
hNX : MulAction.fixedPoints (↥N) α ≠ ⊤
is_transN : MulAction.IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
g : ↥N
⊢ MulAut.conj ↑g • IwaS.T a ≤ N ⊔ IwaS.T a

State before:
case intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_qprim : IsQuasipreprimitive M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
hNX : MulAction.fixedPoints (↥N) α ≠ ⊤
is_transN : MulAction.IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
g : ↥N
⊢ MulAut.conj ↑g • IwaS.T a ≤ N ⊔ IwaS.T a
Tactic:
rintro _ ⟨k, hk, rfl⟩
State after:
case intro.intro.intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_qprim : IsQuasipreprimitive M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
hNX : MulAction.fixedPoints (↥N) α ≠ ⊤
is_transN : MulAction.IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
g : ↥N
k : M
hk : k ∈ ↑(IwaS.T a)
⊢ ((MulDistribMulAction.toMonoidEnd (MulAut M) M) (MulAut.conj ↑g)) k ∈ N ⊔ IwaS.T a

State before:
case intro.intro.intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_qprim : IsQuasipreprimitive M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
hNX : MulAction.fixedPoints (↥N) α ≠ ⊤
is_transN : MulAction.IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
g : ↥N
k : M
hk : k ∈ ↑(IwaS.T a)
⊢ ((MulDistribMulAction.toMonoidEnd (MulAut M) M) (MulAut.conj ↑g)) k ∈ N ⊔ IwaS.T a
Tactic:
have hg' : ↑g ∈ N ⊔ IwaS.T a := Subgroup.mem_sup_left (Subtype.mem g)
State after:
case intro.intro.intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_qprim : IsQuasipreprimitive M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
hNX : MulAction.fixedPoints (↥N) α ≠ ⊤
is_transN : MulAction.IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
g : ↥N
k : M
hk : k ∈ ↑(IwaS.T a)
hg' : ↑g ∈ N ⊔ IwaS.T a
⊢ ((MulDistribMulAction.toMonoidEnd (MulAut M) M) (MulAut.conj ↑g)) k ∈ N ⊔ IwaS.T a

State before:
case intro.intro.intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_qprim : IsQuasipreprimitive M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
hNX : MulAction.fixedPoints (↥N) α ≠ ⊤
is_transN : MulAction.IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
g : ↥N
k : M
hk : k ∈ ↑(IwaS.T a)
hg' : ↑g ∈ N ⊔ IwaS.T a
⊢ ((MulDistribMulAction.toMonoidEnd (MulAut M) M) (MulAut.conj ↑g)) k ∈ N ⊔ IwaS.T a
Tactic:
have hk' : k ∈ N ⊔ IwaS.T a := Subgroup.mem_sup_right hk
State after:
case intro.intro.intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_qprim : IsQuasipreprimitive M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
hNX : MulAction.fixedPoints (↥N) α ≠ ⊤
is_transN : MulAction.IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
g : ↥N
k : M
hk : k ∈ ↑(IwaS.T a)
hg' : ↑g ∈ N ⊔ IwaS.T a
hk' : k ∈ N ⊔ IwaS.T a
⊢ ((MulDistribMulAction.toMonoidEnd (MulAut M) M) (MulAut.conj ↑g)) k ∈ N ⊔ IwaS.T a

State before:
case intro.intro.intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_qprim : IsQuasipreprimitive M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
hNX : MulAction.fixedPoints (↥N) α ≠ ⊤
is_transN : MulAction.IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
g : ↥N
k : M
hk : k ∈ ↑(IwaS.T a)
hg' : ↑g ∈ N ⊔ IwaS.T a
hk' : k ∈ N ⊔ IwaS.T a
⊢ ((MulDistribMulAction.toMonoidEnd (MulAut M) M) (MulAut.conj ↑g)) k ∈ N ⊔ IwaS.T a
Tactic:
exact (N ⊔ IwaS.T a).mul_mem ((N ⊔ IwaS.T a).mul_mem hg' hk') ((N ⊔ IwaS.T a).inv_mem hg')
State after:
no goals