English
The image of canonical embedding lies in the real subspace of the function space consisting of all x such that x_φ = conj(x_{φ̄}) for all φ, i.e., the conjugation symmetry condition.
Русский
Образ канонического вложения лежит в вещественном подполье пространства функций, удовлетворяющем симметрии конъюгации: x_φ = conj(x_{φ̄}) для всех φ.
LaTeX
$$$x \\in (\\mathcal{O}_K)^× \\text{ and } x\\text{ respects conjugation: } x_φ = \\overline{x_{φ̄}}$$$
Lean4
/-- The image of `canonicalEmbedding` lives in the `ℝ`-submodule of the `x ∈ ((K →+* ℂ) → ℂ)` such
that `conj x_φ = x_(conj φ)` for all `∀ φ : K →+* ℂ`. -/
theorem conj_apply {x : ((K →+* ℂ) → ℂ)} (φ : K →+* ℂ) (hx : x ∈ Submodule.span ℝ (Set.range (canonicalEmbedding K))) :
conj (x φ) = x (ComplexEmbedding.conjugate φ) :=
by
refine Submodule.span_induction ?_ ?_ (fun _ _ _ _ hx hy => ?_) (fun a _ _ hx => ?_) hx
· rintro _ ⟨x, rfl⟩
rw [apply_at, apply_at, ComplexEmbedding.conjugate_coe_eq]
· rw [Pi.zero_apply, Pi.zero_apply, map_zero]
· rw [Pi.add_apply, Pi.add_apply, map_add, hx, hy]
· rw [Pi.smul_apply, Complex.real_smul, map_mul, Complex.conj_ofReal]
exact congrArg ((a : ℂ) * ·) hx
