mapBifunctorObjSingle₀ObjIso — Mathlib

English

The hom component of the iso composed with the ι-map equals the canonical ι-map value.

Русский

Гомоморфизм изоморфизма, композиция с ι-отображением равна каноническому значению ι-маршрута.

LaTeX

$$$$ιMapTrifunctorMapObj (bifunctorComp₂₃ F G₂₃) r X_1 X_2 X_3 i_1 i_2 i_3 j h \; \circ \; (mapBifunctorComp₂₃MapObjIso F G₂₃ ρ₂₃ X_1 X_2 X_3).hom j = ιMapBifunctor₁₂BifunctorMapObj F G₂₃ ρ₂₃ X_1 X_2 X_3 i_1 i_2 i_3 j h.$$$$

Lean4

/-- Given `F : C ⥤ D ⥤ D`, `X : C`, `e : F.obj X ≅ 𝟭 D` and `Y : GradedObject J D`,
this is the isomorphism `((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y a ≅ Y a.2`
when `a : I × J` is such that `a.1 = 0`. -/
@[simps!]
noncomputable def mapBifunctorObjSingle₀ObjIso (a : I × J) (ha : a.1 = 0) :
    ((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y a ≅ Y a.2 :=
  (F.mapIso (singleObjApplyIsoOfEq _ X _ ha)).app _ ≪≫ e.app (Y a.2)

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