Aks primality Theorem 6.1 Claim (i) proven

Stream: mathlib4

[metakuntyyy]

So I have tried my best to prove Claim 1 of Theorem 6.1 in https://www3.nd.edu/~andyp/notes/AKS.pdf

I assume I need to clean up the proof a bit

import Mathlib


/-- Theorem 6.1 Claim 1.(i) part 1 of https://www3.nd.edu/~andyp/notes/AKS.pdf -/
theorem aks_6d1c1ip1 (p r a:ℕ )[Fact p.Prime]
 (μ : primitiveRoots r (AlgebraicClosure (ZMod p)) ):
 ((μ:(AlgebraicClosure (ZMod p))) -a)^p = μ ^p-a := by
  let frob := by exact frobeniusEquiv (AlgebraicClosure (ZMod p)) p
  have hmnp : frob.toFun ((↑μ )) =  ((↑μ ^  p)) :=by rfl
  have hmna : frob.toFun (↑a) = (↑a)^p :=by rfl
  have fab := by exact frobenius_natCast (AlgebraicClosure (ZMod p)) p a
  have fab2 : (a^p)= (a:(AlgebraicClosure (ZMod p))) := by exact fab
  have hhh := by exact RingEquiv.map_sub frob (↑μ) ↑a
  have hhhh: frob.toFun (↑μ - ↑a) = frob.toFun (↑μ ) - frob.toFun ↑a := by exact hhh
  conv =>
    rhs
    rw[← fab2]
    rw[← hmna]
    rw[← hmnp]
    rw[← hhhh]
  rfl

/-- Theorem 6.1 Claim 1.(i) part 2 of https://www3.nd.edu/~andyp/notes/AKS.pdf -/
theorem aks_6d1c1ip2  (n p r a:ℕ )[Fact p.Prime] (hdivpn: p∣ n)
 (μ : primitiveRoots r (AlgebraicClosure (ZMod p)) )
 (hz: ((μ:(AlgebraicClosure (ZMod p))) -a)^n = μ ^n-a):
 ((μ:(AlgebraicClosure (ZMod p))) -a)^(n/p) = μ ^(n/p)-a  :=by
  have primegt0 : 0<p:=by exact Nat.pos_of_neZero p
  have sss : n=(n/p)*p := by exact (Nat.div_eq_iff_eq_mul_left primegt0 hdivpn).mp rfl
  rw[sss] at hz
  let frob := by exact frobeniusEquiv (AlgebraicClosure (ZMod p)) p
  have eqfrobinv := congrArg frob.invFun hz
  have ds : frob.invFun (frob.toFun μ) = frob.invFun (μ^p) := by rfl
  have funli := frob.left_inv μ
  have ch : μ = frob.invFun (μ^p) :=by exact id (Eq.symm funli)
  rw[pow_mul] at eqfrobinv
  rw[pow_mul] at eqfrobinv
  have mua := frob.left_inv (((μ:(AlgebraicClosure (ZMod p))) -a)^(n/p))
  have lele : frob.toFun ((↑μ - ↑a) ^ (n / p)) = ((↑μ - ↑a) ^ (n / p))^p := by rfl
  have mu := by exact id (Eq.symm mua)
  conv at mu =>
    rhs
    rhs
    rw[lele]
  rw[← mu] at eqfrobinv
  have frfun : frob.toFun ((↑μ ^ (n / p)) ^ p - ↑a) = frob.toFun ((↑μ ^ (n / p)) ^ p ) - frob.toFun ↑a :=by simp
  have frcfun := by exact congrArg frob.invFun frfun
  have ap: (a: (ZMod p))^p = a := by exact ZMod.pow_card _
  have fab := by exact frobenius_natCast (AlgebraicClosure (ZMod p)) p a
  have fab2 : (a^p)= (a:(AlgebraicClosure (ZMod p))) := by exact fab
  have hmnp : frob.toFun ((↑μ ^ (n / p))) =  ((↑μ ^ (n / p)))^p :=by rfl
  have hmna : frob.toFun (↑a) = (↑a)^p :=by rfl
  have hhh := by exact RingEquiv.map_sub frob (↑μ ^ (n / p)) ↑a
  have hhhh : frob.toFun ((↑μ ^ (n / p))-a)=frob.toFun (↑μ ^ (n / p)) - frob.toFun ↑a := by exact hhh
  conv at eqfrobinv =>
    rhs
    rhs
    rw[← fab2]
    rw[← hmnp]
    rw[← hmna]
    rw[← hhhh]
  have mumu := frob.left_inv  (↑μ ^ (n / p) - ↑a)
  rw[mumu] at eqfrobinv
  exact eqfrobinv

[metakuntyyy]

I had some trouble with tactics, I assume that this can be shortened and that it can be much smoother, I just don't know how... yet.

[metakuntyyy]

I have opened https://github.com/leanprover-community/mathlib4/pull/19526/files. How do I find out with stuff I need to import? Currently it's import Mathlib

[Kim Morrison]

#min_imports

[Kim Morrison]

You will need to rename the lemma

[Kim Morrison]

Please put spaces on both sides of all colons

[metakuntyyy]

What name of the lemma do you suggest?

[metakuntyyy]

I was thinking of prime_is_introspective_for_linear_factors

[metakuntyyy]

According to Definition 4.4 https://www.cse.iitk.ac.in/users/manindra/algebra/primality_v6.pdf

[Johan Commelin]

@metakuntyyy I am a bit confused by your lemma. Isn't it a very special case of

import Mathlib

lemma prime_is_introspective_for_linear_factors (p a : ℕ) [Fact p.Prime]
    (K : Type*) [Field K] [CharP K p]
    (μ : K) :
    ((μ : K) - a)^p = μ^p-a := by
  simp [← frobenius_def]

[metakuntyyy]

Indeed, I think you are right. Looking at https://www3.nd.edu/~andyp/notes/AKS.pdf it seems that both results are true in either a finite field or its algebraic closure. Here it appears to be almost definitionally equal to the Frobenius definition. But I think the second one is not correct with those hypotheses because of

  let frob := by exact frobeniusEquiv (AlgebraicClosure (ZMod p)) p

Basically I've tried to specialise the hypotheses to match the part of the theorem I've tried to prove verbatim, so that readers can follow the proof steps along.

Would pulling the variables out of the theorem help? There seem to be a lot of definitions in theorem 6.1
I was wondering about this hypothesis in Theorem 6.1

Let $\mu \in \bar{\mathbb{F}_p}$ be a primitive r-th root of unity.

[metakuntyyy]

I guess this is because the definition of a number and a polynomial to be introspective seems to be a local only definition specifically for the proof of the AKS algorithm. I couldn't find this condition elsewhere.

[Kim Morrison]

(Just noting that trying to write the proof so that it closely follows the paper is somewhat antithetical to PRing it to Mathlib. We'd prefer that things are done in generality, using reusable components, over allowing a reader to follow along from a paper.)

[metakuntyyy]

Ah I see. How do you feel about using private lemmas instead, for example for each of the claims? I'm quite sure that only the final result will be of relevance and any lemmas/claims in between will be "technical" noise.

I'm not sure how the lemmas can be generalised as they are a specialisation of other lemmas in mathlib for the purpose of this proof.

[Johan Commelin]

I think that is fine, at least during development. But probably during PR review you will be asked to either inline or unprivate those lemmas.

[metakuntyyy]

Alright, I'll try to get Claim 1 proven and its dependent definitions. Once I stumble upon some hurdles or need some help I'll post here. It might take me some time, or a lot of time.