Skip to content

Brouwer fixed points on complex… to Fundamental groups of…

Highlights

TheoremBrouwer fixed points on complex disks#

For c : ℂ and r ≥ 0, every continuous complex-valued map on Metric.closedBall c r has a fixed point if it maps the sphere boundary into that ball, without any interior image bound.

Quoted from the highlights in formalization.yaml of FormalFrontier/sphere-topology at commit 672d46f9, Apache-2.0.

Lean

Read from the source at commit 672d46f9, without running Lean.

Sources
LeanComplex.exists_fixedPoint_closedBall_of_boundary_mapsTo · Complex.exists_fixedPoint_closedBall

TheoremHairy-ball theorem for the metric two-sphere#

Every continuous map V from the unit sphere in EuclideanSpace ℝ (Fin 3) to EuclideanSpace ℝ (Fin 3) satisfying ⟨p, V(p)⟩ = 0 at every sphere point p vanishes somewhere.

Quoted from the highlights in formalization.yaml of FormalFrontier/sphere-topology at commit 672d46f9, Apache-2.0.

Lean

Read from the source at commit 672d46f9, without running Lean.

Sources
LeanSphereTopology.sphere2_exists_zero_of_orthogonal_field

DefinitionFree fundamental groups of circle bouquets#

For any label type I and independent ambient and label universes, FreeGroup I is multiplicatively equivalent to the fundamental group of the point-wide-pushout CircleBouquet.space I at its common point, sending each free generator to its included counterclockwise complex-unit-circle loop, including for empty I.

Quoted from the highlights in formalization.yaml of FormalFrontier/sphere-topology at commit 672d46f9, Apache-2.0.

Lean

Read from the source at commit 672d46f9, without running Lean.

Sources
LeanCircleBouquet.generatorEquiv · CircleBouquet.generatorEquiv_of

DefinitionSphere cogroups and sharp cocommutativity#

For every n : ℕ and universe u, Metric.Sphere.cogroup n gives the last-axis-north-based ULift.{u} of the unit sphere in EuclideanSpace ℝ (Fin (n + 2)) a group-object structure in the ordinary opposite based-homotopy category, whose specified ordered-pinch monoid structure is commutative exactly when 0 < n.

Quoted from the highlights in formalization.yaml of FormalFrontier/sphere-topology at commit 672d46f9, Apache-2.0.

Lean

Read from the source at commit 672d46f9, without running Lean.

Sources
LeanMetric.Sphere.cogroup · Metric.Sphere.cogroup_isCommMonObj_iff

TheoremNontrivial second homotopy group of the metric two-sphere#

In every universe u, the second homotopy group of Metric.Sphere.basedSpace.{u} 1, the last-axis-north-based ULift.{u} of the unit sphere in EuclideanSpace ℝ (Fin 3), is nontrivial.

Quoted from the highlights in formalization.yaml of FormalFrontier/sphere-topology at commit 672d46f9, Apache-2.0.

Lean

Read from the source at commit 672d46f9, without running Lean.

Sources
LeanHomotopyGroup.nontrivial_sphere_two

Headline results

Quoted from the headline results in README.md of FormalFrontier/sphere-topology at commit 672d46f9, Apache-2.0.

TheoremH-space fundamental groups commute#

FundamentalGroup.mul_comm applies at the unit of any H-space, using only its two relative unit homotopies. No associativity, commutativity or strict unit laws for the multiplication are assumed. Continuous multiplication with a strict unit also gives Path.mul_homotopic_trans, without associativity or inverses.

Quoted from the headline results in README.md of FormalFrontier/sphere-topology at commit 672d46f9, Apache-2.0.

Lean

Read from the source at commit 672d46f9, without running Lean.

Sources
LeanFundamentalGroup.mul_comm

Normalized circle fundamental groups and degree. For real T ≠ 0, AddCircle.fundamentalGroupEquivInt is supplied by Fundamental Groupoids and identifies π₁(AddCircle T, 0) with Multiplicative ℤ, including signed periods, lifted endpoints and agreement with the complex unit circle. Circle.degree classifies free homotopy of arbitrary continuous circle self-maps. Composition multiplies degree, while pointwise multiplication adds it, including multiset products with repeated factors. The map z ↦ z^n has degree n : ℤ, and degree different from 1 is a sufficient, not necessary, fixed-point condition. No based-map premise is needed.

