Skip to content

Fundamental groupoids

Endomorphism transport, chosen-vertex equivalences and connectedness of fundamental groupoids, with small-path generation and constructed strict descent along arbitrary indexed open covers into arbitrary categories. Based van Kampen for two-open covers with a common basepoint and path-connected opens and intersection, as a unique-homomorphism universal property and a pushout of groups. A path-connected based open core and charts with that common pairwise overlap give a colimit of their inclusion star when the core and charts cover the space. The raw group colimit is multiplicatively equivalent to the ambient fundamental group, preserving every leg in both directions with independent space and index universes. Inclusion-directed covers by neighborhoods of a supplied basepoint give colimits without path connectedness or intersection closure, with a universal property for arbitrary target monoids in independent universes. Monotone neighborhood covers indexed by directed preorders give the same universal property with compatibility only along index inequalities, and colimit data for the canonical preorder diagram. Signed-period additive-circle and complex-circle fundamental groups have integer coordinates, with signed-loop, inverse, endpoint, nonidentity and homeomorphism-compatibility laws, using Mathlib's quotient coverings. Continuous maps act functorially on path components, with equal actions for homotopic maps, in independent space universes without separation assumptions. Based postcomposition on generalized loops and homotopy quotients for every cube-index type, with positive homomorphisms, based-homotopy invariance and fundamental-group compatibility. Homotopy quotients commute with arbitrary dependent products for all cube indices in independent universes, by coordinate evaluation and loop assembly; for nonempty cube indices with decidable equality this is a multiplicative equivalence for the existing group structures. Raw cubical homotopy quotients canonically identify with path components of the same compact-open generalized-loop spaces, naturally in based postcomposition and compatibly with the empty-index comparison. For singleton index types, the generalized-loop space is homeomorphic to the compact-open based path space through Mathlib's singleton-coordinate equivalence, with full forward and inverse evaluation, constant/reflexive-path laws and based-postcomposition naturality. Index and space universes are independent, without separation or local compactness assumptions on the target. The based homotopy-fiber point projection has class image equal to the preimage of the constant class for every cube index, with range–kernel form for the existing positive groups. On whole based quotient hom-sets [Z,-], the original fiber projection, forward-loop inclusion and loop map give three successive range–constant-class preimage identities for every original based source (Z,z0). Ordinary ULift handles independent Z,E,B universes; homotopy is relative to {z0}, with arbitrary ordinary topologies and no geometric hypotheses. The pointed homotopy-fiber chain complex has lifted cubical homotopy quotients of the base, total space and fiber in successive degrees, is exact in the pointed-set sense at every positive chain degree, and admits chain maps for strict based squares. Its incoming differential need not surject onto the terminal path-component term of the base. Equivalences of cube-index types induce quotient equivalences by reindexing representatives, with inverse, identity, composition and based-postcomposition laws in independent universes. For nonempty indices with decidable equality, the same maps are multiplicative for the existing group structures, without requiring corresponding selected axes. The continuous identity from Mathlib's CompHaus-test topology to the original target topology induces a natural equivalence on every cubical homotopy quotient, multiplicative for nonempty indices with decidable equality. Probe, cube-index and target universes are independent. Unchanged functions lift continuously from every universe-parameterized compactly generated source. Ordinary products preserve universe-parameterized compact generation when one factor is locally compact. For such a compactly generated factor P and any topological A, the refinement of P × A is homeomorphic to P times the refinement of A by the identity functions. Supplied relative homotopies from compactly generated sources lift with unchanged joint cylinder functions, endpoints and arbitrary fixed subsets, with counit inverse and naturality laws. Coverings induce canonical quotient-map injections for nonempty cube indices and bijections for nontrivial indices, without decidable equality. For nontrivial indices with decidable equality, the stock homotopy groups are multiplicatively equivalent, with forward postcomposition and inverse represented by a chosen based generalized-loop lift. Coordinate-face cube boundaries are path connected for nontrivial indices, including infinite ones. Finite cube boundaries are closed, including the empty-index case. For every index type, the boundary complement with its subtype topology is homeomorphic to the real product on that type; for finite indices it is locally compact. A Hausdorff space maps continuously to the one-point compactification of any open subspace by retaining that subspace and collapsing its complement to infinity, without a local compactness assumption. Adding a disjoint point gives a surjection, even for the whole space, and a quotient map when the ambient space is compact. For compact Hausdorff ambient spaces, collapse pullback is a homeomorphism between continuous maps based at infinity and ambient maps equal to the chosen point outside the open subspace, with ordinary compact-open/subtype topologies. Its finite-cube specialization identifies generalized loops with based maps from the one-point compactification of the cube-boundary complement, including empty indices and arbitrary topological targets in independent universes. Relative affine interpolation fixes any agreement subset for maps into real modules with continuous addition and scalar multiplication. Generalized loops in such modules are homotopic relative to the cube boundary to their constant loops, and all their homotopy quotients are subsingletons, including empty indices and arbitrary chosen points. Generic covering-map lifting and based equivalences, monodromy, equivariant fiber maps and deck-group centralizers. A covering map is proper exactly when every point fiber is finite, without separation, local compactness or uniform-degree assumptions. Fiber finiteness is locally constant, with clopen locus including empty fibers and excluding infinite ones. On a preconnected base, properness is equivalent to finiteness of the fiber at any given point. For preconnected total space and a supplied total-space point, finiteness of its fiber suffices without base connectedness or surjectivity. With path-connected total space, monodromy identifies the based fiber with left cosets of the induced image, and properness is equivalent to that subgroup having finite index. The canonical comparison from the categorical coproduct of fundamental groupoids to the fundamental groupoid of the topological coproduct is an equivalence, for arbitrary families without connectivity assumptions. Semilocal simple connectivity uses chosen-center loops contracting in the ambient space, with induced-map reflection, local-homeomorphism transport, covering consequences and a locally path-connected neighborhood refinement. Radial deformations of punctured closed and open balls onto spheres are available in arbitrary real normed spaces. Positive real scaling identifies Circle with each positive-radius complex sphere. Scaling and normalization give strict retractions and circle-fixing deformations of punctured balls. Ordered two-factor based wedges are strictly isomorphic to binary wedges, and both nested binary three-factor wedges flatten strictly to the finite wedge. Forward and inverse maps preserve the ordered factor inclusions and common point, for possibly different factors in an arbitrary common universe. In the named cartesian structure on the ordinary opposite based-homotopy category, the unop of the associator followed by left-nested flattening equals right-nested flattening after applying the quotient functor. Positive-radius inner circles classify punctured complex-ball fundamental groups by the integers, with normalization and scaling maps and a nontrivial positive generator. Compatible functions on a disk attachment descend uniquely to any target type, and continuous descent has the same underlying function. Removing the centres of an arbitrary family of attached closed complex unit disks gives a subspace that strongly deformation retracts onto the original space image, for arbitrary unbased circle maps and independent space and disk-index universes, without connectivity or separation assumptions. For a selected attaching map taking 1 to a chosen point, the punctured component has a path-connected thickened chart with contractible disk piece and punctured-open-disk overlap. Its positive half-radius generator retracts to the positive attaching loop class. For an entirely based family, these charts and the core form an Option-indexed open cover of the attachment component with path-connected members and pairwise intersections, including the empty disk family. Commuting squares of source and target homeomorphisms induce homeomorphisms of ordinary compact-open homotopy fibers at corresponding specified points, with point, full-path, inverse, identity, composition and projection laws. Fibers of product maps are homeomorphic to products of ordinary homotopy fibers, preserving both retained source points and full same-time paths, naturally for arbitrary continuous squares in independent universes. A free source factor splits from the fiber of f composed with first projection: the result is HomotopyFiber f b times the free factor, retaining both source coordinates and the entire original path. Whole continuous-map diagrams, inverse and constructor laws and same-time evaluation hold for arbitrary topologies in three independent universes; arbitrary-square naturality with a continuous free-factor map uses six independent universes. For f equal to identity, the full identity-fiber factor remains.

