# Zulip Chat Archive

## Stream: new members

### Topic: Subgroup of a subgroup should be a subgroup

#### Marc Masdeu (Jul 31 2020 at 09:00):

Given a group G, I defined its two-torsion subgroup. I would like to show that this operation is idempotent:

```
def two_torsion_subgroup (G : Type*) [comm_group G] : subgroup G :=
{ carrier := {z : G | z * z = 1},
one_mem' := by simp,
mul_mem' := λ a b (ha : a * a = 1) (hb : b * b = 1),
begin
dsimp at *,
rw [mul_mul_mul_comm a b a b, ha, hb],
refine mul_one 1,
end,
inv_mem' := λ a (ha : a * a = 1), by {tidy, rw mul_inv_eq_one, refine inv_eq_of_mul_eq_one ha}
}
lemma two_torsion_group_iterate : two_torsion_subgroup G = two_torsion_subgroup ((subgroup.to_group (two_torsion_subgroup G)) :=
begin
sorry
end
```

The lemma doesn't typecheck:

```
type mismatch at application
two_torsion_subgroup (two_torsion_subgroup G).to_group
term
(two_torsion_subgroup G).to_group
has type
group ↥(two_torsion_subgroup G) : Type u_1
but is expected to have type
Type u_1 : Type (u_1+1)
```

What am I doing wrong?

#### Kenny Lau (Jul 31 2020 at 09:01):

read the error

#### Kenny Lau (Jul 31 2020 at 09:01):

`(two_torsion_subgroup G).to_group`

is the "proof" that `two_torsion_subgroup G`

is a group

#### Kenny Lau (Jul 31 2020 at 09:02):

so it should read `two_torsion_subgroup G = two_torsion_subgroup (two_torsion_subgroup G)`

#### Kenny Lau (Jul 31 2020 at 09:02):

except that this won't typecheck as well

#### Marc Masdeu (Jul 31 2020 at 09:02):

Yes, what you suggest is the first thing that I tried.

#### Kenny Lau (Jul 31 2020 at 09:02):

because LHS is a subgroup of `G`

while RHS is a subgroup of `two_torsion_subgroup G`

#### Marc Masdeu (Jul 31 2020 at 09:03):

I want to "coerce" somehow the subgroup to a group...

#### Kenny Lau (Jul 31 2020 at 09:04):

the lemma should be `two_torsion_subgroup (two_torsion_subgroup G) = \top`

#### Kenny Lau (Jul 31 2020 at 09:04):

then you can coerce it however you want

#### Kenny Lau (Jul 31 2020 at 09:04):

I don't think the coercion is defined in mathlib though

#### Kenny Lau (Jul 31 2020 at 09:04):

the sub-object API's need some work

#### Kenny Lau (Jul 31 2020 at 09:05):

for now I hope `two_torsion_subgroup (two_torsion_subgroup G) = \top`

is good enough

#### Marc Masdeu (Jul 31 2020 at 09:05):

What is this good for?

```
instance : has_coe_to_sort (subgroup G) := ⟨_, λ G, (G : Type*)⟩
```

#### Kenny Lau (Jul 31 2020 at 09:06):

this allows you to treat `two_torsion_subgroup G`

as a type

#### Kenny Lau (Jul 31 2020 at 09:06):

instead of just a subgroup of `G`

#### Marc Masdeu (Jul 31 2020 at 09:07):

So wouldn't that help my original goal? I want to put G and two_torsion_subgroup G both as the same Type, so that I can compare their respective two_torsion_subgroups

#### Marc Masdeu (Jul 31 2020 at 09:09):

