algHom_ext'' — Mathlib

English

If two unitization morphisms φ, ψ from Unitization R A to C agree after precomposing with the canonical inr embedding, then φ = ψ.

Русский

Если две отображения типа Unitization R A →ₐ[R] C совпадают после предварительного композиционирования с inrNonUnitalAlgHom(R,A), то они равны.

LaTeX

$$$(∀ a\in A)\; φ(\mathrm{inr}(a))=ψ(\mathrm{inr}(a)) \Rightarrow φ=ψ.$$$

Lean4

theorem algHom_ext'' {F : Type*} [FunLike F (Unitization R A) C] [AlgHomClass F R (Unitization R A) C] {φ ψ : F}
    (h : ∀ a : A, φ a = ψ a) : φ = ψ :=
  algHom_ext h (fun r => by simp only [AlgHomClass.commutes])

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