Cyclotomic character of Frobenius element

Stream: new members

[Chengyan Hu]

Hi! My final aim is to prove the value of the cyclotomic character at Frob_I is #A/PA where P = I ∩ A, and now I'm trying to apply AlgHom.IsArithFrobAt.apply_of_pow_eq_one but I have several confusions here:

1. I think the proof of this lemma is by first observe the situation mod p and then construct back.
   By a lemma 1 - ζ ^ ((q + k - i) * j) ∈ Q, prove our aim by sum of geometric sequence.
   However, I can't understand the proof of 1 - ζ ^ ((q + k - i) * j) ∈ Q.

2. It's mentioned that apply_of_pow_eq_one only works for m not in Q, but I can't see why m in Q makes an issue.

3. I think PadicInt.ext_of_toZModPow may helps a lot if we can deal with the case p^i in Q, or prove p^i can't be in Q, and hope for some advice about this.
   Sincerely thanks a lot in advance!

[Chengyan Hu]

I put the lemma AlgHom.IsArithFrobAt.apply_of_pow_eq_one here for convenience.

/-- Suppose `S` is a domain, and `φ : S →ₐ[R] S` is a Frobenius at `Q : Ideal S`.
Let `ζ` be a `m`-th root of unity with `Q ∤ m`, then `φ` sends `ζ` to `ζ ^ q`. -/
lemma apply_of_pow_eq_one [IsDomain S] {ζ : S} {m : ℕ} (hζ : ζ ^ m = 1) (hk' : ↑m ∉ Q) :
    φ ζ = ζ ^ Nat.card (R ⧸ Q.under R) := by
  set q := Nat.card (R ⧸ Q.under R)
  have hm : m ≠ 0 := by rintro rfl; exact hk' (by simp)
  obtain ⟨k, hk, hζ⟩ := IsPrimitiveRoot.exists_pos hζ hm
  have hk' : ↑k ∉ Q := fun h ↦ hk' (Q.mem_of_dvd (Nat.cast_dvd_cast (hζ.2 m ‹_›)) h)
  have : NeZero k := ⟨hk.ne'⟩
  obtain ⟨i, hi, e⟩ := hζ.eq_pow_of_pow_eq_one (ξ := φ ζ) (by rw [← map_pow, hζ.1, map_one])
  have (j) : 1 - ζ ^ ((q + k - i) * j) ∈ Q := by
    rw [← Ideal.mul_unit_mem_iff_mem _ ((hζ.isUnit k.pos_of_neZero).pow (i * j)),
      sub_mul, one_mul, ← pow_add, ← add_mul, tsub_add_cancel_of_le (by linarith), add_mul,
        pow_add, pow_mul _ k, hζ.1, one_pow, mul_one, pow_mul, e, ← map_pow, mul_comm, pow_mul]
    exact H _
  have h₁ := sum_mem (t := Finset.range k) fun j _ ↦ this j
  have h₂ := geom_sum_mul (ζ ^ (q + k - i)) k
  rw [pow_right_comm, hζ.1, one_pow, sub_self, mul_eq_zero, sub_eq_zero] at h₂
  rcases h₂ with h₂ | h₂
  · simp [h₂, pow_mul, hk'] at h₁
  replace h₂ := congr($h₂ * ζ ^ i)
  rw [one_mul, ← pow_add, tsub_add_cancel_of_le (by linarith), pow_add, hζ.1, mul_one] at h₂
  rw [h₂, e]

[Andrew Yang]

This is just because ζ ^ k = 1 (by ζ being a primitive k-th root of unity) and φ ζ = ζ ^ i for some i (by (φ ζ) ^ k = 1 and ζ being primitive) which implies ζ ^ q = ζ ^ i mod Q (by the definition of frobenius)

[Andrew Yang]

As of why m ∉ Q is needed, you can write out the "sum of geometric sequence" argument and see where it is needed. The easiest example where m ∈ Q is when ζ is a p-th root of unity, R = ℤ, S = ℤ[ζ] and Q = <1 - ζ>. The residue field S/Q is 𝔽ₚ so the identity map is a frobenius at p but the identity map clearly doesn't take ζ to ζ ^ p,

[Chengyan Hu]

Ah I see! Thanks a lot.