English
The number of non-real embeddings equals twice the number of complex places: card { φ: K →+* ℂ // ¬IsReal φ } = 2 · nrComplexPlaces K.
Русский
Число невещественных вложений равно двойке числу комплексных мест.
LaTeX
$$$\left| \{ \varphi: K \to \mathbb{C} \mid \lnot \operatorname{IsReal}(\varphi) \} \right| = 2 \cdot nrComplexPlaces(K).$$$
Lean4
theorem card_complex_embeddings : card { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } = 2 * nrComplexPlaces K :=
by
suffices
∀ w : { w : InfinitePlace K // IsComplex w }, #{φ : { φ // ¬ComplexEmbedding.IsReal φ } | mkComplex φ = w} = 2
by
rw [Fintype.card, Finset.card_eq_sum_ones, ← Finset.sum_fiberwise _ (fun φ => mkComplex φ)]
simp_rw [Finset.sum_const, this, smul_eq_mul, mul_one, Fintype.card, Finset.card_eq_sum_ones, Finset.mul_sum,
Finset.sum_const, smul_eq_mul, mul_one]
rintro ⟨w, hw⟩
convert card_filter_mk_eq w
· rw [← Fintype.card_subtype, ← Fintype.card_subtype]
refine Fintype.card_congr (Equiv.ofBijective ?_ ⟨fun _ _ h => ?_, fun ⟨φ, hφ⟩ => ?_⟩)
· exact fun ⟨φ, hφ⟩ => ⟨φ.val, by rwa [Subtype.ext_iff] at hφ⟩
· rwa [Subtype.mk_eq_mk, ← Subtype.ext_iff, ← Subtype.ext_iff] at h
· refine ⟨⟨⟨φ, not_isReal_of_mk_isComplex (hφ.symm ▸ hw)⟩, ?_⟩, rfl⟩
rwa [Subtype.ext_iff, mkComplex_coe]
· simp_rw [mult, not_isReal_iff_isComplex.mpr hw, ite_false]
