Zulip Chat Archive

Stream: new members

Topic: defining power on groups


view this post on Zulip Jason KY. (Feb 26 2020 at 16:05):

Hi! I am trying to experiment a bit with groups and I am a bit confused about the following,

I have defined my powers as

-- definition of powers
@[simp] def group_pow_nat {G : Type} [group G] : G    G
| g 0 := 1
| g (n + 1) := group_pow_nat g n * g
instance group_has_pow_nat {G : Type} [group G] : has_pow G  := group_pow_nat

@[simp] def group_pow {G : Type} [group G] : G    G
| g (int.of_nat 0) := 1
| g (int.of_nat n) := group_pow_nat g n
| g -[1+ n] := group_pow_nat g⁻¹ (n + 1)
instance group_has_pow {G : Type} [group G] : has_pow G  := group_pow

Which seems to work as I want it to. So my question is how should I show the following

lemma pow_int_of_nat {g : G} {n : } : g ^ (int.of_nat n) = group_pow_nat g n := sorry

I thought rflwould work however it seems that is not the case.
Thanks in advance!

view this post on Zulip Jason KY. (Feb 26 2020 at 16:07):

Btw I am using this definition as groups

class has_group_notation (G : Type) extends has_mul G, has_one G, has_inv G

-- definition of the group structure
class group (G : Type) extends has_group_notation G :=
(mul_assoc :  (a b c : G), a * b * c = a * (b * c))
(one_mul :  (a : G), 1 * a = a)
(mul_left_inv :  (a : G), a⁻¹ * a = 1)

view this post on Zulip Reid Barton (Feb 26 2020 at 16:07):

You would at least need a pattern match on n into 0 and other because there is one in the definition of group_pow. But then the pattern match there is quite unnecessary, isn't it?

view this post on Zulip Reid Barton (Feb 26 2020 at 16:07):

i.e. just delete the first line of the definition of group_pow, and it looks okay

view this post on Zulip Jason KY. (Feb 26 2020 at 16:08):

Wow! That worked perfectly! Thanks

view this post on Zulip Jason KY. (Feb 27 2020 at 20:01):

Hi again!
Is there an easy way of solving this?

example (n : ) : -[1+ n] + 1 = -[1+ (n - 1)] := sorry

view this post on Zulip Reid Barton (Feb 27 2020 at 20:08):

Well, it's not true

view this post on Zulip Reid Barton (Feb 27 2020 at 20:08):

is it?

view this post on Zulip Patrick Massot (Feb 27 2020 at 20:08):

Wrong for n=0

view this post on Zulip Jason KY. (Feb 27 2020 at 20:12):

Oh! Right

view this post on Zulip Scott Morrison (Feb 27 2020 at 20:48):

What happened to that automatic counter-example finder?

view this post on Zulip Alex J. Best (Feb 27 2020 at 20:53):

https://github.com/cipher1024/slim_check or https://gitlab.binets.fr/pablo.le-henaff/nunchaku-lean ?

view this post on Zulip Scott Morrison (Feb 27 2020 at 21:10):

But if @Simon Hudon wants to PR slim_check to mathlib I'd use it. :-)

view this post on Zulip Simon Hudon (Feb 27 2020 at 21:12):

It's planned. I should have time to put on mathlib in a few weeks, I can do it then

view this post on Zulip Jason KY. (Mar 05 2020 at 19:19):

I am trying to define normal and central subgroups for a bundled subgroup and I am wondering whats the best way of doing it.
Is it better to define it as a class or should it be a prop?

This is how I've done it for now:

def center (G : Type) [group G] := {g : G |  k : G, k * g = g * k}

class central_subgroup (K : subgroup G) :=
(center :  k  K, k  mygroup.center G)

view this post on Zulip Kevin Buzzard (Mar 05 2020 at 19:21):

If you're bundling subgroups then center G should have type subgroup G rather than set G

view this post on Zulip Kevin Buzzard (Mar 05 2020 at 19:22):

But I don't know whether central_subgroup should be a predicate is_central or a class or another structure

view this post on Zulip Reid Barton (Mar 05 2020 at 21:55):

Class versus not depends on whether you want to use type class inference. I wouldn't want to use it here, but tastes differ.

view this post on Zulip Reid Barton (Mar 05 2020 at 21:56):

Structure versus just making a def that's a Prop doesn't make a big difference, you can think of the structure as introducing a little bit of abstraction

view this post on Zulip Reid Barton (Mar 05 2020 at 21:57):

The structure is pretty much a slightly more heavyweight way to do the same thing

view this post on Zulip Reid Barton (Mar 05 2020 at 21:57):

Note if you have a class/structure it will never be inferred as a Prop, so you would definitely want to add that

view this post on Zulip Reid Barton (Mar 05 2020 at 21:57):

I would tend to call it is_central

view this post on Zulip Jason KY. (Mar 05 2020 at 22:00):

Alright! I will make it a prop then, it'll be easier to work with! :)

view this post on Zulip Reid Barton (Mar 05 2020 at 22:05):

For normal subgroups there might be a specific reason to use a class, namely so that you can make the quotient a group. But another way to handle it is to bundle the subgroup + proof that it's normal and define the quotient by that.


Last updated: May 12 2021 at 22:15 UTC