natTrans₃_ext — Mathlib

English

Again, a standard extensionality principle for natural transformations in the localized/trifunctor setting.

Русский

Еще одно экзистенциальное принципиальное свойство экстенсивности для натрансформаций в локализованной/трёхфункторной среде.

LaTeX

$$$\forall\; {\tau,\tau'}:\ F_1'\to F_2',\; (\forall X_1,X_2,X_3,\; \text{components coincide}) \Rightarrow \tau=\tau'$$$

Lean4

theorem natTrans₃_ext {τ τ' : F₁' ⟶ F₂'}
    (h :
      ∀ (X₁ : C₁) (X₂ : C₂) (X₃ : C₃),
        ((τ.app (L₁.obj X₁)).app (L₂.obj X₂)).app (L₃.obj X₃) =
          ((τ'.app (L₁.obj X₁)).app (L₂.obj X₂)).app (L₃.obj X₃)) :
    τ = τ' :=
  uncurry₃.map_injective (natTrans_ext (L₁.prod (L₂.prod L₃)) (W₁.prod (W₂.prod W₃)) (fun _ ↦ h _ _ _))

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