(but it doesn't work)

```
lemma two_torsion_group_iterate' : two_torsion_subgroup (has_coe_to_sort (two_torsion_subgroup G)) = two_torsion_subgroup G :=
begin
sorry
end
```

gives

```
type mismatch at application
two_torsion_subgroup G
term
G
has type
Type u_1 : Type (u_1+1)
but is expected to have type
Type (max (max 1 (u_1+1)) (?+1)) : Type ((max (max 1 (u_1+1)) (?+1))+1)
```

#### Kenny Lau (Jul 31 2020 at 09:10):

you don't use `has_coe_to_sort`

#### Kenny Lau (Jul 31 2020 at 09:10):

again, the correct term is `two_torsion_subgroup (two_torsion_subgroup G)`

#### Kenny Lau (Jul 31 2020 at 09:10):

where the inner `two_torsion_subgroup G`

has been coerced to a type by the instance you posted

#### Kenny Lau (Jul 31 2020 at 09:11):

before that, `two_torsion_subgroup G`

is just a subgroup of `G`

#### Kenny Lau (Jul 31 2020 at 09:11):

it is after it has been coerced to a type that you can even say that `two_torsion_subgroup G`

is a group

#### Kenny Lau (Jul 31 2020 at 09:11):

only types can be groups

#### Kenny Lau (Jul 31 2020 at 09:12):

and to be clear, when we say `X`

is a group, what we mean is that we have an instance of `group X`

#### Kenny Lau (Jul 31 2020 at 09:12):

which allows you to write things like `1 : X`

#### Marc Masdeu (Jul 31 2020 at 09:12):

Yes, the I am still confused by how groups/subgroups are implemented...

#### Marc Masdeu (Jul 31 2020 at 09:12):

I'll see if the solution that you proposed is enough for what I wanted!

#### Kenny Lau (Jul 31 2020 at 09:12):

`subgroup G`

is the type of subgroups of `G`

#### Kenny Lau (Jul 31 2020 at 09:13):

i.e. `S : subgroup G`

means "`S`

is a subgroup of `G`

"

#### Kenny Lau (Jul 31 2020 at 09:13):

so there's no reason to suppose that `S`

is a type

#### Kenny Lau (Jul 31 2020 at 09:13):

but then that instance coerces `S`

to a type (printed as some thick up arrow followed by `S`

, but to type it you just type `S`

)

#### Kenny Lau (Jul 31 2020 at 09:14):

so now `subgroup S`

makes sense

#### Kenny Lau (Jul 31 2020 at 09:14):

and `U : subgroup S`

means "`U`

is a subgroup of the result of the coercion of `S`

into a type"

#### Kenny Lau (Jul 31 2020 at 09:14):

note that (coerced) `S`

and `G`

are incomparable types

#### Kenny Lau (Jul 31 2020 at 09:15):

as in, given `x : S`

and `g : G`

, you cannot make the statement `x = g`

#### Kenny Lau (Jul 31 2020 at 09:15):

in Lean all distinct types are incomparable

#### Marc Masdeu (Jul 31 2020 at 09:16):

And what you are saying is that there's no good way to make S and G of the same type... That's too bad.

#### Kenny Lau (Jul 31 2020 at 09:16):

so in practice you should treat `S`

as another group isomorphic to the subgroup of `G`

also called `S`

#### Kenny Lau (Jul 31 2020 at 09:17):

here's how the type coercion works

#### Kenny Lau (Jul 31 2020 at 09:17):

given `x : S`

, you can coerce it to `x : G`

(printed with a little up-arrow, but to type it you just type `x : G`

)

#### Kenny Lau (Jul 31 2020 at 09:17):

the little up-arrow is a "hidden function"

#### Kenny Lau (Jul 31 2020 at 09:17):

because, again, types in Lean are incomparable

#### Kenny Lau (Jul 31 2020 at 09:18):

given `x : G`

and `hx : x \in S`

(i.e. `hx`

is a proof that `x`

is an element of `S`

), you can form `\<x, hx\> : S`

#### Marc Masdeu (Jul 31 2020 at 09:19):

Oh so in one way it's automatic, in the other I need this bracket notation... that's useful.

#### Kenny Lau (Jul 31 2020 at 09:19):

so they are distinct types with (partial) functions going both ways

#### Marc Masdeu (Jul 31 2020 at 09:20):

(and BTW, I have no clue how to make progress in that lemma, although it's mathematically trivial)

#### Kenny Lau (Jul 31 2020 at 09:20):

similarly, `subgroup S`

and `subgroup G`

are incomparable types

#### Kenny Lau (Jul 31 2020 at 09:20):

you cannot ever state that their terms are equal

#### Kenny Lau (Jul 31 2020 at 09:20):

but again, you can define (partial) functions going both ways

#### Kenny Lau (Jul 31 2020 at 09:20):

it's just that this hasn't been done in mathlib

#### Kenny Lau (Jul 31 2020 at 09:21):

for no other reason than itself

#### Kenny Lau (Jul 31 2020 at 09:21):

and anyway, even if you have that function, you would still need my lemma to prove the "mathematically correct" version

#### Kenny Lau (Jul 31 2020 at 09:21):

Marc Masdeu said:

(and BTW, I have no clue how to make progress in that lemma, although it's mathematically trivial)

you can start with (some variant of) `eq_top`

(use the Ctrl+space trick!)

#### Kenny Lau (Jul 31 2020 at 09:27):

```
import group_theory.subgroup
def two_torsion_subgroup (G : Type*) [comm_group G] : subgroup G :=
{ carrier := {z : G | z * z = 1},
one_mem' := mul_one 1,
mul_mem' := λ a b (ha : a * a = 1) (hb : b * b = 1),
calc (a * b) * (a * b)
= (a * a) * (b * b) : mul_mul_mul_comm _ _ _ _
... = 1 * 1 : by rw [ha, hb]
... = 1 : mul_one _,
inv_mem' := λ a (ha : a * a = 1),
calc a⁻¹ * a⁻¹
= (a * a)⁻¹ : (mul_inv _ _).symm
... = 1⁻¹ : by rw ha
... = 1 : one_inv
}
theorem two_torsion_subgroup_idem (G : Type*) [comm_group G] :
two_torsion_subgroup (two_torsion_subgroup G) = ⊤ :=
show two_torsion_subgroup (two_torsion_subgroup G) = ⊤, from eq_top_iff.2 $
show ⊤ ≤ two_torsion_subgroup (two_torsion_subgroup G), from λ x hx,
show x * x = 1, from subtype.eq $
show (x * x : G) = 1, from x.2
```

#### Kenny Lau (Jul 31 2020 at 09:28):

right, so the two functions I told you about going between `G`

and `S`

are not enough for you to prove this lemma

#### Kenny Lau (Jul 31 2020 at 09:28):

there's also the theorem that the function from `S`

to `G`

is surjective

#### Kenny Lau (Jul 31 2020 at 09:28):

i.e. if `x y : S`

such that `(x : G) = y`

then `x = y`

#### Kenny Lau (Jul 31 2020 at 09:28):

this theorem is called `subtype.eq`

#### Marc Masdeu (Jul 31 2020 at 09:30):

Wow thanks! This is so helpful!

#### Kenny Lau (Jul 31 2020 at 09:31):

note that Lean elaborates from outside to inside, so `(x * x : G)`

actually means `(\u x * \u x : G)`

(`\u`

being the coercion from `S`

to `G`

)

#### Kenny Lau (Jul 31 2020 at 09:31):

Lean first sees the `*`

and figures out that both operands must be terms of `G`

#### Kenny Lau (Jul 31 2020 at 09:32):

but actually typing out the arrow sometimes causes errors

#### Kenny Lau (Jul 31 2020 at 09:32):

so don't type out the arrow

#### Kenny Lau (Jul 31 2020 at 09:32):

well, not typing it sometimes causes errors, in different situations (such as the coercion from `finset`

to `set`

)

#### Kenny Lau (Jul 31 2020 at 09:44):

```
import group_theory.subgroup
def two_torsion_subgroup (G : Type*) [comm_group G] : subgroup G :=
{ carrier := {z : G | z * z = 1},
one_mem' := mul_one 1,
mul_mem' := λ a b (ha : a * a = 1) (hb : b * b = 1),
calc (a * b) * (a * b)
= (a * a) * (b * b) : mul_mul_mul_comm _ _ _ _
... = 1 * 1 : by rw [ha, hb]
... = 1 : mul_one _,
inv_mem' := λ a (ha : a * a = 1),
calc a⁻¹ * a⁻¹
= (a * a)⁻¹ : (mul_inv _ _).symm
... = 1⁻¹ : by rw ha
... = 1 : one_inv
}
theorem two_torsion_subgroup_idem (G : Type*) [comm_group G] :
two_torsion_subgroup (two_torsion_subgroup G) = ⊤ :=
show two_torsion_subgroup (two_torsion_subgroup G) = ⊤, from eq_top_iff.2 $
show ⊤ ≤ two_torsion_subgroup (two_torsion_subgroup G), from λ x hx,
show x * x = 1, from subtype.eq $
show (x * x : G) = 1, from x.2
section missing_from_mathlib
instance subgroup.subgroup (G : Type*) [group G] (S : subgroup G) : has_coe (subgroup S) (subgroup G) :=
⟨subgroup.map S.subtype⟩
@[simp] lemma subgroup.coe_top' {G : Type*} [group G] (S : subgroup G) : ((⊤ : subgroup S) : subgroup G) = S :=
le_antisymm (subgroup.map_le_iff_le_comap.2 $ λ x _, x.2) (λ x hx, ⟨⟨x, hx⟩, trivial, rfl⟩)
end missing_from_mathlib
theorem two_torsion_subgroup_idem' (G : Type*) [comm_group G] :
((two_torsion_subgroup (two_torsion_subgroup G) : subgroup _) : subgroup G) = two_torsion_subgroup G :=
by rw [two_torsion_subgroup_idem, subgroup.coe_top']
```

#### Kenny Lau (Jul 31 2020 at 09:44):

@Marc Masdeu here's the "mathematically correct" statement and why it uses my lemma anyways

#### Mario Carneiro (Jul 31 2020 at 09:47):

good job kenny

#### Kenny Lau (Jul 31 2020 at 09:48):

thanks

#### Kenny Lau (Jul 31 2020 at 09:48):

I don't have time to build the subobject API yet though

#### Marc Masdeu (Jul 31 2020 at 09:49):

You guys are great

#### Marc Masdeu (Jul 31 2020 at 11:34):

This will be the last one for today, I promise:

```
lemma prod_identity_general {g : two_torsion_subgroup G} (h : (g : G) ≠ (1 : G)):
((∏ x : G, x) : G)= g^(fintype.card (two_torsion_subgroup G) / 2 : ℕ) :=
begin
rw prod_all_eq_prod_two_torsion,
have htors : ∀ (x : two_torsion_subgroup G), x * x = 1,
{
intro x,
rw ←mem_two_torsion_iff_square_eq_one,
rw two_torsion_subgroup_idem,
solve_by_elim,
},
have h' : g ≠ 1, by finish,
norm_cast,
rw ←prod_identity htors h',
sorry
end
```

I end up with the following state:

```
G : Type u_1
_inst_1 : comm_group G
_inst_2 : fintype G
htors : ∀ (x : ↥G2), x * x = 1
⊢ ∏ (g : ↥(two_torsion_subgroup G)), ↑g = ↑∏ (x : ↥two_torsion_subgroup G), x
```

I want to apply finset.prod_hom with something like lam x : two_torsion_subgroup G, x : G,

but it doesn't let me. This is probably some form of a similar problem that I have faced before, but I continuously get stuck with these sorts...

#### Marc Masdeu (Jul 31 2020 at 13:42):

@Kenny Lau I rewrote a M(N)WE hoping that it's a one-liner what I'm missing...

#### Kenny Lau (Jul 31 2020 at 14:02):

```
import group_theory.subgroup data.fintype.basic
open_locale classical big_operators
section missing_from_mathlib
instance subgroup.coe_is_monoid_hom {G : Type*} [group G] (H : subgroup G) : is_monoid_hom (coe : H → G) :=
by refine {..}; intros; refl
end missing_from_mathlib
lemma prod_coerce {G : Type*} [comm_group G] [fintype G] {H : subgroup G} : ∏ x : H, (x:G) = ((∏ x : H, x) : H) :=
finset.prod_hom _ _
```

#### Kenny Lau (Jul 31 2020 at 14:06):

@Marc Masdeu coe and coe_sort etc are not meant to be used explicitly

#### Kenny Lau (Jul 31 2020 at 14:07):

we use at most an uparrow

#### Marc Masdeu (Jul 31 2020 at 14:07):

Thanks! I really didn't need the lemma, my code works now after the `instance`

line.

#### Marc Masdeu (Jul 31 2020 at 14:09):

How would I figure this up on my own? I mean, I wanted to `apply finset.prod_hom`

and saw the error, and I was trying (unsuccessfully) to create a monoid_hom... I guess I still don't understand `instance`

...

#### Kenny Lau (Jul 31 2020 at 14:29):

the error says failed to synthesize instance

#### Kenny Lau (Jul 31 2020 at 14:29):

the typeclass system is like Lean's notebook

#### Kenny Lau (Jul 31 2020 at 14:30):

whenever you tell Lean about one instance, Lean marks it down in her notebook

#### Kenny Lau (Jul 31 2020 at 14:30):

this is called the type-class system

#### Kenny Lau (Jul 31 2020 at 14:30):

so whenever you require an instance, you ask Lean what she has learnt, and she will find the knowledge from her notebook

#### Marc Masdeu (Jul 31 2020 at 14:30):

Instance means "example of"?

#### Kenny Lau (Jul 31 2020 at 14:30):

no

#### Kenny Lau (Jul 31 2020 at 14:30):

instance just means something to mark down in her notebook

#### Kevin Buzzard (Jul 31 2020 at 14:30):

It means definition in the notebook

#### Kenny Lau (Jul 31 2020 at 14:31):

e.g. the group structure on a type

#### Kenny Lau (Jul 31 2020 at 14:31):

the fact that a specific function is a homomorphism

#### Kenny Lau (Jul 31 2020 at 14:31):

etc

#### Marc Masdeu (Jul 31 2020 at 14:32):

I see. So properties of objects that I may want Lean to use in the future...?

#### Kenny Lau (Jul 31 2020 at 14:32):

if you do `#check @finset.prod_hom`

you will see:

```
finset.prod_hom :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [_inst_1 : comm_monoid β] [_inst_2 : comm_monoid γ]
(s : finset α) {f : α → β} (g : β → γ) [_inst_3 : is_monoid_hom g],
∏ (x : α) in s, g (f x) = g (∏ (x : α) in s, f x)
```

#### Kenny Lau (Jul 31 2020 at 14:32):

the arguments in square brackets are what you ask Lean from her notebook

#### Kenny Lau (Jul 31 2020 at 14:33):

`[comm_monoid \b]`

means "ask Lean to provide a commutative monoid structure on beta"

#### Marc Masdeu (Jul 31 2020 at 14:33):

Instances vs square-brackets is as far as my knowledge goes on this...

#### Kenny Lau (Jul 31 2020 at 14:33):

when you use it you don't need to provide the argument explicitly

#### Kenny Lau (Jul 31 2020 at 14:33):

Lean will search her notebook for you

#### Kenny Lau (Jul 31 2020 at 14:33):

the arguments in curly brackets are also implicit, but they work using a different system

#### Kenny Lau (Jul 31 2020 at 14:34):

so e.g. Lean knows that Z is a comm_monoid

#### Kenny Lau (Jul 31 2020 at 14:34):

so this theorem `finset.prod_hom`

can be applied for beta being Z

#### Marc Masdeu (Jul 31 2020 at 14:34):

So it's an automated set of hypotheses, sort of. I could write a lemma that said something like:

```
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (_inst_1 : comm_monoid β) (_inst_2 : comm_monoid γ)
(s : finset α) {f : α → β} (g : β → γ) (_inst_3 : is_monoid_hom g),
∏ (x : α) in s, g (f x) = g (∏ (x : α) in s, f x)
```

but then it would be more annoying to use. Is that right?

#### Kenny Lau (Jul 31 2020 at 14:35):

exactly

#### Kenny Lau (Jul 31 2020 at 14:35):

then you would have to explicitly provide the "proof" that beta is a comm monoid

#### Marc Masdeu (Jul 31 2020 at 14:35):

Oh nice! Lean didn't tell me which of the three instances couldn't make sense of. Is there a way to ask for that?

#### Kenny Lau (Jul 31 2020 at 14:35):

which will be something like `int.comm_monoid`

#### Kenny Lau (Jul 31 2020 at 14:36):

```
failed to synthesize type class instance for
G : Type u_1,
_inst_1 : comm_group G,
_inst_2 : fintype G,
H : subgroup G
⊢ is_monoid_hom coe
```

#### Kenny Lau (Jul 31 2020 at 14:36):

read the error

#### Marc Masdeu (Jul 31 2020 at 14:37):

Oh! Sorry, I see. It'd be nice that there was a modification of apply (like convert) that introduced this as a new goal...

#### Kenny Lau (Jul 31 2020 at 14:37):

why not prove it separately?

#### Kenny Lau (Jul 31 2020 at 14:37):

keep proofs short but many

#### Marc Masdeu (Jul 31 2020 at 14:38):

When in tactic mode, it's nice when you can keep applying results that you know will allow you to make progress (in this case, `prod.hom`

), and get asked for the hypotheses later.

#### Kenny Lau (Jul 31 2020 at 14:40):

I guess it makes some sense

#### Kenny Lau (Jul 31 2020 at 14:44):

```
import group_theory.subgroup data.fintype.basic
open_locale classical big_operators
lemma prod_coerce {G : Type*} [comm_group G] [fintype G] {H : subgroup G} : ∏ x : H, (x:G) = ((∏ x : H, x) : H) :=
begin
convert finset.prod_hom _ _
end
/-
tactic failed, there are unsolved goals
state:
G : Type u_1,
_inst_1 : comm_group G,
_inst_2 : fintype G,
H : subgroup G
⊢ is_monoid_hom coe
-/
```

#### Kenny Lau (Jul 31 2020 at 14:44):

this is the best I can do @Marc Masdeu

#### Jalex Stark (Jul 31 2020 at 15:06):

you can get the instances as goals by using `@`

#### Jalex Stark (Jul 31 2020 at 15:06):

if you look at the type of `@prod_hom`

, you'll see that it has explicit arguments for the typeclass instances

#### Jalex Stark (Jul 31 2020 at 15:07):

so if you `apply @prod_hom`

with appropriate underscores, the instances will appear as goals

#### Marc Masdeu (Jul 31 2020 at 16:10):

Thanks guys! All these tricks should be documented somewhere. Like the Tactic cheatsheet, they'd very useful for noobs...

#### Jalex Stark (Jul 31 2020 at 16:12):

better documentation and tutorialization is definitely a goal

#### Jalex Stark (Jul 31 2020 at 16:13):

from my rereading, most of this conversation was just explaining what typeclasses are

#### Jalex Stark (Jul 31 2020 at 16:13):

#tpil chapter 10 is all about type classes

#### Jalex Stark (Jul 31 2020 at 16:15):

type classes probably get a more gentle introduction in #mil

Last updated: May 11 2021 at 14:11 UTC