Revision #1303 → #2035 · back to history
modifiedChain complexb6f1acc3a4ed
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | ChainComplex |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Algebra.Homology.HomologicalComplex |
| note | — | ChainComplex is defined as a HomologicalComplex with the down-Nat shape, directly formalizing the article's notion. |
| status | — | formalized |
modifiedGroup of cyclesbc6754603f38
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | HomologicalComplex.cycles |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex |
| note | — | HomologicalComplex.cycles K i is the i-th cycles object, formalizing ker d_n in a chain complex. |
| status | — | formalized |
modifiedGroup of boundariesa78a0a5565bb
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | HomologicalComplex.opcycles |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex |
| note | — | Mathlib has no standalone HomologicalComplex.boundaries; boundaries appear only implicitly through the image-to-cycles factorization and opcycles in the ShortComplex API. |
| status | — | partial |
modifiedHomology group of a chain complex661947c669bd
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | HomologicalComplex.homology |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex |
| note | — | HomologicalComplex.homology K i defines the i-th homology of a homological complex (kernel mod image) categorically. |
| status | — | formalized |
modifiedHomology theorycae62c57c7a5
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | HomologicalComplex.homologyFunctor |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex |
| note | — | Mathlib has the general categorical homology-functor machinery but no axiomatic Eilenberg–Steenrod "homology theory" structure. |
| status | — | partial |
modifiedHomology theory as a functor6570c98ad817
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | HomologicalComplex.homologyFunctor |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex |
| note | — | HomologicalComplex.homologyFunctor is the n-th homology as a functor on the category of homological complexes. |
| status | — | formalized |
modifiedHomology of a topological space6e4c40465d5d
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | AlgebraicTopology.singularHomologyFunctor |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.AlgebraicTopology.SingularHomology.Basic |
| note | — | AlgebraicTopology.singularHomologyFunctor C n defines the n-th singular homology functor on TopCat with coefficients in C. |
| status | — | formalized |
modifiedBoundary in a chain complex8be3b31485f1
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | HomologicalComplex.opcycles |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex |
| note | — | Boundaries appear only implicitly as image of d via the ShortComplex homology data; there is no standalone HomologicalComplex.boundaries decl. |
| status | — | partial |
modifiedCycle in a chain complexb5391a0a0097
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | HomologicalComplex.cycles |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex |
| note | — | HomologicalComplex.cycles K i directly formalizes the kernel of the differential. |
| status | — | formalized |
modifiedHomology groups of a topological space025043d317df
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | AlgebraicTopology.singularHomologyFunctor |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.AlgebraicTopology.SingularHomology.Basic |
| note | — | The n-th singular homology of a topological space is defined as singularHomologyFunctor C n applied to coefficients and the space. |
| status | — | formalized |
modifiedHomology of the circle711a6ebedce9
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No Mathlib computation of the singular homology of S^1 was found. |
| status | — | not_formalized |
modifiedHomology of the 2-sphere9ec3c37db85d
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No Mathlib computation of the singular homology of S^2 was found. |
| status | — | not_formalized |
modifiedHomology of the n-spherea2517b9ecead
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No Mathlib computation of H_*(S^n) was found. |
| status | — | not_formalized |
modifiedHomology of the 2-balld89acb5e361b
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No Mathlib computation of the singular homology of a disk was found. |
| status | — | not_formalized |
modifiedHomology of the torusfe5b9592a075
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No Mathlib computation of H_*(T^2) was found. |
| status | — | not_formalized |
modifiedHomology of the n-torus25a5c0b93a44
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No Mathlib computation of H_*(T^n) was found. |
| status | — | not_formalized |
modifiedHomology of the projective plane39e49e26aee4
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No Mathlib computation of H_*(RP^2) was found. |
| status | — | not_formalized |
addedTorsion in homologyb7111da159be
modifiedChain complex (general construction)99a19558b2ab
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | HomologicalComplex |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.Algebra.Homology.HomologicalComplex |
| note | — | HomologicalComplex generalizes the article's construction to any complex shape over a category with zero morphisms. |
| status | — | formalized |
addedBoundary of a boundary is zerod417beaf1d1c
modifiedBoundaries and cycles65b0dfdac261
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | HomologicalComplex.cycles |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex |
| note | — | Cycles are formalized as HomologicalComplex.cycles; boundaries exist only implicitly via the imageToCycles/opcycles factorization in the ShortComplex API. |
| status | — | partial |
modifiedn-th homology groupfa2a9dd2fea0
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | HomologicalComplex.homology |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex |
| note | — | HomologicalComplex.homology K n is the n-th homology of a homological complex. |
| status | — | formalized |
modifiedExact chain complexb50dd6c0007f
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | HomologicalComplex.ExactAt |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex |
| note | — | HomologicalComplex.ExactAt K i (and exactness at every degree) formalizes the article's notion of an exact chain complex. |
| status | — | formalized |
modifiedReduced homology groups89ce43f45355
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Loogle finds no decl with reducedHomology in its name. |
| status | — | not_formalized |
modifiedSimplicial homology groupsbe8052daa190
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | AlgebraicTopology.alternatingFaceMapComplex |
| mathlib.match_kind | — | invocation |
| mathlib.module | — | Mathlib.AlgebraicTopology.AlternatingFaceMapComplex |
| note | — | The alternating face map complex of a simplicial object exists and its homology gives simplicial homology, but no top-level `simplicialHomology` decl was found. |
| status | — | partial |
modifiedSingular homology groups4246466b6718
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | AlgebraicTopology.singularHomologyFunctor |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.AlgebraicTopology.SingularHomology.Basic |
| note | — | AlgebraicTopology.singularHomologyFunctor is the n-th singular homology functor on TopCat. |
| status | — | formalized |
modifiedCohomology groups62b0a82d9ef6
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | CochainComplex |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.Algebra.Homology.HomologicalComplex |
| note | — | CochainComplex is a HomologicalComplex with up-Nat shape; cohomology is obtained by applying HomologicalComplex.homology to a cochain complex. |
| status | — | formalized |
modifiedHomotopy groupbf9b094f4b51
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | FundamentalGroup |
| mathlib.match_kind | — | special_case |
| mathlib.module | — | Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup |
| note | — | Mathlib defines FundamentalGroup (π_1) and has Mathlib/Topology/Homotopy/HomotopyGroup.lean, but a general π_n decl does not appear in the public API surface. |
| status | — | partial |
modifiedHurewicz theoremfec5e655da4e
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Loogle finds no Hurewicz-named decl in Mathlib. |
| status | — | not_formalized |
addedHurewicz isomorphism: H_1 is abelianization of pi_11c366f5e6874
modifiedFigure eight homotopy vs homology72e49a4baa30
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No Mathlib treatment of the figure-eight wedge S^1 ∨ S^1 with its homotopy/homology contrast was found. |
| status | — | not_formalized |
modifiedSimplicial homology construction27a4ba824b63
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | AlgebraicTopology.alternatingFaceMapComplex |
| mathlib.match_kind | — | invocation |
| mathlib.module | — | Mathlib.AlgebraicTopology.AlternatingFaceMapComplex |
| note | — | The alternating face map complex is the standard model for simplicial homology in Mathlib, but no top-level simplicialHomology functor is exposed. |
| status | — | partial |
modifiedSingular homology construction6d4ec856c5ee
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | AlgebraicTopology.singularHomologyFunctor |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.AlgebraicTopology.SingularHomology.Basic |
| note | — | Singular homology is defined as a functor on TopCat via the singular chain complex. |
| status | — | formalized |
modifiedGroup homology / derived functors46fb98246bfa
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | groupHomology |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.RepresentationTheory.Homological.GroupHomology.Basic |
| note | — | groupHomology A n is the n-th group homology of a k-linear G-representation, computed via the inhomogeneous chains complex. |
| status | — | formalized |
modifiedMorphism of chain complexesfd86c28e8988
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | HomologicalComplex.Hom |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Algebra.Homology.HomologicalComplex |
| note | — | HomologicalComplex.Hom defines morphisms (chain maps) between homological complexes, making them into a category. |
| status | — | formalized |
modifiedHomology as covariant functor of objects156f957965e0
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | HomologicalComplex.homologyFunctor |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex |
| note | — | HomologicalComplex.homologyFunctor C c n is the covariant n-th homology functor on the category of homological complexes. |
| status | — | formalized |
modifiedCohomology as contravariant functorbf8423dd81f9
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | CochainComplex |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.Algebra.Homology.HomologicalComplex |
| note | — | CochainComplex provides the cochain framework but the article's specific covariant/contravariant distinction is not packaged as a single decl. |
| status | — | partial |
modifiedEuler characteristic2ae149aa4856
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | HomologicalComplex.eulerChar |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Algebra.Homology.EulerCharacteristic |
| note | — | HomologicalComplex.eulerChar is the Euler characteristic as an alternating sum of ranks of complex objects. |
| status | — | formalized |
modifiedEuler characteristic from homology76bbf9b690fb
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | HomologicalComplex.homologyEulerChar |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Algebra.Homology.EulerCharacteristic |
| note | — | HomologicalComplex.homologyEulerChar computes the Euler characteristic from homology, matching the chain-level version. |
| status | — | formalized |
modifiedLong exact sequence from short exact sequencef090fc88bf1e
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | HomologicalComplex.HomologySequence.snakeInput |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Algebra.Homology.HomologySequence |
| note | — | HomologicalComplex.HomologySequence.snakeInput packages a short exact sequence of complexes into a SnakeInput, yielding the long exact homology sequence via the snake lemma. |
| status | — | formalized |
addedZig-zag lemma (connecting homomorphisms)904c0439ebdd
modifiedBrouwer fixed point theorem6baf3fc61517
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No Brouwer fixed-point theorem for the disk was found in Mathlib (only unrelated Brouwer-style results in order theory). |
| status | — | not_formalized |
modifiedInvariance of domain42f37440fcb6
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Loogle finds no invarianceOfDomain decl. |
| status | — | not_formalized |
modifiedHairy ball theoremcee6a734126c
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No hairy-ball theorem was found in Mathlib. |
| status | — | not_formalized |
modifiedBorsuk–Ulam theorem9c4caf49e8cf
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No Borsuk–Ulam decl was found in Mathlib. |
| status | — | not_formalized |
modifiedInvariance of dimension1136aac421c9
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No invariance-of-dimension result was found in Mathlib. |
| status | — | not_formalized |
modifiedJordan curve theorem (shrinking curves on sphere)da84c8a54c0f
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No Jordan curve theorem was found in Mathlib. |
| status | — | not_formalized |
modifiedKlein bottled795390740a7
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No Klein bottle topological space appears in Mathlib (only Klein four-group, an unrelated namesake). |
| status | — | not_formalized |
modifiedProjective plane surfaceb2c24655bec8
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Real projective plane as a topological surface does not appear to be formalized. |
| status | — | not_formalized |
modifiedClosed surfaces from polygon gluing385169ebb5e5
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Polygon-gluing construction of closed surfaces is not present in Mathlib. |
| status | — | not_formalized |
modifiedClassification via connected sum071552241b54
| Field | From #1303 | To #2035 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | The classification of closed surfaces via connected sum is not formalized in Mathlib. |
| status | — | not_formalized |