functorObjProj_pos — Mathlib

English

If m < n, there is a natural projection from the level-n sequential product to the m-th factor M_m, realized by the corresponding Pi-projection and the canonical identification of the level-n object with the product.

Русский

Если m < n, существует естественная проекция из уровня-n sequential product на m-й фактор M_m, реализованная через соответствующую Pi-проекцию и каноническое равенство между объектами.

LaTeX

$$$\\forall n,m:\\mathbb{N},\\; m < n \\Rightarrow f_{n\\to m}:\\mathrm{functorObj}\\ M\\ N\\ n \\longrightarrow M_m\\quad(=\\mathrm{Pi}.\\pi_m\\,_{(\\text{functorObj } M N n)})$$$

Lean4

/-- The projection map from `functorObj M N n` to `M m`, when `m < n` -/
noncomputable def functorObjProj_pos (n m : ℕ) (h : m < n) : functorObj M N n ⟶ M m :=
  Pi.π (fun m ↦ if _ : m < n then M m else N m) m ≫ eqToHom (functorObj_eq_pos (by cutsat))

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