lift_algHom_comp_left — Mathlib

English

The pushout descent composed with the left map recovers f.

Русский

Опускание через пушаут и композиция с левой стрелкой восстанавливают отображение f.

LaTeX

$$ (Algebra.pushoutDesc S' f g H).comp (toAlgHom R S S') = f$$

Lean4

theorem lift_algHom_comp_left [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 S S') = f :=
  AlgHom.ext fun x => (Algebra.pushoutDesc_left S' f g H x :)

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