English
In a three-object diagram with pushout on the left, the whole rectangle is a pushout iff the right square is a pushout.
Русский
В диаграмме из трёх объектов слева пушаут, вся правая часть диаграммы является пушаутом тогда и только тогда, когда правая подплощадь пушаут.
LaTeX
$$Algebra.IsPushout.comp_iff$$
Lean4
@[ext (iff := false)]
theorem algHom_ext [H : Algebra.IsPushout R S R' S'] {A : Type*} [Semiring A] [Algebra R A] {f g : S' →ₐ[R] A}
(h₁ : f.comp (toAlgHom R R' S') = g.comp (toAlgHom R R' S'))
(h₂ : f.comp (toAlgHom R S S') = g.comp (toAlgHom R S S')) : f = g :=
by
ext x
refine H.1.inductionOn x _ ?_ ?_ ?_ ?_
· simp only [map_zero]
· exact AlgHom.congr_fun h₁
· intro s s' e
rw [Algebra.smul_def, map_mul, map_mul, e]
congr 1
exact (AlgHom.congr_fun h₂ s :)
· intro s₁ s₂ e₁ e₂
rw [map_add, map_add, e₁, e₂]
