ι_mapBifunctor₁₂BifunctorDesc

English

There is a constructor for morphisms from the object mapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j, i.e. a canonical arrow from that object to A given by a family of arrows f.

Русский

Существует конструктор морфизмов из объекта mapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j, то есть каноническая стрелка в A, задаваемая семейством стрелок f.

LaTeX

$$$$mapBifunctorBifunctor₂₃Desc\;: \; mapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j \to A.$$$$

Lean4

@[reassoc (attr := simp)]
theorem ι_mapBifunctor₁₂BifunctorDesc (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : r ⟨i₁, i₂, i₃⟩ = j) :
    ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ mapBifunctor₁₂BifunctorDesc f = f i₁ i₂ i₃ h :=
  Cofan.IsColimit.fac (isColimitCofan₃MapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ j) _ ⟨_, h⟩

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