comp_ofId — Mathlib

English

For any algebra hom φ: A →ₐ[R] B, composing with the identity embedding recovers the other identity embedding: φ ∘ ofId_R_A = ofId_R_B.

Русский

Для любого гомоморфизма φ: A →ₐ[R] B композиция с алгебраической вставкой от R в A возвращает вставку от R в B: φ ∘ ofId_R_A = ofId_R_B.

LaTeX

$$$ φ \\circ (\\mathrm{ofId}\\; R\\; A) = (\\mathrm{ofId}\\; R\\; B) $$$

Lean4

@[simp]
theorem comp_ofId (φ : A →ₐ[R] B) : φ.comp (Algebra.ofId R A) = Algebra.ofId R B := by ext

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