Subfamily retractions and… to Covering-space lifts of…

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

DefinitionSubfamily retractions and continuous factorization#

TopCat.widePushoutPointSubfamilyRetraction retracts onto any subfamily, with an embedding inclusion whose range includes the common point. This inclusion is closed exactly when the chosen-point singleton in every omitted factor is closed; retained factors need no separation hypothesis. A continuous map factors through that inclusion exactly when its support lies in the subfamily, without separation or compactness assumptions. For T₁ factors, every compact-domain map factors through a finite subfamily. The circle-bouquet application retains the endpoints of based loops, including included positive original-circle loops.

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.widePushoutPointSubfamilyRetraction

TheoremStrict finite-stage factorization of compact homotopies#

TopCat.exists_finite_widePushout_point_subfamily_homotopyRel factors a prescribed compact-image relative homotopy in a point-wide-pushout of T₁ factors through a finite subfamily containing any prescribed finite set. Recovery holds at every pair of parameters, including both endpoint maps and arbitrary relative subsets. Compact domains suffice, without source separation, factor compactness or countability. At a fixed subfamily, existence of a relative or path homotopy is reflected without T₁ or compactness. CircleBouquet.loop_homotopic_iff_exists_finite_subfamily gives finite-stage detection for based loops in arbitrary circle bouquets; the stronger homotopy theorem recovers a supplied based homotopy itself.

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.exists_finite_widePushout_point_subfamily_homotopyRel

DefinitionArbitrary-index circle bouquets#

CircleBouquet.space is the wide pushout of based complex circles, with a common point even for the empty family and independent index/ambient universes. Inclusions, descent and extensionality give its universal property; retractions detect the positive generators as nonidentity. CircleBouquet.generatorEquiv identifies its fundamental group with FreeGroup I, sending each free generator to the included counterclockwise circle class. CircleBouquet.lift gives the unique extension of arbitrary generator values to a homomorphism into any group, in an independent target universe. Distinct included positive generators do not commute. The inverse equivalence is noncomputable; no geometric word-extraction algorithm is asserted. The continuous map CircleBouquet.relabel σ realizes arbitrary relabelings, preserving the original positive generators and commuting with FreeGroup.map σ. Source and target ambient and label universes are independent, including empty or infinite families and noninjective label maps. The universal property is natural under precomposition by this map through CircleBouquet.lift_comp_relabel. Its topological criteria characterize closed embeddings exactly by injective label maps and quotient maps exactly by surjective label maps. Relabeling is a closed map exactly when every label fiber is finite; the bouquet has the weak/final topology, not the Hawaiian-earring subspace topology. The induced fundamental-group homomorphism is injective or surjective exactly when the label map has the corresponding property. Its kernel is the normal closure of the differences positiveGenerator i * (positiveGenerator k)⁻¹ for equal labels σ i = σ k, by CircleBouquet.ker_mapOfEq_relabel; no surjectivity assumption is needed.

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
LeanCircleBouquet.space

DefinitionDiagonal equivalence for non-antipodal pairs#

In any real normed vector space, Metric.Sphere.diagonalHomotopyEquiv has the diagonal as its forward map and first projection as its inverse. Normalized affine interpolation stays in the non-antipodal-pair subspace and fixes the diagonal. No finite-dimensionality or nonemptiness hypothesis is needed.

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.diagonalHomotopyEquiv

Continuous hairy-ball theorem for S². sphere2_exists_zero_of_orthogonal_field says every V : C(sphere2, E3) pointwise orthogonal to the radius has a zero. In any real inner-product space, a nowhere-zero continuous orthogonal field on the metric unit sphere gives an explicit identity-to-antipodal homotopy (TangentField), without finite dimensionality. Only the zero theorem specializes to Euclidean three-space.

Circle/S² homology and antipodal sign. Ordered punctures give H̃₁(S¹; ℤ) ≅ ℤ and H̃₂(S²; ℤ) ≅ ℤ, in the unit-sphere models in EuclideanSpace ℝ (Fin 2) and EuclideanSpace ℝ (Fin 3) (Circle, Sphere). The circle basis is upper minus lower; the equator coordinate is ordered (x,y). SphereAntipodal computes -id on ordinary and reduced integral H₂, hence multiplication by -1 in the fixed integer coordinate and nonhomotopy to identity.

DefinitionCovering-space lifts of simplices#

For a covering p : Y ⟶ X, IsCoveringMap.singularLiftEquiv identifies the lift fiber of a singular simplex with a point fiber by evaluation at any point. Restriction is bijective for every simplex operator, including degeneracies and faces omitting vertex zero. There are no nonemptiness, connectedness, local connectedness, surjectivity or finite- sheet assumptions on the base or total space. The singular map is equifibered.

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
LeanIsCoveringMap.singularLiftEquiv

Finite-fiber covering transfer. For p : Y ⟶ X, IsCoveringMap p and finite point fibers, singularChainComplexTransfer uses coefficient objects in any preadditive category with coproducts indexed in the space universe; object and morphism universes are independent. Ordinary homology adds only CategoryWithHomology and uses q : ℕ. A simplex maps to the sum of its lifts. Transfer then pushforward is d • id if every point fiber has cardinality d; finiteness is a separate premise. No constant degree, nonemptiness, surjectivity or connectedness is needed for the construction.

Subdivision and cover-small chains. Integral signed subdivision Sd and its support-preserving prism H satisfy ∂H + H∂ = id − Sd (Subdivision). For an open cover, inclusion of finite-support chains small in a cover member is a quasi-isomorphism (SmallChains). Space and cover-index universes may differ; no global nonemptiness is assumed. Cover-respecting continuous maps and refinements induce compatible chain maps.

Ordered ordinary and reduced Mayer–Vietoris. Two opens covering a space give difference (c,−c) followed by sum, all three successive ordinary exactness positions, ordered-cover naturality and cover-swap minus sign (MayerVietoris). The reduced low-degree boundary uses open-intersection homology and is an isomorphism when both H̃₀ and H̃₁ vanish on each open. The reduced degree-zero sequence is exact at the biproduct for every two-open cover; its final map is epic when the intersection is nonempty, not unconditionally (ReducedMayerVietoris).

Components and path connectedness. Components presents the augmentation kernel by nonbasepoint path components, with categorical coefficients. In a preadditive category with the requisite coproducts and homology, H₀(X; R) ⟶ R is invertible exactly when X is path connected if R is nonzero; nonemptiness is a conclusion (Connectedness). For nonempty X, integral H̃₀(X)=0 is equivalent to path connectedness. Reduced homology is nonnegative, with augmentation kernel in degree zero, ordinary homology in positive degrees and H̃₀(∅)=0; no degree-minus-one convention is asserted. Contractible-space premises include nonemptiness.

Covering foundations from Fundamental Groupoids. The dependency supplies based unique lifting, monodromy, maps of covers, deck actions and based equal-image equivalences; Sphere re-exports the five deprecated covering module paths below. The guide gives the distinct connectedness and local path connectedness hypotheses for each result. These are not a general classification of coverings.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.