English
In a tower with E/K algebraic, there is a bijection Emb F E × Emb E K ≃ Emb F K.
Русский
В башне с E/K алгебраично существует биекция между вложениями F→E и E→K и вложениями F→K.
LaTeX
$$$\mathrm{Emb}_F(E) \times \mathrm{Emb}_E(K) \simeq \mathrm{Emb}_F(K)$$$
Lean4
/-- If `K / E / F` is a field extension tower, such that `K / E` is algebraic,
then there is a non-canonical bijection
`Field.Emb F E × Field.Emb E K ≃ Field.Emb F K`. A corollary of `algHomEquivSigma`. -/
def embProdEmbOfIsAlgebraic [Algebra E K] [IsScalarTower F E K] [Algebra.IsAlgebraic E K] :
Emb F E × Emb E K ≃ Emb F K :=
let e : ∀ f : E →ₐ[F] AlgebraicClosure K, @AlgHom E K _ _ _ _ _ f.toRingHom.toAlgebra ≃ Emb E K := fun f ↦
(@embEquivOfIsAlgClosed E K _ _ _ _ _ f.toRingHom.toAlgebra).symm
(algHomEquivSigma (A := F) (B := E) (C := K) (D := AlgebraicClosure K) |>.trans
(Equiv.sigmaEquivProdOfEquiv e) |>.trans <|
Equiv.prodCongrLeft <| fun _ : Emb E K ↦
AlgEquiv.arrowCongr (@AlgEquiv.refl F E _ _ _) <|
(IsAlgClosure.equivOfAlgebraic E K (AlgebraicClosure K) (AlgebraicClosure E)).restrictScalars F).symm
