ι_mapBifunctorBifunctor₂₃Desc

English

Canonical isomorphism between the trifunctor action and the sequential bifunctor actions on graded objects.

Русский

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

LaTeX

$$$$mapTrifunctorMapObj (bifunctorComp₂₃ F G₂₃) r X_1 X_2 X_3 \cong mapBifunctorMapObj F ρ₂₃.q X_1 (mapBifunctorMapObj G₂₃ ρ₂₃.p X_2 X_3).$$$$

Lean4

@[reassoc (attr := simp)]
theorem ι_mapBifunctorBifunctor₂₃Desc (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : r ⟨i₁, i₂, i₃⟩ = j) :
    ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ mapBifunctorBifunctor₂₃Desc f = f i₁ i₂ i₃ h :=
  Cofan.IsColimit.fac (isColimitCofan₃MapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ j) _ ⟨_, h⟩

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