English
Composition with the identity AlgHom leaves an AlgHom unchanged, and similarly the other side with identity yields the same map.
Русский
Сложение с идентичным AlgHom не меняет отображение, аналогично и слева-налево.
LaTeX
$$$\\text{comp\_id} : (\\text{AlgHom}.id R A).comp φ = φ$ and $\\text{id\_comp} : (\\text{AlgHom}.id R B).comp φ = φ$$$
Lean4
/-- If `φ₁` and `φ₂` are `R`-algebra homomorphisms with the
domain of `φ₁` equal to the codomain of `φ₂`, then
`φ₁.comp φ₂` is the algebra homomorphism `x ↦ φ₁ (φ₂ x)`.
-/
def comp (φ₁ : B →ₐ[R] C) (φ₂ : A →ₐ[R] B) : A →ₐ[R] C :=
{ φ₁.toRingHom.comp ↑φ₂ with commutes' := fun r : R => by rw [← φ₁.commutes, ← φ₂.commutes]; rfl }
