OAI/AlgebraicTopology/Cubical/Realization.lean

GitHub source file

121 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EilenbergGanea.artinDescendingData line 18

   Source documentation

   Actual right-angled Artin descending cubes supplied by the proved signed trace normal form. None of the contractibility hypotheses are postulated.

   def artinDescendingData : DescendingCube.Data
       (fun x : Letter V => letterValue (artinGenerator L) (invLetter x)) where
   …

   Mentions: OAI.EilenbergGanea.DescendingCube.Data, OAI.EilenbergGanea.artinGenerator

2. abbrev OAI.EilenbergGanea.ArtinDescendingRealization line 45
3. theorem OAI.EilenbergGanea.artinDescending_contractible line 51

   Source documentation

   Contractibility of the actual weak descending-cube realization of the Artin group, proved by an explicit globally continuous radial-shell flow.

   theorem artinDescending_contractible : ContractibleSpace (ArtinDescendingRealization L) :=
   …

   Mentions: OAI.EilenbergGanea.ArtinDescendingRealization

4. structure OAI.EilenbergGanea.CubeRealization.Cell line 63

   Source documentation

   Positive closed cubes of the actual Cayley cubical model.

   structure Cell where
   …

5. structure OAI.EilenbergGanea.CubeRealization.Point line 69

   Source documentation

   Points are represented by the unique open cube containing them.

   @[ext] structure Point (f : V → G)
       (comm : ∀ v w, L.Adj v w → Commute (f v) (f w)) where
   …

6. def OAI.EilenbergGanea.CubeRealization.active line 79
7. theorem OAI.EilenbergGanea.CubeRealization.mem_active line 81
8. def OAI.EilenbergGanea.CubeRealization.pointCell line 84
9. def OAI.EilenbergGanea.CubeRealization.product line 90
10. theorem OAI.EilenbergGanea.CubeRealization.product_empty line 94
11. abbrev OAI.EilenbergGanea.CubeRealization.Coordinates line 97
12. def OAI.EilenbergGanea.CubeRealization.ones line 99
13. theorem OAI.EilenbergGanea.CubeRealization.mem_ones line 103
14. theorem OAI.EilenbergGanea.CubeRealization.ones_subset line 108
15. def OAI.EilenbergGanea.CubeRealization.normalizedCoord line 113
16. theorem OAI.EilenbergGanea.CubeRealization.normalizedCoord_mem line 117
17. theorem OAI.EilenbergGanea.CubeRealization.normalizedCoord_notMem line 123
18. def OAI.EilenbergGanea.CubeRealization.characteristic line 129

    Source documentation

    Boundary coordinates equal to1 translate the initial vertex; coordinates0 or1 are dropped from the unique open face.

    def characteristic (c : Cell (G := G) L) (x : Coordinates c) : Point (G := G) L f comm where
    …

    Mentions: OAI.EilenbergGanea.CubeRealization.Cell, OAI.EilenbergGanea.CubeRealization.Coordinates, OAI.EilenbergGanea.CubeRealization.Point

19. theorem OAI.EilenbergGanea.CubeRealization.characteristic_coord line 157
20. def OAI.EilenbergGanea.CubeRealization.pointCoordinates line 163

    Source documentation

    Canonical coordinates in the unique open cell.

    def pointCoordinates (p : Point (G := G) L f comm) : Coordinates (pointCell p) :=
    …

    Mentions: OAI.EilenbergGanea.CubeRealization.Point, OAI.EilenbergGanea.CubeRealization.Coordinates, OAI.EilenbergGanea.CubeRealization.pointCell

21. theorem OAI.EilenbergGanea.CubeRealization.pointCoordinates_coe line 166
22. theorem OAI.EilenbergGanea.CubeRealization.ones_pointCoordinates line 169
23. theorem OAI.EilenbergGanea.CubeRealization.characteristic_point line 178
24. abbrev OAI.EilenbergGanea.CubeRealization.CubeSum line 188
25. def OAI.EilenbergGanea.CubeRealization.evaluation line 190
26. theorem OAI.EilenbergGanea.CubeRealization.evaluation_surjective line 193
27. instance OAI.EilenbergGanea.CubeRealization.pointTopology line 199

    Source documentation

    The weak topology of the actual closed cubes, without asserting any missing geometric/homological properties of this construction.

    instance pointTopology : TopologicalSpace (Point (G := G) L f comm) :=
    …

    Mentions: OAI.EilenbergGanea.CubeRealization.Point

