subgroup of abelian group is normal

Stream: new members

[Thomas Laraia]

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]

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

[Kevin Buzzard]

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]

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]

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]

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]

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