union_isExtendible — Mathlib

English

If a family of intermediate fields c is a chain and each member is extendible, then their union is extendible.

Русский

Если семейство промежуточных полей c образует цепь и каждый элемент можно продолжить, то их объединение является продолжимым.

LaTeX

$$$\\text{Union } c \\; \\text{hc}.IsExtendible$ given each σ in c is extendible.$$

Lean4

theorem union_isExtendible [alg : Algebra.IsAlgebraic F E] [Nonempty c] (hext : ∀ σ ∈ c, σ.IsExtendible) :
    (union c hc).IsExtendible := fun S ↦ by
  let Ω := adjoin F (S : Set E) →ₐ[F] K
  have ⟨ω, hω⟩ : ∃ ω : Ω, ∀ π : c, ∃ θ ≥ π.1, ⟨_, ω⟩ ≤ θ ∧ θ.carrier = π.1.1 ⊔ adjoin F S :=
    by
    by_contra!; choose π hπ using this
    have := finiteDimensional_adjoin (S := (S : Set E)) fun _ _ ↦ (alg.isIntegral).1 _
    have ⟨π₀, hπ₀⟩ := hc.directed.finite_le π
    have ⟨θ, hθπ, hθ⟩ := hext _ π₀.2 S
    rw [← adjoin_le_iff] at hθ
    let θ₀ := θ.emb.comp (inclusion hθ)
    have := (hπ₀ θ₀).trans hθπ
    exact hπ θ₀ ⟨_, θ.emb.comp <| inclusion <| sup_le this.1 hθ⟩ ⟨le_sup_left, this.2⟩ ⟨le_sup_right, fun _ ↦ rfl⟩ rfl
  choose θ ge hθ eq using hω
  have : IsChain (· ≤ ·) (Set.range θ) :=
    by
    simp_rw [← restrictScalars_adjoin_eq_sup, restrictScalars_adjoin] at eq
    rintro _ ⟨π₁, rfl⟩ _ ⟨π₂, rfl⟩ -
    wlog h : π₁ ≤ π₂ generalizing π₁ π₂
    · exact (this _ _ <| (hc.total π₁.2 π₂.2).resolve_left h).symm
    refine .inl (le_iff.mpr ⟨?_, algHom_ext_of_eq_adjoin _ (eq _) ?_⟩)
    · rw [eq, eq]; exact adjoin.mono _ _ _ (Set.union_subset_union_left _ h.1)
    rintro x (hx | hx)
    · change (θ π₂).emb (inclusion (ge π₂).1 <| inclusion h.1 ⟨x, hx⟩) = (θ π₁).emb (inclusion (ge π₁).1 ⟨x, hx⟩)
      rw [(ge π₁).2, (ge π₂).2, h.2]
    · change
        (θ π₂).emb (inclusion (hθ π₂).1 ⟨x, subset_adjoin _ _ hx⟩) =
          (θ π₁).emb (inclusion (hθ π₁).1 ⟨x, subset_adjoin _ _ hx⟩)
      rw [(hθ π₁).2, (hθ π₂).2]
  refine
    ⟨union _ this,
      le_of_carrier_le_iSup (fun π ↦ le_union c hc π.2) (fun π ↦ (ge π).trans <| le_union _ _ ⟨_, rfl⟩)
        (carrier_union _ _).le,
      ?_⟩
  simp_rw [carrier_union, iSup_range', eq]
  exact
    (subset_adjoin _ _).trans
      (SetLike.coe_subset_coe.mpr <| le_sup_right.trans <| le_iSup_of_le (Classical.arbitrary _) le_rfl)

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