Subgroup of a subgroup should be a subgroup

Stream: new members

[Marc Masdeu]

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]

read the error

[Kenny Lau]

(two_torsion_subgroup G).to_group is the "proof" that two_torsion_subgroup G is a group

[Kenny Lau]

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

[Kenny Lau]

except that this won't typecheck as well

[Marc Masdeu]

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

[Kenny Lau]

because LHS is a subgroup of G while RHS is a subgroup of two_torsion_subgroup G

[Marc Masdeu]

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

[Kenny Lau]

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

[Kenny Lau]

then you can coerce it however you want

[Kenny Lau]

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

[Kenny Lau]

the sub-object API's need some work

[Kenny Lau]

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

[Marc Masdeu]

What is this good for?

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

[Kenny Lau]

this allows you to treat two_torsion_subgroup G as a type

[Kenny Lau]

instead of just a subgroup of G

[Marc Masdeu]

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]

(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]

you don't use has_coe_to_sort

[Kenny Lau]

again, the correct term is two_torsion_subgroup (two_torsion_subgroup G)

[Kenny Lau]

where the inner two_torsion_subgroup G has been coerced to a type by the instance you posted

[Kenny Lau]

before that, two_torsion_subgroup G is just a subgroup of G

[Kenny Lau]

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]

only types can be groups

[Kenny Lau]

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]

which allows you to write things like 1 : X

[Marc Masdeu]

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

[Marc Masdeu]

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

[Kenny Lau]

subgroup G is the type of subgroups of G

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

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]

so now subgroup S makes sense

[Kenny Lau]

and U : subgroup S means "U is a subgroup of the result of the coercion of S into a type"

[Kenny Lau]

note that (coerced) S and G are incomparable types

[Kenny Lau]

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

[Kenny Lau]

in Lean all distinct types are incomparable

[Marc Masdeu]

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]

so in practice you should treat S as another group isomorphic to the subgroup of G also called S

[Kenny Lau]

here's how the type coercion works

[Kenny Lau]

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]

the little up-arrow is a "hidden function"

[Kenny Lau]

because, again, types in Lean are incomparable

[Kenny Lau]

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]

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

[Kenny Lau]

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

[Marc Masdeu]

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

[Kenny Lau]

similarly, subgroup S and subgroup G are incomparable types

[Kenny Lau]

you cannot ever state that their terms are equal

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

for no other reason than itself

[Kenny Lau]

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

[Kenny Lau]

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]

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]

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]

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

[Kenny Lau]

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

[Kenny Lau]

this theorem is called subtype.eq

[Marc Masdeu]

Wow thanks! This is so helpful!

[Kenny Lau]

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]

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

[Kenny Lau]

but actually typing out the arrow sometimes causes errors

[Kenny Lau]

so don't type out the arrow

[Kenny Lau]

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

[Kenny Lau]

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]

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

[Mario Carneiro]

good job kenny

[Kenny Lau]

thanks

[Kenny Lau]

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

[Marc Masdeu]

You guys are great

[Marc Masdeu]

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]

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

[Kenny Lau]

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]

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

[Kenny Lau]

we use at most an uparrow

[Marc Masdeu]

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

[Marc Masdeu]

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]

the error says failed to synthesize instance

[Kenny Lau]

the typeclass system is like Lean's notebook

[Kenny Lau]

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

[Kenny Lau]

this is called the type-class system

[Kenny Lau]

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

[Marc Masdeu]

Instance means "example of"?

[Kenny Lau]

no

[Kenny Lau]

instance just means something to mark down in her notebook

[Kevin Buzzard]

It means definition in the notebook

[Kenny Lau]

e.g. the group structure on a type

[Kenny Lau]

the fact that a specific function is a homomorphism

[Kenny Lau]

etc

[Marc Masdeu]

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

[Kenny Lau]

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]

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

[Kenny Lau]

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

[Marc Masdeu]

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

[Kenny Lau]

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

[Kenny Lau]

Lean will search her notebook for you

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Marc Masdeu]

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]

exactly

[Kenny Lau]

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

[Marc Masdeu]

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]

which will be something like int.comm_monoid

[Kenny Lau]

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]

read the error

[Marc Masdeu]

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]

why not prove it separately?

[Kenny Lau]

keep proofs short but many

[Marc Masdeu]

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]

I guess it makes some sense

[Kenny Lau]

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]

this is the best I can do @Marc Masdeu

[Jalex Stark]

you can get the instances as goals by using @

[Jalex Stark]

if you look at the type of @prod_hom, you'll see that it has explicit arguments for the typeclass instances

[Jalex Stark]

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

[Marc Masdeu]

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

[Jalex Stark]

better documentation and tutorialization is definitely a goal

[Jalex Stark]

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

[Jalex Stark]

#tpil chapter 10 is all about type classes

[Jalex Stark]

type classes probably get a more gentle introduction in #mil