toLinearMap_ofAlgEquiv — Mathlib

English

For an AlgEquiv f: A ≃ₐ[R] B together with counit_comp and map_comp_comul, the linear map underlying the corresponding coalgebra equivalence equals f.

Русский

Для AlgEquiv f: A ≃ₐ[R] B при counit_comp и map_comp_comul линейное отображение, соответствующее коалгебраической эквивалентности, равно f.

LaTeX

$$$(\\text{ofAlgEquiv } f\\; counit\\_comp\\; map\\_comp\\_comul) : A \\to_{\\ell} B = f$$$

Lean4

@[simp]
theorem toLinearMap_ofAlgEquiv (f : A ≃ₐ[R] B) (counit_comp map_comp_comul) :
    (ofAlgEquiv f counit_comp map_comp_comul : A →ₗ[R] B) = f :=
  rfl

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