lift_algHom_comp_right — Mathlib

English

Two algebra homomorphisms from a pushout S' to A are equal if they agree on both leg maps.

Русский

Два алгебра-гомоморфизма из пушаута равны, если они совпадают по обеим ногам.

LaTeX

$$AlgHom.ext$$

Lean4

theorem lift_algHom_comp_right [Algebra.IsPushout R S R' S'] {A : Type*} [Semiring A] [Algebra R A] (f : S →ₐ[R] A)
    (g : R' →ₐ[R] A) (H) : (Algebra.pushoutDesc S' f g H).comp (toAlgHom R R' S') = g :=
  AlgHom.ext fun x => (Algebra.pushoutDesc_right S' f g H x :)

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