Zulip Chat Archive

Stream: new members

Topic: Subgroup of a subgroup should be a subgroup


view this post on Zulip 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?

view this post on Zulip Kenny Lau (Jul 31 2020 at 09:01):

read the error

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jul 31 2020 at 09:02):

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

view this post on Zulip Kenny Lau (Jul 31 2020 at 09:02):

except that this won't typecheck as well

view this post on Zulip Marc Masdeu (Jul 31 2020 at 09:02):

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

view this post on Zulip 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

view this post on Zulip Marc Masdeu (Jul 31 2020 at 09:03):

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

view this post on Zulip Kenny Lau (Jul 31 2020 at 09:04):

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

view this post on Zulip Kenny Lau (Jul 31 2020 at 09:04):

then you can coerce it however you want

view this post on Zulip Kenny Lau (Jul 31 2020 at 09:04):

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

view this post on Zulip Kenny Lau (Jul 31 2020 at 09:04):

the sub-object API's need some work

view this post on Zulip Kenny Lau (Jul 31 2020 at 09:05):

for now I hope two_torsion_subgroup (two_torsion_subgroup G) = \top is good enough

view this post on Zulip Marc Masdeu (Jul 31 2020 at 09:05):

What is this good for?

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

view this post on Zulip Kenny Lau (Jul 31 2020 at 09:06):

this allows you to treat two_torsion_subgroup G as a type

view this post on Zulip Kenny Lau (Jul 31 2020 at 09:06):

instead of just a subgroup of G

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Kenny Lau (Jul 31 2020 at 09:10):

you don't use has_coe_to_sort

view this post on Zulip Kenny Lau (Jul 31 2020 at 09:10):

again, the correct term is two_torsion_subgroup (two_torsion_subgroup G)

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jul 31 2020 at 09:11):

before that, two_torsion_subgroup G is just a subgroup of G

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jul 31 2020 at 09:11):

only types can be groups

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jul 31 2020 at 09:12):

which allows you to write things like 1 : X

view this post on Zulip Marc Masdeu (Jul 31 2020 at 09:12):

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

view this post on Zulip Marc Masdeu (Jul 31 2020 at 09:12):

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

view this post on Zulip Kenny Lau (Jul 31 2020 at 09:12):

subgroup G is the type of subgroups of G

view this post on Zulip Kenny Lau (Jul 31 2020 at 09:13):

i.e. S : subgroup G means "S is a subgroup of G"

view this post on Zulip Kenny Lau (Jul 31 2020 at 09:13):

so there's no reason to suppose that S is a type

view this post on Zulip 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)

view this post on Zulip Kenny Lau (Jul 31 2020 at 09:14):

so now subgroup S makes sense

view this post on Zulip 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"

view this post on Zulip Kenny Lau (Jul 31 2020 at 09:14):

note that (coerced) S and G are incomparable types

view this post on Zulip Kenny Lau (Jul 31 2020 at 09:15):

as in, given x : S and g : G, you cannot make the statement x = g

view this post on Zulip Kenny Lau (Jul 31 2020 at 09:15):

in Lean all distinct types are incomparable

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jul 31 2020 at 09:17):

here's how the type coercion works

view this post on Zulip 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)

view this post on Zulip Kenny Lau (Jul 31 2020 at 09:17):

the little up-arrow is a "hidden function"

view this post on Zulip Kenny Lau (Jul 31 2020 at 09:17):

because, again, types in Lean are incomparable

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Jul 31 2020 at 09:19):

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

view this post on Zulip 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)

view this post on Zulip Kenny Lau (Jul 31 2020 at 09:20):

similarly, subgroup S and subgroup G are incomparable types

view this post on Zulip Kenny Lau (Jul 31 2020 at 09:20):

you cannot ever state that their terms are equal

view this post on Zulip Kenny Lau (Jul 31 2020 at 09:20):

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

view this post on Zulip Kenny Lau (Jul 31 2020 at 09:20):

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

view this post on Zulip Kenny Lau (Jul 31 2020 at 09:21):

for no other reason than itself

view this post on Zulip 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

view this post on Zulip 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!)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jul 31 2020 at 09:28):

there's also the theorem that the function from S to G is surjective

view this post on Zulip Kenny Lau (Jul 31 2020 at 09:28):

i.e. if x y : S such that (x : G) = y then x = y

view this post on Zulip Kenny Lau (Jul 31 2020 at 09:28):

this theorem is called subtype.eq

view this post on Zulip Marc Masdeu (Jul 31 2020 at 09:30):

Wow thanks! This is so helpful!

view this post on Zulip 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)

view this post on Zulip Kenny Lau (Jul 31 2020 at 09:31):

Lean first sees the * and figures out that both operands must be terms of G

view this post on Zulip Kenny Lau (Jul 31 2020 at 09:32):

