الانتقال إلى المحتوى
The Lumenary
مسار الدهشةاختياري · لا يُقيَّم أبدًاينطلق من Composition

Arrows that compose

هذه الصفحة غير مترجمة بعدُ إلى العربية، لذلك تُعرض باللغة English.

ساعد في الترجمة →
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

التجربة

أسهم تتركّب

انقر على الأسهم لتبني مسارًا. كل مسار يتركّب في سهم واحد — والأقواس لا تهمّ أبدًا.

fghAidABidBCidCDidD

السهم المركّب

ابدأ بالنقر على أي سهم.

طريقتان لوضع الأقواس في ⁦h ∘ g ∘ f⁩

x(g∘f)(x)h((g∘f)(x))(h∘g)(f(x))
1x11
2z00
3x11

يتفق العمودان الأخيران دائمًا: ⁦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∘g∘fh \circ g \circ f always agreed. These are exactly the laws that define a category:

    • a collection of objects;
    • for any two objects X,YX, Y, a collection of arrows (or morphisms) X→YX \to Y;
    • a composition of arrows X→YX \to Y and Y→ZY \to Z into an arrow X→ZX \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مُختبَر حاسوبيًاصاغه الذكاء الاصطناعي · بانتظار المراجعة البشرية
    5

    إلى أين يقود هذا

    العودة إلى Compositionجميع مسارات الدهشة