English
Restriction to a normal subfield defines a group homomorphism from automorphisms of K to automorphisms of E, compatible with composition.
Русский
Ограничение нормального подполя задаёт гомоморфизм группы автоморфизмов K в автоморфизм E, совместимый с композициями.
LaTeX
$$$\text{restrictNormalHom} : (K\simeq^_{F} K) \to (E\simeq^_{F} E)$ is a group homomorphism$$
Lean4
/-- The group homomorphism given by restricting an algebra isomorphism to itself
is the identity map. -/
@[simp]
theorem restrictNormalHom_id (F K : Type*) [Field F] [Field K] [Algebra F K] [Normal F K] :
AlgEquiv.restrictNormalHom K = MonoidHom.id (K ≃ₐ[F] K) :=
by
ext f x
dsimp only [restrictNormalHom, MonoidHom.mk'_apply, MonoidHom.id_apply]
apply (algebraMap K K).injective
rw [AlgEquiv.restrictNormal_commutes]
simp only [Algebra.algebraMap_self, RingHom.id_apply]
