ι_mapBifunctorComp₂₃MapObjIso_inv

English

Equality of ιMapBifunctorBifunctor₂₃MapObj when second index matches via hpq.

Русский

Равенство ιMapBifunctorBifunctor₂₃MapObj при совпадении второго индекса через hpq.

LaTeX

$$$$ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i_1 i_2 i_3 j h = (F.obj (X_1 i_1)).map (ιMapBifunctorMapObj G₂₃ ρ₂₃.p X_2 X_3 i_2 i_3 i_2₃ h₂₃) ≫ ιMapBifunctorMapObj F ρ₂₃.q X_1 (mapBifunctorMapObj G₂₃ ρ₂₃.p X_2 X_3) i_1 i₂₃ j (by rw [← h, ← h₂₃, ← ρ₂₃.hpq])$$$$

Lean4

@[reassoc (attr := simp)]
theorem ι_mapBifunctorComp₂₃MapObjIso_inv (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) :
    ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫
        (mapBifunctorComp₂₃MapObjIso F G₂₃ ρ₂₃ X₁ X₂ X₃).inv j =
      ιMapTrifunctorMapObj (bifunctorComp₂₃ F G₂₃) r X₁ X₂ X₃ i₁ i₂ i₃ j h :=
  CofanMapObjFun.inj_iso_hom (isColimitCofan₃MapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ j) _ h

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