OAI/Algebra/GroupRing/ConedMap.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TorsionFreeZeroDivisors.MapEuler.homeFace line 22
2. lemma OAI.TorsionFreeZeroDivisors.MapEuler.home_cycle line 25
3. def OAI.TorsionFreeZeroDivisors.MapEuler.vertexSide line 27
4. def OAI.TorsionFreeZeroDivisors.MapEuler.centralDeleted line 30
5. def OAI.TorsionFreeZeroDivisors.MapEuler.pressure line 34
6. lemma OAI.TorsionFreeZeroDivisors.MapEuler.pressure_subset line 38
7. lemma OAI.TorsionFreeZeroDivisors.MapEuler.pressure_cover line 42
8. theorem OAI.TorsionFreeZeroDivisors.MapEuler.triangular_dart line 65

   Source documentation

   A weighted centroid face and at most three boundary occurrences force one fundamental separator to remove or put on its small side at least one third of the active vertices. Active vertices have unit cost; all others have zero.

   theorem triangular_dart (active : Finset (Cycle σ)) (root : Cycle σ)
       (htri : ∀ c : Cycle φ,(members φ c).card≤3) :
       ∃ c : Cycle φ,∃ d∈members φ c,
         2*(vertexSide σ α ha T hT hz ht active d).card≤active.card ∧
         active.card≤3*(pressure σ α ha T hT hz ht active root c d).card := by
   …

   Mentions: OAI.TorsionFreeZeroDivisors.MapEuler.vertexSide, OAI.TorsionFreeZeroDivisors.MapEuler.pressure

9. lemma OAI.TorsionFreeZeroDivisors.MapEuler.opposite_disjoint_pressure line 97

   Source documentation

   The opposite retained side of a fundamental cut is disjoint from its pressure set.

   lemma opposite_disjoint_pressure (active : Finset (Cycle σ)) (root : Cycle σ)
       (c : Cycle φ) (d : O) :
       Disjoint (active.filter (fun v=>v∉fundamentalVertices σ α T ht root d ∧
         homeFace σ α v∉cotreeSide σ α ha T hT hz ht d))
         (pressure σ α ha T hT hz ht active root c d) := by
   …

   Mentions: OAI.TorsionFreeZeroDivisors.MapEuler.fundamentalVertices, OAI.TorsionFreeZeroDivisors.MapEuler.homeFace, OAI.TorsionFreeZeroDivisors.MapEuler.cotreeSide, OAI.TorsionFreeZeroDivisors.MapEuler.pressure

10. theorem OAI.TorsionFreeZeroDivisors.MapEuler.triangular_balanced_fundamental line 112

    Source documentation

    The literal two-root-path separator balances both retained sides in a triangular genus-zero map. This is the sharp bounded-radius crux; no planar embedding or separator theorem is imported.

    theorem triangular_balanced_fundamental (active : Finset (Cycle σ)) (root : Cycle σ)
        (htri : ∀ c : Cycle φ,(members φ c).card≤3) :
        ∃ d : O,
          3*(active.filter (fun v=>v∉fundamentalVertices σ α T ht root d ∧
            homeFace σ α v∈cotreeSide σ α ha T hT hz ht d)).card≤2*active.card ∧
          3*(active.filter (fun v=>v∉fundamentalVertices σ α T ht root d ∧
            homeFace σ α v∉cotreeSide σ α ha T hT hz ht d)).card≤2*active.card := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.MapEuler.fundamentalVertices, OAI.TorsionFreeZeroDivisors.MapEuler.homeFace, OAI.TorsionFreeZeroDivisors.MapEuler.cotreeSide

11. abbrev OAI.TorsionFreeZeroDivisors.ConedMap.Dart line 148

    Source documentation

    Original darts plus one radial pair for each face corner. Radial true is at the new face center, radial false at the original vertex.

    abbrev Dart (O : Type) := O ⊕ (O × Bool)

12. def OAI.TorsionFreeZeroDivisors.ConedMap.old line 149
13. def OAI.TorsionFreeZeroDivisors.ConedMap.radial line 150
14. def OAI.TorsionFreeZeroDivisors.ConedMap.center line 151
15. def OAI.TorsionFreeZeroDivisors.ConedMap.rotation line 153
16. def OAI.TorsionFreeZeroDivisors.ConedMap.pairing line 175
17. lemma OAI.TorsionFreeZeroDivisors.ConedMap.rotation_old line 177
18. lemma OAI.TorsionFreeZeroDivisors.ConedMap.rotation_radial line 178
19. lemma OAI.TorsionFreeZeroDivisors.ConedMap.rotation_center line 179
20. lemma OAI.TorsionFreeZeroDivisors.ConedMap.pairing_old line 180
21. lemma OAI.TorsionFreeZeroDivisors.ConedMap.pairing_radial line 181
22. lemma OAI.TorsionFreeZeroDivisors.ConedMap.pairing_center line 182
23. lemma OAI.TorsionFreeZeroDivisors.ConedMap.pairing_involutive line 184
24. lemma OAI.TorsionFreeZeroDivisors.ConedMap.face_old line 195
25. lemma OAI.TorsionFreeZeroDivisors.ConedMap.face_center line 196
26. lemma OAI.TorsionFreeZeroDivisors.ConedMap.face_radial line 197
27. lemma OAI.TorsionFreeZeroDivisors.ConedMap.vertex_radial line 199
28. lemma OAI.TorsionFreeZeroDivisors.ConedMap.vertex_old_apply line 200
29. lemma OAI.TorsionFreeZeroDivisors.ConedMap.vertex_center_apply line 202
30. def OAI.TorsionFreeZeroDivisors.ConedMap.vertexRaw line 207

    Source documentation

    Literal vertex classification: original vertices and the inserted face centers.

    def vertexRaw : Dart O → Cycle σ ⊕ Cycle φ
      | .inl x => .inl (cycle σ x)
      | .inr (x,false) => .inl (cycle σ x)
      | .inr (x,true) => .inr (cycle φ x)

    Mentions: OAI.TorsionFreeZeroDivisors.ConedMap.Dart

