of_equiv_equiv — Mathlib

English

Given compatible algebra maps f and g making a commutative square with F, if E/F is Galois then M/N is Galois.

Русский

При совместимых отображениях алгебр f и g, удовлетворяющих диагонали, если E/F Галуа, то M/N Галуа.

LaTeX

$$IsGalois M N$$

Lean4

theorem of_equiv_equiv {M N : Type*} [Field N] [Field M] [Algebra M N] [Algebra.IsAlgebraic F E] [h : IsGalois F E]
    {f : F ≃+* M} {g : E ≃+* N} (hcomp : (algebraMap M N).comp f = (g : E →+* N).comp (algebraMap F E)) :
    IsGalois M N :=
  isGalois_iff.mpr ⟨Algebra.IsSeparable.of_equiv_equiv f g hcomp, Normal.of_equiv_equiv hcomp⟩

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