The kernel of a homomorphism ϕ : G → H is a subgroup of G

Stream: new members

[Isak Colboubrani]

Apologies if this is a silly question (I'm a beginner!), but here goes:

I’ve seen the statement "the kernel of a homomorphism ϕ : G → H is a subgroup of G" formalized as:

example (φ : G →* H) : Subgroup G := by
  exact φ.ker

Now, if we treat the proof as a black box:

example (φ : G →* H) : Subgroup G := by
  sorry

It doesn’t seem to say anything specifically about the kernel, does it?

More precisely, my reading of "(φ : G →* H) : Subgroup G" is: "given a homomorphism φ : G → H, I can construct a subgroup of G".

So, what am I missing here?

Is there a way to formalize the statement "the kernel of a homomorphism ϕ : G → H is a subgroup of G" such that we don’t have to look inside the proof itself to confirm it’s really saying that it is specifically the kernel that is a subgroup of G?

[Abraham Solomon]

Maybe something like

example (φ : G →* H) : (φ.ker:Subgroup G) := by
  sorry

[Etienne Marion]

This does not work. Typing are not Lean statements. What you want to do here is this:

import Mathlib

example {G H : Type*} [Group G] [Group H] (φ : G →* H) :
    IsSubgroup (φ.ker : Set G) := sorry

[Isak Colboubrani]

I guess I’m trying to figure out whether there’s a deeper reason experts formalize the statement as example (φ : G →* H) : Subgroup G := φ.ker (such as in this example Formalizing Mathematics 2024), or if it’s simply a brief example where it’s assumed that whoever reads it will look at both the statement and the proof together to piece together the overall statement.

[Etienne Marion]

This is not really a formalization of the fact you're talking about, it's just an example that this works. docs#MonoidHom.ker is defined to be a subgroup, this is where it is formalized.

[Abraham Solomon]

Etienne Marion said:

This does not work. Typing are not Lean statements. What you want to do here is this:

import Mathlib

example {G H : Type*} [Group G] [Group H] (φ : G →* H) :
    IsSubgroup (φ.ker : Set G) := sorry

Thanks for the helpful comment, would you mind explaining why it doesn't work?
That is, i can form the statement:

variable [Group G] [MulOneClass H]
example (φ : G →* H) : (φ.ker:Subgroup G) := by
  sorry

And my answer was about how to annotate his example, for it not to be a black box and to say that the kernel is a subgroup. So anything informative would be greatly appreciated!

[Aaron Liu]

The conclusion of the the theorem should go on the right side of the :. In this case, you have (φ.ker:Subgroup G). This means that you are trying to make an element of type (φ.ker:Subgroup G). In other words, an element of φ.ker.

import Mathlib

variable [Group G] [MulOneClass H]
example (φ : G →* H) : (φ.ker:Subgroup G) := by
  exact 1 -- `φ.ker` is a `Subgroup`, so in particular it must contain `1`.

Writing (φ.ker:Subgroup G) is called a type annotation and it means something like "φ.ker, which is a Subgroup G". So for example I could write (1 : Rat) = 1 + 0 and it would mean "1 (which is a Rat) equals 1 + 0". In Lean this is not a statement that could be true or false, but rather a judgement that must be true or your code won't compile.

[Abraham Solomon]

Aaron Liu said:

The conclusion of the the theorem should go on the right side of the :. In this case, you have (φ.ker:Subgroup G). This means that you are trying to make an element of type (φ.ker:Subgroup G). In other words, an element of φ.ker.

import Mathlib

variable [Group G] [MulOneClass H]
example (φ : G →* H) : (φ.ker:Subgroup G) := by
  exact 1 -- `φ.ker` is a `Subgroup`, so in particular it must contain `1`.

Writing (φ.ker:Subgroup G) is called a type annotation and it means something like "φ.ker, which is a Subgroup G". So for example I could write (1 : Rat) = 1 + 0 and it would mean "1 (which is a Rat) equals 1 + 0". In Lean this is not a statement that could be true or false, but rather a judgement that must be true or your code won't compile.

I was simply answering the question, of treating it like a black box, and formalising the statement saying that it is the kernel thats the subgroup.

[Etienne Marion]

As Aaron pointed out, example (φ : G →* H) : (φ.ker:Subgroup G) does not mean "$\mathrm{ker(}\phi)$ is a subgroup of G" but merely "there exists an element in $\mathrm{ker}(\phi)$". It is the same as

example (φ : G →* H) : φ.ker

[Aaron Liu]

Abraham Solomon said:

I was simply answering the question, of treating it like a black box, and formalising the statement saying that it is the kernel thats the subgroup.

How would you write the opposite statement, "φ.ker is not a Subgroup G"?

[Damiano Testa]

I also think that there is a related discussion here that might be relevant.

[Damiano Testa]

Correctness of definitions is up to the human: you are in charge of making sure that your code describes what you want.

[Damiano Testa]

Correctness of proofs is left to the computer.

[Damiano Testa]

The theorem statements should encode enough properties of your definitions that they uniquely characterise them, so that you can be "sure" that you defined what you wanted.

[Johan Commelin]

@Abraham Solomon To formalize the statement: "$ker(\phi)$ is a subgroup" we must first agree on what the formal definition of "kernel" is.
In mathlib, the kernel of a group homomorphism is a subgroup by definition. So there is nothing left to prove.

However, if you say the kernel is only a subset, then there is of course something left to prove.

This means that one way to formalize your claim is to prove

example : (φ.ker : Set G) = {x | φ x = 0} := sorry

or alternatively something like $x \in \ker(\phi) \iff \phi(x) = 0$.

[Ruben Van de Velde]

I was going to suggest looking at the definition of ker, but it's not very beginner-friendly. Alternatively you can build it yourself:

import Mathlib
example [Group G] [Group H] (φ : G →* H) : Subgroup G where
  carrier := { x | φ x = 1 }
  mul_mem' {a b} ha hb := by simp_all
  one_mem' := by simp_all
  inv_mem' {x} hx := by simp_all

(And note that Johan is confusing the kernel of additive and multiplicative groups)

[Eric Wieser]

Does it help to think about how you might state "the addition of two natural numbers is a natural number"? In both cases, the return type of the operation in question makes the mathematical question vacuous.

[Isak Colboubrani]

Johan Commelin said:

Abraham Solomon To formalize the statement: "$ker(\phi)$ is a subgroup" we must first agree on what the formal definition of "kernel" is.

That is indeed a good point; I should have made it clearer in my original post. The undergraduates I will show this to are accustomed to the definitions in Dummit & Foote, so I will use the following definition and result:

Definition. If ϕ is a homomorphism ϕ: G → H, the kernel of ϕ is the set { g ∈ G | ϕ(g)=1 } and will be denoted by ker ϕ (here 1 is the identity of H).

Theorem. Let G and H be groups and let ϕ: G → H be a homomorphism. ker ϕ is a subgroup of G.

[Kevin Buzzard]

When I give this exercise to my undergraduates, I just write

import Mathlib
example [Group G] [Group H] (φ : G →* H) : Subgroup G where
  carrier := { x | φ x = 1 }
  mul_mem' := sorry
  one_mem' := sorry
  inv_mem' := sorry

[Edward van de Meent]

alternatively, you could ask them to prove

example [Group G] [Group H] (φ : G →* H) : ∃ (s : Subgroup G), ∀ x, x ∈ s ↔ φ x = 1

[Li Xuanji]

It might be helpful to note that in Mathlib, a subgroup is a structure consisting of 4 fields, only one of which (called the "carrier") is a set. The other 3 fields are proofs that the carrier obeys certain properties. E.g. when defining the subgroup of rotations of a dihedral group I have to give the definition of the carrier (which is 1 line long) and then 3 proofs (which are longer):

import Mathlib.Tactic
import Mathlib.GroupTheory.SpecificGroups.Dihedral

namespace DihedralGroup

def Rot (n : ℕ): Subgroup (DihedralGroup n) where
  carrier := { r i | i : ZMod n }
  mul_mem' := by
    intros a b a_is_ri b_is_ri
    cases' a_is_ri with i1 r_i1_is_a
    cases' b_is_ri with i2 r_i1_is_b
    use i1 + i2
    rw [←r_i1_is_a, ←r_i1_is_b]
    rw [r_mul_r]
  one_mem' := by
    use 0
    rfl
  inv_mem' := by
    intros x x_in_A
    cases' x_in_A with i ri_is_x
    use -i
    rw [← ri_is_x]
    rfl

So the translation of the definition of a kernel is more like:

Definition. If ϕ is a homomorphism ϕ: G → H, the kernel of ϕ, denoted by φ.ker is a structure consisting of four fields:

• φ.ker.carrier, a set defined as { g ∈ G | ϕ(g)=1 }
• φ.ker.mul_mem', a proof that (ker φ).carrier is closed under multiplication
• φ.ker.one_mem', a proof that (ker φ).carrier contains 1
• φ.ker.inv_mem', a proof that (ker φ).carrier is closed under inversion

The slightly awkward thing is that the only way built-in to access the carrier set without redefining it is to say φ.ker.carrier, which is taking the "set + proofs" objects and forgetting the proofs

[Philippe Duchon]

Kevin Buzzard said:

When I give this exercise to my undergraduates, I just write

import Mathlib
example [Group G] [Group H] (φ : G →* H) : Subgroup G where
  carrier := { x | φ x = 1 }
  mul_mem' := sorry
  one_mem' := sorry
  inv_mem' := sorry

In this case, simp seems way too powerful for this to make up an exercise. It looks a bit like Lean's version of "just write what you need to prove and check that it works", except in this case you don't even have to write what you need to prove.

[Kevin Buzzard]

If you don't want the simplifier to be able to do it then make your own groups. I also set this as an exercise, I use five axioms (left and right identity, left and right inverse, associativity). Or make your own group homomorphisms, I do this too (but using Lean's groups)

