Theorem - Transitivity of subgroups

Stream: general

[ZHAO Jinxiang]

I don't know how to write the following theorems in lean:

If H is a subgroup of G and K is a subgroup of H, then K is a subgroup of H.

[Johan Commelin]

If you have A B C : subgroup G and h1 : A ≤ B and h2 : B ≤ C then h1.trans h2 will be a term of A ≤ C.
If you have H : subgroup G and K : subgroup H, then K : subgroup G does not type check. You will have to apply subgroup.map to the canonical group hom from H to G.

[ZHAO Jinxiang]

I'm using mathlib's subgroup def. But this seems not valid code

import tactic -- imports all the Lean tactics
import group_theory.subgroup.basic -- import Lean's subgroups

variables {G : Type*} [group G]

lemma subgroup_trans (H : subgroup G) (K : subgroup H) :  (K : subgroup G)   :=
begin
  sorry,
end

image.png

[Johan Commelin]

Indeed, that doesn't type check.
If K has type subgroup H, it can not also have type subgoup G.

[Johan Commelin]

You could argue that there should be a coercion from subgroup H to subgroup G, but mathlib doesn't have that.

[Johan Commelin]

So you need to use subgroup.map.

[ZHAO Jinxiang]

Let me have a try

[ZHAO Jinxiang]

Is there any function to make a coercion from subgroup H to subgroup G without writing monoid_hom by my self?

[Kevin Buzzard]

docs#subgroup.map

[ZHAO Jinxiang]

def subgroup.map {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) (H : subgroup G) : subgroup N

I need to provide (f : G →* N). That means I need to provide a instance of monoid_hom.

Is there any helper function help me to provide this?

[Johan Commelin]

I guess H.subtype is that map

[Johan Commelin]

You could try filling it in by library_search

[Johan Commelin]

subgroup.map (by library_search) K

[ZHAO Jinxiang]

import tactic -- imports all the Lean tactics
import group_theory.subgroup.basic -- import Lean's subgroups

variables {G : Type*} [group G]

lemma subgroup_trans (H : subgroup G) (K : subgroup H) : subgroup.map H.subtype K :=
begin
  sorry,
end

image.png

[Johan Commelin]

That's not a lemma.

[Johan Commelin]

subgroup.map H.subtype K is a subgroup of G.

[ZHAO Jinxiang]

Thank you very much for your patient answer. :heart_kiss:
I have another question.
So how do I state that K is a subgroup of G ? :joy:

[Johan Commelin]

It is not.

[Kevin Buzzard]

I don't know how to write the following theorems in lean: If H is a subgroup of G and K is a subgroup of H, then K is a subgroup of H.

That is not a "theorem" in Lean. It is a construction, so it is a definition.

[ZHAO Jinxiang]

I know it's not type-theoretically correct. But in textbooks written in set theory, there is such a proposition:

If H is a subgroup of G and K is a subgroup of H, then K is a subgroup of H.

I want to formalize it with lean .

[ZHAO Jinxiang]

Oh, I know, it is a definition. So I need't prove this.

[Kevin Buzzard]

The textbooks also talk about things like "the first isomorphism theorem" which is also a definition. I'm just pointing out that if you are not precise with language then it can lead you to ask informal questions about a system where it is not clear what you are actually asking. You ask "So how do I state that K is a subgroup of G ?" A better question on this chat is "here is some code, how do I fill in the sorry"? It is very hard to answer a question of the form "So how do I state that K is a subgroup of G ?" because you have not precisely stated the types of everything in the question. You might have one mental model of K but when you formalise you might find that there are several ways to represent the idea in type theory, and your mental model of K might correspond to several different things at the same time.

[Hanting Zhang]

ZHAO Jinxiang said:

I know it's not type-theoretically correct. But in textbooks written in set theory, there is such a proposition:

If H is a subgroup of G and K is a subgroup of H, then K is a subgroup of H.

I want to formalize it with lean .

The problem with this is that the predicate is a subgroupdoesn't exist in lean, so you shouldn't think it about that way. Instead, you can ask "Given two pieces of data, i.e. a subgroup H of G and a subgroup K of H, construct the subgroup of G that naturally identifies with K."

[Kevin Buzzard]

A formal and unhelpful answer to your question would be something like: subgroup G is the type of subgroups of G. If you have a term K whose type is subgroup G then it is a subgroup of G by definition. If it does not have type subgroup G then it is not a subgroup of G, by definition (e.g. it might be a subset of G), so you can't prove it's a subgroup of G. One thing which helped me when I was trying to learn this stuff is that groups and subgroups are defined in an asymmetric way in Lean: a group is a type, and a subgroup is a term. In particular "a subgroup is a group" when written naively in Lean does not even make sense on a syntactic level. This is why precision is important when formalising.

[ZHAO Jinxiang]

Thank you very much for your patient answers. :heart_kiss: I learned a lot from the discussions here.

Today is the Chinese Dragon Boat Festival. I wish you a happy day.