equivLim — Mathlib

English

There is a canonical equivalence between embeddings of a truncated field E⟮<i⟯ into an algebraic closure Ē and the limit of the inverse system of embeddings of E⟮<j⟯ into Ē, as j ranges below i.

Русский

Существует каноническое эквивалентное отображение между вложениями E⟮<i⟯ в алг Closure Ē и пределом обратной системы вложений E⟮<j⟯ в Ē при j<i.

LaTeX

$$$\\text{equivLim} : (E⟮

Lean4

/-- If `i` is a limit, the type of embeddings of `E⟮<i⟯` into `Ē` is
the limit of the types of embeddings of `E⟮<j⟯` for `j < i`. -/
def equivLim : (E⟮<i⟯ →ₐ[F] Ē) ≃ limit (embFunctor F E) i
    where
  toFun f := ⟨fun j ↦ embFunctor _ _ (id j.2 : j < i).le f, fun _ _ _ ↦ rfl⟩
  invFun
    f :=
    if h : Nonempty (Iio i) then
      Subalgebra.iSupLift _ directed_filtration f.1 (fun _ _ h ↦ (f.2 <| filtration.map_rel_iff.mp h).symm) _ <| by
        rw [← iSup_filtration hi, toSubalgebra_iSup_of_directed directed_filtration]
    else (Algebra.ofId F Ē).comp ((equivOfEq (eq_bot_of_not_nonempty hi h)).trans <| botEquiv F E)
  left_inv
    f := by
    split_ifs with h
    · ext ⟨x, hx⟩
      rw [← iSup_filtration hi, mem_toSubalgebra, ← SetLike.mem_coe, coe_iSup_of_directed directed_filtration,
        mem_iUnion] at hx
      rw [Subalgebra.iSupLift_of_mem _ _ (by exact hx.choose_spec)]; rfl
    · apply AlgHom.ext
      rw [((equivOfEq (eq_bot_of_not_nonempty hi h)).trans <| botEquiv F E).forall_congr_left]
      simp
  right_inv
    f :=
    Subtype.ext <|
      funext fun j ↦ by
        have := Nonempty.intro j
        simp_rw [dif_pos this]
        apply Subalgebra.iSupLift_comp_inclusion

Похожие утверждения