lift_lsmul_comp_counit_comp_comul

English

The composed map of lift and lsmul with counit and comul equals the identity map on the tensor product.

Русский

Слоение lift, lsmul с counit и comul даёт тождественную карту на тензорном произведении.

LaTeX

$$$\\mathrm{TensorProduct}.lift(\\mathrm{.lsmul}\\;\\mathrm{R}\\;\\mathrm{A} \\circ\\mathrm{counit}) \\circ\\mathrm{\\;$, ...} = \\mathrm{id}$$$

Lean4

theorem lift_lsmul_comp_counit_comp_comul : TensorProduct.lift (.lsmul R A ∘ₗ counit) ∘ₗ comul = .id :=
  by
  have := rTensor_counit_comp_comul (R := R) (A := A)
  apply_fun (TensorProduct.lift (LinearMap.lsmul R A) ∘ₗ ·) at this
  rw [LinearMap.rTensor, ← LinearMap.comp_assoc, TensorProduct.lift_comp_map, LinearMap.compl₂_id] at this
  ext
  simp [this]

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