Lagmental Vicfred

Brouwer's Fixed-Point Theorem Forbids a Retraction by Vicfred

Every continuous self-map of a closed disk has a fixed point. The formulas are more useful when each symbol has a job rather than merely decorating the theorem.

Set-up

A CW complex is assembled by attaching disks \(D^n\) along maps from their boundaries \(S^{n-1}\). Cellular chains convert the attaching data into algebra.

$$ f:D^n\to D^n $$

I read the first line as input and the second as output. The symbols \(\forall\) and \(\exists\) are not interchangeable, and neither may be upgraded silently to \(\Longleftrightarrow\).

$$ \exists x\in D^n,\qquad f(x)=x $$

The calculation

Now evaluate one representative case. The result should agree with the structural law above, but it is obtained without assuming the conclusion.

$$ f(x)\ne x\ \forall x\Longrightarrow r(x)=x+t_x(x-f(x))\in S^{n-1},\qquad r|_{S^{n-1}}=\operatorname{id} $$

What survives abstraction

The aligned summary deliberately puts the datum and conclusion on different rows. Mathematically, this is the distinction between specifying an object and proving a property of it.

$$ \begin{aligned} \mathsf{D}\;&:\quad f:D^n\to D^n,\\[5pt] \mathsf{C}\;&:\quad \exists x\in D^n,\qquad f(x)=x. \end{aligned} $$

The boundary

Euler characteristic is homotopy invariant for finite CW complexes, but equal Euler characteristics do not imply homotopy equivalence.

$$ \boxed{\begin{gathered} \text{compact conclusion}\\[-2pt] \exists x\in D^n,\qquad f(x)=x \end{gathered}} $$

The important habit is to remember what was fixed before the calculation began and what was proved only afterward. The final display preserves that order.

This article was posted on Mon 07 September 2020. Facts and circumstances may have changed since publication.
Please contact me before jumping to conclusions if something seems wrong or unclear.