Quoted from the project description in formalization.yaml of FormalFrontier/fundamental-groupoids at commit ce38a38f, Apache-2.0.

6 articles: 5 for highlights of its formalization.yaml whose declarations the scan finds and 1 for headline results in its README whose declaration link names a declaration the scan finds in the linked file. Its other headline results are quoted where they stand.

Facts

From the repository and its formalization.yaml; the review and automation statements are quoted as written.

  • Repository: FormalFrontier/fundamental-groupoids, read at commit ce38a38f (2026-11-05).
  • Lean toolchain v4.34.0-rc2, Mathlib at 83abb3e7.
  • License: Apache-2.0.
  • Authors: Formal Frontier Agents.
  • Review status: “unchecked”.
  • Automation: agent; framework “Formal Frontier agents and Lean 4”; tool setup “AI-assisted Lean formalization and mathematical documentation.”

Literature

The sources its formalization.yaml names, with their relationship to it.

  • A Concise Course in Algebraic Topology, J. Peter May, Revised author PDF, Chapter 1 §§3, 5, 7 and Chapter 2 §§4–5, 7–8. Chapter 3 §§2–4, 7 for covering-space monodromy, lifting and maps of covers. Chapter 5 §§1–2, printed pp. 39–41, for compact-Hausdorff tests and kification. Chapter 8 §§5–6, printed pp. 61–62 (PDF pp. 69–70), for the homotopy-fiber model, arbitrary-based-source and finite-degree exactness, especially printed p. 62. Chapter 9 §§1, 4, printed pp. 65–67, for based homotopy groups and the classical finite-degree covering isomorphism (book; adapts).

Builds on

Used by

Highlights

TheoremBased van Kampen for intersection-closed open covers#

For an arbitrarily indexed, binary-intersection-closed open cover of X by path-connected neighborhoods of a common point x, homomorphisms from the local fundamental groups to any group, compatible along every inclusion, determine a unique homomorphism from π₁(X,x), and the inclusion cocone is a colimit in GrpCat at the space universe, with independent space, index and target-group universes.

Quoted from the highlights in formalization.yaml of FormalFrontier/fundamental-groupoids at commit ce38a38f, Apache-2.0.

