How to define the order of an element for non-finite groups?

Stream: new members

[Ariel Fridman]

I am learning how to use lean 3 by solving Dummit & Foote's Abstract Algebra.
I am also not using mathlib's group or group_theory modules, since I want to do everything myself (C will do that to ya ^^').
In D&F, the order of an element g is defined as the smallest natural number n for which g^n = 1, or \infty if such a number doesn't exist.
I've looked at the mathlib implementation, and it looks like the order there is defined only for finite groups, which is unsuitable for my needs.

Any tips about how would one go about implementing an order function that does what I need?

[Johan Commelin]

Yes, this ought to be refactored in mathlib

[Kevin Buzzard]

I think that a better definition would be that the "order" of an element of infinite order should be 0.

[Kevin Buzzard]

Then the natural map from the integers to G sending 1 to g has kernel principal generated by order g.

[Johan Commelin]

open_locale classical

noncomputable def order_of' {G : Type*} [group G] (g : G) : ℕ :=
if h : ∃ n : ℕ, 0 < n ∧ g ^ n = 1 then nat.find h else 0

[Johan Commelin]

We just need someone with the time and energy to rewrite that part of mathlib

[Yakov Pechersky]

Is it possible to case on fintype or not?

[Ariel Fridman]

Thank you!

Just to see that I understand how this works:
It tries to check if there exists an n: N which is the order of g, and finds it, or otherwise returns zero.

But how does it know if a proof of that exists (aka, h exists)? Does it make me provide a proof of that when I try t assert that the order of g is 5 (for example)?

[Kevin Buzzard]

Twitter rant : https://twitter.com/XenaProject/status/1301802013278318593?s=20

Here's a funny thing. The set** of ideals of the integers is canonically isomorphic to the natural numbers {0, 1, 2...}. Ideals have a multiplication and it agrees with natural number multiplicatuon. Ideals also have an addition -- and it doesn't! Can we use this? ** Type 1/n

- The Xena Project (@XenaProject)

[Kevin Buzzard]

You shouldn't worry about the definition, because as well as the definition you need an API for the definition -- that would be part of the refactoring.

[Kevin Buzzard]

For example if G was a finite group then Lean would know that some n existed (e.g. the order of G)

[Johan Commelin]

@Ariel Fridman If you want to prove order_of' g = 5 you will need to show that g ^ 5 = 1 and you will need to show that g ^ 1 ... g ^ 4 are not 1.

[Johan Commelin]

Of course there is redundance there, so you will want helper lemmas that make your life easier.

[Johan Commelin]

E.g., a lemma that says that order_of' g = n iff g ^ n = 1 and g ^ k \ne 1 for all proper divisors k of n.

[Ariel Fridman]

@Johan Commelin I see. Thanks!

[Kevin Buzzard]

Note that that statement, once corrected to "all proper divisosrs k of n", remains true for n=0 with my convention ;-)

[Ariel Fridman]

I am probably dense, because I can't seem to be able to prove even simple statements using this definition ^^'.

What I am trying to prove:

noncomputable def order_of' {G : Type*} [group G] (g : G) : ℕ :=
  if h : ∃ n : ℕ, 0 < n ∧ g ^ n = 1 then nat.find h else 0

notation `|` g `|` := order_of' g

example {G: Type*} [group G] (g: G) : g = 1 → |g| = 1 := sorry

I tried providing a term of type ∃ n : ℕ , 0 < n ∧ g^n = 1, which was quite easy to prove, but that wasn't it.
Could you please explain what exactly an I supposed to provide/prove, or at least point me in the direction of some docs in which its explained?

[Ariel Fridman]

and if possible, the same for the other direction (i.e. |g| = 1 → g = 1), since I also haven't been able to see on how to case on it, or desugar it.

[Yakov Pechersky]

What are your imports?

[Shing Tak Lam]

import algebra.group.basic
import data.nat.enat
import tactic.interval_cases

variables {G : Type*} [group G]

open_locale classical

noncomputable def order_of' {G : Type*} [group G] (g : G) : ℕ :=
  if h : ∃ n : ℕ, 0 < n ∧ g ^ n = 1 then nat.find h else 0

notation `|` g `|` := order_of' g

example (g : G) : |(1 : G)| = 1 :=
begin
  unfold order_of',
  have h : ∃ n, 0 < n ∧ (1 : G) ^ n = 1,
  { use [1, zero_lt_one, one_pow _] },
  rw dif_pos h,
  rw nat.find_eq_iff,
  split,
  { simp },
  { intros n hn hc,
    cases hc with h1 h2,
    interval_cases n }
end

example (g : G) (hg : |g| = 1) : g = 1 :=
begin
  unfold order_of' at hg,
  split_ifs at hg,
  { have := nat.find_spec h,
    cases this with h1 h2,
    rwa [hg, pow_one] at h2 },
  { contradiction }
end

(obviously can be golfed)

[Ariel Fridman]

Yakov Pechersky said:

What are your imports?

just tactic and init.data.int. I don't actually use group, but rather a typeclass I made myself called Group.

[Ariel Fridman]

@Shing Tak Lam Thank you!, I'll look at it and try to understand what you're doing.

[Johan Commelin]

@Ariel Fridman The definition uses nat.find, so you will have to use lemmas about nat.find.

[Johan Commelin]

If you Ctrl-click on it (assuming you are using VScode as editor), then you will go to the definition.

[Johan Commelin]

Just below it will be 10 useful lemmas for using it

[Bryan Gin-ge Chen]

Note that you usually don't have to import anything that starts with init, all of that comes "for free" in every Lean file, unless you put prelude at the top of your file. If you do happen to have prelude at the top of your file, you would have gotten everything in init by importing tactic.

[Ariel Fridman]

@Johan Commelin I'll take a look at it, thanks!

[Ariel Fridman]

@Bryan Gin-ge Chen and thank you for this tip. so init just an autoinclude prelude? I assumed it was part of mathlib, but I guess I was wrong.

[Bryan Gin-ge Chen]

Yep, everything in init. is part of what we call "core Lean", and can be found in the community Lean 3 repository here.