Construction of an equivalence between primitive roots

Stream: mathlib4

[metakuntyyy]

I'm trying to prove that if e is coprime with r, then the e-th power is an bijection of primitive roots.

So far everything seems great-ish, I can't get rid of the casts though. I would like to have $a^{(b-c)} = a^b*a^{-c}$, but I can't get rid of the cast to K. If I try to use https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Group/Subgroup/Defs.html#Subgroup.coe_zpow, but I can't get convert the final equation into an equation where I have a group structure.

import Mathlib

theorem coprmGcd (x y :ℤ) (h: IsCoprime x y ): IsCoprime (x.gcdA y) y :=by
  rw[IsCoprime]
  rw[IsCoprime] at h
  have ⟨ a,b,hh⟩ :=h
  have g := Int.gcd_eq_gcd_ab x y
  have gg : ↑(x.gcd y) =1 :=by exact Int.isCoprime_iff_gcd_eq_one.mp h
  rw[gg] at g
  use x
  use x.gcdB y
  symm at g
  conv =>
    lhs
    rhs
    rw[mul_comm]
  exact g


def isomm {K:Type*}[Field K](e:ℕ) (r:ℕ) (h: e.Coprime r) (h2:0<r): (primitiveRoots r K) ≃ (primitiveRoots r K) :=by

  refine Equiv.mk ?_ ?_ ?_ ?_
  · intro ⟨ μ,q⟩
    rw[mem_primitiveRoots] at q
    refine Subtype.mk (μ^e) ?_
    rw[mem_primitiveRoots]
    · refine IsPrimitiveRoot.pow_of_coprime q ?_ ?_
      exact h
    repeat assumption
  · intro ⟨ μ,q⟩
    rw[mem_primitiveRoots] at q
    refine Subtype.mk (μ^(Nat.gcdA e r)) ?_
    rw[mem_primitiveRoots]
    · refine IsPrimitiveRoot.zpow_of_gcd_eq_one q ?_ ?_
      have coco:= coprmGcd e r (Nat.Coprime.isCoprime h)
      rw[← Int.isCoprime_iff_gcd_eq_one]
      exact coco
    repeat assumption

  have dl := Int.gcd_eq_gcd_ab e r
  have eq1 : 1 = ↑((e:ℤ).gcd ↑r) :=by exact Eq.symm (Tactic.NormNum.int_gcd_helper rfl rfl h)
  rw[← eq1] at dl
  have ringy : (e:ℤ) * ((e:ℤ).gcdA ↑r) = 1 - r* (e:ℤ).gcdB r :=by
    exact Eq.symm ((fun {b a c} ↦ Int.sub_eq_iff_eq_add.mpr) dl)
  have d : 0 ≠ r :=by exact Ne.symm (Nat.ne_zero_of_lt h2)
  have nz :NeZero r := NeZero.mk d.symm
  · rw[Function.LeftInverse]
    simp
    intro a ha
    have sss :(a ^ e) ^ e.gcdA r = (a ^ (e:ℤ)) ^ e.gcdA r :=by simp only [zpow_natCast]
    rw[sss]
    rw[← zpow_mul]
    have gcda: e.gcdA r = (e:ℤ).gcdA r :=by
      rfl
    rw[gcda]
    rw[ringy]
    rw[mem_primitiveRoots] at ha
    have dsj := IsPrimitiveRoot.toRootsOfUnity ha
    have fff := IsPrimitiveRoot.val_toRootsOfUnity_coe ha
    rw[← fff]
    have ddd : (ha.toRootsOfUnity :Kˣ)^((1 - (r:ℤ) * (e:ℤ).gcdB r) ) =(ha.toRootsOfUnity :Kˣ) :=by
      sorry
    have efe := congrArg (Units.coeHom K) ddd
    --have sc := Subgroup.coe_zpow (rootsOfUnity r K) ha.toRootsOfUnity 4
    sorry
    exact h2
  · rw[Function.RightInverse]
    rw[Function.LeftInverse]
    simp
    intro a ha
    sorry

[metakuntyyy]

All I want is to use this theorem https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Group/Basic.html#zpow_sub

[Kevin Buzzard]

Not an answer to your question, but your code would be much more readable if it looked like this:

