English
Let S be a commutative semiring, R a semiring, and M an additive commutative monoid with compatible S- and R-structures so that TrivSqZeroExt S R M exists. The canonical lift construction built from the injections inlAlgHom and inrHom acts as the identity on the base algebra homomorphism when evaluated on the canonical injections. In particular, applying lift to the standard injections yields the identity map on the trivial square-zero extension.
Русский
Пусть S — коммутативная полугруппа, R — полугруппа, M — аддитивная коммутативная моноидная структура с совместимыми S- и R-смулениями, так что существует тривиальное квадрат-zero расширение TrivSqZeroExt S R M. Обычное построение лифта, получаемое из вложений inlAlgHom и inrHom, действует как тождественный отображение на базовом алгебраическом отображении: при применении лифта к каноническим вложениям получаем тождественный гомоморфизм.
LaTeX
$$$\\ lift\\ (inlAlgHom\\ S\\ R\\ M)\\ (inrHom\\ R\\ M|.restrictScalars\\ S)\\ (inr\\_mul\\_inr\\ R)\\ (fun\\ _\\ _ => (inl\\_mul\\_inr\\ _\\ _).symm)\\ (fun\\ _\\ _ => (inr\\_mul\\_inl\\ _\\ _).symm) = AlgHom.id S (tsze R M) $$$
Lean4
/-- When applied to `inr` and `inl` themselves, `lift` is the identity. -/
@[simp]
theorem lift_inlAlgHom_inrHom :
lift (inlAlgHom _ _ _) (inrHom R M |>.restrictScalars S) (inr_mul_inr R) (fun _ _ => (inl_mul_inr _ _).symm)
(fun _ _ => (inr_mul_inl _ _).symm) =
AlgHom.id S (tsze R M) :=
algHom_ext' (lift_comp_inlHom _ _ _ _ _) (lift_comp_inrHom _ _ _ _ _)
