objMap — Mathlib

English

There is a functorial map that sends a morphism φ: f ⟶ g in arrows to a morphism obj I κ f.hom ⟶ obj I κ g.hom, compatible with composition and identities.

Русский

Существует отображение-функтор, которое переводит морфизм φ между стрелками в морфизм между соответствующими объектами, совместимо с композициями и тождественными.

LaTeX

$${f g h : Arrow C} (φ : f ⟶ g) (ψ : g ⟶ h) : objMap I κ (φ ≫ ψ) = objMap I κ φ ≫ objMap I κ ψ$$

Lean4

/-- The functoriality of the intermediate object in the
factorization of the small object argument. -/
noncomputable def objMap {f g : Arrow C} (φ : f ⟶ g) : obj I κ f.hom ⟶ obj I κ g.hom :=
  ((iteration I κ).map φ).left

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