English
There is a natural order-preserving bijection between the subfields E of L containing F and the intermediate fields of L over F obtained by extending scalars; its inverse sends an intermediate field back to the corresponding subfield.
Русский
Существует естественная порядочно-биекция между подполями E L, содержащими F, и промежуточными полями L над F, получаемая расширением скаляров; обратная карта восстанавливает соответствующее подполье.
LaTeX
$$$\{ E: {\!\!\!} E\_L\;\bigm|\; F \le E \}\;\cong_o\; \text{IntermediateField } F L$$
Lean4
/-- `Subfield.extendScalars.orderIso` bundles `Subfield.extendScalars`
into an order isomorphism from
`{ E : Subfield L // F ≤ E }` to `IntermediateField F L`. Its inverse is
`IntermediateField.toSubfield`. -/
@[simps]
def orderIso : { E : Subfield L // F ≤ E } ≃o IntermediateField F L
where
toFun E := extendScalars E.2
invFun E := ⟨E.toSubfield, fun x hx ↦ E.algebraMap_mem ⟨x, hx⟩⟩
map_rel_iff'
{E E'} := by
simp only [Equiv.coe_fn_mk]
exact extendScalars_le_extendScalars_iff _ _