28. theorem OAI.EilenbergGanea.CubeRealization.evaluation_quotient line 202
29. theorem OAI.EilenbergGanea.CubeRealization.characteristic_continuous line 205
30. def OAI.EilenbergGanea.CubeInterpolation.translation line 215
31. theorem OAI.EilenbergGanea.CubeInterpolation.translation_apply line 223
32. def OAI.EilenbergGanea.CubeInterpolation.blend line 226
33. theorem OAI.EilenbergGanea.CubeInterpolation.blend_apply line 229
34. theorem OAI.EilenbergGanea.CubeInterpolation.blend_zero line 232
35. theorem OAI.EilenbergGanea.CubeInterpolation.blend_one line 233
36. theorem OAI.EilenbergGanea.CubeInterpolation.blend_commute line 235
37. def OAI.EilenbergGanea.CubeInterpolation.operator line 244
38. theorem OAI.EilenbergGanea.CubeInterpolation.operator_empty line 249
39. theorem OAI.EilenbergGanea.CubeInterpolation.operator_insert line 251
40. theorem OAI.EilenbergGanea.CubeInterpolation.operator_congr line 257
41. theorem OAI.EilenbergGanea.CubeInterpolation.operator_continuous line 264

    Source documentation

    Every cubical interpolation coordinate is a genuine finite polynomial.

    theorem operator_continuous {Z : Type*} [TopologicalSpace Z]
        (s : Finset V) (hs) (x : Z → V → ℝ) (hx : ∀ v ∈ s, Continuous (fun z => x z v))
        (φ : G → ℝ) (a : G) : Continuous (fun z => operator f s hs (x z) φ a) := by
    …

    Mentions: OAI.EilenbergGanea.CubeInterpolation.operator

42. theorem OAI.EilenbergGanea.CubeInterpolation.operator_subset line 276

    Source documentation

    Zero coordinates may be deleted without changing the interpolation.

    theorem operator_subset (s t : Finset V) (ht : (t : Set V).Pairwise (fun v w => Commute (f v) (f w)))
        (hst : s ⊆ t) (x : V → ℝ) (hx : ∀ v ∈ t, v ∉ s → x v = 0) :
        operator f t ht x = operator f s (ht.mono hst) x := by
    …

    Mentions: OAI.EilenbergGanea.CubeInterpolation.operator

43. theorem OAI.EilenbergGanea.CubeInterpolation.commute_ite_one line 311
44. theorem OAI.EilenbergGanea.CubeInterpolation.noncommProd_ite line 314
45. def OAI.EilenbergGanea.CubeInterpolation.normalize line 330
46. theorem OAI.EilenbergGanea.CubeInterpolation.translation_blend_commute line 332
47. theorem OAI.EilenbergGanea.CubeInterpolation.operator_normalize line 337
48. theorem OAI.EilenbergGanea.CubeInterpolation.operator_nonneg line 373

    Source documentation

    Nonnegative vertex data interpolate nonnegatively throughout every cube.

    theorem operator_nonneg (s : Finset V) (hs) (x : V → ℝ)
        (hx : ∀ v ∈ s, x v ∈ Set.Icc (0 : ℝ) 1)
        (φ : G → ℝ) (hφ : ∀ a, 0 ≤ φ a) (a : G) : 0 ≤ operator f s hs x φ a := by
    …

    Mentions: OAI.EilenbergGanea.CubeInterpolation.operator

49. theorem OAI.EilenbergGanea.CubeInterpolation.operator_pos line 385

    Source documentation

    The initial vertex has strictly positive weight in its own open cube.

    theorem operator_pos (s : Finset V) (hs) (x : V → ℝ)
        (hx : ∀ v ∈ s, x v ∈ Set.Ico (0 : ℝ) 1)
        (φ : G → ℝ) (hφ : ∀ a, 0 ≤ φ a) (a : G) (ha : 0 < φ a) :
        0 < operator f s hs x φ a := by
    …

    Mentions: OAI.EilenbergGanea.CubeInterpolation.operator