Disk boundary degree and non-retraction. Every continuous map G : C(Metric.closedBall (0 : ℂ) 1, Circle) has boundary restriction of degree zero, so that restriction is not the identity on Circle (Disk). The boundary map is the coordinate-preserving inclusion of the complex unit circle into the closed unit disk; no basedness premise is imposed. This is not a theorem about arbitrary-dimensional disks or an extension converse.

Forward intersections with spheres. In a real inner-product affine space, Sphere.rayInter continues from q through a distinct closed-ball point x to the sphere, with parameter at least one even when q is outside the ball. For a closed-ball start, positive sphere-intersection parameters are characterized by the upper root, and a boundary second point is fixed, including the diagonal. The total parameter and point formulas are jointly continuous on the whole off-diagonal; boundary starts agree with Mathlib's Sphere.secondInter when x is in the closed ball. No finite-dimensionality, completeness or global radius-sign assumption is needed.

Continuous ray maps and boundary-only strict retractions. In a real inner-product affine torsor, Sphere.rayInterMap turns an ambient-valued continuous map f on a closed ball, with f x ≠ x at every point, into a continuous map to its sphere. If boundary points have images in the closed ball, composition with the boundary inclusion is exactly the identity. No image condition is imposed on interior points; a fixed-point-free continuous closed-ball selfmap is a specialization. Vector and point universes are independent, and radii are arbitrary real numbers, with no finite-dimensionality, completeness or nontriviality premise. This generalizes the boundary-fixing construction in May's closed-disk argument (Chapter 1, §6), not a fixed-point theorem in this generality.

Generic stereographic geometry. For E : Type u with [NormedAddCommGroup E] and [InnerProductSpace ℝ E], let S := Metric.sphere (0 : E) 1 be the canonical sphere subtype, p q : S, H := (ℝ ∙ (p : E))ᗮ and σ := stereographic (norm_eq_of_mem_sphere p). stereographicHomeomorph p identifies ({p}ᶜ : Set S) with H; for hpq : p ≠ q, stereographicOverlapHomeomorph p q hpq identifies ({p}ᶜ ∩ {q}ᶜ : Set S) with H \ {σ q}. These retain Mathlib's factor-2 stereographic map: the excluded pole is +p, and the one-pole inverse sends 0 to -p. The overlap target deletes zero exactly when q = -p.

DefinitionLast-axis one-point compactification coordinates#

EuclideanSpace.onePointHomeomorphSphere identifies OnePoint (EuclideanSpace ℝ (Fin n)) with the unit sphere in EuclideanSpace ℝ (Fin (n+1)), for every n, including zero. Infinity maps to the last unit vector and finite zero to its antipode. Finite coordinates have denominator ‖x‖²+4, and the off-pole inverse has coordinates 2*p_i/(1-p_last). The underlying append-zero-last linear isometry also applies over RCLike scalars; only the sphere homeomorphism is real.

Quoted from the headline results in README.md of FormalFrontier/sphere-topology at commit 672d46f9, Apache-2.0.

Lean

Read from the source at commit 672d46f9, without running Lean.

Sources
LeanEuclideanSpace.onePointHomeomorphSphere

DefinitionFinite generalized loops and based sphere-map classes#

