English
There is a primitive additive character on a finite field F with values in ℂ when the characteristic is different from that of F and the construction uses zmodChar together with the cyclotomic extension.
Русский
Существует примитивная аддитивная характеристика на конечном поле F со значениями в ℂ, если характеристика поля отличается от характеристики F и используется zmodChar вместе с циклотомическим расширением.
LaTeX
$$AddChar.FiniteField.primitiveChar F ℂ$$
Lean4
/-- There is a primitive additive character on the finite field `F` if the characteristic
of the target is different from that of `F`.
We obtain it as the composition of the trace from `F` to `ZMod p` with a primitive
additive character on `ZMod p`, where `p` is the characteristic of `F`. -/
noncomputable def primitiveChar (F F' : Type*) [Field F] [Finite F] [Field F'] (h : ringChar F' ≠ ringChar F) :
PrimitiveAddChar F F' := by
let p := ringChar F
haveI hp : Fact p.Prime := ⟨CharP.char_is_prime F _⟩
let pp := p.toPNat hp.1.pos
have hp₂ : ¬ringChar F' ∣ p :=
by
rcases CharP.char_is_prime_or_zero F' (ringChar F') with hq | hq
· exact mt (Nat.Prime.dvd_iff_eq hp.1 (Nat.Prime.ne_one hq)).mp h.symm
· rw [hq]
exact fun hf => Nat.Prime.ne_zero hp.1 (zero_dvd_iff.mp hf)
let ψ := primitiveZModChar pp F' (neZero_iff.mp (NeZero.of_not_dvd F' hp₂))
letI : Algebra (ZMod p) F := ZMod.algebra _ _
let ψ' := ψ.char.compAddMonoidHom (Algebra.trace (ZMod p) F).toAddMonoidHom
have hψ' : ψ' ≠ 1 := by
obtain ⟨a, ha⟩ := FiniteField.trace_to_zmod_nondegenerate F one_ne_zero
rw [one_mul] at ha
exact ne_one_iff.2 ⟨a, fun hf => ha <| (ψ.prim.zmod_char_eq_one_iff pp <| Algebra.trace (ZMod p) F a).mp hf⟩
exact ⟨ψ.n, ψ', IsPrimitive.of_ne_one hψ'⟩
