symm_comp — Mathlib

English

Let e be a bialgebra equivalence A ≃ₐc[R] B. Then the inverse e^{-1} composed with e is the identity on A, i.e. e.symm ∘ e = id_A as a coalgebra morphism.

Русский

Пусть e — биалгебровая эквивалентность A ≃ₐc[R] B. Тогда обратная к ней e^{-1} последовательно с e дает тождественное отображение на A, т.е. e.symm ∘ e = id_A как коалгеброморфизм.

LaTeX

$$$(e^{-1} \\circ e) = \\mathrm{id}_A$$$

Lean4

@[simp]
theorem symm_comp (e : A ≃ₐc[R] B) : (e.symm : B →ₐc[R] A).comp e = .id R A :=
  BialgHom.coe_algHom_injective e.toAlgEquiv.symm_comp

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