but actually typing out the arrow sometimes causes errors

view this post on Zulip Kenny Lau (Jul 31 2020 at 09:32):

so don't type out the arrow

view this post on Zulip 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)

view this post on Zulip 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']

view this post on Zulip Kenny Lau (Jul 31 2020 at 09:44):

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

view this post on Zulip Mario Carneiro (Jul 31 2020 at 09:47):

good job kenny

view this post on Zulip Kenny Lau (Jul 31 2020 at 09:48):

thanks

view this post on Zulip Kenny Lau (Jul 31 2020 at 09:48):

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

view this post on Zulip Marc Masdeu (Jul 31 2020 at 09:49):

You guys are great

view this post on Zulip 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...

view this post on Zulip 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...

view this post on Zulip 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 _ _

view this post on Zulip Kenny Lau (Jul 31 2020 at 14:06):

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

view this post on Zulip Kenny Lau (Jul 31 2020 at 14:07):

we use at most an uparrow

view this post on Zulip Marc Masdeu (Jul 31 2020 at 14:07):

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

view this post on Zulip 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...

view this post on Zulip Kenny Lau (Jul 31 2020 at 14:29):

the error says failed to synthesize instance

view this post on Zulip Kenny Lau (Jul 31 2020 at 14:29):

the typeclass system is like Lean's notebook

view this post on Zulip Kenny Lau (Jul 31 2020 at 14:30):

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

view this post on Zulip Kenny Lau (Jul 31 2020 at 14:30):

this is called the type-class system

view this post on Zulip 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

view this post on Zulip Marc Masdeu (Jul 31 2020 at 14:30):

Instance means "example of"?

view this post on Zulip Kenny Lau (Jul 31 2020 at 14:30):

no

view this post on Zulip Kenny Lau (Jul 31 2020 at 14:30):

instance just means something to mark down in her notebook

view this post on Zulip Kevin Buzzard (Jul 31 2020 at 14:30):

It means definition in the notebook

view this post on Zulip Kenny Lau (Jul 31 2020 at 14:31):

e.g. the group structure on a type

view this post on Zulip Kenny Lau (Jul 31 2020 at 14:31):

the fact that a specific function is a homomorphism

view this post on Zulip Kenny Lau (Jul 31 2020 at 14:31):

etc

view this post on Zulip Marc Masdeu (Jul 31 2020 at 14:32):

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

view this post on Zulip 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)

view this post on Zulip Kenny Lau (Jul 31 2020 at 14:32):

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

view this post on Zulip Kenny Lau (Jul 31 2020 at 14:33):

[comm_monoid \b] means "ask Lean to provide a commutative monoid structure on beta"

view this post on Zulip Marc Masdeu (Jul 31 2020 at 14:33):

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

view this post on Zulip Kenny Lau (Jul 31 2020 at 14:33):

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

view this post on Zulip Kenny Lau (Jul 31 2020 at 14:33):

Lean will search her notebook for you

view this post on Zulip Kenny Lau (Jul 31 2020 at 14:33):

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

view this post on Zulip Kenny Lau (Jul 31 2020 at 14:34):

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

view this post on Zulip Kenny Lau (Jul 31 2020 at 14:34):

so this theorem finset.prod_hom can be applied for beta being Z

view this post on Zulip 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?

view this post on Zulip Kenny Lau (Jul 31 2020 at 14:35):

exactly

view this post on Zulip Kenny Lau (Jul 31 2020 at 14:35):

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

view this post on Zulip 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?

view this post on Zulip Kenny Lau (Jul 31 2020 at 14:35):

which will be something like int.comm_monoid

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jul 31 2020 at 14:36):

read the error

view this post on Zulip 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...

view this post on Zulip Kenny Lau (Jul 31 2020 at 14:37):

why not prove it separately?

view this post on Zulip Kenny Lau (Jul 31 2020 at 14:37):

keep proofs short but many

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Jul 31 2020 at 14:40):

I guess it makes some sense

view this post on Zulip 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
-/

view this post on Zulip Kenny Lau (Jul 31 2020 at 14:44):

this is the best I can do @Marc Masdeu

view this post on Zulip Jalex Stark (Jul 31 2020 at 15:06):

you can get the instances as goals by using @

view this post on Zulip 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

view this post on Zulip Jalex Stark (Jul 31 2020 at 15:07):

so if you apply @prod_hom with appropriate underscores, the instances will appear as goals

view this post on Zulip 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...

view this post on Zulip Jalex Stark (Jul 31 2020 at 16:12):

better documentation and tutorialization is definitely a goal

view this post on Zulip Jalex Stark (Jul 31 2020 at 16:13):

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

view this post on Zulip Jalex Stark (Jul 31 2020 at 16:13):

#tpil chapter 10 is all about type classes

view this post on Zulip 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