natTrans_ext — Mathlib

English

Two natural transformations to CatPullback objects are equal if they agree after whiskering with the projection functors on both sides.

Русский

Два натуральных преобразования в CatPullback-объекты равны, если они совпадают после взвешивания с проекциями по обе стороны.

LaTeX

$$$\\text{natTrans}_{J,K}(\\alpha, \\beta)\\;\\Rightarrow\\; \\alpha = \\beta$ по компонентам.$$

Lean4

/-- To check equality of two natural transformations of functors to a `CategoricalPullback`, it
suffices to do so after whiskering with the projections. -/
@[ext]
theorem natTrans_ext {J K : X ⥤ F ⊡ G} {α β : J ⟶ K} (e₁ : whiskerRight α (π₁ F G) = whiskerRight β (π₁ F G))
    (e₂ : whiskerRight α (π₂ F G) = whiskerRight β (π₂ F G)) : α = β :=
  by
  ext x
  · exact congrArg (fun t ↦ t.app x) e₁
  · exact congrArg (fun t ↦ t.app x) e₂

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