English
If L/K is algebraic, the K-subalgebras of L are in bijective correspondence with the intermediate fields of L/K; more precisely, there is an order isomorphism between Subalgebra K L and IntermediateField K L.
Русский
Если L/K алгебраическое, то K-подалгебры L и промежуточные поля L/K устанавливают биекция между собой; существует отношения равномощности (порядковое изоморфирование) между Subalgebra K L и IntermediateField K L.
LaTeX
$$$ \text{subalgebraEquivIntermediateField} : Subalgebra K L \simeq_o IntermediateField K L $$$
Lean4
/-- If `L/K` is algebraic, the `K`-subalgebras of `L` are all fields. -/
def subalgebraEquivIntermediateField [Algebra.IsAlgebraic K L] : Subalgebra K L ≃o IntermediateField K L
where
toFun
S := S.toIntermediateField fun x hx => S.inv_mem_of_algebraic (Algebra.IsAlgebraic.isAlgebraic ((⟨x, hx⟩ : S) : L))
invFun S := S.toSubalgebra
left_inv _ := toSubalgebra_toIntermediateField _ _
right_inv := toIntermediateField_toSubalgebra
map_rel_iff' := Iff.rfl
