English
If E and K are isomorphic as F-algebras, then finSepDegree F E = finSepDegree F K.
Русский
Если E и K изоморфны как F-алгебры, то финальная разделяемая степень одинакова: finSepDegree F E = finSepDegree F K.
LaTeX
$$$\\text{finSepDegree } F E = \\text{finSepDegree } F K$ при наличии изоморфизма $E \\cong_F K$$$
Lean4
/-- A random bijection between `Field.Emb F E` and `Field.Emb F K` when `E` and `K` are isomorphic
as `F`-algebras. -/
def embEquivOfEquiv (i : E ≃ₐ[F] K) : Emb F E ≃ Emb F K :=
AlgEquiv.arrowCongr i <|
AlgEquiv.symm <| by
let _ : Algebra E K := i.toAlgHom.toRingHom.toAlgebra
have : Algebra.IsAlgebraic E K := by
constructor
intro x
have h := isAlgebraic_algebraMap (R := E) (A := K) (i.symm.toAlgHom x)
rw [show ∀ y : E, (algebraMap E K) y = i.toAlgHom y from fun y ↦ rfl] at h
simpa only [AlgEquiv.toAlgHom_eq_coe, AlgHom.coe_coe, AlgEquiv.apply_symm_apply] using h
apply AlgEquiv.restrictScalars (R := F) (S := E)
exact IsAlgClosure.equivOfAlgebraic E K (AlgebraicClosure K) (AlgebraicClosure E)
