equivMaximalRealSubfield — Mathlib

English

If F is totally real and K/F is a CM-extension, then F is isomorphic to the maximal real subfield of K; more precisely, there exists a field isomorphism F ≃+* maximalRealSubfield(K).

Русский

Если F полностью реально и K/F — CM-подплетение, тогда F изоморфно максимальному реальному подполю K; существует изоморфизм F ≃+* maximalRealSubfield(K).

LaTeX

$$$\\exists\\; \\text{isomorphism } F \\cong\\mathrm{maximalRealSubfield}(K)$$$

Lean4

/-- Any field `F` such that `K/F` is a CM-extension is isomorphic to the maximal real subfield of `K`.
-/
noncomputable def equivMaximalRealSubfield : F ≃+* maximalRealSubfield K :=
  (algebraMap F K).rangeRestrictFieldEquiv.trans
    (RingEquiv.subfieldCongr
      (by
        have := IsTotallyReal.ofRingEquiv (algebraMap F K).rangeRestrictFieldEquiv
        have : IsQuadraticExtension (algebraMap F K).fieldRange K :=
          {
            finrank_eq_two' :=
              (IsQuadraticExtension.finrank_eq_two F K) ▸
                Algebra.finrank_eq_of_equiv_equiv (algebraMap F K).rangeRestrictFieldEquiv.symm (RingEquiv.refl K)
                  (by ext; simp; rfl) }
        exact eq_maximalRealSubfield K (algebraMap F K).fieldRange))

Похожие утверждения