English
Two natural transformations from F to F' are equal if their whiskerings along inclLeft and inclRight are equal.
Русский
Два натуральных преобразования между F и F' равны, если их ослабления по inclLeft и inclRight совпадают.
LaTeX
$$$ \text{natTransExt}: \; \alpha = \beta \;\text{ if } \; (\mathrm{inclLeft}\ C D).\mathrm{whiskerLeft} \alpha = (\mathrm{inclLeft}\ C D).\mathrm{whiskerLeft} \beta \; \&\; (\mathrm{inclRight}\ C D).\mathrm{whiskerLeft} \alpha = (\mathrm{inclRight}\ C D).\mathrm{whiskerLeft} \beta $$$
Lean4
/-- Two natural transformations between functors out of a join are equal if they are so
after whiskering with the inclusions. -/
theorem natTrans_ext {F F' : C ⋆ D ⥤ E} {α β : F ⟶ F'}
(h₁ : whiskerLeft (inclLeft C D) α = whiskerLeft (inclLeft C D) β)
(h₂ : whiskerLeft (inclRight C D) α = whiskerLeft (inclRight C D) β) : α = β :=
by
ext t
cases t with
| left t => exact congrArg (fun x ↦ x.app t) h₁
| right t => exact congrArg (fun x ↦ x.app t) h₂
