hom_ext — Mathlib

English

Two 2-morphisms out of a left Kan extension are equal if their compositions with each triangle 2-morphism are equal.

Русский

Два 2-морфизма из левого кан-расширения равны, если их композиции с каждым треугольным 2-морфизмом равны.

LaTeX

$$$\forall \; H : \text{IsKan } t, \; \forall k, \; \forall \tau,\tau': t.extension \to k,\; (t.unit \; \circ f \triangleleft \tau) = (t.unit \; \circ f \triangleleft \tau') \Rightarrow \tau = \tau'.$$$

Lean4

/-- Two 2-morphisms out of a left Kan extension are equal if their compositions with
each triangle 2-morphism are equal. -/
theorem hom_ext (H : IsKan t) {k : b ⟶ c} {τ τ' : t.extension ⟶ k} (w : t.unit ≫ f ◁ τ = t.unit ≫ f ◁ τ') : τ = τ' :=
  StructuredArrow.IsUniversal.hom_ext H w

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