The no-retraction theorem and Brouwer's fixed-point theorem

The boundary sphere ∂Dⁿ = TopCat.diskBoundary n is not a retract of the disk Dⁿ = TopCat.disk n (TauCeti.noRetraction_diskBoundary), and consequently every continuous self-map of Dⁿ has a fixed point (TauCeti.brouwerFixedPoint_topCatDisk). The theorem then passes to every nonempty compact convex subset of a finite-dimensional real normed space (TauCeti.brouwerFixedPoint_compactConvex), with no assumption that the set has nonempty interior.

For n = 0 the boundary is empty while the disk is a point, so there is no map at all from the disk to its boundary. For n = m + 1, apply reduced singular homology in degree m with integer coefficients to maps i : Sᵐ ⟶ Dᵐ⁺¹ and r : Dᵐ⁺¹ ⟶ Sᵐ with i ≫ r = 𝟙: the identity of H~ₘ(Sᵐ; ℤ) ≅ ℤ (TauCeti.reducedSingularHomologyTopCatSphereIso) would factor as i_* followed by r_* through H~ₘ(Dᵐ⁺¹; ℤ), which vanishes as the disk is contractible (TauCeti.isZero_reducedSingularHomologyFunctor_of_contractibleSpace).

A self-map f of the disk without fixed points gives a retraction of the boundary inclusion, sending x to the point where the ray from f x through x meets the boundary sphere (ContinuousMap.closedBallRayRetraction), so no such f exists.

A nonempty compact convex set C has a point c of its intrinsic interior, and is then homeomorphic to the closed unit ball of the direction V of its affine span (TauCeti.convexClosedBallHomeomorph). Since V is finite-dimensional, its closed unit ball is homeomorphic to the disk of dimension finrank ℝ V (TauCeti.closedBallHomeomorphOfFinrankEq), and the fixed-point property is invariant under homeomorphisms (Homeomorph.forall_exists_isFixedPt_iff).

Main results

• TauCeti.noRetraction_diskBoundary: ∂Dⁿ is not a retract of Dⁿ; in particular the boundary inclusion ∂Dⁿ ⟶ Dⁿ has no retraction.
• TauCeti.brouwerFixedPoint_topCatDisk: Brouwer's fixed-point theorem for Dⁿ.
• TauCeti.brouwerFixedPoint_compactConvex: Brouwer's fixed-point theorem for a nonempty compact convex subset of a finite-dimensional real normed space.
• TauCeti.brouwerFixedPoint_compactConvex_finiteSpan: the same for a compact convex set lying in a finite-dimensional subspace of an arbitrary real normed space, and TauCeti.brouwerFixedPoint_compactConvex_continuousOn for a function of the ambient space that is continuous on a compact convex set with finite-dimensional span and maps it into itself.
• TauCeti.brouwerFixedPoint_closedBall: closed balls of nonnegative radius.

References

• A. Hatcher, Algebraic Topology, Section 2.1, Corollary 2.15.

theorem TauCeti.noRetraction_diskBoundary (n : ℕ) : IsEmpty (CategoryTheory.Retract (TopCat.diskBoundary n) (TopCat.disk n))

The no-retraction theorem: the boundary sphere ∂Dⁿ of the disk is not a retract of the disk Dⁿ. That is, there are no maps i : ∂Dⁿ ⟶ Dⁿ and r : Dⁿ ⟶ ∂Dⁿ with i ≫ r = 𝟙; in particular the boundary inclusion TopCat.diskBoundaryInclusion n has no retraction. This includes n = 0, where the boundary is empty.

theorem TauCeti.brouwerFixedPoint_topCatDisk (n : ℕ) (f : TopCat.disk n ⟶ TopCat.disk n) : ∃ (x : ↑(TopCat.disk n)), Function.IsFixedPt (⇑(CategoryTheory.ConcreteCategory.hom f)) x

Brouwer's fixed-point theorem: every continuous self-map of the disk Dⁿ has a fixed point.

theorem TauCeti.brouwerFixedPoint_compactConvex {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {C : Set E} (hC : IsCompact C) (hconv : Convex ℝ C) (hne : C.Nonempty) (f : C(↑C, ↑C)) : ∃ (x : ↑C), Function.IsFixedPt (⇑f) x

Brouwer's fixed-point theorem for compact convex sets: every continuous self-map of a nonempty compact convex subset of a finite-dimensional real normed space has a fixed point. The set may have empty interior.

theorem TauCeti.brouwerFixedPoint_closedBall {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (x : E) {r : ℝ} (hr : 0 ≤ r) (f : C(↑(Metric.closedBall x r), ↑(Metric.closedBall x r))) : ∃ (y : ↑(Metric.closedBall x r)), Function.IsFixedPt (⇑f) y

Brouwer's fixed-point theorem for closed balls: every continuous self-map of a closed ball of nonnegative radius in a finite-dimensional real normed space has a fixed point.

theorem TauCeti.brouwerFixedPoint_compactConvex_finiteSpan {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : Submodule ℝ E) [FiniteDimensional ℝ ↥V] {C : Set E} (hCV : C ⊆ ↑V) (hC : IsCompact C) (hconv : Convex ℝ C) (hne : C.Nonempty) (f : C(↑C, ↑C)) : ∃ (x : ↑C), Function.IsFixedPt (⇑f) x

Brouwer's fixed-point theorem for compact convex sets in a finite-dimensional subspace: every continuous self-map of a nonempty compact convex set C lying in a finite-dimensional subspace V of an arbitrary real normed space has a fixed point.

theorem TauCeti.brouwerFixedPoint_compactConvex_continuousOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {C : Set E} [FiniteDimensional ℝ ↥(Submodule.span ℝ C)] (hC : IsCompact C) (hconv : Convex ℝ C) (hne : C.Nonempty) {f : E → E} (hf : ContinuousOn f C) (hfC : Set.MapsTo f C C) : ∃ x ∈ C, Function.IsFixedPt f x

Brouwer's fixed-point theorem for compact convex sets, for a function on the ambient space: a function continuous on a nonempty compact convex subset C of a real normed space, whose span is finite-dimensional, and mapping C into itself has a fixed point in C.