of — Mathlib · SciLib

English

In the category of R-algebras, composing morphisms corresponds to function composition on the underlying carriers.

Русский

В категории R-алгебр компоновка морфизмов соответствует композиции функций между базовыми носителями.

LaTeX

$$$\forall f:\, A \to B,\ g:\, B \to C,\ a:\, A,\ (f \;\ggg\; g)\; a = g(f(a))$$$

Lean4

/-- The object in the category of R-algebras associated to a type equipped with the appropriate
typeclasses. This is the preferred way to construct a term of `AlgCat R`. -/
abbrev of (X : Type v) [Ring X] [Algebra R X] : AlgCat.{v} R :=
  ⟨X⟩

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