English
A relation between the quadratic character values across two fields F and F' connecting their cardinalities via a 'cardinal product' formula.
Русский
Связь значений квадратичного характера между полями F и F' через их кардинальности.
LaTeX
$$$χ_F(|F'|) = χ_{F'}(χ_F(-1)\cdot |F|)$$$
Lean4
/-- The relation between the values of the quadratic character of one field `F` at the
cardinality of another field `F'` and of the quadratic character of `F'` at the cardinality
of `F`. -/
theorem quadraticChar_card_card [DecidableEq F] (hF : ringChar F ≠ 2) {F' : Type*} [Field F'] [Fintype F']
[DecidableEq F'] (hF' : ringChar F' ≠ 2) (h : ringChar F' ≠ ringChar F) :
quadraticChar F (Fintype.card F') = quadraticChar F' (quadraticChar F (-1) * Fintype.card F) :=
by
let χ := (quadraticChar F).ringHomComp (algebraMap ℤ F')
have hχ₁ : χ ≠ 1 := by
obtain ⟨a, ha⟩ := quadraticChar_exists_neg_one' hF
refine ne_one_iff.mpr ⟨a, ?_⟩
simpa only [ringHomComp_apply, ha, eq_intCast, Int.cast_neg, Int.cast_one, χ] using
Ring.neg_one_ne_one_of_char_ne_two hF'
have h := Char.card_pow_card hχ₁ ((quadraticChar_isQuadratic F).comp _) h hF'
rw [← quadraticChar_eq_pow_of_char_ne_two' hF'] at h
exact (IsQuadratic.eq_of_eq_coe (quadraticChar_isQuadratic F') (quadraticChar_isQuadratic F) hF' h).symm
