English
If E ⊆ K is a subfield, E is totally real, E⊆K is quadratic, then E equals maximalRealSubfield(K).
Русский
Если E ⊆ K, E полностью реально и E⊆K квадратично, то E равно maximalRealSubfield(K).
LaTeX
$$$E\\subseteq K\\;\\wedge\\; E^{+}\\subseteq K\\;\\wedge\\; [K:E]=2 \\Rightarrow E=\\mathrm{maximalRealSubfield}(K)$$$
Lean4
/-- A `ℂ`-basis of `ℂ^n` that is also a `ℤ`-basis of the `integerLattice`. -/
noncomputable def latticeBasis [NumberField K] : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ) := by
classical
-- Let `B` be the canonical basis of `(K →+* ℂ) → ℂ`. We prove that the determinant of
-- the image by `canonicalEmbedding` of the integral basis of `K` is nonzero. This
-- will imply the result.
let B := Pi.basisFun ℂ (K →+* ℂ)
let e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ (𝓞 K) :=
Fintype.equivOfCardEq ((Embeddings.card K ℂ).trans (finrank_eq_card_basis (integralBasis K)))
let M := B.toMatrix (fun i => canonicalEmbedding K (integralBasis K (e i)))
suffices M.det ≠ 0 by
rw [← isUnit_iff_ne_zero, ← Basis.det_apply, ← Basis.is_basis_iff_det] at this
exact (basisOfPiSpaceOfLinearIndependent this.1).reindex e
let N := Algebra.embeddingsMatrixReindex ℚ ℂ (fun i => integralBasis K (e i)) RingHom.equivRatAlgHom
rw [show M = N.transpose by { ext : 2; rfl
}]
rw [Matrix.det_transpose, ← pow_ne_zero_iff two_ne_zero]
convert (map_ne_zero_iff _ (algebraMap ℚ ℂ).injective).mpr (Algebra.discr_not_zero_of_basis ℚ (integralBasis K))
rw [← Algebra.discr_reindex ℚ (integralBasis K) e.symm]
exact
(Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two ℚ ℂ (fun i => integralBasis K (e i))
RingHom.equivRatAlgHom).symm
