Composition · The Lumenary

引入H

One thing after another

To convert a price from Kenyan shillings to Indian rupees, a travel app might first convert shillings to US dollars, then dollars to rupees. To edit a photo, you might rotate it and then crop it. To make chapati, you mix, then knead, then roll, then cook.

Each step is a function, and doing them in sequence produces a new function. This act of chaining is called composition. It is one of the simplest ideas in mathematics — and, as we'll see, one of the deepest.

定义H

The composite of two functions

定义— composition

If $f : A \to B$ and $g : B \to C$ , their composite $g \circ f : A \to C$ is the function

(g \circ f)(x) = g\big(f(x)\big).

Read $g \circ f$ as " $g$ after $f$ ": apply $f$ first, then $g$ .

The composite only makes sense when the codomain of $f$ matches the domain of $g$ — the output of the first step must be a valid input for the second.

定义— identity function

For every set $A$ , the identity function $\mathrm{id}_A : A \to A$ is defined by $\mathrm{id}_A(x) = x$ . It does nothing — and that turns out to be important.

探索

Explore: composition machines

复合机器

让一个数依次通过两台机器。顺序重要吗？

第一台机器 f然后是机器 g输入 x = 3

g ∘ f先 f，后 g

3

加 1

x ↦ x + 1

→ 4

乘 2

x ↦ 2x

→ 8

f ∘ g先 g，后 f

3

乘 2

x ↦ 2x

→ 6

加 1

x ↦ x + 1

→ 7

结果不同：8 对 7。复合的顺序很重要。

例题讲解H

Worked examples

例— Order matters

Let $f(x) = x + 1$ and $g(x) = 2x$ , both from $\Z$ to $\Z$ . Then

(g \circ f)(x) = 2(x + 1) = 2x + 2, \qquad (f \circ g)(x) = 2x + 1.

At $x = 0$ these give $2$ and $1$ . So $g \circ f \neq f \circ g$ : composition is not commutative.

例— A three-step chain

Let $h(x) = x^2$ as well. Then $(h \circ g \circ f)(x) = h(g(f(x))) = \big(2(x + 1)\big)^2 = 4(x + 1)^2$ . At $x = 2$ : $f(2) = 3$ , $g(3) = 6$ , $h(6) = 36$ .

例— Undoing

Let $p(x) = x + 5$ and $q(x) = x - 5$ . Then $q \circ p = \mathrm{id}_\Z$ and $p \circ q = \mathrm{id}_\Z$ : each undoes the other. Functions like this are called inverses of one another.

证明H

The laws of composition

定理— associativity

For all $f : A \to B$ , $g : B \to C$ , $h : C \to D$ : $\quad h \circ (g \circ f) = (h \circ g) \circ f$ .

证明

Both sides are functions from $A$ to $D$ , so we compare them at an arbitrary $x \in A$ :

\big(h \circ (g \circ f)\big)(x) = h\big((g \circ f)(x)\big) = h\big(g(f(x))\big), \qquad \big((h \circ g) \circ f\big)(x) = (h \circ g)\big(f(x)\big) = h\big(g(f(x))\big).

They agree at every $x$ , so they are the same function.

∎

Because of associativity we can safely write $h \circ g \circ f$ with no brackets at all.

定理— identity laws

For every $f : A \to B$ : $\quad f \circ \mathrm{id}_A = f$ and $\mathrm{id}_B \circ f = f$ .

证明

$(f \circ \mathrm{id}_A)(x) = f(\mathrm{id}_A(x)) = f(x)$ and $(\mathrm{id}_B \circ f)(x) = \mathrm{id}_B(f(x)) = f(x)$ for every $x \in A$ .

∎

定理— composites of injections

If $f : A \to B$ and $g : B \to C$ are both injective, then $g \circ f$ is injective.

证明

Suppose $(g \circ f)(x) = (g \circ f)(y)$ , i.e. $g(f(x)) = g(f(y))$ . Since $g$ is injective, $f(x) = f(y)$ . Since $f$ is injective, $x = y$ .

∎

The same pattern of reasoning shows that composites of surjections are surjective, and therefore composites of bijections are bijective.

形式化数学F

Composition in Lean

In Lean, $g \circ f$ is written g ∘ f, and it is defined as fun x => g (f x). That makes associativity true by definition — Lean accepts the proof rfl, "both sides are literally the same":

comp_assocLean 4在此由基本事实证明已形式化验证