def isomm {K : Type*} [Field K] (e : ℕ) (r : ℕ) (h : e.Coprime r) (h2 : 0 < r) :
    (primitiveRoots r K) ≃ (primitiveRoots r K) where
  toFun μh := ⟨μh.1 ^ e, sorry⟩
  invFun νh := ⟨νh.1 ^ (Nat.gcdA e r), sorry⟩
  left_inv := sorry
  right_inv := sorry

[metakuntyyy]

Fair enough, here is a more readable variant. The problem still stands. :anguish:

import Mathlib

theorem coprmGcd (x y :ℤ) (h: IsCoprime x y ): IsCoprime (x.gcdA y) y :=by
  rw[IsCoprime]
  rw[IsCoprime] at h
  have ⟨ a,b,hh⟩ :=h
  have g := Int.gcd_eq_gcd_ab x y
  have gg : ↑(x.gcd y) =1 :=by exact Int.isCoprime_iff_gcd_eq_one.mp h
  rw[gg] at g
  use x
  use x.gcdB y
  symm at g
  conv =>
    lhs
    rhs
    rw[mul_comm]
  exact g


def isomm2 {K : Type*} [Field K] (e : ℕ) (r : ℕ) (h : e.Coprime r) (h2 : 0 < r) :
    (primitiveRoots r K) ≃ (primitiveRoots r K) where
  toFun μh := ⟨μh.1 ^ e, by
    rw[mem_primitiveRoots]
    have primr :=μh.2
    rw[mem_primitiveRoots] at primr
    refine IsPrimitiveRoot.pow_of_coprime primr ?_ ?_
    exact h
    repeat assumption
    ⟩
  invFun νh := ⟨νh.1 ^ (Nat.gcdA e r), by
    rw[mem_primitiveRoots]
    have primr := νh.2
    rw[mem_primitiveRoots] at primr
    · refine IsPrimitiveRoot.zpow_of_gcd_eq_one primr ?_ ?_
      have coco:= coprmGcd e r (Nat.Coprime.isCoprime h)
      rw[← Int.isCoprime_iff_gcd_eq_one]
      exact coco
    repeat assumption⟩
  left_inv := by
    have dl := Int.gcd_eq_gcd_ab e r
    have eq1 : 1 = ↑((e:ℤ).gcd ↑r) :=by exact Eq.symm (Tactic.NormNum.int_gcd_helper rfl rfl h)
    rw[← eq1] at dl
    have ringy : (e:ℤ) * ((e:ℤ).gcdA ↑r) = 1 - r* (e:ℤ).gcdB r :=by
      exact Eq.symm ((fun {b a c} ↦ Int.sub_eq_iff_eq_add.mpr) dl)
    have d : 0 ≠ r :=by exact Ne.symm (Nat.ne_zero_of_lt h2)
    have nz :NeZero r := NeZero.mk d.symm
    rw[Function.LeftInverse]
    simp
    intro a ha
    have sss :(a ^ e) ^ e.gcdA r = (a ^ (e:ℤ)) ^ e.gcdA r :=by simp only [zpow_natCast]
    rw[sss]
    rw[← zpow_mul]
    have gcda: e.gcdA r = (e:ℤ).gcdA r :=by
      rfl
    rw[gcda]
    rw[ringy]
    rw[mem_primitiveRoots] at ha
    have dsj := IsPrimitiveRoot.toRootsOfUnity ha
    have fff := IsPrimitiveRoot.val_toRootsOfUnity_coe ha
    rw[← fff]
    have ddd : (ha.toRootsOfUnity :Kˣ)^((1 - (r:ℤ) * (e:ℤ).gcdB r) ) =(ha.toRootsOfUnity :Kˣ) :=by
      sorry
    have efe := congrArg (Units.coeHom K) ddd
    --have sc := Subgroup.coe_zpow (rootsOfUnity r K) ha.toRootsOfUnity 4
    have tete := zpow_sub (ha.toRootsOfUnity) 1 ( (r:ℤ) * (e:ℤ).gcdB r)
    sorry
    exact h2
  right_inv := by
    rw[Function.RightInverse]
    rw[Function.LeftInverse]
    simp
    intro a ha
    sorry

[metakuntyyy]

I'm stuck at the final sorry of left_inv.