English
A transfer lemma for comparing lifts: two lifts are ordered iff there exists a comparison map making the embeddings equal after transport.
Русский
Лемма переноса для сравнения подполей: два подполя упорядочены тогда и только тогда, когда существует отображение сравнения, приводящее вложения к одному и тому же базовому полю.
LaTeX
$$$L_1 \\le L_2 \\iff \\exists h: L_1.carrier \\le L_2.carrier,\\ L_2.emb \\circ (inclusion\\, h) = L_1.emb$$$
Lean4
noncomputable instance : OrderBot (Lifts F E K)
where
bot := ⟨⊥, (Algebra.ofId F K).comp (botEquiv F E)⟩
bot_le
L :=
⟨bot_le, fun x ↦ by
obtain ⟨x, rfl⟩ := (botEquiv F E).symm.surjective x
simp_rw [AlgHom.comp_apply, AlgHom.coe_coe, AlgEquiv.apply_symm_apply]
exact L.emb.commutes x⟩