/-- Composition is **associative**: `h ∘ (g ∘ f) = (h ∘ g) ∘ f`.

Why does `rfl` prove it? By definition `(g ∘ f) = fun x => g (f x)`. Unfolding the
definition on both sides, each one becomes `fun x => h (g (f x))` — literally the same
function. Lean accepts `rfl` ("both sides are the same by definition") because its kernel
unfolds definitions and simplifies `(fun x => …) a` automatically. -/
theorem comp_assoc (f : α → β) (g : β → γ) (h : γ → δ) : h ∘ (g ∘ f) = (h ∘ g) ∘ f := rfl

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

id_compLean 4在此由基本事实证明已形式化验证

/-- Doing nothing first changes nothing: `id ∘ f = f`. Both sides send `x` to `f x`, and
Lean identifies `fun x => f x` with `f` (η-conversion), so `rfl` works. -/
theorem id_comp (f : α → β) : id ∘ f = f := rfl

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

comp_not_commLean 4在此由基本事实证明已形式化验证

/-- Composition is **not commutative**: "double, then add 1" differs from
"add 1, then double". At `0` the first gives `1` and the second gives `2`. -/
theorem comp_not_comm :
    (fun n : Int => n + 1) ∘ (fun n : Int => 2 * n) ≠ (fun n : Int => 2 * n) ∘ (fun n : Int => n + 1) := by
  intro h
  -- Evaluate both sides at `0`.
  have h0 : (2 * 0 + 1 : Int) = 2 * (0 + 1) := congrFun h 0
  -- But `2 * 0 + 1 = 1` and `2 * (0 + 1) = 2`.
  exact absurd h0 (by decide)

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

injective_compLean 4在此由基本事实证明已形式化验证

/-- A composite of injective functions is injective.
If `g (f a) = g (f b)`, injectivity of `g` gives `f a = f b`, and then injectivity of `f`
gives `a = b`. (Core analogue: `Function.Injective.comp`.) -/
theorem injective_comp {f : α → β} {g : β → γ} (hg : Injective g) (hf : Injective f) :
    Injective (g ∘ f) := by
  intro a b h
  -- `h : g (f a) = g (f b)`
  have hfab : f a = f b := hg h
  exact hf hfab

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

surjective_compLean 4在此由基本事实证明已形式化验证

/-- A composite of surjective functions is surjective.
To hit `c`, first find `b` with `g b = c`, then `a` with `f a = b`; then `g (f a) = c`.
(Core analogue: `Function.Surjective.comp`.) -/
theorem surjective_comp {f : α → β} {g : β → γ} (hg : Surjective g) (hf : Surjective f) :
    Surjective (g ∘ f) := by
  intro c
  obtain ⟨b, hb⟩ := hg c      -- `hb : g b = c`
  obtain ⟨a, ha⟩ := hf b      -- `ha : f a = b`
  refine ⟨a, ?_⟩
  show g (f a) = c
  rw [ha, hb]

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

计算C

Checking every function on a small set

Composing functions: associative, but order mattersPython有限穷举检验反例已通过计算测试

"""Composing finite functions: associativity, identities and order.

A function on a finite set X is stored as a dict {x: f(x)}. The composite
g o f ("g after f") sends x to g(f(x)). On the 3-element set X = {0, 1, 2} we
check associativity h o (g o f) = (h o g) o f for every triple of functions,
check the identity laws, and search for functions with g o f != f o g.

Runs unchanged in the browser (Pyodide) using only the standard library.
"""

from itertools import product
import textwrap

X = (0, 1, 2)

def all_functions(domain, codomain=None):
    """Return every function domain -> codomain (default: domain -> domain) as a dict."""
    domain = list(domain)
    codomain = domain if codomain is None else list(codomain)
    return [dict(zip(domain, values)) for values in product(codomain, repeat=len(domain))]

def identity(domain):
    """The identity function on ``domain``: every x goes to itself."""
    return {x: x for x in domain}

def compose(g, f):
    """Return g o f, the function x -> g(f(x)) ("first f, then g").

    Raises ValueError if some output of f is not an input of g, because then
    g o f is not defined.
    """
    missing = set(f.values()) - set(g)
    if missing:
        raise ValueError(f"g o f is undefined: g has no value at {sorted(missing)}")
    return {x: g[f[x]] for x in f}

