Hypotheses on a group

Stream: new members

[Joey Lupo]

What is the canonical way to say "Let G be a finite, cyclic group of order q with generator g"? Right now I have

variables (G : Type) [group G] [is_cyclic G] [fintype G]

but I'm not sure how to get a hold of variables q or gfor the rest of the file and not have to unpack the definition of G in every proof.

[Yakov Pechersky]

That's good, now do

obtain ⟨g, hg⟩ := is_cyclic.exists_generator

or something akin to it

[Kevin Buzzard]

you could just add variables (q : nat) (hGq : fintype.card G = q)

[Eric Wieser]

Or even something silly like local notation `q` := fintype.card

[Yakov Pechersky]

There is docs#order_eq_card_gpowers

[Yakov Pechersky]

Seemingly missing an [is_cyclic G] subgroup.gpowers g = \top lemma.

[Yakov Pechersky]

There is the inverse, in docs#is_cyclic_of_order_of_eq_card

[Joey Lupo]

Okay, thank you for the help. Right now I have

variables {G : Type} [fintype G] [group G] [is_cyclic G]
variables (g : G) (hGg : ∀ (x : G), x ∈ subgroup.gpowers g)
variables (q : ℕ) (q_pos : 0 < q) (hGq : fintype.card G = q)

I guess my question now is the [is_cyclic G] seems redundant given that I manually defined the equivalent hGg, i.e. I'm not really taking advantage of the typeclass system by doing this. I am not exactly sure how to use the is_cyclic.exists_generator G proposition to get a hold of the particular g since the obtain tactic isn't working in this scope.

[Mario Carneiro]

If a typeclass argument is implied by a hypothesis, you should remove the typeclass argument only if it isn't used in the statement of the lemma

[Joey Lupo]

Yea, I guess my point was it seems (to me) like it would be better practice (or cleaner at least) to use the typeclass and then get the g from the is_cyclic rather than just manually writing the definition.

[Mario Carneiro]

It seems like you want g to be fixed, though?

[Mario Carneiro]

is_cyclic says only that there exists a generator, so there is no g to refer to

[Mario Carneiro]

If g doesn't appear in the statement of the lemma though, then you should just use obtain ⟨g, hg⟩ := is_cyclic.exists_generator G at the start of the proof

[Mario Carneiro]

it might help to give a #mwe

[Joey Lupo]

Interesting, wouldn't the "there exists" imply we should be able to say okay, call the thing that exists "g"?

[Yakov Pechersky]

That's precisely what obtain does.

[Mario Carneiro]

Joey Lupo said:

Interesting, wouldn't the "there exists" imply we should be able to say okay, call the thing that exists "g"?

Yes, but you can't refer to g outside the scope of that part of the proof, so in particular it can't appear in the theorem statement

[Joey Lupo]

btw, I don't have a MWE yet so sorry about that. I am basically trying to write these hypotheses at the beginning of the file so as to say, "for the rest of this file, let G be a finite, cyclic group with order q and generator g"

[Mario Carneiro]

That's just what you wrote, except you don't need [is_cyclic G]

[Mario Carneiro]

you don't need (q_pos : 0 < q), that's implied by the fact that q is the cardinality of a group

[Mario Carneiro]

But if the theorems you want to state don't use q and/or g in them, it will be more convenient for users of your theorem to have the [is_cyclic G] assumption instead of q and g

[Mario Carneiro]

but they are equivalent, since users can always use obtain ⟨g, hg⟩ := is_cyclic.exists_generator G before applying your lemma

[Joey Lupo]

Okay, then I think I have something that works for my purpose. But to push the point a little further- how come I was able to use fintype in the hypothesis of q, but can't use is_cyclic in the hypothesis of g? Does that just come down to the typeclass code not including that functionality?
Also, Yakor, I wasn't able to get this basic line to work

 variables {G : Type} [fintype G] [group G] [is_cyclic G]
obtain ⟨g, hg⟩ := is_cyclic.exists_generator G

[Joey Lupo]

Yea I guess the obtain should be in the context of a proof

[Mario Carneiro]

obtain is a tactic, it is supposed to go in a proof

[Mario Carneiro]

the things that appear at the top level are things like theorem, lemma, def, variable (aka "commands")

[Mario Carneiro]

how come I was able to use fintype in the hypothesis of q, but can't use is_cyclic in the hypothesis of g? Does that just come down to the typeclass code not including that functionality?

I don't understand what you mean by this. For fintype.card G to be well formed, fintype G has to be a previous typeclass argument

[Mario Carneiro]

Nothing in your variables similarly needs is_cyclic G for well formedness, so it can be safely removed

[Mario Carneiro]

you might need it for the lemmas though, you haven't shown any theorem statements yet

[Joey Lupo]

Yes, I understand that I can remove is_cyclic.

What I mean is that it would be nice to be able to use the is_cyclic typeclass to get a hypothesis on a g defined at the top-level in the same way that I use the fintype typeclass to get a hypothesis on a q defined at the top-level.

[Mario Carneiro]

If g is a random element and is_cyclic G, that doesn't say anything about whether g is a cyclic generator

[Mario Carneiro]

is_cyclic is a property of the whole group, not any particular element

[Mario Carneiro]

What you would need is some kind of is_cyclic_generator g class or hypothesis, defined to be ∀ (x : G), x ∈ subgroup.gpowers g. So far, this has not been useful enough to need

[Joey Lupo]

I guess I was envisioning something along the lines of

variables (G : Type) [group G] [is_cyclic G]
                    (g : G) (hG : g = G.generator)

[Mario Carneiro]

G.generator is not a function

[Mario Carneiro]

If a group is cyclic, there is not necessarily any distinguished generator

[Mario Carneiro]

and is_cyclic is defined using an existential so you can't extract a particular witness from it

[Mario Carneiro]

By contrast, when fintype G, there is a unique number q which is the cardinality of G, which is why the fintype.card function can exist

[Mario Carneiro]

if a finite group could have multiple witnesses to finiteness then that function wouldn't exist

[Mario Carneiro]

So if you want to refer to a particular generator, you have to explicitly unpack it into the two assumptions "g is an element of G" and "g is a cyclic generator of G"

[Mario Carneiro]

and the conjunction of these two is stronger than the original is_cyclic G assumption

[Joey Lupo]

Interesting. I agree that equals was not the right idea. So are you arguing in the last two lines that having something like

variables (G : Type) [group G] [is_cyclic G]
                    (g : G) (hG : G.generator g)

where hG is equivalent to (hGg : ∀ (x : G), x ∈ subgroup.gpowers g) should be outside the scope of the is_cyclictypeclass functionality?

[Yakov Pechersky]

If you have [is_cyclic G], then (hG : G.generator g) is true for any g : G, so you don't need that hypothesis. Do you have an example of a theorem statement you want to make regarding such gs?

[Mario Carneiro]

Yakov Pechersky said:

If you have [is_cyclic G], then (hG : G.generator g) is true for any g : G, so you don't need that hypothesis. Do you have an example of a theorem statement you want to make regarding such gs?

Not every element of a cyclic group is a generator. The identity almost never is

[Yakov Pechersky]

Ah yes, apologies.