adjoin_algHom_ext — Mathlib

English

If S is a subset with S = adjoin F s, then any two F-algebra homomorphisms from S that agree on s are equal.

Русский

Если S = adjoin F s, то любые два F-алгебро-гомоморфизма из S, совпадающие на s, равны.

LaTeX

$$$\\text{algHom\_ext\_of\_eq\_adjoin}_{F,S}(h, φ_1, φ_2) : (\\forall x\\in s, φ_1 x = φ_2 x) \\Rightarrow φ_1 = φ_2.$$$

Lean4

theorem adjoin_algHom_ext {s : Set E} ⦃φ₁ φ₂ : adjoin F s →ₐ[F] K⦄
    (h : ∀ x hx, φ₁ ⟨x, subset_adjoin _ _ hx⟩ = φ₂ ⟨x, subset_adjoin _ _ hx⟩) : φ₁ = φ₂ :=
  AlgHom.ext fun ⟨x, hx⟩ ↦
    adjoin_induction _ h (fun _ ↦ φ₂.commutes _ ▸ φ₁.commutes _)
      (fun _ _ _ _ h₁ h₂ ↦ by convert congr_arg₂ (· + ·) h₁ h₂ <;> rw [← map_add] <;> rfl) (fun _ _ ↦ eq_on_inv₀ _ _)
      (fun _ _ _ _ h₁ h₂ ↦ by convert congr_arg₂ (· * ·) h₁ h₂ <;> rw [← map_mul] <;> rfl) hx

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