50. theorem OAI.EilenbergGanea.CubeInterpolation.operator_vanish line 402

    Source documentation

    No interpolation value detects a vertex below its initial height. At the initial height it detects only the initial vertex itself.

    theorem operator_vanish (h : G →* Multiplicative ℤ) (hf : ∀ v, (h (f v)).toAdd = 1)
        (s : Finset V) (hs) (x : V → ℝ) (φ : G → ℝ) (a : G)
        (ha : φ a = 0) (hφ : ∀ b, (h a).toAdd < (h b).toAdd → φ b = 0) :
        operator f s hs x φ a = 0 := by
    …

    Mentions: OAI.EilenbergGanea.CubeInterpolation.operator

51. theorem OAI.EilenbergGanea.CubeInterpolation.operator_linear line 417

    Source documentation

    Interpolation of a group homomorphism is the ordinary affine coordinate.

    theorem operator_linear (h : G →* Multiplicative ℝ) (s : Finset V) (hs)
        (x : V → ℝ) (a : G) :
        operator f s hs x (fun a => (h a).toAdd) a =
          (h a).toAdd + ∑ v ∈ s, x v * (h (f v)).toAdd := by
    …

    Mentions: OAI.EilenbergGanea.CubeInterpolation.operator

52. theorem OAI.EilenbergGanea.CubeRealization.cellComm line 441
53. def OAI.EilenbergGanea.CubeRealization.fullCoord line 447
54. theorem OAI.EilenbergGanea.CubeRealization.fullCoord_mem line 451
55. theorem OAI.EilenbergGanea.CubeRealization.fullCoord_notMem line 455
56. theorem OAI.EilenbergGanea.CubeRealization.fullCoord_continuous line 459
57. theorem OAI.EilenbergGanea.CubeRealization.ones_eq_filter line 467
58. theorem OAI.EilenbergGanea.CubeRealization.normalize_fullCoord line 478
59. def OAI.EilenbergGanea.CubeRealization.interpolation line 487
60. theorem OAI.EilenbergGanea.CubeRealization.active_characteristic_subset line 490
61. theorem OAI.EilenbergGanea.CubeRealization.interpolation_characteristic line 497

    Source documentation

    Literal face compatibility of multilinear vertex interpolation.

    theorem interpolation_characteristic (c : Cell (G := G) L) (x : Coordinates c) (φ : G → ℝ) :
    …

    Mentions: OAI.EilenbergGanea.CubeRealization.Cell, OAI.EilenbergGanea.CubeRealization.Coordinates

62. theorem OAI.EilenbergGanea.CubeRealization.interpolation_continuous line 512

    Source documentation

    These separating coordinates are continuous for the actual weak topology.

    theorem interpolation_continuous (φ : G → ℝ) :
        Continuous (fun p : Point (G := G) L f comm => interpolation L f comm p φ) := by
    …

    Mentions: OAI.EilenbergGanea.CubeRealization.Point, OAI.EilenbergGanea.CubeRealization.interpolation

63. theorem OAI.EilenbergGanea.CubeRealization.interpolation_vertex_pos line 524
64. theorem OAI.EilenbergGanea.CubeRealization.interpolation_vertex_zero line 532
65. theorem OAI.EilenbergGanea.CubeRealization.interpolation_base_eq line 542
66. theorem OAI.EilenbergGanea.CubeRealization.interpolation_exponent line 566
67. theorem OAI.EilenbergGanea.CubeRealization.interpolation_injective line 579

    Source documentation

    Interpolation distances separate actual points, not merely vertices.

    theorem interpolation_injective : Function.Injective
        (fun p : Point (G := G) L f comm => fun φ : G → ℝ => interpolation L f comm p φ) := by
    …

    Mentions: OAI.EilenbergGanea.CubeRealization.Point, OAI.EilenbergGanea.CubeRealization.interpolation

68. theorem OAI.EilenbergGanea.CubeRealization.point_t2 line 594

    Source documentation

    Hausdorffness follows from continuous multilinear vertex functions.

    theorem point_t2 : T2Space (Point (G := G) L f comm) :=
    …

    Mentions: OAI.EilenbergGanea.CubeRealization.Point

