adjoin_ext — Mathlib

English

The extensionality principle for adjoin: two homomorphisms are equal if they agree on generators.

Русский

Принцип экстенсивности для adjoin: два гомоморфизма равны, если они совпадают на генераторах.

LaTeX

$$$\\text{ext}_{\\operatorname{adjoin}}(s)$$$

Lean4

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

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