OAI/GroupTheory/Kervaire/Annulus.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KervaireRibbon.annulus line 12
  2. def OAI.KervaireRibbon.pairing line 13
  3. lemma OAI.KervaireRibbon.annulus_planar line 16
  4. def OAI.KervaireRibbon.markAnnulus line 55

    Source documentation

    Adding a zero-sign marked corner just inserts a bivalent boundary point.

    def markAnnulus (ρ : Perm I) (i : I) : Perm ((I ⊕ I) ⊕ (PUnit : Type)) :=
…
  5. lemma OAI.KervaireRibbon.markAnnulus_marker line 59
  6. lemma OAI.KervaireRibbon.markAnnulus_disk line 62
  7. lemma OAI.KervaireRibbon.markAnnulus_outside line 65
  8. lemma OAI.KervaireRibbon.markAnnulus_planar line 72
  9. lemma OAI.KervaireRibbon.markAnnulus_circle line 81
  10. def OAI.KervaireRibbon.basePotential line 97
  11. def OAI.KervaireRibbon.baseSign line 99
  12. lemma OAI.KervaireRibbon.base_corner_disk line 103
  13. lemma OAI.KervaireRibbon.base_corner_outside line 108
  14. lemma OAI.KervaireRibbon.base_corner_marker line 119
  15. def OAI.KervaireRibbon.OuterRibbon.base line 125

    Source documentation

    The annulus between a single oppositely oriented relator disk and its outside word has a literal genus-zero ribbon witness.

    def OuterRibbon.base (ρ : Perm I) (hρ : ∀ i j, ρ.SameCycle i j) (a : I → A)
    (s : I → ℤ) (hs : ∀ i, s i = 1 ∨ s i = -1) (i : I) (l : List I)
    (hc : Circle ρ i l) (hn : (i::l).Nodup) (hcover : ∀ j, j ∈ i::l) :
    OuterRibbon (D := (I⊕I)⊕(PUnit : Type)) (V := (PUnit : Type)) ρ a s (Sum.inr PUnit.unit) ((i::l).map (fun j ↦ Sum.inl (Sum.inr j))) := by
…

    Mentions: OAI.KervaireRibbon.Circle, OAI.KervaireRibbon.OuterRibbon

  16. lemma OAI.KervaireRibbon.OuterRibbon.value_base line 171