natTrans_ext — Mathlib

English

A reiterated form of NatTrans_ext: whiskering preserves equality of natural transformations from Quotient functors.

Русский

Повторная формулировка NatTrans_ext: ослабление сохранено под-whiskering.

LaTeX

$$$\forall F,G: Quotient(r) \to D,\; \tau_1,\tau_2:\, F \Rightarrow G\;\text{— если } \, \mathrm{whiskerLeft}(\mathrm{Quotient.functor}\ r)\tau_1 = \mathrm{whiskerLeft}(\mathrm{Quotient.functor}\ r)\tau_2, \text{ то } \tau_1 = \tau_2.$$$

Lean4

theorem natTrans_ext {F G : Quotient r ⥤ D} (τ₁ τ₂ : F ⟶ G)
    (h : whiskerLeft (Quotient.functor r) τ₁ = whiskerLeft (Quotient.functor r) τ₂) : τ₁ = τ₂ :=
  NatTrans.ext (by ext1 ⟨X⟩; exact NatTrans.congr_app h X)

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