whiskerLeftFunctor — Mathlib

English

See above: whiskerLeft defines a way to precompose a ComposableArrows with a Fin-category functor.

Русский

См. выше: whiskerLeft задаёт способ предкомпозиции ComposableArrows с функтором Fin.

LaTeX

$$$$ \\text{whiskerLeft}: \\text{ComposableArrows} C m \\to (Fin(n+1) \\to Fin(m+1)) \\to \\text{ComposableArrows} C n $$$$

Lean4

/-- The functor `ComposableArrows C m ⥤ ComposableArrows C n` obtained by precomposition with
a functor `Fin (n + 1) ⥤ Fin (m + 1)`. -/
@[simps!]
def whiskerLeftFunctor (Φ : Fin (n + 1) ⥤ Fin (m + 1)) : ComposableArrows C m ⥤ ComposableArrows C n
    where
  obj F := F.whiskerLeft Φ
  map f := Functor.whiskerLeft Φ f

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