[GOAL]
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
⊢ charpoly (M ^ Fintype.card K) = charpoly M
[PROOFSTEP]
cases (isEmpty_or_nonempty n).symm
[GOAL]
case inl
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
⊢ charpoly (M ^ Fintype.card K) = charpoly M
[PROOFSTEP]
cases' CharP.exists K with p hp
[GOAL]
case inl.intro
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp : CharP K p
⊢ charpoly (M ^ Fintype.card K) = charpoly M
[PROOFSTEP]
letI := hp
[GOAL]
case inl.intro
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp : CharP K p
this : CharP K p := hp
⊢ charpoly (M ^ Fintype.card K) = charpoly M
[PROOFSTEP]
rcases FiniteField.card K p with ⟨⟨k, kpos⟩, ⟨hp, hk⟩⟩
[GOAL]
case inl.intro.intro.mk.intro
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ ↑{ val := k, property := kpos }
⊢ charpoly (M ^ Fintype.card K) = charpoly M
[PROOFSTEP]
haveI : Fact p.Prime := ⟨hp⟩
[GOAL]
case inl.intro.intro.mk.intro
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ ↑{ val := k, property := kpos }
this : Fact (Nat.Prime p)
⊢ charpoly (M ^ Fintype.card K) = charpoly M
[PROOFSTEP]
dsimp at hk 
[GOAL]
case inl.intro.intro.mk.intro
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ charpoly (M ^ Fintype.card K) = charpoly M
[PROOFSTEP]
rw [hk]
[GOAL]
case inl.intro.intro.mk.intro
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ charpoly (M ^ p ^ k) = charpoly M
[PROOFSTEP]
apply (frobenius_inj K[X] p).iterate k
[GOAL]
case inl.intro.intro.mk.intro.a
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ (↑(frobenius K[X] p))^[k] (charpoly (M ^ p ^ k)) = (↑(frobenius K[X] p))^[k] (charpoly M)
[PROOFSTEP]
repeat' rw [iterate_frobenius (R := K[X])]; rw [← hk]
[GOAL]
case inl.intro.intro.mk.intro.a
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ (↑(frobenius K[X] p))^[k] (charpoly (M ^ p ^ k)) = (↑(frobenius K[X] p))^[k] (charpoly M)
[PROOFSTEP]
rw [iterate_frobenius (R := K[X])]
[GOAL]
case inl.intro.intro.mk.intro.a
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ charpoly (M ^ p ^ k) ^ p ^ k = (↑(frobenius K[X] p))^[k] (charpoly M)
[PROOFSTEP]
rw [← hk]
[GOAL]
case inl.intro.intro.mk.intro.a
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ charpoly (M ^ Fintype.card K) ^ Fintype.card K = (↑(frobenius K[X] p))^[k] (charpoly M)
[PROOFSTEP]
rw [iterate_frobenius (R := K[X])]
[GOAL]
case inl.intro.intro.mk.intro.a
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ charpoly (M ^ Fintype.card K) ^ Fintype.card K = charpoly M ^ p ^ k
[PROOFSTEP]
rw [← hk]
[GOAL]
case inl.intro.intro.mk.intro.a
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ charpoly (M ^ Fintype.card K) ^ Fintype.card K = charpoly M ^ Fintype.card K
[PROOFSTEP]
rw [iterate_frobenius (R := K[X])]
[GOAL]
case inl.intro.intro.mk.intro.a
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ charpoly (M ^ Fintype.card K) ^ Fintype.card K = charpoly M ^ Fintype.card K
[PROOFSTEP]
rw [← FiniteField.expand_card]
[GOAL]
case inl.intro.intro.mk.intro.a
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ ↑(expand K (Fintype.card K)) (charpoly (M ^ Fintype.card K)) = charpoly M ^ Fintype.card K
[PROOFSTEP]
unfold charpoly
[GOAL]
case inl.intro.intro.mk.intro.a
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ ↑(expand K (Fintype.card K)) (det (charmatrix (M ^ Fintype.card K))) = det (charmatrix M) ^ Fintype.card K
[PROOFSTEP]
rw [AlgHom.map_det, ← coe_detMonoidHom, ← (detMonoidHom : Matrix n n K[X] →* K[X]).map_pow]
[GOAL]
case inl.intro.intro.mk.intro.a
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ ↑detMonoidHom (↑(AlgHom.mapMatrix (expand K (Fintype.card K))) (charmatrix (M ^ Fintype.card K))) =
    ↑detMonoidHom (charmatrix M ^ Fintype.card K)
