isoEquivBialgEquiv — Mathlib

English

There is an equivalence between isomorphisms in CommBialgCat and BialgEquiv between the underlying X and Y.

Русский

Существует эквиваленция между изоморфизмами в CommBialgCat и BialgEquiv между базовыми X и Y.

LaTeX

$$$ (\mathrm{Iso}(\mathrm{CommBialgCat})(\mathrm{of}\,R X, \mathrm{of}\,R Y)) \simeq (X \simeq_{\mathrm{R-bialg}} Y)$$$

Lean4

/-- Bialgebra equivalences between `Bialgebra`s are the same as isomorphisms in `CommBialgCat`. -/
@[simps]
def isoEquivBialgEquiv : (of R X ≅ of R Y) ≃ (X ≃ₐc[R] Y)
    where
  toFun := bialgEquivOfIso
  invFun := isoMk
  left_inv _ := rfl
  right_inv _ := rfl

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