ofHom_comp — Mathlib

English

Let f: X →ₐ[R] Y and g: Y →ₐ[R] Z be algebra homomorphisms. The morphism corresponding to their composition under ofHom is the composition of the images: ofHom(g ∘ f) = ofHom(f) ∘ ofHom(g).

Русский

Пусть f: X →ₐ[R] Y и g: Y →ₐ[R] Z — алгебраические гомоморфизмы. Морфизм их композиции через ofHom равен композиции образов: ofHom(g ∘ f) = ofHom(f) ∘ ofHom(g).

LaTeX

$$$\\operatorname{ofHom}(g \\circ f) = \\operatorname{ofHom}(f) \\circ \\operatorname{ofHom}(g)$$$

Lean4

@[simp]
theorem ofHom_comp {X Y Z : Type v} [Ring X] [Ring Y] [Ring Z] [Algebra R X] [Algebra R Y] [Algebra R Z] (f : X →ₐ[R] Y)
    (g : Y →ₐ[R] Z) : ofHom (g.comp f) = ofHom f ≫ ofHom g :=
  rfl

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