Theorems · Definition · field theory

AlgEquiv.liftNormal

{F : Type u_1} →
  [inst : Field F] →
    {K₁ : Type u_3} →
      {K₂ : Type u_4} →
        [inst_1 : Field K₁] →
          [inst_2 : Field K₂] →
            [inst_3 : Algebra F K₁] →
              [inst_4 : Algebra F K₂] →
                (K₁ ≃ₐ[F] K₂) →
                  (E : Type u_6) →
                    [inst_5 : Field E] →
                      [inst_6 : Algebra F E] →
                        [inst_7 : Algebra K₁ E] →
                          [inst_8 : Algebra K₂ E] →
                            [IsScalarTower F K₁ E] → [IsScalarTower F K₂ E] → [Normal F E] → Gal(E/F)

If E/Kᵢ/F are towers of fields with E/F normal then we can lift an algebra isomorphism ϕ : K₁ ≃ₐ[F] K₂ to ϕ.liftNormal E : Gal(E/F).

Defined in

Mathlib.FieldTheory.Normal.Basic

Cited by

6 results in Mathlib

Foundations

Depth 149 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldFieldFieldAlgebraAlgebraFieldAlgebraAlgebraAlgebraIsScalarTowerIsScalarTowerNormal