any element with correct order generates a cyclic group

Stream: Is there code for X?

[Kenny Lau]

import Mathlib

notation3 "IsGenerator" ζ => Function.Surjective fun x : ℤ ↦ ζ ^ x

example {G : Type*} [Group G] [Finite G]
    (ζ : G) (hζ : orderOf ζ = Nat.card G) : IsGenerator ζ :=
  sorry

(Update: removed IsCyclic hypothesis)

[Kenny Lau]

proof:

import Mathlib

notation3 "IsGenerator" ζ => Function.Surjective fun x : ℤ ↦ ζ ^ x

example {G : Type*} [Group G] [Finite G] (ζ : G) (hζ : orderOf ζ = Nat.card G) : IsGenerator ζ := by
  unfold Function.Surjective
  simp_rw [← Subgroup.mem_zpowers_iff, ← Subgroup.eq_top_iff', ← Subgroup.card_eq_iff_eq_top,
    Nat.card_zpowers, hζ]

[Damiano Testa]

I thought that unfold Function.Surjective would have thrown an error and crashed your computer!

[Kenny Lau]

we should really look at these definitions that we have and fix them by adding the _def lemmas... It's a very very bad idea imo to rely on definitional unfolding!

[Johan Commelin]

It is not clear to me which definition you are complaining about.

[Kenny Lau]

/-- A function `f : α → β` is called surjective if every `b : β` is equal to `f a`
for some `a : α`. -/
@[expose]
def Surjective (f : α → β) : Prop :=
  ∀ b, Exists fun a => f a = b

[Kenny Lau]

here's a small script to print the 1693 definitions in Mathlib that are Prop-valued:

import Mathlib

def Test (f : Nat → Nat) : Prop := f 3 = 4

open Lean Elab Command
#eval show CommandElabM Unit from do
  let env ← getEnv
  for (name, val) in env.constants.toList do
    let .defnInfo val := val | continue
    let .regular _ := val.hints | continue
    let .safe := val.safety | continue
    if val.type.getForallBodyMaxDepth 100 == .sort 0 then
      logInfo name

[Andrew Yang]

try Function.Surjective.eq_def

[Johan Commelin]

Kenny Lau said:

we should really look at these definitions that we have and fix them by adding the _def lemmas... It's a very very bad idea imo to rely on definitional unfolding!

I think that relying on the defeq of Function.Surjective is not a problem. And very convenient!

[Kenny Lau]

that does work

[Kenny Lau]

@Johan Commelin yes, i'm saying that the lack of _def is the problem, not relying on defeq

[Kenny Lau]

anyway I'll stop here and make an RFC: #31745

[Kevin Buzzard]

I agree that not having surjective_def is a problem. When I'm doing live demos in front of undergraduates I usually choose a random thing to prove on the fly, sometimes asking the audience what mathematics they already know. Twice in October I spoke to undergraduates and in October the new ones don't know anything, except that most of them have heard of surjective, so I prove composite of two surjective functions is surjective (on the basis that it's a nice proof of something that everyone in the room understands) but I usually make a fool of myself trying to rw [surjective_def] and ultimately give up and just unfold Function.Surjective.

[Kenny Lau]

maybe this is an #xy problem, why does rw work with other definitions but not Function.Surjective?

@[expose]
def test : Nat → Nat := fun n ↦ 3

example : test 3 = 4 := by
  rw [test]

[Riccardo Brasca]

This work, doesn't it?

def test : Nat → Nat := fun n ↦ 3

example : Function.Surjective test := by
  rw [Function.Surjective]

[Kenny Lau]

why didn't it work in my code above?

[Riccardo Brasca]

Hmm, maybe I am confused, but rw [Surjective] in

def Surjective {α β : Type} (f : α → β) : Prop :=
  ∀ b, Exists fun a => f a = b

def test : Nat → Nat := fun n ↦ 3

example : Surjective test := by
  rw [Surjective]
  sorry

unfolds the definition as expected.

[Etienne Marion]

Kenny Lau said:

why didn't it work in my code above?

Are you referring to your first proof? This works in the web editor.

import Mathlib

notation3 "IsGenerator" ζ => Function.Surjective fun x : ℤ ↦ ζ ^ x

example {G : Type*} [Group G] [Finite G] (ζ : G) (hζ : orderOf ζ = Nat.card G) : IsGenerator ζ := by
  rw [Function.Surjective]
  simp_rw [← Subgroup.mem_zpowers_iff, ← Subgroup.eq_top_iff', ← Subgroup.card_eq_iff_eq_top,
    Nat.card_zpowers, hζ]

[Kenny Lau]

hmm, that's very strange, maybe I just spelt it wrong the first time :melt:

[Kenny Lau]

in which case I apologise for the noise

[Kevin Buzzard]

Oh rw [Surjective] works for my situation too (although it is a little counterintuitive).