def show(f):
    """Write a function on 0..n-1 as its list of values, e.g. [1, 0, 2] means 0->1, 1->0, 2->2."""
    return "[" + ", ".join(str(f[x]) for x in sorted(f)) + "]"

def check_associativity(functions):
    """Check h o (g o f) == (h o g) o f for all triples; return (triples, failures)."""
    triples = 0
    failures = []
    for f, g, h in product(functions, repeat=3):
        triples += 1
        if compose(h, compose(g, f)) != compose(compose(h, g), f):
            failures.append((f, g, h))
    return triples, failures

def check_identity_laws(functions, domain):
    """Check id o f == f == f o id for every f; return (functions_checked, failures)."""
    ident = identity(domain)
    failures = [f for f in functions if not (compose(ident, f) == f == compose(f, ident))]
    return len(functions), failures

def commuting_pairs(functions):
    """Return the list of ordered pairs (f, g) with g o f == f o g."""
    return [(f, g) for f, g in product(functions, repeat=2) if compose(g, f) == compose(f, g)]

def first_noncommuting_pair(functions):
    """Return the first ordered pair (f, g) with g o f != f o g, or None if all commute."""
    for f, g in product(functions, repeat=2):
        if compose(g, f) != compose(f, g):
            return f, g
    return None

def main():
    functions = all_functions(X)
    n = len(functions)
    print(f"X = {{0, 1, 2}} has 3^3 = {n} functions X -> X.")
    print("A function is written as its list of values: [1, 0, 2] means 0->1, 1->0, 2->2.")
    print("g o f means 'first f, then g': (g o f)(x) = g(f(x)).")
    print()
    triples, failures = check_associativity(functions)
    print(f"Associativity h o (g o f) = (h o g) o f: {triples} triples checked, {len(failures)} failures")
    checked, failures = check_identity_laws(functions, X)
    print(f"Identity laws id o f = f = f o id:     {checked} functions checked, {len(failures)} failures")
    print()
    f, g = first_noncommuting_pair(functions)
    print("But order matters. First pair found with g o f != f o g:")
    print(f"  f = {show(f)}   g = {show(g)}")
    print(f"  g o f = {show(compose(g, f))}   f o g = {show(compose(f, g))}")
    swap, cycle = {0: 1, 1: 0, 2: 2}, {0: 1, 1: 2, 2: 0}
    print("A friendlier pair: s = swap 0 and 1, r = rotate 0->1->2->0:")
    print(f"  s = {show(swap)}   r = {show(cycle)}")
    print(f"  r o s = {show(compose(cycle, swap))}   s o r = {show(compose(swap, cycle))}")
    pairs = commuting_pairs(functions)
    print(f"Only {len(pairs)} of the {n * n} ordered pairs commute.")
    print()
    print("Why associativity always holds: both sides send x to h(g(f(x))).")
    print()
    print(textwrap.fill(
        f"Epistemic status: all {triples} triples and all {n} functions on this "
        "3-element set were checked, a proof by exhaustion for this set only; the "
        "one-line argument above proves associativity for all functions. A single "
        "non-commuting pair is a genuine counterexample: composition is not "
        "commutative in general.",
        width=78,
    ))

if __name__ == "__main__":
    main()

完全在你的浏览器中、在一个隔离的工作线程里运行。不会向服务器发送任何内容。

与范畴论的联系H

The first category

Step back and look at what we have:

objects: sets $A, B, C, \dots$ ;
arrows between them: functions $f : A \to B$ ;
a way to compose arrows when they line up: $g \circ f$ ;
an identity arrow $\mathrm{id}_A$ for every object;

and two laws: composition is associative, and identities are neutral. Any collection of objects and arrows with these features is called a category. Sets and functions form the category usually called $\mathbf{Set}$ .

This is not just a new name. Groups with homomorphisms, vector spaces with linear maps, shapes with continuous maps, even the integers ordered by $\le$ — each of these forms a category, and theorems proved about categories in general apply to all of them at once.

In Lean, types and functions form a category in exactly this sense. The proofs of the laws are the ones you saw above:

typesCategoryLean 4已形式化验证

/-- **Types and functions form a category.** Objects are Lean types (in universe `u`),
arrows `X → Y` are functions, and `comp f g` is `g ∘ f` (first `f`, then `g`).
All three laws hold by `rfl` (see `Lumenary.Composition.comp_assoc` for why).

