left_tensor_tensorObj₃_ext — Mathlib

English

Inverse pentagon identity for associators in the graded setting, relating the inverses of associators to the tensorial structure.

Русский

Обратная пентагональная когерентность для ассоциатора в градуированной设, связывающая обратные ассоциаторы с тензорной структурой.

LaTeX

$$$$ \text{pentagon}^{-1} = \text{(appropriate inverse coherence equation)} $$$$

Lean4

@[ext (iff := false)]
theorem left_tensor_tensorObj₃_ext {j : I} {A : C} (Z : C) (f g : Z ⊗ tensorObj X₁ (tensorObj X₂ X₃) j ⟶ A)
    [H : HasGoodTensorTensor₂₃ X₁ X₂ X₃] [hZ : HasLeftTensor₃ObjExt Z X₁ X₂ X₃ j]
    (h :
      ∀ (i₁ i₂ i₃ : I) (h : i₁ + i₂ + i₃ = j),
        (_ ◁ ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) ≫ f = (_ ◁ ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) ≫ g) :
    f = g :=
  by
  refine
    (@isColimitOfPreserves C _ C _ _ _ _ ((curriedTensor C).obj Z) _
          (isColimitCofan₃MapBifunctorBifunctor₂₃MapObj (H := H) (j := j)) hZ).hom_ext
      ?_
  intro ⟨⟨i₁, i₂, i₃⟩, hi⟩
  exact h _ _ _ hi

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