subsingleton_hom — Mathlib

English

The hom-sets in the free monoidal category over C are subsingleton; any two morphisms between the same objects are equal due to normalization and naturality arguments.

Русский

Гом-множества в свободной моноидальной категории над C являются одноэлементными; любые два морфизма между одними и теми же объектами равны.

LaTeX

$$$ \forall X,Y \in F C, \; \#\mathrm{Hom}(X,Y) = 1 $$$

Lean4

/-- The monoidal coherence theorem. -/
instance subsingleton_hom : Quiver.IsThin (F C) := fun X Y =>
  ⟨fun f g => by
    have hfg : (fullNormalize C).map f = (fullNormalize C).map g := Subsingleton.elim _ _
    have hf := NatIso.naturality_2 (fullNormalizeIso.{u} C) f
    have hg := NatIso.naturality_2 (fullNormalizeIso.{u} C) g
    exact hf.symm.trans (Eq.trans (by simp only [Functor.comp_map, hfg]) hg)⟩

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