functorMap — Mathlib

English

There is a canonical family of transition maps between successive levels of the sequential product, forming a natural transformation that encodes how the first step relates to the previous one.

Русский

Существует каноническая последовательность переходных отображений между последовательными уровнями произведения, образующая естественную трансформацию, описывающую как первый шаг связан с предшествующим.

LaTeX

$$$\\mathrm{functorMap}: \\forall n, \\mathrm{functorObj}\\ M\\ N\\ (n+1) \\longrightarrow \\mathrm{functorObj}\\ M\\ N\\ n$$$

Lean4

/-- The transition maps in the sequential limit of products -/
noncomputable def functorMap : ∀ n, functorObj M N (n + 1) ⟶ functorObj M N n :=
  by
  intro n
  refine
    Limits.Pi.map fun m ↦
      if h : m < n then eqToHom ?_ else if h' : m < n + 1 then eqToHom ?_ ≫ f m ≫ eqToHom ?_ else eqToHom ?_
  all_goals split_ifs; try rfl; try cutsat

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