English
There is a bijection between field embeddings F→E and the product of factor structures over all indices i, encoding each embedding by its action on the successive layers.
Русский
Существует биекция между вложениями полей F→E и произведением факторных структур по всем индексам i, кодирующая вложение действием на последовательные слои.
LaTeX
$$$\\mathrm{embEquivPi} : \\mathrm{Field Embeddings}\; F E \\;\cong\\; \\prod_{i} \\mathrm{factor}(F,E,i)$$$
Lean4
/-- A bijection between `E →ₐ[F] Ē` and the product of `E⟮<i⁺⟯ →ₐ[E⟮<i⟯] Ē` over all `i : ι`. -/
def embEquivPi : Field.Emb F E ≃ ∀ i : ι, factor (F := F) (E := E) i :=
let e := globalEquiv (fun i _ ↦ ⟨_, equivSucc_coherence i⟩) (fun _ hi ↦ ⟨equivLim hi, fun _ _ ↦ rfl⟩) ⊤
(topEquiv.arrowCongr .refl).symm.trans <|
e.trans <|
.trans (.piCongrSet WithTop.range_coe.symm) <|
.symm <| .piCongr (.ofInjective _ WithTop.coe_injective) fun _ ↦ .refl _
