Milnor.lean`

70 declarations, 0 contain sorry, 0 declared as axioms

Functoriality and product additivity on actual higher homotopy groups. This is geometric support for the literal finite idempotent diagrams.

def OAI.GroupRingTopology.Milnor.boundedInclusion line 20
def OAI.GroupRingTopology.Milnor.boundedContraction line 24
lemma OAI.GroupRingTopology.Milnor.compactMap_bounded line 31
lemma OAI.GroupRingTopology.Milnor.compactMap_nullhomotopic line 44
lemma OAI.GroupRingTopology.Milnor.sphereFillable line 49
lemma OAI.GroupRingTopology.Milnor.contractible line 66
def OAI.GroupRingTopology.Milnor.translate line 80
lemma OAI.GroupRingTopology.Milnor.translate_one line 82
lemma OAI.GroupRingTopology.Milnor.translate_mul line 84
lemma OAI.GroupRingTopology.Milnor.translate_mono line 86
lemma OAI.GroupRingTopology.Milnor.translate_valid line 88
def OAI.GroupRingTopology.Milnor.orbitSpan line 91
lemma OAI.GroupRingTopology.Milnor.orbitSpan_le line 100
lemma OAI.GroupRingTopology.Milnor.orbitSpan_mono line 101
lemma OAI.GroupRingTopology.Milnor.orbitSpan_contains line 105
lemma OAI.GroupRingTopology.Milnor.orbitSpan_invariant line 109
lemma OAI.GroupRingTopology.Milnor.orbitSpan_bounded line 114
def OAI.GroupRingTopology.Milnor.Controlled line 125
Source documentation
Uniform finite orbit control, not compactness of the infinite free orbit.
```
def Controlled (K : PreAbstractSimplicialComplex (ℕ × G)) : Prop :=
…
```
lemma OAI.GroupRingTopology.Milnor.controlled_orbitSpan line 128
lemma OAI.GroupRingTopology.Milnor.controlled_bounded line 129
lemma OAI.GroupRingTopology.Milnor.orbitSpan_finite_representatives line 134
def OAI.GroupRingTopology.Milnor.vertexMap line 153
def OAI.GroupRingTopology.Milnor.faceImage line 154
def OAI.GroupRingTopology.Milnor.imageShapes line 155
lemma OAI.GroupRingTopology.Milnor.faceImage_translate line 157
lemma OAI.GroupRingTopology.Milnor.faceImage_valid line 161
lemma OAI.GroupRingTopology.Milnor.faceImage_controlled line 165
lemma OAI.GroupRingTopology.Milnor.unionFace_valid line 174
def OAI.GroupRingTopology.Milnor.unionShapes line 199
lemma OAI.GroupRingTopology.Milnor.translate_union line 202
lemma OAI.GroupRingTopology.Milnor.unionFace_controlled line 205
def OAI.GroupRingTopology.Milnor.fresh line 218
Source documentation
A fresh relayer fixes layer zero, so the ensuing straight homotopies are based. Positive layers move above every old layer under consideration.
```
def fresh (N : ℕ) (i : ℕ) : ℕ := if i = 0 then 0 else N+i
```
lemma OAI.GroupRingTopology.Milnor.fresh_zero line 219
lemma OAI.GroupRingTopology.Milnor.fresh_injective line 220
lemma OAI.GroupRingTopology.Milnor.fresh_cross line 229
def OAI.GroupRingTopology.Milnor.shapeBound line 244
lemma OAI.GroupRingTopology.Milnor.orbit_below_bound line 246
def OAI.GroupRingTopology.Milnor.relayerFresh line 254
def OAI.GroupRingTopology.Milnor.relayerTarget line 256
lemma OAI.GroupRingTopology.Milnor.relayerLeftValid line 259
lemma OAI.GroupRingTopology.Milnor.relayerRightValid line 267
lemma OAI.GroupRingTopology.Milnor.relayerLeftMapValid line 278
lemma OAI.GroupRingTopology.Milnor.relayerRightMapValid line 283
lemma OAI.GroupRingTopology.Milnor.relayerFreshMapValid line 288
def OAI.GroupRingTopology.Milnor.relayerLeftMap line 293
def OAI.GroupRingTopology.Milnor.relayerRightMap line 295
def OAI.GroupRingTopology.Milnor.relayerFreshMap line 297
def OAI.GroupRingTopology.Milnor.relayerLeftHomotopy line 300
def OAI.GroupRingTopology.Milnor.relayerRightHomotopy line 302
def OAI.GroupRingTopology.Milnor.relayerHomotopy line 305
lemma OAI.GroupRingTopology.Milnor.relayerLeftPure line 308
lemma OAI.GroupRingTopology.Milnor.relayerRightPure line 315
lemma OAI.GroupRingTopology.Milnor.relayerLeftHomotopy_fixed line 323
lemma OAI.GroupRingTopology.Milnor.relayerRightHomotopy_fixed line 328
theorem OAI.GroupRingTopology.Milnor.relayerHomotopy_fixed line 335
Source documentation
The controlled relayer comparison is stationary on all layer-zero points.
```
theorem relayerHomotopy_fixed (x : Simplicial.Space (orbitSpan S)) (g : G)
    (hx : x.1 = Finsupp.single (0,g) 1) (t : I) :
    relayerHomotopy φ S α β hα hβ hα0 hβ0 (t,x) = relayerLeftMap φ S α β hα hα0 x := by
