English
Given F ≤ E, restrict yields an intermediate field K E that reflects F ≤ E. It is the inverse of extendScalars.
Русский
Пусть F ≤ E. Рrestrict возвращает промежуточное поле K E, отражающее F ≤ E; это обратное расширению.
LaTeX
$$$\\text{restrict}\\;:\\; \\text{IntermediateField}(K,E)$ is the inverse of \\text{extendScalars}$(\\cdot)$.$$
Lean4
/-- `IntermediateField.extendScalars.orderIso` bundles `IntermediateField.extendScalars`
into an order isomorphism from
`{ E : IntermediateField K L // F ≤ E }` to `IntermediateField F L`. Its inverse is
`IntermediateField.restrictScalars`. -/
@[simps]
def orderIso : { E : IntermediateField K L // F ≤ E } ≃o IntermediateField F L
where
toFun E := extendScalars E.2
invFun E := ⟨E.restrictScalars K, 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 _ _
