Theorems · Theorem · field theory

IsScalarTower.AlgEquiv.restrictNormalHom_comp

∀ (F : Type u_6) (K₁ : Type u_7) (K₂ : Type u_8) (K₃ : Type u_9) [inst : Field F] [inst_1 : Field K₁]
  [inst_2 : Field K₂] [inst_3 : Field K₃] [inst_4 : Algebra F K₁] [inst_5 : Algebra F K₂] [inst_6 : Algebra F K₃]
  [inst_7 : Algebra K₁ K₂] [inst_8 : Algebra K₁ K₃] [inst_9 : Algebra K₂ K₃] [inst_10 : IsScalarTower F K₁ K₃]
  [inst_11 : IsScalarTower F K₁ K₂] [inst_12 : IsScalarTower F K₂ K₃] [IsScalarTower K₁ K₂ K₃] [inst_14 : Normal F K₁]
  [inst_15 : Normal F K₂],
  AlgEquiv.restrictNormalHom K₁ = (AlgEquiv.restrictNormalHom K₁).comp (AlgEquiv.restrictNormalHom K₂)

In a scalar tower K₃/K₂/K₁/F with K₁ and K₂ normal over F, the group homomorphism which restricts algebra isomorphisms of K₃ to K₁ is equal to the composition of the group homomorphism given by restricting an algebra isomorphism of K₃ to K₂ and the group homomorphism given by restricting an algebra isomorphism of K₂ to K₁.

Defined in

Mathlib.FieldTheory.Normal.Defs

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldFieldFieldFieldAlgebraAlgebraAlgebraAlgebraAlgebraAlgebraIsScalarTowerIsScalarTowerIsScalarTowerIsScalarTowerNormalNormal