Algebraic topology

The Lean Pool projects whose card's first MSC2020 code is in class 55, Algebraic topology: 3 articles, one per card.

ClassDirected Topology in Lean 4#

Foundational library for directed topological spaces, dipaths, dihomotopy, the fundamental category functor, and a directed Van Kampen pushout theorem.

Quoted from the card LeanPool/projects/directed-topology-lean-4.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 4 main results, each with its informal statement quoted from the card. The scan finds 4 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanDirectedSpace · Dipath · DirectedVanKampen.directed_van_kampen

DefinitionEilenberg–Zilber theorem for bisimplicial objects#

For a bisimplicial object X in an abelian category, constructs a chain homotopy equivalence between the total complex of the alternating face map double complex of X and the alternating face map complex of its diagonal. The equivalence is built from the shuffle map and the Alexander–Whitney map. On normalized complexes, shuffle followed by Alexander–Whitney is the identity, and the other composite is homotopic to the identity via the Eilenberg–Mac Lane recursive homotopy. The result is then transported to the unnormalized complexes along the Moore normalization comparisons. The development includes the combinatorics of (p, q)-shuffles, their signs, and the cancellation of diagonal boundary terms.

Quoted from the card LeanPool/projects/eilenberg-zilber.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 2 main results, each with its informal statement quoted from the card. The scan finds 2 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

  • LeanPool.EilenbergZilber.BisimplicialObject.eilenbergZilber (def; a main declaration), declared in LeanPool/EilenbergZilber/BisimplicialNormalized.lean, line 755: “For every bisimplicial object X in an abelian category, the total complex of the double complex obtained by taking alternating face map complexes in both simplicial directions is chain homotopy equivalent to the alternating face map complex of the diagonal simplicial object of X.” Its source, as the card gives it: “Generalized Eilenberg–Zilber theorem for bisimplicial objects in an abelian category: Dold–Puppe, "Homologie nicht-additiver Funktoren. Anwendungen", Ann. Inst. Fourier 11 (1961), 201–312, Satz 2.9 (Eilenberg–Zilber–Cartier); the homology-level statement is Weibel, An Introduction to Homological Algebra (1994), Theorem 8.5.1. The product case X_{p,q} = K_p ⊗ L_q is Eilenberg–Zilber, "On products of complexes", Amer. J. Math. 75 (1953), 200–204.”
  • LeanPool.EilenbergZilber.BisimplicialObject.eilenbergZilberNormalized (def), declared in LeanPool/EilenbergZilber/BisimplicialNormalized.lean, line 733: “The total complex of the bi-normalized Moore double complex of X is chain homotopy equivalent to the normalized Moore complex of the diagonal, via the shuffle and Alexander–Whitney maps; shuffle followed by Alexander–Whitney is the identity.” Its source, as the card gives it: “Eilenberg–Mac Lane, "On the groups H(Π, n), II", Ann. of Math. 60 (1954), 49–139, Theorem 2.1a, stated there for products of complexes and generalized here to an arbitrary bisimplicial object in an abelian category.”
Project
Sources
LeanLeanPool.EilenbergZilber.BisimplicialObject.eilenbergZilber

TheoremWhitehead's theorem for CW-complexes#

Formalizes Whitehead's theorem — a continuous map between CW-complexes that induces isomorphisms on all homotopy groups is a homotopy equivalence — including the supporting theory of CW-complexes, relative homotopy groups, the homotopy extension property, and compression of maps.

Quoted from the card LeanPool/projects/whitehead-theorem.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists one main result, with its informal statement quoted from the card. The scan finds its declaration in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanWhiteheadTheorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.