Multiplying Elements in a Normal Subgroup

Stream: general

[Roshan Kohli]

I am trying to use the normality of P to show that k*g^(-1)*k^(-1) is in P so the full product is an element of P. I am unsure of what lemmas to apply here. Would it be a good idea to have a subgoal to show the conjugate of g^(-1) is an element of P first?

variable (G : Type*) [Group G] [Fintype G] (P Q : Subgroup G)

theorem mul (g : P) (k : Q) (hP : (P : Subgroup G).Normal)
(hQ : (Q : Subgroup G).Normal) : (g*k*g⁻¹*k⁻¹ : G) ∈ P := by
  sorry

[Adam Topaz]

How is docs#Subgroup.Normal defined?

[Emilie (Shad Amethyst)]

It's specifically that for any h ∈ H, where H is a normal subgroup, ∀ g : G, MulAut.conj g • h ∈ H

[Adam Topaz]

Right so I would use associativity to write it as g times the rest, use P.mul_mum then Normal.conj_mem

[Roshan Kohli]

I'll give this a go, thank you

[Emilie (Shad Amethyst)]

I believe you can also go the other route of showing that since k ∈ Q, g * k * g⁻¹ ∈ Q and k⁻¹ ∈ Q

[Emilie (Shad Amethyst)]

Which indicates that you can drop one of hP or hQ :)

[Richard Copley]

Also, things will be smoother if you take hypotheses of the form "$x$ is a member of H" instead of "$x$ is of type ↥H":

theorem mul (g k : G) (hg : g ∈ P) (hk : k ∈ Q) (hP : P.Normal) (hQ : Q.Normal) :
    (g * k * g⁻¹ * k⁻¹ : G) ∈ P := by
  sorry

[Roshan Kohli]

Emilie (Shad Amethyst) said:

I believe you can also go the other route of showing that since k ∈ Q, g * k * g⁻¹ ∈ Q and k⁻¹ ∈ Q

Yes I will need that too for the larger proof I am in the process of completing thank you

[Roshan Kohli]

Thanks I have managed to prove this now.

[Notification Bot]

Roshan Kohli has marked this topic as resolved.

[Notification Bot]

Roshan Kohli has marked this topic as unresolved.

[Roshan Kohli]

As per my previous post I was attempting to adapt the proof I had to use in my larger proof. However since in the previous post I assumed g was in P it made it a lot easier. I do not necessarily have the same hypothesis here. I have broken down my code to include only the important points necessary to show the product is in P. Can someone help me with converting the type of g to be what it needs to be. Thanks

import Mathlib

variable (p : ℕ) [Fact p.Prime] (q : ℕ) [Fact q.Prime] (G : Type*) [Group G] [Fintype G]

theorem bigtheorem (P : Sylow p G) (Q : Sylow q G) : IsCyclic G := by

-- obtain the generator of P and say P is normal
  have p3 : IsCyclic P := by sorry
  obtain ⟨g, gP⟩ := IsCyclic.exists_generator (α := P)
  have p8 : (P : Subgroup G).Normal := by sorry

-- obtain the generator of Q and say Q is normal
  have q3 : IsCyclic Q := by sorry
  obtain ⟨k, kQ⟩ := IsCyclic.exists_generator (α := Q)
  have q8 : (Q : Subgroup G).Normal := by sorry

-- what I am having trouble proving given my previous post
  have in_P : (g*k*g⁻¹*k⁻¹ : G) ∈ P := by sorry

  sorry

[Adam Topaz]

  have in_P : (g*k*g⁻¹*k⁻¹ : G) ∈ P := by
    simp_rw [mul_assoc (g : G)]
    apply P.mul_mem g.prop
    apply p8.conj_mem
    apply P.inv_mem g.prop

[Adam Topaz]

you could easily golf the last three lines if you want.

[Roshan Kohli]

I still get this error in my actual full proof
image.png

[Roshan Kohli]

I don't know how to switch to ↑P

[Adam Topaz]

it looks like you have two Ps`

[Adam Topaz]

the tombstone tells you that a new P was introduced, while g : P was a term of the original P.

[Roshan Kohli]

ah i see, I'll see what I can do to resolve this issue