lift_comp_includeLeft — Mathlib

English

The lift with includeLeft and includeRight is the identity on A ⊗_R B.

Русский

Лифт с includeLeft и includeRight является тождественным отображением на A ⊗_R B.

LaTeX

$$$\\mathrm{lift}\\;\\mathrm{includeLeft}\\;\\mathrm{includeRight}\\; hfg = \\mathrm{id}_{S}(A \\otimes_R B).$$$

Lean4

@[simp]
theorem lift_comp_includeLeft (f : A →ₐ[S] C) (g : B →ₐ[R] C) (hfg : ∀ x y, Commute (f x) (g y)) :
    (lift f g hfg).comp includeLeft = f :=
  AlgHom.ext <| by simp

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