ιMapBifunctorBifunctor₂₃MapObj_eq

English

Extensionality principle for ιMapBifunctorBifunctor₂₃MapObj: two morphisms from the same source that agree on all indices must be equal.

Русский

Принцип экстентности для ιMapBifunctorBifunctor₂₃MapObj: две стрелы из одного и того же источника, совпадающие на всех индексах, равны.

LaTeX

$$$$f = g \Rightarrow ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i_1 i_2 i_3 j h = ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i_1 i_2 i_3 j h$$$$

Lean4

@[reassoc]
theorem ιMapBifunctorBifunctor₂₃MapObj_eq (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) (i₂₃ : ρ₂₃.I₂₃)
    (h₂₃ : ρ₂₃.p ⟨i₂, i₃⟩ = i₂₃) :
    ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h =
      (F.obj (X₁ i₁)).map (ιMapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃ i₂ i₃ i₂₃ h₂₃) ≫
        ιMapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) i₁ i₂₃ j (by rw [← h, ← h₂₃, ← ρ₂₃.hpq]) :=
  by
  subst h₂₃
  rfl

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