69. theorem OAI.EilenbergGanea.CubeRealization.Cell.ext line 608
70. abbrev OAI.EilenbergGanea.CubeRealization.DimCell line 612
71. def OAI.EilenbergGanea.CubeRealization.coordEquiv line 615
72. def OAI.EilenbergGanea.CubeRealization.chartCoordinates line 618
73. def OAI.EilenbergGanea.CubeRealization.cubeCoordinatesInv line 621
74. theorem OAI.EilenbergGanea.CubeRealization.chartCoordinates_continuous line 625
75. theorem OAI.EilenbergGanea.CubeRealization.cubeCoordinatesInv_continuous line 632
76. theorem OAI.EilenbergGanea.CubeRealization.cubeCoordinatesInv_mem_disk line 639
77. theorem OAI.EilenbergGanea.CubeRealization.chartCoordinates_cubeCoordinatesInv line 649
78. theorem OAI.EilenbergGanea.CubeRealization.chartCoordinates_disk line 657
79. theorem OAI.EilenbergGanea.CubeRealization.chartCoordinates_open line 667
80. theorem OAI.EilenbergGanea.CubeRealization.cubeCoordinatesInv_open line 676
81. theorem OAI.EilenbergGanea.CubeRealization.characteristic_open_cell line 686
82. def OAI.EilenbergGanea.CubeRealization.chartInverse line 708

    Source documentation

    Real inverse coordinates of an open cube, without any assumed chart.

    def chartInverse {n : ℕ} (c : DimCell (G := G) (L := L) n)
    …

    Mentions: OAI.EilenbergGanea.CubeRealization.DimCell

83. theorem OAI.EilenbergGanea.CubeRealization.chart_left_inv line 713
84. theorem OAI.EilenbergGanea.CubeRealization.chart_right_inv line 722
85. theorem OAI.EilenbergGanea.CubeRealization.chartInverse_mem_source line 732
86. def OAI.EilenbergGanea.CubeRealization.chart line 744

    Source documentation

    The actual positive-cube open chart.

    def chart {n : ℕ} (c : DimCell (G := G) (L := L) n) :
    …

    Mentions: OAI.EilenbergGanea.CubeRealization.DimCell

87. theorem OAI.EilenbergGanea.CubeRealization.chart_continuous line 755
88. theorem OAI.EilenbergGanea.CubeRealization.chartInverse_continuousOn line 762
89. theorem OAI.EilenbergGanea.CubeRealization.cubeCoordinatesInv_chart line 787
90. theorem OAI.EilenbergGanea.CubeRealization.chart_image_disk line 794
91. theorem OAI.EilenbergGanea.CubeRealization.chart_image_ball line 804
92. def OAI.EilenbergGanea.CubeRealization.faceCell line 809

    Source documentation

    Finite collection containing every closed face of a fixed cube.

    def faceCell (c : Cell (G := G) L) (o a : Finset V) : Cell (G := G) L where
    …

    Mentions: OAI.EilenbergGanea.CubeRealization.Cell

93. def OAI.EilenbergGanea.CubeRealization.faces line 814
94. def OAI.EilenbergGanea.CubeRealization.dimFaces line 817
95. theorem OAI.EilenbergGanea.CubeRealization.pointCell_characteristic_mem_faces line 820
96. theorem OAI.EilenbergGanea.CubeRealization.boundary_dimension_lt line 831

    Source documentation

    Every point on a characteristic sphere lies in a strictly lower open cube.

    theorem boundary_dimension_lt {n : ℕ} (c : DimCell (G := G) (L := L) n)
    …

    Mentions: OAI.EilenbergGanea.CubeRealization.DimCell

97. theorem OAI.EilenbergGanea.CubeRealization.chart_mapsTo line 857
98. def OAI.EilenbergGanea.CubeRealization.cwComplex line 878

    Source documentation

    The ordinary CW structure follows from the genuine normalized-cube gluing; no combinatorial homology or contractibility assertion enters this definition.

    @[instance_reducible] def cwComplex : CWComplex (univ : Set (Point (G := G) L f comm)) where
    …

    Mentions: OAI.EilenbergGanea.CubeRealization.Point

99. theorem OAI.EilenbergGanea.CubeInterpolation.operator_support line 925

    Source documentation

    A nonzero interpolation value comes from one of the finitely many corners.

    theorem operator_support (s : Finset V)
        (hs : (s : Set V).Pairwise (fun v w => Commute (f v) (f w)))
        (x : V → ℝ) (φ : G → ℝ) (a : G) (h : operator f s hs x φ a ≠ 0) :
        ∃ (t : Finset V) (ht : t ⊆ s), φ (a * t.noncommProd f (hs.mono ht)) ≠ 0 := by
    …

    Mentions: OAI.EilenbergGanea.CubeInterpolation.operator

