English
If S ⊆ E and φ1, φ2: adjoin F S →ₐ[F] K are F-algebra homomorphisms that agree on the generators from S, then φ1 = φ2.
Русский
Если S ⊆ E и φ1, φ2: adjoin F S →ₐ[F] K — алгебра-гомоморфизмы, совпадающие на порождающих S, то φ1 = φ2.
LaTeX
$$$\\\\text{adjoin\_hom\_ext}_{F,S}(φ_1,φ_2) : \\\\forall x (hx), φ_1 ⟨x, hx⟩ = φ_2 ⟨x, hx⟩ \\\\Rightarrow φ_1 = φ_2.$$$
Lean4
@[elab_as_elim]
theorem adjoin_induction {s : Set E} {p : ∀ x ∈ adjoin F s, Prop} (mem : ∀ x hx, p x (subset_adjoin _ _ hx))
(algebraMap : ∀ x, p (algebraMap F E x) (algebraMap_mem _ _))
(add : ∀ x y hx hy, p x hx → p y hy → p (x + y) (add_mem hx hy)) (inv : ∀ x hx, p x hx → p x⁻¹ (inv_mem hx))
(mul : ∀ x y hx hy, p x hx → p y hy → p (x * y) (mul_mem hx hy)) {x} (h : x ∈ adjoin F s) : p x h :=
Subfield.closure_induction (fun x hx ↦ Or.casesOn hx (fun ⟨x, hx⟩ ↦ hx ▸ algebraMap x) (mem x))
(by simp_rw [← (_root_.algebraMap F E).map_one]; exact algebraMap 1) add
(fun x _ h ↦ by simp_rw [← neg_one_smul F x, Algebra.smul_def]; exact mul _ _ _ _ (algebraMap _) h) inv mul h
