Zulip Chat Archive

Stream: new members

Topic: subgroup of abelian group is normal


Thomas Laraia (Jul 21 2021 at 16:16):

I am seeing if I can expand on groups and subgroups in formalising-mathematics and want to show that a subgroup of an abelian group is normal.
I am now in the sorry in the last bit, where I need to show ↑h ∈ H₁, I have redefined in some places a few times to try and find something I know I can finish up but haven't quite hit the mark.

import tactic

namespace paulo

class group (G : Type) extends has_mul G, has_one G, has_inv G :=
(mul_assoc :  (a b c : G), a * b * c = a * (b * c))
(one_mul :  (a : G), 1 * a = a)
(mul_left_inv :  (a : G), a⁻¹ * a = 1)

variables {G: Type} [group G]

namespace group

def is_abelian (G : Type) [group G] :=  (a b : G), a * b = b * a

structure subgroup (G : Type) [group G] :=
(carrier : set G)
(one_mem' : (1 : G)  carrier)
(mul_mem' {x y} : x  carrier  y  carrier  x * y  carrier)
(inv_mem' {x} : x  carrier  x⁻¹  carrier)

variables (H : subgroup G)

instance : has_mem G (subgroup G) := λ m H, m  H.carrier

instance : has_coe (subgroup G) (set G) := λ H, H.carrier

@[simp] lemma mem_carrier {g : G} : g  H.carrier  g  H :=
begin
  -- true by definition
  refl
end

theorem one_mem : (1 : G)  H :=
begin
  apply H.one_mem',
end

/-- A subgroup is closed under multiplication. -/
theorem mul_mem {x y : G} : x  H  y  H  x * y  H :=
begin
  -- what do you think?
  apply H.mul_mem',
end

/-- A subgroup is closed under inverse -/
theorem inv_mem {x : G} : x  H  x⁻¹  H :=
begin
  -- what do you think?
  apply H.inv_mem',
end

@[simp] lemma mem_coe {g : G} : g  (H : set G)  g  H :=
begin
  -- true by definition
  refl
end

namespace subgroup

def is_normal_subgroup :=  (g : G),  (h : H), g*h*g⁻¹  H

lemma abelian_subgroups_normal {G₁ : Type} [group G₁] (hyp : is_abelian G₁) (H₁ : subgroup G₁) : is_normal_subgroup H₁ :=
begin
  intros g h,
  unfold is_abelian at hyp,
  rw hyp,
  rw  mul_assoc,
  rw mul_left_inv,
  rw one_mul,
  sorry,
end

end subgroup

end group

end paulo

Patrick Massot (Jul 21 2021 at 16:20):

What about changing your last definition to def is_normal_subgroup := ∀ (g : G), ∀ h, h ∈ H → g*h*g⁻¹ ∈ H?

Kevin Buzzard (Jul 21 2021 at 16:20):

Right, Patrick has hit the nail on the head. You can finish your proof with

  cases h with actual_h h_proof,
  exact h_proof,

Patrick Massot (Jul 21 2021 at 16:21):

lemma abelian_subgroups_normal {G₁ : Type} [group G₁] (hyp : is_abelian G₁) (H₁ : subgroup G₁) : is_normal_subgroup H₁ :=
begin
  intros g h h_in,
  rwa [hyp,  mul_assoc, mul_left_inv, one_mul]
end

(using my definition)

Kevin Buzzard (Jul 21 2021 at 16:23):

Although G is a type (it has type Type), H is not a type; it's a term. It has type subgroup G. So h : H should not even make sense! The only reason it does make sense is that there is a coercion from subgroup G to Type sending the term H to the type ↥H (this is what you see in your goal). If then you have a term h : ↥H then h is actually a pair, consisting of a term actual_h : G (otherwise known as ↑h : G) and a proof h_proof that actual_h \in H. You need to take your h apart to get to the actual group elements. Patrick's approach avoids this problem.

It is a shock to mathematicians that subgroups are not "the same as" groups, but they are at different levels of the type hierarachy (universes, types, terms).

Thomas Laraia (Jul 21 2021 at 16:41):

Patrick Massot said:

What about changing your last definition to def is_normal_subgroup := ∀ (g : G), ∀ h, h ∈ H → g*h*g⁻¹ ∈ H?

Right, I think I had another questioned answered recently where I made the same error. I will try with the new definition.

Kevin Buzzard said:

Right, Patrick has hit the nail on the head. You can finish your proof with

  cases h with actual_h h_proof,
  exact h_proof,

I see! I'm struggling to recognize actual_h ∈ has_coe_t_aux.coe H₁ and ⟨actual_h, h_proof⟩ ∈ H₁ as the same thing. I think your second explanation is giving me more of an understanding of coercion though, so positives all around.

Kevin Buzzard (Jul 21 2021 at 16:57):

exact h_proof solves that goal, so all that noise about coe must just definitionally vanish.


Last updated: Dec 20 2023 at 11:08 UTC