English
Given an algebra equivalence χ: K1 ≃ₐ[F] K2, restricting χ yields an automorphism on E, compatible with the tower.
Русский
Дано эквивалентность χ: K1 ≃ₐ[F] K2; ее ограничение даёт автоморфизм на E, совместимый с тензорной башней.
LaTeX
$$$\text{restrictNormal } χ : E \cong_F E$$$
Lean4
/-- In a scalar tower `K₃/K₂/K₁/F` with `K₁` and `K₂` are normal over `F`, the group homomorphism
given by the restriction of algebra isomorphisms of `K₃` to `K₁` is equal to the composition of
the group homomorphism given by the restricting an algebra isomorphism of `K₃` to `K₂` and
the group homomorphism given by the restricting an algebra isomorphism of `K₂` to `K₁` -/
theorem restrictNormalHom_comp (F K₁ K₂ K₃ : Type*) [Field F] [Field K₁] [Field K₂] [Field K₃] [Algebra F K₁]
[Algebra F K₂] [Algebra F K₃] [Algebra K₁ K₂] [Algebra K₁ K₃] [Algebra K₂ K₃] [IsScalarTower F K₁ K₃]
[IsScalarTower F K₁ K₂] [IsScalarTower F K₂ K₃] [IsScalarTower K₁ K₂ K₃] [Normal F K₁] [Normal F K₂] :
AlgEquiv.restrictNormalHom K₁ =
(AlgEquiv.restrictNormalHom K₁).comp (AlgEquiv.restrictNormalHom (F := F) (K₁ := K₃) K₂) :=
by
ext f x
apply (algebraMap K₁ K₃).injective
rw [IsScalarTower.algebraMap_eq K₁ K₂ K₃]
simp only [AlgEquiv.restrictNormalHom, MonoidHom.mk'_apply, RingHom.coe_comp, Function.comp_apply, ← algebraMap_apply,
AlgEquiv.restrictNormal_commutes, MonoidHom.coe_comp]
