Revision #1260 → #2102 · back to history
modifiedGenus (intuitive notion)c8f49cb829e7
| Field | From #1260 | To #2102 |
|---|
| note | No topological notion of genus (number of handles) is defined anywhere in Mathlib. | No topological notion of genus (number of handles) is defined anywhere in Mathlib (grep for 'genus' in Mathlib returns no files). |
addedGenus–Euler-characteristic relation for closed surfaces74a6f7c8c107
modifiedNon-orientable genus66c68de063ec
| Field | From #1260 | To #2102 |
|---|
| note | Non-orientable genus and cross-caps are not formalized in Mathlib (a grep for crossCap/Klein bottle finds only the KleinFour group). | Non-orientable genus and cross-caps are not formalized in Mathlib (grep for crossCap and Klein bottle finds nothing topological). |
addedNon-orientable genus–Euler-characteristic relation2266f84de3d6
modifiedNon-orientable genus of projective plane and Klein bottle454105842a98
| Field | From #1260 | To #2102 |
|---|
| note | Mathlib has no projective-plane or Klein-bottle surface with an associated genus. | Mathlib's only ProjectivePlane is the combinatorial incidence-geometry one (Mathlib.Combinatorics.Configuration), with no Klein-bottle surface or genus. |
modifiedGenus of a knotdca586227972
| Field | From #1260 | To #2102 |
|---|
| note | Mathlib contains no knot theory, Seifert surfaces, or knot genus. | Mathlib contains no knot theory, Seifert surfaces, or knot genus (grep for Seifert finds nothing). |
modifiedGenus of a handlebodydfefa8d075ec
| Field | From #1260 | To #2102 |
|---|
| note | Handlebodies and their genus are absent from Mathlib. | Handlebodies and their genus are absent from Mathlib (grep for handlebody finds nothing). |
modifiedElliptic curve as genus 1 curvee30a2fdac04f
| Field | From #1260 | To #2102 |
|---|
| note | Mathlib formalizes elliptic curves as Weierstrass curves with invertible discriminant (WeierstrassCurve.IsElliptic), not via the genus-1-with-rational-point characterization. | Mathlib formalizes elliptic curves as Weierstrass curves with invertible discriminant (WeierstrassCurve.IsElliptic, confirmed), not via the genus-1-with-rational-point characterization. |
modifiedGenus formula via Riemann–Roch72c066e9e266
| Field | From #1260 | To #2102 |
|---|
| note | Mathlib has no Riemann–Roch theorem for curves and no degree-genus formula. | Mathlib has no Riemann–Roch theorem for curves and no degree-genus formula (grep for RiemannRoch finds nothing). |
modifiedGenus of an oriented manifold (cobordism)54b0fb838565
| Field | From #1260 | To #2102 |
|---|
| note | Cobordism and genera in the sense of cobordism invariants are not present in Mathlib. | Cobordism and genera in the sense of cobordism invariants are not present in Mathlib (the only 'cobord' matches are 'coborder' of immersions). |
modifiedEuler characteristic is not a genus17ee0df37990
| Field | From #1260 | To #2102 |
|---|
| note | Mathlib has an algebraic Euler characteristic (HomologicalComplex.eulerChar) but no cobordism framework in which to state that it fails to be a genus. | Mathlib has an algebraic Euler characteristic (in Mathlib.Algebra.Homology.EulerCharacteristic) but no cobordism framework in which to state that it fails to be a genus. |