OAI/GroupTheory/Kervaire/Capping.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.KervaireRibbon.suppress_paired line 15
  2. lemma OAI.KervaireRibbon.suppress_involutive_all line 22
  3. lemma OAI.KervaireRibbon.suppress_fixed_all line 39
  4. def OAI.KervaireRibbon.capSign line 48
  5. lemma OAI.KervaireRibbon.capSign_other line 51
  6. lemma OAI.KervaireRibbon.suppress_sign line 55
  7. lemma OAI.KervaireRibbon.suppress_u_except line 82
  8. theorem OAI.KervaireRibbon.cap_alignment line 103

    Source documentation

    At a freely cancellable outside pair, the two remaining band endpoints can be aligned without changing any corner. The same-face case is exactly where the analytic planar-boundary theorem is needed.

    theorem cap_alignment [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)
…

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