Arrows that compose · The Lumenary

1

问题

What do functions between sets, maps between groups and continuous maps between shapes have in common? What if we studied only the arrows?

先动手做实验，再往下读。探索没有错误的方式。

2

实验

可以复合的箭头

点击箭头来构造一条路径。每条路径都复合成一个箭头——括号怎么加都无所谓。

你的复合箭头

点击任意一个箭头开始。

给 h ∘ g ∘ f 加括号的两种方式

x	(g∘f)(x)	h((g∘f)(x))	(h∘g)(f(x))
1	x	1	1
2	z	0	0
3	x	1	1

最后两列总是一致：h ∘ (g ∘ f) = (h ∘ g) ∘ f。这就是结合律。

3

提示（如果你需要）

4

这是怎么回事

Every path of arrows in the experiment composed to a single arrow, the identity arrows changed nothing, and the two ways of bracketing $h \circ g \circ f$ always agreed. These are exactly the laws that define a category:

a collection of objects;
for any two objects $X, Y$ , a collection of arrows (or morphisms) $X \to Y$ ;
a composition of arrows $X \to Y$ and $Y \to Z$ into an arrow $X \to Z$ ;
an identity arrow on every object;

such that composition is associative and identities are neutral.

Here is that definition in Lean. Our version writes composition in "diagrammatic" order — first the left arrow, then the right — the same convention Mathlib uses for its ≫ notation:

CategoryLean 4已形式化验证

/-- A **category** has objects, and for any two objects `X` and `Y` a type `Hom X Y` of
morphisms (arrows) from `X` to `Y`, together with
* an identity arrow `id X : Hom X X` for every object, and
* composition: from `f : Hom X Y` and `g : Hom Y Z` we get `comp f g : Hom X Z`,
such that identities do nothing (`id_comp`, `comp_id`) and composition is associative.

**Order of composition:** `comp f g` means "first `f`, then `g`" (diagrammatic order).
Mathlib uses the same order and writes it `f ≫ g`; ordinary function composition `g ∘ f`
lists the same two steps the other way round. -/
class Category.{v₁, u₁} (Obj : Type u₁) : Type (max u₁ (v₁ + 1)) where
  /-- The arrows from `X` to `Y`. -/
  Hom : Obj → Obj → Type v₁
  /-- The identity arrow on `X`. -/
  id : (X : Obj) → Hom X X
  /-- `comp f g`: first `f`, then `g`. -/
  comp : {X Y Z : Obj} → Hom X Y → Hom Y Z → Hom X Z
  /-- Doing nothing first changes nothing. -/
  id_comp : ∀ {X Y : Obj} (f : Hom X Y), comp (id X) f = f
  /-- Doing nothing afterwards changes nothing. -/
  comp_id : ∀ {X Y : Obj} (f : Hom X Y), comp f (id Y) = f
  /-- Composing three arrows does not depend on the bracketing. -/
  assoc : ∀ {W X Y Z : Obj} (f : Hom W X) (g : Hom X Y) (h : Hom Y Z),
    comp (comp f g) h = comp f (comp g h)

使用的公理: 未使用公理formal/Lumenary/Category.lean在 Lean 网页编辑器中试一试

Sets with functions form a category. So do groups with group homomorphisms, vector spaces with linear maps, and topological spaces with continuous maps. Even a single monoid is a category, with one object whose arrows are the monoid's elements:

monoidAsCategoryLean 4已形式化验证

/-- **A monoid is a category with one object.** Take a single object (the only element of
`Unit`); its arrows are the elements of `M`; composing arrows is multiplying; the identity
arrow is `one`. The category laws are exactly the monoid laws.
(Declared with `abbrev` so that Lean can unfold it when it is used as an instance.) -/
abbrev monoidAsCategory {M : Type u} (m : Monoid' M) : Category.{u, 0} Unit where
  Hom _ _ := M
  id _ := m.one
  comp f g := m.mul f g
  id_comp f := m.one_mul f
  comp_id f := m.mul_one f
  assoc f g h := m.mul_assoc f g h

使用的公理: 未使用公理formal/Lumenary/Category.lean在 Lean 网页编辑器中试一试

Once many areas of mathematics are seen as categories, we can compare them with arrows too. A structure-preserving map between categories is called a functor. Category theory, introduced by Samuel Eilenberg and Saunders Mac Lane in 1945, is the study of these patterns — and it has become a common language for algebra, topology, logic and the theory of programming languages.

已形式化验证 · 3 Lean已通过计算测试AI 起草 · 等待人工审校

5

问题

实验

提示（如果你需要）

这是怎么回事

由此通向何处