100. abbrev OAI.EilenbergGanea.CubeRealization.CliqueIndex line 959

     Source documentation

     Actual finite cliques, including the empty clique.

     abbrev CliqueIndex := {s : Finset V // (s : Set V).Pairwise L.Adj}

101. def OAI.EilenbergGanea.CubeRealization.cliqueProduct line 961
102. def OAI.EilenbergGanea.CubeRealization.vertexStar line 963
103. theorem OAI.EilenbergGanea.CubeRealization.vertexStar_open line 966
104. theorem OAI.EilenbergGanea.CubeRealization.mem_vertexStar_self line 969
105. theorem OAI.EilenbergGanea.CubeRealization.vertexStar_base line 972
106. theorem OAI.EilenbergGanea.CubeRealization.vertexStar_finite_bases line 983

     Source documentation

     Only finitely many initial vertices occur in an open vertex star.

     theorem vertexStar_finite_bases (b : G) :
         (Point.base '' vertexStar L f comm b).Finite := by
     …

     Mentions: OAI.EilenbergGanea.CubeRealization.vertexStar

107. theorem OAI.EilenbergGanea.CubeRealization.compact_finite_bases line 992

     Source documentation

     Every compact set in the actual realization has finitely many initial vertices. The initial-vertex function itself need not be continuous.

     theorem compact_finite_bases {K : Set (Point (G := G) L f comm)} (hK : IsCompact K) :
     …

     Mentions: OAI.EilenbergGanea.CubeRealization.Point

108. def OAI.EilenbergGanea.CubeRealization.cliqueCell line 1006

     Source documentation

     Every point with prescribed initial vertex belongs to some closed positive cube at that vertex.

     def cliqueCell (b : G) (s : CliqueIndex L) : Cell (G := G) L := ⟨b,s.val,s.property⟩

     Mentions: OAI.EilenbergGanea.CubeRealization.CliqueIndex, OAI.EilenbergGanea.CubeRealization.Cell

109. theorem OAI.EilenbergGanea.CubeRealization.vertexStar_compact_neighborhood line 1008
110. theorem OAI.EilenbergGanea.CubeRealization.point_weaklyLocallyCompact line 1031

     Source documentation

     Local compactness is proved from finite generator stars and the actual closed-cube maps, not asserted as a cubical-model input.

     theorem point_weaklyLocallyCompact : WeaklyLocallyCompactSpace (Point (G := G) L f comm) :=
     …

     Mentions: OAI.EilenbergGanea.CubeRealization.Point

111. instance OAI.EilenbergGanea.CubeRealization.pointMulAction line 1043

     Source documentation

     Deck translations on the literal positive-cube realization.

     instance pointMulAction : MulAction G (Point (G := G) L f comm) where
     …

     Mentions: OAI.EilenbergGanea.CubeRealization.Point

112. theorem OAI.EilenbergGanea.CubeRealization.smul_base line 1049
113. theorem OAI.EilenbergGanea.CubeRealization.smul_coord line 1053
114. def OAI.EilenbergGanea.CubeRealization.translateCell line 1056
115. theorem OAI.EilenbergGanea.CubeRealization.smul_characteristic line 1060
116. instance OAI.EilenbergGanea.CubeRealization.pointContinuousConstSMul line 1065
117. instance OAI.EilenbergGanea.CubeRealization.pointIsCancelSMul line 1075
118. instance OAI.EilenbergGanea.CubeRealization.pointProperlyDiscontinuousSMul line 1082
119. instance OAI.EilenbergGanea.CubeRealization.subgroupContinuousConstSMul line 1099
120. instance OAI.EilenbergGanea.CubeRealization.subgroupProperlyDiscontinuousSMul line 1104
121. theorem OAI.EilenbergGanea.CubeRealization.subgroup_quotient_covering line 1114

     Source documentation

     The actual quotient by any subgroup is a covering map. No contractibility or classifying-space identification is assumed in this theorem.

     theorem subgroup_quotient_covering (H : Subgroup G) :
         IsQuotientCoveringMap
           (Quotient.mk (MulAction.orbitRel H (Point (G := G) L f comm))) H := by
     …

     Mentions: OAI.EilenbergGanea.CubeRealization.Point