Main results

The main results that the formalization.yaml of FormalFrontier/sphere-topology lists under status.main_results at commit 672d46f9, each that the scan finds declared in the file the yaml gives, with its line. They are listed here, not made articles: in several Formal Frontier libraries this list is close to the whole API. The notes are the yaml's.

The scan does not find 1 of them; the library's page names it.

Declaration Kind Where Note
Metric.Sphere.id_not_nullhomotopic_two theorem SphereTopology/Homotopy/HomotopyGroup/SphereNontrivial.lean, line 51 The identity of Metric.Sphere.basedSpace 1, the unit two-sphere in EuclideanSpace real (Fin 3) lifted to any universe, is not homotopic to any constant map, without a basedness restriction on the homotopy.
Metric.Sphere.homotopyQuotient_id_ne_const_two theorem SphereTopology/Homotopy/HomotopyGroup/SphereNontrivial.lean, line 70 The quotient classes of the identity and the constant endomorphism at the last-axis north pole of Metric.Sphere.basedSpace 1 are distinct in the based-homotopy category.
HomotopyGroup.nontrivial_sphere_two theorem SphereTopology/Homotopy/HomotopyGroup/SphereNontrivial.lean, line 108 The existing homotopy group on Fin 2 of Metric.Sphere.basedSpace 1 at its last-axis north pole is nontrivial in every universe. This is a named theorem, not a global instance or a computation of the group.
Metric.Sphere.cogroup_isCommMonObj_iff theorem SphereTopology/Homotopy/SphereCocommutativity.lean, line 119 For every n >= 0 in any universe, the specified sphere cogroup of dimension n + 1 satisfies IsCommMonObj exactly when 0 < n. Its multiplication is the original ordered-pinch class; this is a named property, not a global instance.
Metric.Sphere.cogroup_not_isCommMonObj_zero theorem SphereTopology/Homotopy/SphereCocommutativity.lean, line 95 The specified cogroup of the original circle S1 is not commutative, in every universe, as detected by the positive generators of Sphere's original two-circle bouquet through the sphere-map and first-homotopy-group comparisons.
Metric.Sphere.cogroup_isCommMonObj theorem SphereTopology/Homotopy/SphereCocommutativity.lean, line 80 In sphere dimensions n + 2 >= 2, the specified monoid object underlying the metric sphere cogroup satisfies Mathlib's IsCommMonObj; its multiplication remains the original ordered-pinch class. This is a named property, not a global instance.
HomotopyGroup.mulOppositeEquivSphereHom def SphereTopology/Homotopy/HomotopyGroup/SphereCogroup.lean, line 217 For every n >= 0 and arbitrary X : BasedTopCat in universe u, the multiplicative opposite of the homotopy group on Fin (n + 1) is multiplicatively equivalent to the canonical group-valued Yoneda evaluation of Metric.Sphere.cogroup n; its elements unop to outgoing sphere-map classes.
HomotopyGroup.mulOppositeEquivSphereHom_apply_op theorem SphereTopology/Homotopy/HomotopyGroup/SphereCogroup.lean, line 237 The forward characteristic sends MulOpposite.op a to (HomotopyGroup.equivSphereHom (n + 1) X a).op, without inversion or a change of representative.
HomotopyGroup.mulOppositeEquivSphereHom_symm_apply theorem SphereTopology/Homotopy/HomotopyGroup/SphereCogroup.lean, line 247 The inverse characteristic sends every incoming morphism f to MulOpposite.op ((HomotopyGroup.equivSphereHom (n + 1) X).symm f.unop).
HomotopyGroup.mulOppositeEquivSphereHom_naturality theorem SphereTopology/Homotopy/HomotopyGroup/SphereCogroup.lean, line 258 Based postcomposition by h : X to Y agrees with the group-valued Yoneda action on (Q.map h).op.op, where Q is BasedTopCat.homotopyQuotient.
Metric.Sphere.cogroup def SphereTopology/Homotopy/SphereCogroup.lean, line 1200 The lifted original positive-dimensional sphere, based at its last-axis north pole, is a stock group object in the ordinary opposite based-homotopy category; its fields are opposite to the classes of pinch, collapse and first-coordinate reflection.
Metric.Sphere.cogroupGrpObj def SphereTopology/Homotopy/SphereCogroup.lean, line 1192 Named group-object data, with no global instance; local installation gives the stock group on outgoing based homotopy classes into any based target.
Metric.Sphere.pinchToWedge_comp_apply theorem SphereTopology/Homotopy/SphereCogroup.lean, line 192 Postcomposing the pointed pinch with an arbitrary map from the binary wedge evaluates by the original ordered fold of its two inclusion restrictions.
HomotopyGroup.equivSphereHom def SphereTopology/Homotopy/HomotopyGroup/SphereHom.lean, line 134 For every n >= 0 and arbitrary X : BasedTopCat in universe u, finite-cube homotopy classes on Fin n are equivalent as sets to based-homotopy-category morphisms from the north-based ULift of the unit n-sphere to X.
HomotopyGroup.equivSphereHom_class theorem SphereTopology/Homotopy/HomotopyGroup/SphereHom.lean, line 170 The forward image of a Fin n cube representative is the class of GenLoop.sphereHomeomorph n precomposed with ULift.down, including n = 0.
HomotopyGroup.equivSphereHom_symm_map theorem SphereTopology/Homotopy/HomotopyGroup/SphereHom.lean, line 213 The inverse image of a based unit n-sphere map class is its sphere representative precomposed with ULift.up and then pulled back along Cube.collapseToSphere n, including dimension zero.
HomotopyGroup.equivSphereHom_symm_map_eq_class theorem SphereTopology/Homotopy/HomotopyGroup/SphereHom.lean, line 237 Any Fin n generalized loop with values t ↦ f.right.hom (ULift.up (Cube.collapseToSphere n t)) represents the inverse image of the class of the based sphere map f.
Metric.Sphere.pinch_comp_collapseToSphere theorem SphereTopology/Geometry/SpherePinch.lean, line 92 The positive-dimensional sphere pinch pulls back to coordinate-zero concatenation of the two original collapse-inclusion loops.
Metric.Sphere.pinch_nondegenerate theorem SphereTopology/Geometry/SpherePinch.lean, line 190 Fixed quarter and three-quarter cube witnesses map to distinct non-head values in the two original sphere factors.
Metric.Sphere.pinch_fold_class theorem SphereTopology/Homotopy/HomotopyGroup/SpherePinch.lean, line 66 Folding based maps F then G corresponds to J(G) * J(F) under the inverse sphere-class comparison and the existing multiplication, including dimension one.
Metric.Sphere.pinch_retraction_homotopicRel theorem SphereTopology/Homotopy/HomotopyGroup/SpherePinch.lean, line 148 Both original factor retractions composed with the positive-dimensional sphere pinch are homotopic to the identity relative to the last-axis north pole.
Metric.Sphere.pinch_fold_homotopicRel_swap theorem SphereTopology/Homotopy/HomotopyGroup/SpherePinch.lean, line 246 In sphere dimensions n + 2, folding arbitrary based maps in either order after the original pinch gives maps homotopic relative to the specified north pole; targets need only a topology in an independent universe.
Metric.Sphere.pinch_homotopicRel_swap theorem SphereTopology/Homotopy/HomotopyGroup/SpherePinch.lean, line 289 In sphere dimensions n + 2, the original categorical factor swap after the pinch is homotopic to the pinch relative to the last-axis north pole.
CircleBouquet.generatorMap_bijective theorem SphereTopology/Homotopy/CircleBouquet/FundamentalGroup.lean, line 1118 The included counterclockwise circle classes freely generate the fundamental group of an arbitrary-index circle bouquet, including an empty family.
CircleBouquet.generatorEquiv def SphereTopology/Homotopy/CircleBouquet/FundamentalGroup.lean, line 1124 A multiplicative equivalence from FreeGroup I to the bouquet fundamental group whose forward homomorphism is the prescribed generator map.
CircleBouquet.lift def SphereTopology/Homotopy/CircleBouquet/FundamentalGroup.lean, line 1149 Arbitrary generator values extend uniquely to homomorphisms into a group in an independent universe; this is not arbitrary extension into monoids.
CircleBouquet.positiveGenerator_mul_ne_mul theorem SphereTopology/Homotopy/CircleBouquet/FundamentalGroup.lean, line 1290 Positive classes from distinct included circles do not commute.
Complex.exists_fixedPoint_closedBall_of_boundary_mapsTo theorem SphereTopology/Homotopy/Disk.lean, line 188 A complex-valued continuous map on a closed ball with arbitrary center and nonnegative radius has a fixed point if its sphere-boundary images lie in that ball; no interior image bound or extension to the plane is assumed.
Complex.exists_fixedPoint_closedBall theorem SphereTopology/Homotopy/Disk.lean, line 203 Every continuous self-map of a complex closed ball with arbitrary center and nonnegative radius has a fixed point in that same ball, including the radius-zero case.
Circle.degree_comp_closedBall_inclusion theorem SphereTopology/Homotopy/Disk.lean, line 74 Every continuous map from the complex closed unit disk to Circle has degree-zero boundary restriction along the stock sphere-to-closed-ball inclusion, without a basedness premise.
Circle.comp_closedBall_inclusion_ne_id theorem SphereTopology/Homotopy/Disk.lean, line 95 The same boundary restriction is not the identity of Circle; this is the complex unit-disk non-retraction theorem.
TopCat.widePushoutPointRetraction_jointly_injective theorem SphereTopology/Topology/WidePushout/Separation.lean, line 62 The selected-factor retractions jointly distinguish points of an arbitrary chosen-point wide pushout, including the empty family, without separation or finiteness assumptions.
TopCat.t0Space_widePushoutPoint_iff theorem SphereTopology/Topology/WidePushout/Separation.lean, line 127 A chosen-point wide pushout is T0 exactly when every factor is T0, with no separation premise on either side.
TopCat.t1Space_widePushoutPoint_iff theorem SphereTopology/Topology/WidePushout/Separation.lean, line 137 A chosen-point wide pushout is T1 exactly when every factor is T1, with no separation premise on either side.
TopCat.t2Space_widePushoutPoint_iff theorem SphereTopology/Topology/WidePushout/Separation.lean, line 147 A chosen-point wide pushout is Hausdorff exactly when every factor is Hausdorff, with no separation premise on either side.
IsCoveringMap.singularChainComplexTransfer def SphereTopology/Homology/Singular/Transfer.lean, line 53 All-simplex singular chain transfer for a covering map with finite point fibers, with a coefficient object in a preadditive category with the requisite coproducts.
IsCoveringMap.summandι_singularChainComplexTransfer_f theorem SphereTopology/Homology/Singular/Transfer.lean, line 73 The characteristic formula specifies a singular simplex's image as the sum of all its lifts.
IsCoveringMap.singularChainComplexTransfer_comp_map theorem SphereTopology/Homology/Singular/Transfer.lean, line 86 The sheet formula specifies transfer followed by pushforward as d times identity when finite point fibers all have cardinality d.
IsCoveringMap.singularHomologyTransfer def SphereTopology/Homology/Singular/Transfer.lean, line 104 The induced ordinary singular homology transfer in every nonnegative degree, requiring CategoryWithHomology.
IsCoveringMap.singularHomologyTransfer_comp_map theorem SphereTopology/Homology/Singular/Transfer.lean, line 123 The ordinary homology sheet formula has the same finite-fiber and constant-cardinality hypotheses as the chain formula.
Metric.Sphere.homotopyAntipodalOfUnitOrthogonal def SphereTopology/Homotopy/TangentField.lean, line 57 A continuous unit orthogonal field gives an identity-to-antipodal homotopy in any real inner-product space.
Metric.Sphere.homotopyAntipodalOfNowhereZeroOrthogonal def SphereTopology/Homotopy/TangentField.lean, line 92 Normalization supplies the same homotopy from a nowhere-zero orthogonal field; no finite-dimensional premise.
AlgebraicTopology.singularSubdivision_boundary theorem SphereTopology/Homology/Singular/Subdivision.lean, line 1553 Signed barycentric subdivision commutes with the integral singular boundary; separate naturality and degree-zero identity laws are provided.
AlgebraicTopology.singularHomotopy_boundary theorem SphereTopology/Homology/Singular/Subdivision.lean, line 1609 The support-preserving prism obeys boundary-H plus H-boundary equals identity minus subdivision, with a separate degree-zero law.
AlgebraicTopology.exists_singularSubdivisionIterate_chain_cover_small theorem SphereTopology/Homology/Singular/Subdivision.lean, line 1425 A finite-support integral chain has a common subdivision exponent making every supported simplex small for the open cover.
AlgebraicTopology.quasiIso_smallSingularChainInclusion theorem SphereTopology/Homology/Singular/SmallChains.lean, line 490 Cover-small integral singular chains include by a quasi-isomorphism, with arbitrary ambient and cover-index universes and no nonemptiness assumption.
AlgebraicTopology.smallSingularChainMap_comp_inclusion theorem SphereTopology/Homology/Singular/SmallChains.lean, line 171 Cover-compatible continuous maps commute with small-chain inclusion; refinement has its own inclusion law.
AlgebraicTopology.twoOpenSmallShortExact theorem SphereTopology/Homology/Singular/MayerVietoris.lean, line 635 Ordered two-open small-chain short exact sequence, with difference (c,-c) followed by sum.
AlgebraicTopology.twoOpenMayerVietoris_exact_at_intersection theorem SphereTopology/Homology/Singular/MayerVietoris.lean, line 1222 Ordinary integral Mayer-Vietoris exactness at the open-subspace intersection for a two-open cover.
AlgebraicTopology.twoOpenMayerVietoris_exact_at_biprod theorem SphereTopology/Homology/Singular/MayerVietoris.lean, line 1258 Exactness at the biproduct of the open-set homology objects.
AlgebraicTopology.twoOpenMayerVietoris_exact_at_space theorem SphereTopology/Homology/Singular/MayerVietoris.lean, line 1293 Exactness at ambient homology before the connecting boundary, including the H1-to-H0 segment.
AlgebraicTopology.twoOpenMayerVietorisδ_naturality_induced theorem SphereTopology/Homology/Singular/MayerVietoris.lean, line 1083 Connecting-map naturality for a continuous map preserving the specified ordered opens.
AlgebraicTopology.twoOpenMayerVietorisδ_swap_eq_neg theorem SphereTopology/Homology/Singular/MayerVietoris.lean, line 868 Reversing the ordered cover gives the integral minus sign after the explicit intersection swap.
AlgebraicTopology.integralSingularHomologyMap_eq_neg_id_of_twoOpen_swap theorem SphereTopology/Homology/Singular/MayerVietoris.lean, line 1687 A cover-swapping map acts by minus identity only with the transported-intersection identity and monic connecting-map hypotheses.
TopCat.reducedSingularHomologyFunctor def SphereTopology/Homology/Singular/Reduced.lean, line 256 Nonnegative reduced integral homology: the augmentation kernel in degree zero and ordinary homology in positive degrees.
TopCat.reducedSingularHomologyIsoOfHomotopyEquiv def SphereTopology/Homology/Singular/Reduced.lean, line 457 Homotopy equivalences induce reduced homology isomorphisms in every nonnegative degree.
TopCat.isZero_reducedSingularHomology_of_contractible theorem SphereTopology/Homology/Singular/Reduced.lean, line 521 Reduced homology vanishes for a space with a ContractibleSpace instance; this premise includes nonemptiness.
TopCat.isZero_reducedSingularHomologyZero_empty theorem SphereTopology/Homology/Singular/Reduced.lean, line 534 The empty space has zero degree-zero augmentation kernel; this is not a degree-minus-one convention.
TopCat.reducedSingularHomologyZeroTwoPointIntegerIso_swap theorem SphereTopology/Homology/Singular/Reduced.lean, line 807 Two-point transposition acts by minus identity in the fixed integral basis [false]-[true].
TopCat.isIso_singularHomology₀ε_iff_pathConnectedSpace theorem SphereTopology/Homology/Singular/Connectedness.lean, line 77 For a nonzero coefficient object in a preadditive category with small coproducts and homology, total H0 augmentation is invertible exactly when the space is path connected; nonemptiness is a conclusion, not an assumption.
TopCat.isZero_reducedSingularHomologyZero_iff_pathConnectedSpace theorem SphereTopology/Homology/Singular/Connectedness.lean, line 101 For a nonempty space, integral reduced H0 vanishes exactly when the space is path connected; nonemptiness is essential.
AlgebraicTopology.twoOpenReducedMayerVietorisδZero def SphereTopology/Homology/Singular/ReducedMayerVietoris.lean, line 127 The low-degree boundary lands in reduced H0 of the open-subspace intersection, with explicit ordinary-homology comparison.
AlgebraicTopology.twoOpenReducedMayerVietoris_exact_intersectionZero theorem SphereTopology/Homology/Singular/ReducedMayerVietoris.lean, line 586 Reduced low-degree exactness at the intersection, with separate naturality and ordered-cover swap laws.
AlgebraicTopology.twoOpenReducedMayerVietorisIsoOfAcyclicOpens def SphereTopology/Homology/Singular/ReducedMayerVietoris.lean, line 738 The reduced H1-to-H0 boundary is an isomorphism when both H0 and H1 vanish for each of the two opens.
SphereTopology.circlePunctureIntersectionHomotopyEquiv def SphereTopology/Homology/Singular/Circle.lean, line 409 The metric unit circle's east/west puncture intersection deforms to two points, with false=upper and true=lower.
SphereTopology.reducedSingularHomologyOneSphereOneIntegerIso def SphereTopology/Homology/Singular/Circle.lean, line 462 Explicit reduced H1 of the unit sphere in EuclideanSpace real (Fin 2) is isomorphic to the integers.
SphereTopology.circleReducedMayerVietoris_swap_eq_neg theorem SphereTopology/Homology/Singular/Circle.lean, line 546 The geometric ordered circle cover retains the reduced Mayer-Vietoris minus sign on reversal.
SphereTopology.sphere2PunctureIntersectionEquatorHomotopyEquiv def SphereTopology/Homology/Singular/Sphere.lean, line 425 The north/south puncture intersection of the standard metric S2 deforms to its equator by normalized (x,y,t*z); equator points are fixed.
SphereTopology.sphere2EquatorHomeomorphSphere1 def SphereTopology/Homology/Singular/Sphere.lean, line 507 Equator-to-circle coordinates preserve the ordered pair (x,y), without an implicit orientation reversal.
SphereTopology.reducedSingularHomologyTwoSphereTwoIntegerIso def SphereTopology/Homology/Singular/Sphere.lean, line 643 Explicit reduced H2 of the unit sphere in EuclideanSpace real (Fin 3) is isomorphic to the integers.
SphereTopology.sphere2PunctureIntersectionAntipodal_homotopic_id theorem SphereTopology/Homology/Singular/SphereAntipodal.lean, line 333 The antipodal action on the puncture intersection is homotopic to identity through an equatorial half-turn.
SphereTopology.integralSingularHomologyMap_sphere2Antipodal_two theorem SphereTopology/Homology/Singular/SphereAntipodal.lean, line 431 The antipodal map on the standard metric S2 acts by minus identity on ordinary integral H2, using ordered-cover exchange.
SphereTopology.reducedSingularHomologyTwoSphereTwoIntegerIso_antipodal theorem SphereTopology/Homology/Singular/SphereAntipodal.lean, line 456 In the fixed reduced-H2 integer coordinate, the antipodal action is multiplication by minus one.
SphereTopology.sphere2_id_not_homotopic_antipodal theorem SphereTopology/Homology/Singular/SphereAntipodal.lean, line 471 Identity and antipodal on the standard metric two-sphere are not continuously homotopic.
SphereTopology.sphere2_exists_zero_of_orthogonal_field theorem SphereTopology/Homotopy/HairyBallSphere2.lean, line 46 Every continuous field V from the standard metric S2 to real Euclidean 3-space, pointwise orthogonal to its base point, has a zero.

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

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.