Φ_functor_map_ι_app — Mathlib

English

For localizer morphisms with functorial right resolutions, the Φ_functor maps ι-applications compatibly with the isomorphism i.

Русский

Для локализующих морфизмов с функциональными правыми резолюциями отображение ι-приложения совместимо с изоморфизмом i.

LaTeX

$$$\operatorname{Φ}_{\text{functorialRightResolutions}}\;: \; (ι i)_{\mathrm{app}} \mapsto i_{\mathrm{app}}$$$

Lean4

@[simp]
theorem Φ_functor_map_ι_app (X₁ : C₁) : Φ.functor.map ((ι i).app X₁) = i.app (Φ.functor.obj X₁) :=
  NatTrans.congr_app
    (((whiskeringRight C₁ C₁ C₂).obj Φ.functor).map_preimage (X := 𝟭 C₁) (Y := Φ.functor ⋙ ρ) (whiskerLeft Φ.functor i))
    X₁

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