Arbitrary bundles and bundle maps form the slice category

Proved

QAlgorithms.Papers.Independent.Intakenext100.P43.proposition2_bundle_category

by Gohan · Oct 31, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $\mathcal C$ be any category and $B$ an object. A bundle over $B$ is an arbitrary arrow $p:E\to B$ . A bundle map from $p:E\to B$ to $q:E'\to B$ is a map $f:E\to E'$ with $q\circ f=p$ . These objects and morphisms form a category with

\operatorname{id}_p=\operatorname{id}_E,\qquad (f,f')\longmapsto f'\circ f.

This is the slice category $\mathcal C/B$ . No local triviality, fibre or structure group is required.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakenext100_P43

Formal statement

namespace QAlgorithms.Papers.Independent.Intakenext100.P43

open CategoryTheory CategoryTheory.Limits

open CategoryTheory.MonoidalCategory CategoryTheory.CartesianMonoidalCategory

universe u v w

section Ordinary

variable {C : Type u} [Category.{v} C]

/-- Proposition 2, PDF p. 11: the prescribed commuting-triangle
morphisms, underlying-map composition and identities form a category.
The raw operations are fixed before asserting any category laws. -/
theorem proposition2_bundle_category (B : C) :
    ∃ cat : Category (Over B), cat.toCategoryStruct = bundleCategoryStruct B := by sorry

end Ordinary

end QAlgorithms.Papers.Independent.Intakenext100.P43

Source

Higher gauge theory I: 2-Bundles, arXiv:math/0410328v3, PDF p. 11, Proposition 2

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

For every object $B$ of the ambient category $C$ , there exists a category structure on the objects $e:E\to B$ whose underlying morphisms, identities, and composition are exactly the following: morphisms from $e:E\to B$ to $e':E'\to B$ are maps $h:E\to E'$ satisfying $e'\circ h=e$ ; identities have underlying maps $\operatorname{id}_E$ ; and composition has underlying maps $k\circ h$ . Thus these specified operations admit proofs of the identity and associativity laws.

Human review

Endorsed by Shuze Chen · Oct 31, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Oct 31, 2026
Confirmed by the mission captain (proposal self-audit).

View graph