Arrows that compose · The Lumenary

1

Swali

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

Fanya jaribio kabla ya kuendelea kusoma. Hakuna njia mbaya ya kuchunguza.

2

Jaribio

Mishale inayojumuika

Bofya mishale ili kujenga njia. Kila njia hujumuika kuwa mshale mmoja — na mabano hayajalishi kamwe.

Mshale wako wa mjumuisho

Anza kwa kubofya mshale wowote.

Njia mbili za kuweka mabano katika 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

Safu wima mbili za mwisho hukubaliana daima: h ∘ (g ∘ f) = (h ∘ g) ∘ f. Hiyo ndiyo sifa ya ushirikishi.

3

Vidokezo, ukivitaka

4

Kinachoendelea

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 4Imehakikiwa rasmi

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

Aksiomu zilizotumika: Hakuna aksiomuformal/Lumenary/Category.leanIjaribu katika kihariri cha Lean mtandaoni

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 4Imehakikiwa rasmi

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

Aksiomu zilizotumika: Hakuna aksiomuformal/Lumenary/Category.leanIjaribu katika kihariri cha Lean mtandaoni

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.

Imehakikiwa rasmi · 3 LeanImejaribiwa kikokotoziImeandaliwa na AI · inasubiri ukaguzi wa binadamu

5

Swali

Jaribio

Vidokezo, ukivitaka

Kinachoendelea

Hii inaelekea wapi