pushoutDesc_right — Mathlib

English

Similarly, the pushout descent composed with the right map recovers g.

Русский

Аналогично композиция pushoutDesc с правой стрелкой восстанавливает g.

LaTeX

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

Lean4

@[simp]
theorem pushoutDesc_right [Algebra.IsPushout R S R' S'] {A : Type*} [Semiring A] [Algebra R A] (f : S →ₐ[R] A)
    (g : R' →ₐ[R] A) (H) (x : R') : Algebra.pushoutDesc S' f g H (algebraMap R' S' x) = g x := by
  simp [Algebra.pushoutDesc_apply, Algebra.IsPushout.equiv_symm_algebraMap_right]

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