Alphabeta Math
PropositionStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-11
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The fundamental group is a functor π1:Top∗→Grp\pi_1:\mathbf{Top}_*\to\mathbf{Grp}

Statement

Let Top∗\mathbf{Top}_* have pointed spaces (X,x0)(X,x_0) as objects and basepoint-preserving continuous maps as morphisms. The assignment

π1:Top∗⟶Grp,(X,x0)⟼π1(X,x0)\pi_1:\mathbf{Top}_*\longrightarrow\mathbf{Grp},\qquad (X,x_0)\longmapsto\pi_1(X,x_0)

and f↦f∗f\mapsto f_* is a functor.

Facts & Assumptions

Given: Pointed spaces and basepoint-preserving continuous maps.

[L1]

Spaces and continuous maps form Top\mathbf{Top} (Topological spaces and continuous maps form the large locally small category Top\mathbf{Top}), and groups and homomorphisms form Grp\mathbf{Grp} (Groups and group homomorphisms form the large locally small category Grp\mathbf{Grp}).

[L2]

The induced map f∗f_* on fundamental groups is the homomorphism of The homomorphism on fundamental groups induced by a pointed continuous map, and induced maps satisfy (g∘f)∗=g∗∘f∗(g\circ f)_*=g_*\circ f_* and (1X)∗=1π1(X,x0)(1_X)_*=1_{\pi_1(X,x_0)} (Induced fundamental-group maps are well defined, functorial and invariant under based homotopy).

[L3]

A functor preserves identities and composition (Covariant functor, identity functor, composite functor, and contravariant functor).

Proof

technique · direct
1.1

Basepoint-preserving continuous maps contain identities and are closed under composition, so they form the stated pointed category.

givenL1
2.1

By [L2], every morphism ff is sent to a group homomorphism f∗f_*, and the identity and composite equations required in [L3] hold.

step 1.1L2L3
3.1

Therefore the object and morphism assignments define a functor π1:Top∗→Grp\pi_1:\mathbf{Top}_*\to\mathbf{Grp}.

step 2.1L1L3∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 39 results over 13 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources