Theorems · Definition · field theory

AlgHom.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] → [h : Normal F E] → E →ₐ[F] E

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

Defined in

Mathlib.FieldTheory.Normal.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

FieldFieldFieldAlgebraAlgebraFieldAlgebraAlgebraAlgebraIsScalarTowerIsScalarTowerNormal