mapBifunctorBifunctor₂₃MapObj_ext

English

The two descriptive morphisms built from the cofan coincide with the componentwise description on X and h.

Русский

Два отображения desc, построенные из кокона, совпадают с поэлементным описанием для X и h.

LaTeX

$$$$ιMapBifunctor₂₃Desc f = f i_1 i_2 i_3 h$$$$

Lean4

@[ext]
theorem mapBifunctorBifunctor₂₃MapObj_ext
    {f g : mapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j ⟶ A}
    (h :
      ∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : r ⟨i₁, i₂, i₃⟩ = j),
        ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ f =
          ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ g) :
    f = g :=
  by
  apply Cofan.IsColimit.hom_ext (isColimitCofan₃MapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ j)
  rintro ⟨i, hi⟩
  exact h _ _ _ hi

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