For every n : ℕ, GenLoop.sphereHomeomorph gives a homeomorphism from GenLoop (Fin n) X x to {F : C(Sⁿ, X) // F (EuclideanSpace.northPoint n) = x}, where Sⁿ is the unit sphere in EuclideanSpace ℝ (Fin (n+1)). HomotopyGroup.equivSphereClasses gives a natural set equivalence from HomotopyGroup (Fin n) X x to the existing ZerothHomotopy of this subtype. Inverse representatives precompose with Cube.collapseToSphere. Constants and based postcomposition are preserved, including between targets in independent universes. Equality of sphere-map components is exactly homotopy relative to the singleton last-axis north pole. In dimension one, HomotopyGroup.pi1MulEquivFundamentalGroup_sphereHomeomorph sends the component associated with a based path to that path's fundamental-group class. Targets require only a topology and a chosen point, with no separation, local compactness or well-pointedness hypothesis.

For every n : ℕ and arbitrary X : BasedTopCat.{u}, HomotopyGroup.equivSphereHom is an ordinary set equivalence from HomotopyGroup (Fin n) X.right (BasedTopCat.point X) to morphisms from the north-based ULift.{u} Sⁿ to X in the based-homotopy category. Targets may be any objects of the under category, not only ones presented by BasedTopCat.of, and the construction applies in every universe u. Forward representatives precompose GenLoop.sphereHomeomorph n with ULift.down; inverse representatives have values t ↦ f.right.hom (ULift.up (Cube.collapseToSphere n t)). Here n = 0 means S⁰ and n = 1 means S¹. This set comparison alone specifies no multiplication on the hom-set or group in dimension zero; the positive-dimensional group comparison below uses a multiplicative opposite.

Quoted from the headline results in README.md of FormalFrontier/sphere-topology at commit 672d46f9, Apache-2.0.

Lean

Read from the source at commit 672d46f9, without running Lean.

Sources
LeanGenLoop.sphereHomeomorph

Positive-dimensional sphere pinch and folding. For d = n + 1 > 0, Metric.Sphere.pinch n maps the existing last-axis unit sphere Sᵈ to its two-factor point-wide-pushout. Its cube pullback traverses the left factor before the right factor in coordinate zero; the two closed-half formulas agree at the separating slice, and fixed quarter-point witnesses give distinct non-head values. surjective_pinch and isQuotientMap_pinch show that it is surjective and a quotient map for the topology of that categorical target. pinch_eq_head_iff identifies its head fiber with the equator where ambient coordinate zero vanishes; pinch_eq_pinch_iff says that two points have the same image exactly when they are equal or both lie on that equator. Metric.Sphere.pinchFold is jointly continuous on the ordinary compact-open based-map subtype and preserves simultaneous paths of its factors, for arbitrary topological targets. Its identity/constant folds in opposite orders differ at the left quarter-point, including for the circle. pinch_fold_class compares folding based maps F, G with the existing homotopy-group multiplication: writing J for the inverse sphere-class comparison, the result is J(G) * J(F), including in dimension one. Each original factor retraction composed with the pinch is homotopic to the identity relative to the north pole. pinch_fold_homotopicRel_assoc gives associativity of folding three arbitrary based maps up to north-pole-relative homotopy for every d > 0; its original three-inclusion specialization, pinch_homotopicRel_coassoc, gives coassociativity into the three-factor point-wide-pushout. The two iterated maps are not equal: pinch_coassoc_nondegenerate exhibits their different values at the same cube time 3/8, and three distinct non-head inclusion values of the left nesting. For d = n + 2 ≥ 2, pinch_fold_homotopicRel_swap gives a north-pole-relative homotopy when the two arbitrary based factor maps are interchanged. Its original-inclusion specialization, pinch_homotopicRel_swap, identifies the pinch up to that relative homotopy with the original categorical factor swap after the pinch. Raw folding and based postcomposition allow independently universed targets with only a topology. No dimension-one cocommutativity, zero-sphere pinch or choice of sphere orientation is asserted by these geometric comparisons.

Based coordinate reflections and coinverses. For every positive sphere dimension d = n + 1, including S¹, and every pre-last axis i : Fin (n + 1), coordinateReflection negates exactly ambient coordinate i.castSucc and fixes the last-axis north pole. It is involutive, differs from the identity, and is uniquely determined by its cube pullback: reversing axis i of the original collapse. For an arbitrary based map to a topological space, coordinateReflection_precomp_class identifies precomposition by this reflection with the existing homotopy-group inverse. Folding the pinch with reflection and identity in either order is homotopic to the north constant relative to the north pole, for every such axis; neither folded map is equal to that constant. These results do not require commutativity and do not assert S¹ cocommutativity.

DefinitionHomotopy groups and the sphere-map group#

For n : ℕ and any X : BasedTopCat.{u}, HomotopyGroup.mulOppositeEquivSphereHom gives a multiplicative equivalence from (HomotopyGroup (Fin (n + 1)) X.right (BasedTopCat.point X))ᵐᵒᵖ to the canonical CategoryTheory.yonedaGrp evaluation of Metric.Sphere.cogroup n at op (op (Q.obj X)), where Q := BasedTopCat.homotopyQuotient. Its elements are incoming morphisms to the cogroup carrier in the ordinary opposite based-homotopy category; their unops are outgoing classes from the lifted, north-based Sⁿ⁺¹ to X. These categorical opposites differ from the source's multiplicative opposite. Writing E := HomotopyGroup.equivSphereHom (n + 1) X, mulOppositeEquivSphereHom_apply_op sends MulOpposite.op a to (E a).op; mulOppositeEquivSphereHom_symm_apply sends f to MulOpposite.op (E.symm f.unop), without inversion or a change of representative. mulOppositeEquivSphereHom_naturality identifies based postcomposition by h : X ⟶ Y with the Yoneda action on (Q.map h).op.op. Since folding F, G represents J(G) * J(F), the source opposite matters even for n = 0, which is S¹. No direct group comparison by the same class map without that opposite, S¹ commutativity or group on S⁰ is asserted. Targets require only their topology and chosen point.

Quoted from the headline results in README.md of FormalFrontier/sphere-topology at commit 672d46f9, Apache-2.0.

Lean

Read from the source at commit 672d46f9, without running Lean.

Sources
LeanHomotopyGroup.mulOppositeEquivSphereHom

TheoremNontrivial second homotopy group of S²#

Metric.Sphere.id_not_nullhomotopic_two shows that the identity of the unit two-sphere in EuclideanSpace ℝ (Fin 3), lifted to any universe, is not homotopic to any constant map. Metric.Sphere.homotopyQuotient_id_ne_const_two distinguishes its identity class from the constant class at the last-axis north pole in the based-homotopy category. HomotopyGroup.nontrivial_sphere_two proves that the corresponding π₂ is nontrivial. The sphere is Metric.Sphere.basedSpace 1; no computation of the second homotopy group is asserted.

Quoted from the headline results in README.md of FormalFrontier/sphere-topology at commit 672d46f9, Apache-2.0.

Lean

Read from the source at commit 672d46f9, without running Lean.

Sources
LeanMetric.Sphere.id_not_nullhomotopic_two

Topology of real normed unit spheres. The topology-only APIs in Homotopy.Sphere are stated for E : Type u with [NormedAddCommGroup E] [NormedSpace ℝ E], using its original norm and S := Metric.sphere (0 : E) 1. contractibleSpace_sphere_compl_singleton p gives ContractibleSpace ({p}ᶜ : Set S) without a rank premise; simple connectivity follows from Mathlib's SimplyConnectedSpace.ofContractible. pathConnectedSpace_sphere_compl_poles p q h gives PathConnectedSpace ({p}ᶜ ∩ {q}ᶜ : Set S) for all p,q, including equal poles, when h : 2 < Module.rank ℝ E (cardinal rank). simplyConnectedSpace_unitSphere h gives SimplyConnectedSpace S under the same rank bound, including the usual Sⁿ for n ≥ 2 and infinite-dimensional spaces. No completeness, finite-dimensionality, supplied pole for the whole sphere, ambient connectivity or overlap-nonemptiness assumption is needed. These statements generalize May's finite Euclidean sphere setting; the orthogonal-coordinate charts above still require an inner product.

TheoremCanonical antipodal quotient covering#

For E : Type w with [NormedAddCommGroup E] [NormedSpace ℝ E], Metric.Sphere.isQuotientCoveringMap_toProjectivization makes the canonical continuous map Metric.Sphere.toProjectivization : C(Metric.sphere (0 : E) 1, Projectivization ℝ E) a quotient covering for the scalar action of Metric.sphere (0 : ℝ) 1, whose elements act by identity and negation. The sphere uses the original norm; the target has the quotient topology from nonzero vectors. No inner product, dimension, completeness, local compactness, nonemptiness, nontriviality or freeness hypothesis is required. This includes the zero space's empty-to-empty map and the two-point-to-one-point map for E = ℝ.

Quoted from the headline results in README.md of FormalFrontier/sphere-topology at commit 672d46f9, Apache-2.0.

Lean

Read from the source at commit 672d46f9, without running Lean.

Sources
LeanMetric.Sphere.isQuotientCoveringMap_toProjectivization

DefinitionReal projective fundamental groups and lifted endpoints#

For a real normed space E with 2 < Module.rank ℝ E, Projectivization.fundamentalGroupEquivZModTwo identifies π₁(Projectivization ℝ E, b) with Multiplicative (ZMod 2). A chosen unit lift over the supplied basepoint fixes the lift description, but not the resulting coordinate. The identity means returning to that lift; Multiplicative.ofAdd (1 : ZMod 2) means reaching its antipode. The sphere uses the given norm, with no inner-product, finite-dimensionality or completeness assumption, including infinite cardinal rank.

Quoted from the headline results in README.md of FormalFrontier/sphere-topology at commit 672d46f9, Apache-2.0.

Lean

Read from the source at commit 672d46f9, without running Lean.

Sources
LeanProjectivization.fundamentalGroupEquivZModTwo

Quotient presentations of topological wide pushouts (Fundamental Groupoids). TopCat.widePushoutHomeomorph identifies the quotient of B ⊕ Σ i, X i by b ∼ (i, f i b) with the categorical wide pushout of arbitrary continuous maps f i : B ⟶ X i, preserving the head and every factor. Continuity and descent have an independent target universe; empty and singleton families need no separation, compactness or homotopy assumptions.

TheoremEmbeddings, closed maps and neighborhoods of point-wide-pushouts#

TopCat.isEmbedding_widePushoutDesc_point promotes point-preserving component embeddings to an embedding of the canonical wide pushouts; open or closed component embeddings give an open or closed embedding, respectively. Point reflection and component open or closed maps also suffice for the corresponding map property. The index may be arbitrary or empty, and source and target universes are independent, with no separation assumptions. The ULift caller accommodates smaller original factors. For a given function relabeling factors with finite label fibers, the closed-map criterion assumes closed component maps, point reflection, and the head and factor equations. The function is closed exactly when each omitted target factor has a closed chosen-point singleton, with no continuity or separation assumption. Closed rays based at zero give a proper closed embedding that is not open. For open neighborhoods of the attaching points, TopCat.widePushoutPointNeighborhoodHomeomorph identifies their wide pushout with its open range in the ordinary subtype topology.

Quoted from the headline results in README.md of FormalFrontier/sphere-topology at commit 672d46f9, Apache-2.0.

Lean

Read from the source at commit 672d46f9, without running Lean.

Sources
LeanTopCat.isEmbedding_widePushoutDesc_point

Parametrized continuity and homotopy gluing (Fundamental Groupoids). TopCat.continuous_prod_iff_of_isColimit checks joint continuity on the legs of any supplied topological colimit under Mathlib's LocallyCompactPair P Y hypothesis; a locally compact parameter suffices, with no separation condition on the target. Parameter and target universes are independent. Compatible families on a wide pushout's head and every factor descend continuously, with computation, uniqueness, fixed-parameter and reparametrization laws. Compatible interval homotopies glue at all times, without requiring the common point to stay fixed. Point-relative descent is supplied by TopCat.widePushoutPointHomotopyRel.

DefinitionPoint-relative equivalences and contractions#

TopCat.widePushoutPointHomotopyEquiv descends point-preserving factor maps and supplied relative inverse homotopies. Inverse point preservation follows from the forward maps and left relative homotopies. The chosen relative witnesses compute on the head and every factor. Supplied contractions fixing the attaching points contract the wide pushout, including an empty index family. This is stronger data than ordinary factor contractibility; countably many endpoint-zero intervals give a nontrivial client.

Quoted from the headline results in README.md of FormalFrontier/sphere-topology at commit 672d46f9, Apache-2.0.

Lean

Read from the source at commit 672d46f9, without running Lean.

Sources
LeanTopCat.widePushoutPointHomotopyEquiv

DefinitionFactor retractions and separation of point-wide-pushouts#

TopCat.widePushoutPointRetraction retracts the categorical wide pushout of arbitrary chosen-point spaces onto any selected factor, and each factor inclusion is an embedding. The retractions jointly distinguish points, without separation or finiteness assumptions, even for the empty index family. The pushout is T₀, T₁ or Hausdorff exactly when every factor has that property; factorwise inheritance is available by instance inference. Index and space universes are independent. No embedding into the product is asserted. The circle-bouquet retractions specialize this construction.

Quoted from the headline results in README.md of FormalFrontier/sphere-topology at commit 672d46f9, Apache-2.0.

Lean

Read from the source at commit 672d46f9, without running Lean.

Sources
LeanTopCat.widePushoutPointRetraction

Compact subsets meet finitely many pointed factors. finite_widePushoutPointSupport applies to arbitrary indexed T₁ spaces attached at chosen points. A compact subset of their categorical wide pushout meets only finitely many factors away from the common point. The support API characterizes coverings by the common point plus factor ranges; every continuous map from a compact domain, including a path, has such a finite-factor covering. There is no Hausdorff, compact-factor, countability or finite-index assumption.

DefinitionCharts around a common subset#

TopCat.widePushoutPointChart adjoins one factor to a subset containing the common point. Distinct charts intersect in that subset, and the subset together with the charts covers the pushout, including an empty family. Factorwise path connectedness of its inverse images makes the common subset path connected; a chart then needs path connectedness only of its own whole factor. An open common subset gives open charts, with no separation assumptions.

Quoted from the headline results in README.md of FormalFrontier/sphere-topology at commit 672d46f9, Apache-2.0.

Lean

Read from the source at commit 672d46f9, without running Lean.

Sources
LeanTopCat.widePushoutPointChart

DefinitionFundamental groups of factor-plus-core charts#

TopCat.widePushoutPointChartFundamentalGroupDesc glues homomorphisms on an arbitrary path-connected open neighborhood of the common point and its charts, assuming path connectedness of each whole factor. Only agreement on the core is required. The inclusion-induced core and chart restrictions characterize the result, for arbitrary target groups in an independent universe, empty index families and coincident charts. If each original factor's core-preimage inclusion induces the trivial fundamental-group map, the factor inclusion-induced coproduct map q is split injective. The specified splitting extends factor homomorphisms to arbitrary independently universed monoid targets. These hypotheses alone do not imply surjectivity of q or uniqueness of these extensions. Under just the path-connected core and whole-factor hypotheses, TopCat.widePushoutPointChartFundamentalGroupColimitEquiv identifies the raw group colimit of the core-to-chart star with the ambient fundamental group. Both directions preserve every core and chart inclusion map, including for an empty index family; no core-preimage nullity is needed. With the split-injectivity hypotheses above, FundamentalGroupKernel identifies the kernel of the ambient-to-original-factor-coproduct retraction ρ with the ambient algebraic normal closure of ⋃ i, γᵢ(ker pᵢ). Here γᵢ is induced by chart inclusion; pᵢ comes from restricting the ambient factor collapse to that chart and then applying the inverse ULift homeomorphism to the original factor. Consequently, q is surjective exactly when ker pᵢ ≤ ker γᵢ for every chart. Under this condition, q and the specified ρ form a multiplicative equivalence, and these extensions are unique for arbitrary independently universed monoid targets. For the inclusion family into the ambient fundamental group, this condition is also necessary for uniqueness: when it fails, the identity and q.comp ρ agree on all original-factor restrictions but differ. No simply connected core, path-connected core preimages or chart–factor homotopy equivalences are required. Index and space universes are independent, and an empty family retains its point head. No vanishing of these chart defects or free-product computation from ordinary contractibility of chosen factor neighborhoods is asserted.

Quoted from the headline results in README.md of FormalFrontier/sphere-topology at commit 672d46f9, Apache-2.0.

Lean

Read from the source at commit 672d46f9, without running Lean.

Sources
LeanTopCat.widePushoutPointChartFundamentalGroupDesc

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.