[PROOFSTEP]
apply congr_arg det
[GOAL]
case inl.intro.intro.mk.intro.a
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ ↑(AlgHom.mapMatrix (expand K (Fintype.card K))) (charmatrix (M ^ Fintype.card K)) = charmatrix M ^ Fintype.card K
[PROOFSTEP]
refine' matPolyEquiv.injective _
[GOAL]
case inl.intro.intro.mk.intro.a
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ ↑matPolyEquiv (↑(AlgHom.mapMatrix (expand K (Fintype.card K))) (charmatrix (M ^ Fintype.card K))) =
    ↑matPolyEquiv (charmatrix M ^ Fintype.card K)
[PROOFSTEP]
rw [AlgEquiv.map_pow, matPolyEquiv_charmatrix, hk, sub_pow_char_pow_of_commute, ← C_pow]
[GOAL]
case inl.intro.intro.mk.intro.a
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ ↑matPolyEquiv (↑(AlgHom.mapMatrix (expand K (p ^ k))) (charmatrix (M ^ p ^ k))) = X ^ p ^ k - ↑C (M ^ p ^ k)
[PROOFSTEP]
exact (id (matPolyEquiv_eq_x_pow_sub_c (p ^ k) M) : _)
[GOAL]
case inl.intro.intro.mk.intro.a.h
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ Commute X (↑C M)
[PROOFSTEP]
exact (C M).commute_X
[GOAL]
case inr
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : IsEmpty n
⊢ charpoly (M ^ Fintype.card K) = charpoly M
[PROOFSTEP]
exact congr_arg _ (Subsingleton.elim _ _)
[GOAL]
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
p : ℕ
inst✝ : Fact (Nat.Prime p)
M : Matrix n n (ZMod p)
⊢ charpoly (M ^ p) = charpoly M
[PROOFSTEP]
have h := FiniteField.Matrix.charpoly_pow_card M
[GOAL]
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
p : ℕ
inst✝ : Fact (Nat.Prime p)
M : Matrix n n (ZMod p)
h : charpoly (M ^ Fintype.card (ZMod p)) = charpoly M
⊢ charpoly (M ^ p) = charpoly M
[PROOFSTEP]
rwa [ZMod.card] at h 
[GOAL]
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
⊢ trace (M ^ Fintype.card K) = trace M ^ Fintype.card K
[PROOFSTEP]
cases isEmpty_or_nonempty n
[GOAL]
case inl
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : IsEmpty n
⊢ trace (M ^ Fintype.card K) = trace M ^ Fintype.card K
[PROOFSTEP]
simp [Matrix.trace]
[GOAL]
case inl
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : IsEmpty n
⊢ 0 = 0 ^ Fintype.card K
[PROOFSTEP]
rw [zero_pow Fintype.card_pos]
[GOAL]
case inr
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
⊢ trace (M ^ Fintype.card K) = trace M ^ Fintype.card K
[PROOFSTEP]
rw [Matrix.trace_eq_neg_charpoly_coeff, Matrix.trace_eq_neg_charpoly_coeff, FiniteField.Matrix.charpoly_pow_card,
  FiniteField.pow_card]
[GOAL]
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
p : ℕ
inst✝ : Fact (Nat.Prime p)
M : Matrix n n (ZMod p)
⊢ trace (M ^ p) = trace M ^ p
[PROOFSTEP]
have h := FiniteField.trace_pow_card M
[GOAL]
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
p : ℕ
inst✝ : Fact (Nat.Prime p)
M : Matrix n n (ZMod p)
h : trace (M ^ Fintype.card (ZMod p)) = trace M ^ Fintype.card (ZMod p)
⊢ trace (M ^ p) = trace M ^ p
[PROOFSTEP]
rwa [ZMod.card] at h 
