English
Under algebraicity assumptions, if for every finite set of elements there exists a lift, then there exists a global algebra hom from E to K extending f.
Русский
При алгебраичности, если для каждого конечного множества элементов существует лифт, то существует глобальный AlgHom из E в K, продолжающий f.
LaTeX
$$$[alg : Algebra.IsAlgebraic F E] (\\forall S : Finset E, \\exists \\sigma : Lifts F E K, (S : Set E) ⊆ σ.carrier) \\Rightarrow Nonempty (E →ₐ[F] K)$$$
Lean4
theorem nonempty_algHom_of_exist_lifts_finset [alg : Algebra.IsAlgebraic F E]
(h : ∀ S : Finset E, ∃ σ : Lifts F E K, (S : Set E) ⊆ σ.carrier) : Nonempty (E →ₐ[F] K) :=
by
have : (⊥ : Lifts F E K).IsExtendible := fun S ↦
have ⟨σ, hσ⟩ := h S;
⟨σ, bot_le, hσ⟩
have ⟨ϕ, hϕ⟩ :=
zorn_le₀ {ϕ : Lifts F E K | ϕ.IsExtendible} fun c hext hc ↦
(isEmpty_or_nonempty c).elim (fun _ ↦ ⟨⊥, this, fun ϕ hϕ ↦ isEmptyElim (⟨ϕ, hϕ⟩ : c)⟩) fun _ ↦
⟨_, union_isExtendible c hc hext, le_union c hc⟩
suffices ϕ.carrier = ⊤ from ⟨ϕ.emb.comp <| ((equivOfEq this).trans topEquiv).symm⟩
by_contra!
obtain ⟨α, -, hα⟩ := SetLike.exists_of_lt this.lt_top
let _ : Algebra ϕ.carrier K := ϕ.emb.toAlgebra
let Λ := ϕ.carrier⟮α⟯ →ₐ[ϕ.carrier] K
have := finiteDimensional_adjoin (S := { α }) fun _ _ ↦ ((alg.tower_top ϕ.carrier).isIntegral).1 _
let L (σ : Λ) : Lifts F E K := ⟨ϕ.carrier⟮α⟯.restrictScalars F, σ.restrictScalars F⟩
have hL (σ : Λ) : ϕ < L σ :=
lt_iff.mpr
⟨by simpa only [L, restrictScalars_adjoin_eq_sup, left_lt_sup, adjoin_simple_le_iff],
AlgHom.coe_ringHom_injective σ.comp_algebraMap⟩
have ⟨(ϕ_ext : ϕ.IsExtendible), ϕ_max⟩ := maximal_iff_forall_gt.mp hϕ
simp_rw [Set.mem_setOf, IsExtendible] at ϕ_max; push_neg at ϕ_max
choose S hS using fun σ : Λ ↦ ϕ_max (hL σ)
classical
have ⟨θ, hθϕ, hθ⟩ := ϕ_ext ({ α } ∪ Finset.univ.biUnion S)
simp_rw [Finset.coe_union, Set.union_subset_iff, Finset.coe_singleton, Set.singleton_subset_iff, Finset.coe_biUnion,
Finset.coe_univ, Set.mem_univ, Set.iUnion_true, Set.iUnion_subset_iff] at hθ
have : ϕ.carrier⟮α⟯.restrictScalars F ≤ θ.carrier := by
rw [restrictScalars_adjoin_eq_sup, sup_le_iff, adjoin_simple_le_iff]; exact ⟨hθϕ.1, hθ.1⟩
exact hS ⟨(θ.emb.comp <| inclusion this).toRingHom, hθϕ.2⟩ θ ⟨this, fun _ ↦ rfl⟩ (hθ.2 _)
