RelatorRigidity.lean`

23 declarations, 0 contain sorry, 0 declared as axioms

def OAI.KervaireRibbon.corner line 15
Source documentation
The coefficient on the corner immediately following a dart.
```
def corner (σ θ : Perm D) (u : D → A) (d : D) : A := u (θ d) * (u (σ d))⁻¹
…
```
lemma OAI.KervaireRibbon.corner_gauge line 18

lemma OAI.KervaireRibbon.align_distinct_faces line 29

Source documentation

Independent face gauges can align two vertices precisely when the two relevant faces are distinct.

lemma align_distinct_faces (σ θ : Perm D) (hθ : ∀ d, θ (θ d) = d)
    (u : D → A) {p q : D} (hpq : ¬ (σ*θ).SameCycle p q) :
    ∃ v : D → A, corner σ θ v = corner σ θ u ∧ v q = v p := by
…

Mentions: OAI.KervaireRibbon.corner

lemma OAI.KervaireRibbon.planar_symm line 40
lemma OAI.KervaireRibbon.cap_vertex line 50
lemma OAI.KervaireRibbon.cap_vertex_other line 74
lemma OAI.KervaireRibbon.planar_cap line 87
lemma OAI.KervaireRibbon.suppress_u line 111
lemma OAI.KervaireRibbon.corner_cap line 132
lemma OAI.KervaireRibbon.components_map line 155
lemma OAI.KervaireRibbon.components_equiv line 172
lemma OAI.KervaireRibbon.classes_components_equiv line 182
lemma OAI.KervaireRibbon.planar_equiv line 187
lemma OAI.KervaireRibbon.connected_equiv line 195
lemma OAI.KervaireRibbon.sum_eq_zero_of_opposite line 211
lemma OAI.KervaireRibbon.vertex_balance line 216

lemma OAI.KervaireRibbon.balanced_vertices line 229

Source documentation

Exact positive/negative disk coordinates, derived from the sign conservation of the bands rather than postulated as a balancing hypothesis.

lemma balanced_vertices (ε : V → ℤ) (hε : ∀ v, ε v = 1 ∨ ε v = -1)
    (hzero : (∑ v, ε v) = 0) :
    ∃ q : ({v // ε v = 1} ⊕ {v // ε v = 1}) ≃ V,
      (∀ k, ε (q (Sum.inl k)) = 1) ∧ (∀ k, ε (q (Sum.inr k)) = -1) := by
…

def OAI.KervaireRibbon.vertexNext line 262
def OAI.KervaireRibbon.vertexCorner line 264
theorem OAI.KervaireRibbon.relator_corner_rigidity line 267
structure OAI.KervaireRibbon.DiskAtlas line 348
Source documentation
Disjoint relator disks in a larger ribbon diagram. The other darts may belong to an outside word or be isolated markers from previous cancellations.
```
structure DiskAtlas (ρ : Perm I) (a : I → A) (s : I → ℤ)
    (σ : Perm D) (t : D → ℤ) where
…
```

lemma OAI.KervaireRibbon.disk_sameCycle line 359

Source documentation

Every dart on a word disk lies in the same ribbon component as its chosen representative.

lemma disk_sameCycle (ρ : Perm I) (hρ : ∀ i j, ρ.SameCycle i j)
    (a : I → A) (s : I → ℤ) (σ : Perm D) (t : D → ℤ)
    (b : DiskAtlas (V := V) ρ a s σ t) (v : V) (i j : I) :
…

Mentions: OAI.KervaireRibbon.DiskAtlas

theorem OAI.KervaireRibbon.atlas_component_rigidity line 388

Source documentation

Restricting whole relator disks to one component retains the literal word coordinates, including the actual reversed corners of negative disks.

theorem atlas_component_rigidity [Nonempty I]
    (ρ : Perm I) (hρ : ∀ i j, ρ.SameCycle i j) (a : I → A)
    (s : I → ℤ) (hs : ∀ i, s i = 1 ∨ s i = -1) (hsum : (∑ i, s i) = 1 ∨ (∑ i, s i) = -1)
    (σ θ : Perm D) (hθ : ∀ d, θ (θ d) = d) (t : D → ℤ)
    (ht : ∀ d, t (θ d) = -t d) (hp : planar σ θ)
    (b : DiskAtlas (V := V) ρ a s σ t) (u : D → A) (p : D)
…

Mentions: OAI.KervaireRibbon.planar, OAI.KervaireRibbon.DiskAtlas