[Isak Colboubrani]

Thanks for the very helpful replies. I have now written this in three different ways. Do they look reasonable?

-- Definition:
--   If ϕ is a homomorphism ϕ: G → H, the kernel of ϕ is the set { g ∈ G | ϕ(g)=1 } and
--   will be denoted by ker ϕ (here 1 is the identity of H).
-- Theorem:
--   Let G and H be groups and let ϕ: G → H be a homomorphism. ker ϕ is a subgroup of G.
example [Group G] [Group H] (φ : G →* H) : Subgroup G where
  carrier := { x | φ x = 1 }
  mul_mem' := by simp_all
  one_mem' := by simp
  inv_mem' := by simp

example [Group G] [Group H] (φ : G →* H) : IsSubgroup (φ.ker : Set G) := by
  exact φ.ker.isSubgroup

example [Group G] [Group H] (φ : G →* H) : ∃ (s : Subgroup G), ∀ x, x ∈ s ↔ φ x = 1 := by
  exact ⟨{
    carrier := { x | φ x = 1 },
    mul_mem' := by simp_all,
    one_mem' := by simp,
    inv_mem' := by simp
  }, by simp⟩

[Aaron Liu]

Yes, these look good to me.
Note that the kernel of a group in Mathlib is defined more generally where the codomain is any type where 1 is a two-sided identity to multiplication, not just a group (which also has stuff like associativity and inverses).

[Kevin Buzzard]

IsSubgroup is deprecated and about to be deleted

[Kevin Buzzard]

Note also that by exact does nothing: by switches from term mode to tactic mode and exact switches from tactic mode to term mode.

[Aaron Liu]

Kevin Buzzard said:

IsSubgroup is deprecated and about to be deleted

Really? How do you say a set forms a subgroup then?

[Yaël Dillies]

You don't. You build the set as a subgroup instead

[Aaron Liu]

What about for something like ∀ᶠ n in atTop, IsSubgroup (f n)

[Kevin Buzzard]

That happens in theory but in 1.5 million lines of mathlib it doesn't seem to happen in practice.

[Kevin Buzzard]

And if it really did happen, you could just say stuff like \forall a b \in f n, a * b \in f n or whatever

[Jireh Loreaux]

Or simply: ∀ᶠ in atTop, ∃ H : Subgroup G, (H : Set G) = f n (assuming f : ℕ → Set G or some other index set).

[Kevin Buzzard]

Even better!

[Kevin Buzzard]

In fact what happened in practice was that there were things which were always group homomorphisms but which had been defined as plain functions; the fix nowadays is just to make another definition, defining the group homomorphism as well.