natTrans_hcomp_injective — Mathlib

English

If whiskering with the identity on W.Q sends two transformations τ1, τ2 to the same horizontal composite, then τ1 = τ2.

Русский

Если взвешивание по единице на W.Q отправляет две трансформации τ1, τ2 в одинаковый горизонтальный композиционный объект, то τ1 = τ2.

LaTeX

$$$\mathbb{1}_{W.Q} \;\diamond\; \tau_1 = \mathbb{1}_{W.Q} \;\diamond\; \tau_2 \;\Rightarrow\; \tau_1 = \tau_2$$$

Lean4

theorem natTrans_hcomp_injective {F G : W.Localization ⥤ D} {τ₁ τ₂ : F ⟶ G} (h : 𝟙 W.Q ◫ τ₁ = 𝟙 W.Q ◫ τ₂) : τ₁ = τ₂ :=
  by
  ext X
  have eq := (objEquiv W).right_inv X
  simp only [objEquiv] at eq
  rw [← eq, ← NatTrans.id_hcomp_app, ← NatTrans.id_hcomp_app, h]

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