English
In a scalar tower with normal subextensions, restricting normal homomorphisms along K1 ≃ K2 agrees with restricting along K2 ≃ K3.
Русский
В тензорно-стековой башне нормальные подполя: ограничение гомоморфизмов совпадает при последовательном ограничении через K1≃K2 и K2≃K3.
LaTeX
$$$\text{restrictNormalHom}_{K1} = \bigl(\text{restrictNormalHom}_{K1}\bigr) \circ \text{restrictNormalHom}_{K2}$$$
Lean4
theorem restrictNormalHom_comp_apply (K₁ K₂ : Type*) {F 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₂]
(f : K₃ ≃ₐ[F] K₃) :
AlgEquiv.restrictNormalHom K₁ f = (AlgEquiv.restrictNormalHom K₁) (AlgEquiv.restrictNormalHom K₂ f) := by
rw [IsScalarTower.AlgEquiv.restrictNormalHom_comp F K₁ K₂ K₃, MonoidHom.comp_apply]
