Homomorphisms from Z to G

Stream: new members

[Stepan Nesterov]

Is this the accepted way to talk about group homomorphisms from Z to G?
theorem exercise2_3_19 (g : G) : ∃! φ : (Multiplicative ℤ) →* G, φ (Multiplicative.ofAdd 1) = g := by sorry
It works fine, but it's very confusing when something simps down to g ^ 1, where 1 : Multiplicative ℤ is Multiplicative.ofAdd 0. So I thought I'd ask if there is a better way.
Mathematically, I guess we usually talk about "heteromorphisms" $\varphi : \mathbb{Z} \to G$, $\varphi(x+y) = \varphi(x) \cdot \varphi(y)$.

[Aaron Liu]

docs#AddChar I think we had something like that

[Aaron Liu]

I think you will be better off working with Multiplicative Int though

[Aaron Liu]

How did you end up with g ^ (1 : Multiplicative Int)? Such a thing shouldn't be possible normally.

[Stepan Nesterov]

Aaron Liu said:

How did you end up with g ^ (1 : Multiplicative Int)? Such a thing shouldn't be possible normally.

Here's my proof

import Mathlib.GroupTheory.OrderOfElement
import Mathlib.Algebra.Group.Subgroup.Lattice
import Mathlib.Data.ZMod.Basic

variable (G : Type*) [Group G]

theorem exercise2_3_19 (g : G) : ∃! φ : (Multiplicative ℤ) →* G, φ (Multiplicative.ofAdd 1) = g := by
rw[ExistsUnique]
  use {
    toFun := fun N => g ^ (N.toAdd)
    map_one' := by
--This starts off with g ^ Multiplicative.toAdd 1 = 1
      dsimp
      exact zpow_zero g
    map_mul' := by
      intro m n
--This starts off with g ^ Multiplicative.toAdd (m * n) = g ^ Multiplicative.toAdd m * g ^ Multiplicative.toAdd n
      dsimp
      exact zpow_add g (Multiplicative.toAdd m) (Multiplicative.toAdd n)
  }
  dsimp
  constructor
  · exact zpow_one g
  · intro φ hφ
    rw[MonoidHom.ext_iff]
    intro n
    dsimp
--At this point I had to undo dsimp in a sense
    rw[show n = Multiplicative.ofAdd (n.toAdd) from rfl]
    set m := n.toAdd
    simp only [toAdd_ofAdd]
    nth_rewrite 1 [show m = m • 1 by exact Eq.symm (zsmul_int_one m)]
    rw[show Multiplicative.ofAdd (m • (1 : ℤ)) = (Multiplicative.ofAdd 1) ^ m from rfl]
    rw[map_zpow]
    rw[hφ]

[Aaron Liu]

can you give a #mwe

[Stepan Nesterov]

Well , 1 : Multiplicative Int was really part of my assumptions I guess.

Aaron Liu said:

How did you end up with g ^ (1 : Multiplicative Int)? Such a thing shouldn't be possible normally.

I actually can't tell what (1 : Multiplicative Int) is. Is it the unit of that group, (Multiplicative.ofAdd 0)? Or it is (Multiplicative.ofAdd 1)?

[Aaron Liu]

The point is that you're raising something to a Multiplicative Int power

[Aaron Liu]

that's not normal

[Stepan Nesterov]

But how else would I define a group hom that I want?

[Stepan Nesterov]

Stepan Nesterov said:

Well , 1 : Multiplicative Int was really part of my assumptions I guess.

Aaron Liu said:

How did you end up with g ^ (1 : Multiplicative Int)? Such a thing shouldn't be possible normally.

I actually can't tell what (1 : Multiplicative Int) is. Is it the unit of that group, (Multiplicative.ofAdd 0)? Or it is (Multiplicative.ofAdd 1)?

Upd: #eval (1 : Multiplicative ℤ) gives 0. Which I guess isn't the craziest thing Lean told me about math. Of course the 1 in this group is 0

[Aaron Liu]

After running in the web editor I don't think the problem that you claimed is happening is happening

[Aaron Liu]

So what's the problem that's happening?

[Stepan Nesterov]

Maybe I wasn't clear enough about what I'm asking, sorry.
There is no problem, the proof is fine.
It's just that the notation which flashes on screen is a bit confusing, so I wanted to check if if I did something wrong style-wise.

[Stepan Nesterov]

Aaron Liu said:

The point is that you're raising something to a Multiplicative Int power

Basically I'm raising g to an integer power but then changing n : Int to a defeq element in Multiplicative Int somewhere in the proof. Is this fine in terms of accepted Lean practices?

[Aaron Liu]

Well it's fine

[Aaron Liu]

I think I have a better way though

[Kevin Buzzard]

@Stepan Nesterov here's a golfed version:

import Mathlib.GroupTheory.OrderOfElement
import Mathlib.Algebra.Group.Subgroup.Lattice
import Mathlib.Data.ZMod.Basic

variable (G : Type*) [Group G]

theorem exercise2_3_19 (g : G) :
    ∃! φ : (Multiplicative ℤ) →* G, φ (Multiplicative.ofAdd 1) = g := by
  rw [ExistsUnique]
  use {
    toFun := fun N => g ^ N.toAdd -- no need for brackets
    map_one' := zpow_zero g -- exact works up to defeq, dsimp only changes thing up to defeq
    map_mul' m n := -- move inputs left of `:=`
      zpow_add g (Multiplicative.toAdd m) (Multiplicative.toAdd n)
  }
  refine ⟨zpow_one g, ?_⟩ -- never get two goals so don't need to indent
  intro φ hφ
  ext -- does all the mathematical content for you
  simp [hφ] -- does all the tidying up

[Kevin Buzzard]

Stepan Nesterov said:

Aaron Liu said:

The point is that you're raising something to a Multiplicative Int power

Basically I'm raising g to an integer power but then changing n : Int to a defeq element in Multiplicative Int somewhere in the proof. Is this fine in terms of accepted Lean practices?

I would say that it was not fine but I also don't see you doing this. Where exactly are you abusing defeq?