This is the category of Lean *types*, the type-theoretic analogue of the category **Set**
of sets and functions used in set-theoretic mathematics; Lean types are not ZFC sets, but
they play the same role here. (Mathlib analogue: `CategoryTheory.types`.) -/
instance typesCategory : Category.{u, u + 1} (Type u) where
  Hom X Y := X → Y
  id _ := fun x => x
  comp f g := g ∘ f
  id_comp _ := rfl
  comp_id _ := rfl
  assoc _ _ _ := rfl

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

这是类比，不是形式化构造

Our earlier "machines" picture is a helpful analogy, but a category is defined only by objects, arrows, composition, identities and the two laws. Many categories have arrows that are not functions at all — for example, in a category built from an ordered set, there is an arrow $a \to b$ exactly when $a \le b$ .

练习

Exercises

1. Composition

热身人类思维

Let $f(x) = x + 3$ and $g(x) = x^2$ . Compute $(g \circ f)(2)$ .

2. Composition

热身人类思维

If $f : A \to B$ and $g : B \to C$ , what are the domain and codomain of $g \circ f$ ?

选择一项

g \circ f : A \to C

g \circ f : B \to B

g \circ f : C \to A

3. Composition

核心人类思维

Let $f(x) = 3x$ and $g(x) = x - 2$ . Compute $(g \circ f)(4) - (f \circ g)(4)$ .

4. Composition

挑战人类思维

Suppose $g \circ f$ is injective. Which of these must be true? (Choose all that apply.)

选择所有符合的选项

f

is injective

g

is injective

g \circ f

is surjective

5. Composition

核心形式化

In Lean, comp_assoc is proved by rfl. What does that tell us?

选择一项

Both sides unfold, by definition, to the same function fun x => h (g (f x)).Lean checked associativity on many examples.Associativity is an axiom in Lean.

6. Composition

挑战计算

Finite functions can be stored as dictionaries. Write compose(g, f) returning a dictionary for $g \circ f$ (apply f first!). You may assume every value of f is a key of g.

完全在你的浏览器中、在一个隔离的工作线程里运行。不会向服务器发送任何内容。

常见误解H

Common misconceptions

误解

Reading $g \circ f$ as " $g$ first". It means $f$ first, then $g$ — the function written closest to $x$ in $g(f(x))$ acts first.

误解

"Composition is multiplication of formulas." $(g \circ f)(x)$ means substituting $f(x)$ into $g$ ; it is not $g(x) \cdot f(x)$ .

误解

"If $g \circ f$ is injective, both $f$ and $g$ must be." Only $f$ must be. Try $f : \{1\} \to \{1, 2\}$ with $f(1) = 1$ and $g : \{1, 2\} \to \{1\}$ : $g \circ f$ is injective, but $g$ is not.

误解

"Associative means commutative." Associativity is about brackets ( $h \circ (g \circ f)$ vs $(h \circ g) \circ f$ ); commutativity is about order. Composition has the first property but not the second.

探奇小径

Wonder Trails

探奇小径 · 可选 · 从不评分Arrows that composeWhat do functions between sets, maps between groups and continuous maps between shapes have in common? What if we studied only the arrows?踏上小径探奇小径 · 可选 · 从不评分The product, by its mapsCan you describe the set of pairs

A \times B

without ever looking inside it — only by how functions go into it?踏上小径

与集合论的联系H

Set-theoretic connection

In terms of graphs (sets of ordered pairs), the composite of $f \subseteq A \times B$ and $g \subseteq B \times C$ is

g \circ f = \{\, (a, c) \in A \times C \mid \text{there is } b \in B \text{ with } (a, b) \in f \text{ and } (b, c) \in g \,\}.

The same formula composes arbitrary relations, not just functions — and relations with this composition form another category, usually called $\mathbf{Rel}$ .

历史与全球视野

History and global context

Repeating and chaining transformations is old: geometers and astronomers combined rotations and reflections long before there was a word for composition.
In the 19th century, Évariste Galois, Arthur Cayley and others studied groups of permutations and transformations, where composition is the basic operation.
Samuel Eilenberg and Saunders Mac Lane introduced categories in 1945, in a paper on "natural equivalences" in algebraic topology. Their idea — study objects through the arrows between them — has since spread across mathematics, computer science and logic.

One thing after another

The composite of two functions

Explore: composition machines

Worked examples

The laws of composition

Composition in Lean

Checking every function on a small set

The first category

Exercises

Common misconceptions

Wonder Trails

Set-theoretic connection

History and global context

Further reading