31. lemma OAI.TorsionFreeZeroDivisors.ConedMap.vertexRaw_invariant line 211
32. def OAI.TorsionFreeZeroDivisors.ConedMap.vertices line 221
33. def OAI.TorsionFreeZeroDivisors.ConedMap.vertexInverse line 223
34. lemma OAI.TorsionFreeZeroDivisors.ConedMap.vertices_right_inverse line 226
35. lemma OAI.TorsionFreeZeroDivisors.ConedMap.vertices_left_inverse line 232
36. def OAI.TorsionFreeZeroDivisors.ConedMap.vertexEquiv line 241
37. lemma OAI.TorsionFreeZeroDivisors.ConedMap.vertexEquiv_old line 244
38. lemma OAI.TorsionFreeZeroDivisors.ConedMap.vertexEquiv_radial line 245
39. lemma OAI.TorsionFreeZeroDivisors.ConedMap.vertexEquiv_center line 246
40. def OAI.TorsionFreeZeroDivisors.ConedMap.faceRaw line 249

    Source documentation

    Each coned face is the actual three-cycle old--center--radial.

    def faceRaw : Dart O → O
      | .inl x=>x
      | .inr (x,false)=>φ x
      | .inr (x,true)=>x
    omit [Fintype O] in

    Mentions: OAI.TorsionFreeZeroDivisors.ConedMap.Dart

41. lemma OAI.TorsionFreeZeroDivisors.ConedMap.faceRaw_invariant line 254
42. def OAI.TorsionFreeZeroDivisors.ConedMap.faces line 261
43. lemma OAI.TorsionFreeZeroDivisors.ConedMap.face_cycle_center line 263
44. lemma OAI.TorsionFreeZeroDivisors.ConedMap.face_cycle_radial line 265
45. lemma OAI.TorsionFreeZeroDivisors.ConedMap.faces_left_inverse line 267
46. def OAI.TorsionFreeZeroDivisors.ConedMap.faceEquiv line 276
47. lemma OAI.TorsionFreeZeroDivisors.ConedMap.face_members line 279
48. lemma OAI.TorsionFreeZeroDivisors.ConedMap.triangular line 304
49. lemma OAI.TorsionFreeZeroDivisors.ConedMap.vertex_count line 310
50. lemma OAI.TorsionFreeZeroDivisors.ConedMap.face_count line 312
51. lemma OAI.TorsionFreeZeroDivisors.ConedMap.component_face line 323
52. def OAI.TorsionFreeZeroDivisors.ConedMap.componentRaw line 326
53. lemma OAI.TorsionFreeZeroDivisors.ConedMap.componentRaw_rotation line 329
54. lemma OAI.TorsionFreeZeroDivisors.ConedMap.componentRaw_pairing line 336
55. def OAI.TorsionFreeZeroDivisors.ConedMap.componentForward line 341
56. lemma OAI.TorsionFreeZeroDivisors.ConedMap.component_radial line 343
57. lemma OAI.TorsionFreeZeroDivisors.ConedMap.component_center line 345
58. lemma OAI.TorsionFreeZeroDivisors.ConedMap.component_old_rotation line 347
59. lemma OAI.TorsionFreeZeroDivisors.ConedMap.component_old_pairing line 349
60. def OAI.TorsionFreeZeroDivisors.ConedMap.componentInverse line 351
61. def OAI.TorsionFreeZeroDivisors.ConedMap.componentEquiv line 355
62. def OAI.TorsionFreeZeroDivisors.ConedMap.supportEquiv line 373
63. lemma OAI.TorsionFreeZeroDivisors.ConedMap.support_count line 394
64. lemma OAI.TorsionFreeZeroDivisors.ConedMap.support_card_nat line 401
65. theorem OAI.TorsionFreeZeroDivisors.ConedMap.genusZero line 411

    Source documentation

    Coning all literal face cycles preserves Euler genus zero, with no geometric embedding premise and without identifying or deleting any original vertex.

    theorem genusZero (hz : GenusZero σ α) : GenusZero ρ π := by
    …