PrimitiveRootCoordinates.lean

def primitiveRootCoordinate {n : ℕ} {ζ : Ωˣ}
    (hζ : IsPrimitiveRoot ζ n) (a : ZMod n) : Ωˣ

theorem primitiveRootCoordinate_injective {n : ℕ} {ζ : Ωˣ}
    (hζ : IsPrimitiveRoot ζ n) :
    Function.Injective (primitiveRootCoordinate hζ)

theorem primitiveRootCoordinate_natCast {n : ℕ} {ζ : Ωˣ}
    (hζ : IsPrimitiveRoot ζ n) (a : ℕ) :
    primitiveRootCoordinate hζ (a : ZMod n) = ζ ^ a

theorem primitiveRootCoordinate_eq_pow_val {n : ℕ} [NeZero n] {ζ : Ωˣ}
    (hζ : IsPrimitiveRoot ζ n) (a : ZMod n) :
    primitiveRootCoordinate hζ a = ζ ^ a.val

theorem primitiveRootCoordinate_add {n : ℕ} {ζ : Ωˣ}
    (hζ : IsPrimitiveRoot ζ n) (a b : ZMod n) :
    primitiveRootCoordinate hζ (a + b) =
      primitiveRootCoordinate hζ a * primitiveRootCoordinate hζ b

theorem primitiveRootCoordinate_pow_eq_one {n : ℕ} {ζ : Ωˣ}
    (hζ : IsPrimitiveRoot ζ n) (a : ZMod n) :
    primitiveRootCoordinate hζ a ^ n = 1

theorem primitiveRootCoordinate_surjective_roots {n : ℕ} [NeZero n] {ζ : Ωˣ}
    (hζ : IsPrimitiveRoot ζ n) (z : Ωˣ) (hz : z ^ n = 1) :
    ∃ a : ZMod n, primitiveRootCoordinate hζ a = z

theorem primitiveRootCoordinate_reduction
    (N n m : ℕ) [NeZero N] [NeZero n] (hN : N = n * m) {ζ : Ωˣ}
    (hζ : IsPrimitiveRoot ζ N) (a : ZMod N) :
    primitiveRootCoordinate hζ a ^ m =
      primitiveRootCoordinate (hζ.pow (Nat.pos_of_neZero N) (hN.trans (Nat.mul_comm n m)))
        (ZMod.castHom (by rw [hN]; exact dvd_mul_right n m) (ZMod n) a) := by
  have hcast : ZMod.castHom (by rw [hN]; exact dvd_mul_right n m) (ZMod n) a =
      (a.val : ZMod n) := by
    conv_lhs => rw [← ZMod.natCast_zmod_val a]
    rw [map_natCast]
  rw [hcast, primitiveRootCoordinate_eq_pow_val, primitiveRootCoordinate_natCast,
    pow_right_comm]

theorem primitiveRootCoordinate_cyclotomic
    (p : ℕ) [Fact p.Prime]
    [∀ i : ℕ, HasEnoughRootsOfUnity Ω (p ^ i)]
    (n : ℕ) {ζ : Ωˣ} (hζ : IsPrimitiveRoot ζ (p ^ n))
    (g : Ω ≃+* Ω) (a : ZMod (p ^ n)) :
    Units.map g.toMonoidHom (primitiveRootCoordinate hζ a) =
      primitiveRootCoordinate hζ
        ((cyclotomicCharacter Ω p g : PadicInt p).toZModPow n * a)