mkHom — Mathlib

English

There is a canonical constructor to form a morphism in a product category from two morphisms in the factors.

Русский

Существует канонический конструктор для образования морфизма в произведении из двух морфизмов по компонентам.

LaTeX

$$$\text{mkHom}(f,g): (X_1,Y_1) \to (X_2,Y_2)$$$

Lean4

/-- Construct a morphism in a product category by giving its constituent components.
This constructor should be preferred over `Prod.mk`, because lean infers better the
source and target of the resulting morphism. -/
abbrev mkHom {X₁ X₂ : C} {Y₁ Y₂ : D} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) : (X₁, Y₁) ⟶ (X₂, Y₂) :=
  ⟨f, g⟩

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