subsingleton — Mathlib

English

If the lattice of subalgebras of A has only one element, then there is at most one AlgHom from A to any B.

Русский

Если множество подпалгебр A имеет единственный элемент, то существует не более одного AlgHom из A в B.

LaTeX

$$$ \\text{AlgHom.subsingleton} : [\\mathrm{Subsingleton} (\\mathrm{Subalgebra} R A)] \\Rightarrow \\mathrm{Subsingleton} (A \\to_{R} B) $$$

Lean4

instance _root_.AlgHom.subsingleton [Subsingleton (Subalgebra R A)] : Subsingleton (A →ₐ[R] B) :=
  ⟨fun f g =>
    AlgHom.ext fun a =>
      have : a ∈ (⊥ : Subalgebra R A) := Subsingleton.elim (⊤ : Subalgebra R A) ⊥ ▸ mem_top
      let ⟨_x, hx⟩ := Set.mem_range.mp (mem_bot.mp this)
      hx ▸ (f.commutes _).trans (g.commutes _).symm⟩

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