ofHom — Mathlib

English

Equality of ofHom representations agrees with the concrete category carrier representation.

Русский

Равенство представлений ofHom соответствует представлению носителя в конкретной структуре.

LaTeX

$$$MonCat.ofHom(f) = MonCat.instConcreteCategoryMonoidHomCarrier.ofHom(f).$$$

Lean4

/-- Typecheck a `MonoidHom` as a morphism in `MonCat`. -/
@[to_additive /-- Typecheck an `AddMonoidHom` as a morphism in `AddMonCat`. -/
    ]
abbrev ofHom {X Y : Type u} [Monoid X] [Monoid Y] (f : X →* Y) : of X ⟶ of Y :=
  ConcreteCategory.ofHom (C := MonCat) f

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