OAI/Algebra/GroupRing/CellularFurther.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.GroupRingTopology.Cellular.ChartDisk line 21
  2. abbrev OAI.GroupRingTopology.Cellular.ChartCore line 22
  3. def OAI.GroupRingTopology.Cellular.chartCoreInclusion line 24
  4. def OAI.GroupRingTopology.Cellular.chartCore line 28
  5. lemma OAI.GroupRingTopology.Cellular.chartCore_closedEmbedding line 30
  6. def OAI.GroupRingTopology.Cellular.chartDomain line 39
  7. lemma OAI.GroupRingTopology.Cellular.chartDomain_closed line 41
  8. def OAI.GroupRingTopology.Cellular.coreCoordinate line 44
  9. lemma OAI.GroupRingTopology.Cellular.coreCoordinate_fac line 50
  10. lemma OAI.GroupRingTopology.Cellular.coreCoordinate_frontier line 54
  11. lemma OAI.GroupRingTopology.Cellular.chartDomain_dimH_le line 73
  12. def OAI.GroupRingTopology.Cellular.chartCenter line 86
  13. lemma OAI.GroupRingTopology.Cellular.exists_chart_avoidance line 91

    Source documentation

    A map of smaller dimension can be homotoped off one cell centre, without changing it outside the cell. This works for merely continuous maps, not just piecewise linear maps.

    lemma exists_chart_avoidance [T2Space Y] [CompactSpace K] (e : C(ChartDisk n,Y)) (he : IsOpenEmbedding e) (f : C(K,Y))
    (hdim : dimH (Set.univ : Set K) < n) :
    ∃ (g : C(K,Y)) (H : f.Homotopy g),
      (∀ x, g x ≠ chartCenter e) ∧
      (∀ (t : unitInterval) (x : K), f x ∉ Set.range e → H (t,x) = f x) ∧
      (∀ (t : unitInterval) (x : K), H (t,x) = f x ∨ H (t,x) ∈ Set.range e) := by
…

    Mentions: OAI.GroupRingTopology.Cellular.ChartDisk, OAI.GroupRingTopology.Cellular.chartCenter

  14. lemma OAI.GroupRingTopology.Cellular.homotopy_trans_pointwise line 182
  15. lemma OAI.GroupRingTopology.Cellular.chartCenter_mem_range line 198
  16. lemma OAI.GroupRingTopology.Cellular.exists_finite_chart_avoidance line 201
  17. lemma OAI.GroupRingTopology.Cellular.exists_all_chart_avoidance line 252
  18. def OAI.GroupRingTopology.Attachment.chart line 283
  19. lemma OAI.GroupRingTopology.Attachment.exists_deformation_into_base line 288

    Source documentation

    Maps of dimension below the newly attached cells can be deformed into the old space. The deformation is stationary on the original preimage of it.

    lemma exists_deformation_into_base (f : C(K,Space a))
    (hdim : dimH (Set.univ : Set K) < n) :
    ∃ (g : C(K,X)) (H : f.Homotopy ((⟨base a,continuous_base a⟩ : C(X,Space a)).comp g)),
      ∀ t x, f x ∈ Set.range (base a) → H (t,x) = f x := by
…

    Mentions: OAI.GroupRingTopology.Attachment.Space, OAI.GroupRingTopology.Attachment.base, OAI.GroupRingTopology.Attachment.continuous_base

  20. lemma OAI.GroupRingTopology.GeneralPosition.lipschitz_insertNth line 334
  21. lemma OAI.GroupRingTopology.GeneralPosition.sphere_subset_faces line 346
  22. lemma OAI.GroupRingTopology.GeneralPosition.dimH_cube_boundary_le line 362
  23. lemma OAI.GroupRingTopology.GeneralPosition.dimH_cube_boundary_subtype_le line 375