Arrows that compose · The Lumenary

1

La pregunta

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

Prueba el experimento antes de seguir leyendo. No hay una forma equivocada de explorar.

2

Experimento

Flechas que se componen

Haz clic en las flechas para construir un camino. Todo camino se compone en una sola flecha, y los paréntesis nunca importan.

Tu composición

Empieza haciendo clic en cualquier flecha.

Dos formas de poner paréntesis en 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

Las dos últimas columnas siempre coinciden: h ∘ (g ∘ f) = (h ∘ g) ∘ f. Eso es la asociatividad.

3

Pistas, si las quieres

4

Qué está pasando

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 4Verificado formalmente

/-- 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)

Axiomas utilizados: Ningún axiomaformal/Lumenary/Category.leanPruébalo en el editor web de 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 4Verificado formalmente

/-- **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

Axiomas utilizados: Ningún axiomaformal/Lumenary/Category.leanPruébalo en el editor web de 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.

Verificado formalmente · 3 LeanProbado computacionalmenteRedactado con IA · pendiente de revisión humana

5

La pregunta

Experimento

Pistas, si las quieres

Qué está pasando

Adónde lleva esto