…
```
Mentions: OAI.GroupRingTopology.Simplicial.Space, OAI.GroupRingTopology.Milnor.orbitSpan, OAI.GroupRingTopology.Milnor.relayerHomotopy, OAI.GroupRingTopology.Milnor.relayerLeftMap
def OAI.GroupRingTopology.HomotopyFunctor.loopMap line 355
lemma OAI.GroupRingTopology.HomotopyFunctor.loopMap_homotopic line 358
def OAI.GroupRingTopology.HomotopyFunctor.map line 362
lemma OAI.GroupRingTopology.HomotopyFunctor.map_mk line 365
lemma OAI.GroupRingTopology.HomotopyFunctor.loopMap_const line 368
lemma OAI.GroupRingTopology.HomotopyFunctor.loopMap_transAt line 373
def OAI.GroupRingTopology.HomotopyFunctor.mapHom line 381
lemma OAI.GroupRingTopology.HomotopyFunctor.map_id line 394
lemma OAI.GroupRingTopology.HomotopyFunctor.map_comp line 398
lemma OAI.GroupRingTopology.HomotopyFunctor.map_const line 405
def OAI.GroupRingTopology.HomotopyFunctor.loopPair line 412
lemma OAI.GroupRingTopology.HomotopyFunctor.pair_homotopic line 415
lemma OAI.GroupRingTopology.HomotopyFunctor.product_ext line 424
lemma OAI.GroupRingTopology.HomotopyFunctor.diagonal_split line 435
Source documentation
The diagonal class in a product is the product of its two coordinate classes. This is a statement about genuine based homotopy groups.
```
lemma diagonal_split [DecidableEq N] [Nonempty N] (a : HomotopyGroup N X x) :
    map (y := (x,x)) ((ContinuousMap.id X).prodMk (ContinuousMap.id X)) rfl a =
…
```
Mentions: OAI.GroupRingTopology.HomotopyFunctor.map

theorem OAI.GroupRingTopology.HomotopyFunctor.product_additivity line 456

Source documentation

Product additivity requires no homological comparison or Hurewicz theorem.

theorem product_additivity [DecidableEq N] [Nonempty N] (F : C(X × X,Y))
    (hF : F (x,x) = y) (a : HomotopyGroup N X x) :
    map (F.comp ((ContinuousMap.id X).prodMk (ContinuousMap.id X))) hF a =
      map (F.comp ((ContinuousMap.id X).prodMk (ContinuousMap.const X x))) hF a *
      map (F.comp ((ContinuousMap.const X x).prodMk (ContinuousMap.id X))) hF a := by
…

Mentions: OAI.GroupRingTopology.HomotopyFunctor.map