Lean

Read from the source at commit ce38a38f, without running Lean.

Sources
LeanFundamentalGroup.existsUnique_hom_of_isOpenCover_of_infClosed · FundamentalGroup.isColimitOfIsOpenCover

DefinitionThe fundamental group of the circle is ℤ#

The complex unit circle has π₁(Circle,1) ≃ Multiplicative ℤ with its counterclockwise generator sent to +1, while for every nonzero real period T the equivalence π₁(AddCircle T,0) ≃ Multiplicative ℤ sends the projected real segment from 0 to Tn to n for every integer n.

Quoted from the highlights in formalization.yaml of FormalFrontier/fundamental-groupoids at commit ce38a38f, Apache-2.0.

Lean

Read from the source at commit ce38a38f, without running Lean.

Sources
LeanCircle.fundamentalGroupEquivInt · Circle.fundamentalGroupEquivInt_loop · AddCircle.fundamentalGroupEquivInt · AddCircle.fundamentalGroupEquivInt_loop

TheoremCovering fibers, cosets, properness and homotopy groups#

For a covering p : E → B between arbitrary topological spaces in independent universes, properness is equivalent to finite point fibers and, when E is path connected with chosen e₀, monodromy identifies the fiber over p(e₀) with the left cosets of im(π₁(E,e₀) → π₁(B,p(e₀))) and properness is equivalent to finite index of that image subgroup, while for every e : E postcomposition on based homotopy classes of N-cubes relative to their coordinate-face boundary is injective for nonempty N and bijective for N with at least two elements in an independent cube universe, with a multiplicative equivalence HomotopyGroup N E e ≃* HomotopyGroup N B (p e) in the latter case when N has decidable equality.

Quoted from the highlights in formalization.yaml of FormalFrontier/fundamental-groupoids at commit ce38a38f, Apache-2.0.

Lean

Read from the source at commit ce38a38f, without running Lean.

Sources
LeanIsCoveringMap.isProperMap_iff_finite_fibers · IsCoveringMap.monodromyQuotientEquiv · IsCoveringMap.isProperMap_iff_finiteIndex · IsCoveringMap.injective_homotopyGroup_mapFun · IsCoveringMap.bijective_homotopyGroup_mapFun · IsCoveringMap.homotopyGroupMulEquiv

TheoremFundamental groups of based disk attachments#

For arbitrary based disk attachments, the fundamental group is the quotient by the normal closure of the positive attaching loop classes, compatibly with inclusion and with homomorphisms into every group.

Quoted from the highlights in formalization.yaml of FormalFrontier/fundamental-groupoids at commit ce38a38f, Apache-2.0.

Lean

Read from the source at commit ce38a38f, without running Lean.

Sources
LeanFundamentalGroup.surjective_map_diskAttachmentInclusion · FundamentalGroup.ker_map_diskAttachmentInclusion · FundamentalGroup.diskAttachmentFundamentalGroupQuotientEquiv · FundamentalGroup.diskAttachmentFundamentalGroupHomEquiv

TheoremBased-source and positive-degree homotopy-fiber exactness#

For every original based source (Z,z0), topological E,B in independent Z,E,B universes, f : C(E,B), e0 : E, b : B and h : f e0 = b, let F be the ordinary homotopy fiber, p its projection, J the forward-loop inclusion and Ωf the loop map; on whole based hom-sets [Z,-] relative to {z0}, transported by ordinary ULift, range p_ = f_⁻¹{c_B}, range J_ = p_⁻¹{c_E} and range (Ωf)_ = J_⁻¹{c_F} for constant classes c_X without geometric hypotheses, while the pointed complex S = homotopyFiberSequence f b e0 h, functorial under strict based squares with lifted cubical quotients of B,E,F in degrees 3n,3n+1,3n+2, satisfies range (S.d (n+2) (n+1)).toFun = (S.d (n+1) n).toFun ⁻¹' {(S.X n).point} for every natural n, without asserting terminal π₀B surjectivity, and every nonempty cube index with decidable equality has a natural connecting group homomorphism whose kernel is the range of based postcomposition by f.

Quoted from the highlights in formalization.yaml of FormalFrontier/fundamental-groupoids at commit ce38a38f, Apache-2.0.

Lean

Read from the source at commit ce38a38f, without running Lean.

Sources
LeanBasedTopCat.range_homotopyFiberProjection · BasedTopCat.range_homotopyFiberLoopInclusion · BasedTopCat.range_homotopyFiberLoopMap · HomotopyGroup.homotopyFiberSequence · HomotopyGroup.homotopyFiberSequenceMap · HomotopyGroup.homotopyFiberSequence_exact · ContinuousMap.HomotopyFiber.loopInclusion · HomotopyGroup.homotopyFiberConnectingHom · HomotopyGroup.range_map_eq_ker_homotopyFiberConnectingHom · HomotopyGroup.homotopyFiberConnectingHom_naturality · HomotopyGroup.homotopyFiberConnectingHom_fin_class

Headline results

The 81 headline results of its README are on a page of their own: 1 article, 80 quoted as text.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.