hoFunctor₂_naturality — Mathlib

English

The naturality of the induced functor with respect to morphisms between truncated simplicial sets holds, i.e., the naturality square commutes.

Русский

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

LaTeX

$$$\\text{hoFunctor}_2\\text{_naturality}: f: X\\to Y \\Rightarrow (oneTruncation_2 \\circ Cat.freeRefl)\\map f \\;\\Rightarrow\\; \\mathrm{quotientFunctor}(Y) \\circ f = f \\circ \\mathrm{quotientFunctor}(X)$$$

Lean4

theorem hoFunctor₂_naturality {X Y : SSet.Truncated.{u} 2} (f : X ⟶ Y) :
    (oneTruncation₂ ⋙ Cat.freeRefl).map f ⋙ SSet.Truncated.HomotopyCategory.quotientFunctor Y =
      SSet.Truncated.HomotopyCategory.quotientFunctor X ⋙ mapHomotopyCategory f :=
  rfl

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