English
If E is a subfield of K, E is totally real and K/E is a quadratic extension, then E is the maximal real subfield of K.
Русский
Если E — подполе K, E полностью вещественно и K/E — квадратичное расширение, то E равно максимальному действительному подполю K.
LaTeX
$$$(E\\subseteq K)$, $(E\\text{ totally real})$, $(K/E\\text{ is quadratic})\\Rightarrow E = K^{+}_{\\text{max}}$$$
Lean4
theorem eq_maximalRealSubfield (E : Subfield K) [IsTotallyReal E] [IsQuadraticExtension E K] :
E = maximalRealSubfield K :=
by
refine le_antisymm (IsTotallyReal.le_maximalRealSubfield E) ?_
by_contra! h
have h' : E ⊔ (maximalRealSubfield K) = ⊤ :=
by
let L : IntermediateField E K :=
(E ⊔ (maximalRealSubfield K)).toIntermediateField (fun x ↦ (le_sup_left (a := E)) x.prop)
have :=
((IntermediateField.isSimpleOrder_of_finrank_prime E K
(IsQuadraticExtension.finrank_eq_two E K ▸ Nat.prime_two)).eq_bot_or_eq_top
L).resolve_left
?_
· simpa [L] using congr_arg IntermediateField.toSubfield this
· contrapose! h
rw [← SetLike.coe_set_eq, Subfield.coe_toIntermediateField] at h
rw [← sup_eq_left, ← SetLike.coe_set_eq, h, IntermediateField.coe_bot]
aesop
have : IsTotallyReal K := (h' ▸ isTotallyReal_sup).ofRingEquiv Subring.topEquiv
obtain w : InfinitePlace K := Classical.choice (inferInstance : Nonempty _)
exact (not_isReal_iff_isComplex.mpr (IsTotallyComplex.isComplex w)) (IsTotallyReal.isReal w)
