## 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):

(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

good job kenny

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"?

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

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?

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


#### 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