of — Mathlib · SciLib

English

Construction of an object in BialgCat(R) from an R-bialgebra: given X with ring structure and Bialgebra R-X, form the BialgCat object whose carrier is X.

Русский

Построение объекта в BialgCat(R) из биналгебры: у X есть кольцо и структур биналгебры, образуется объект в BialgCat с носителем X.

LaTeX

$$$$ \text{of}(R,X) \text{ defines an object of } \text{BialgCat}(R) \text{ with carrier } X. $$$$

Lean4

/-- The object in the category of `R`-bialgebras associated to an `R`-bialgebra. -/
@[simps]
def of (X : Type v) [Ring X] [Bialgebra R X] : BialgCat R where carrier := X

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