natTransExtension_hcomp — Mathlib

English

Let W.Q be the localization functor associated with a localization, and let τ be a natural transformation between the composite functors W.Q ⋙ F and W.Q ⋙ G. Then the left whiskering of the identity on W.Q with natTransExtension τ equals τ itself.

Русский

Пусть W.Q является локализационной функторной конструкцией, связанной с локализацией, и пусть τ — натуральное преобразование между композициями W.Q ⋙ F и W.Q ⋙ G. Тогда левое обезличенное взвешивание тождественным натуралным преобразованием на W.Q от natTransExtension(τ) равно τ.

LaTeX

$$$\mathrm{Id}_{W.Q} \;\diamond\; \operatorname{natTransExtension}(\tau) = \tau$$$

Lean4

theorem natTransExtension_hcomp {F G : W.Localization ⥤ D} (τ : W.Q ⋙ F ⟶ W.Q ⋙ G) : 𝟙 W.Q ◫ natTransExtension τ = τ :=
  by simp

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