English
For p ∈ ℚ[X], the number of complex roots equals the number of real roots plus the number of roots not fixed by complex conjugation.
Русский
Для p ∈ ℚ[X] число комплексных корней равно числу действительных корней плюс число корней, не фиксируемых сопряжением.
LaTeX
$$$$ |\\mathrm{root}_{\\mathbb{C}}(p)| = |\\mathrm{root}_{\\mathbb{R}}(p)| + |\\mathrm{not\\;gal\the\tof p}|. $$$$
Lean4
/-- The number of complex roots equals the number of real roots plus
the number of roots not fixed by complex conjugation (i.e. with some imaginary component). -/
theorem card_complex_roots_eq_card_real_add_card_not_gal_inv (p : ℚ[X]) :
(p.rootSet ℂ).toFinset.card =
(p.rootSet ℝ).toFinset.card +
(galActionHom p ℂ (restrict p ℂ (AlgEquiv.restrictScalars ℚ Complex.conjAe))).support.card :=
by
by_cases hp : p = 0
· haveI : IsEmpty (p.rootSet ℂ) := by rw [hp, rootSet_zero]; infer_instance
simp_rw [(galActionHom p ℂ _).support.eq_empty_of_isEmpty, hp, rootSet_zero, Set.toFinset_empty, Finset.card_empty]
have inj : Function.Injective (IsScalarTower.toAlgHom ℚ ℝ ℂ) := (algebraMap ℝ ℂ).injective
rw [← Finset.card_image_of_injective _ Subtype.coe_injective, ← Finset.card_image_of_injective _ inj]
let a : Finset ℂ := ?_
on_goal 1 => let b : Finset ℂ := ?_
on_goal 1 => let c : Finset ℂ := ?_
change a.card = b.card + c.card
have ha : ∀ z : ℂ, z ∈ a ↔ aeval z p = 0 := by intro z; rw [Set.mem_toFinset, mem_rootSet_of_ne hp]
have hb : ∀ z : ℂ, z ∈ b ↔ aeval z p = 0 ∧ z.im = 0 := by
intro z
simp_rw [b, Finset.mem_image, Set.mem_toFinset, mem_rootSet_of_ne hp]
constructor
· rintro ⟨w, hw, rfl⟩
exact ⟨by rw [aeval_algHom_apply, hw, map_zero], rfl⟩
· rintro ⟨hz1, hz2⟩
have key : IsScalarTower.toAlgHom ℚ ℝ ℂ z.re = z := by
ext
· rfl
· rw [hz2]; rfl
exact ⟨z.re, inj (by rwa [← aeval_algHom_apply, key, map_zero]), key⟩
have hc0 :
∀ w : p.rootSet ℂ, galActionHom p ℂ (restrict p ℂ (Complex.conjAe.restrictScalars ℚ)) w = w ↔ w.val.im = 0 :=
by
intro w
rw [Subtype.ext_iff, galActionHom_restrict]
exact Complex.conj_eq_iff_im
have hc : ∀ z : ℂ, z ∈ c ↔ aeval z p = 0 ∧ z.im ≠ 0 := by
intro z
simp_rw [c, Finset.mem_image]
constructor
· rintro ⟨w, hw, rfl⟩
exact ⟨(mem_rootSet.mp w.2).2, mt (hc0 w).mpr (Equiv.Perm.mem_support.mp hw)⟩
· rintro ⟨hz1, hz2⟩
exact ⟨⟨z, mem_rootSet.mpr ⟨hp, hz1⟩⟩, Equiv.Perm.mem_support.mpr (mt (hc0 _).mp hz2), rfl⟩
rw [← Finset.card_union_of_disjoint]
· apply congr_arg Finset.card
simp_rw [Finset.ext_iff, Finset.mem_union, ha, hb, hc]
tauto
· rw [Finset.disjoint_left]
intro z
rw [hb, hc]
tauto
