lift_comp_inlHom — Mathlib

English

Uniqueness of AlgHom from TrivSqZeroExt given prescribed behavior on inl/inr.

Русский

Единственность AlgHom из TrivSqZeroExt при заданном поведении на inl/inr.

LaTeX

$$$ \\text{algHom\_ext'} \\;\\text{provides uniqueness given inl/inr data}$$$

Lean4

@[simp]
theorem lift_comp_inlHom (f : R →ₐ[S] A) (g : M →ₗ[S] A) (hg : ∀ x y, g x * g y = 0)
    (hfg : ∀ r x, g (r •> x) = f r * g x) (hgf : ∀ r x, g (x <• r) = g x * f r) :
    (lift f g hg hfg hgf).comp (inlAlgHom S R M) = f :=
  AlgHom.ext <| lift_apply_inl f g hg hfg hgf

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