OAI/GroupTheory/Kervaire/OuterRibbon.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.KervaireRibbon.OuterRibbon line 16

   Source documentation

   A finite genus-zero relator ribbon with a marked outside vertex. Isolated zero-sign darts are retained, so cap surgery never changes the finite universe.

   structure OuterRibbon (ρ : Perm I) (a : I → A) (s : I → ℤ) (o : D) (l : List D) where
   …

2. def OAI.KervaireRibbon.OuterRibbon.value line 34
3. lemma OAI.KervaireRibbon.dartEval_congr line 39
4. lemma OAI.KervaireRibbon.dartEval_cap line 48
5. lemma OAI.KervaireRibbon.nodup_remove_pair line 77
6. lemma OAI.KervaireRibbon.circle_cap line 89
7. theorem OAI.KervaireRibbon.OuterRibbon.cap line 118

   Source documentation

   Exact cap reduction, including preserved outside word and all relator corners. The analytic rigidity theorem supplies the one necessary alignment.

   theorem OuterRibbon.cap [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)
       {o : D} (pre post : List D) (x y : D)
       (r : OuterRibbon (V := V) ρ a s o (pre++x::y::post))
   …

   Mentions: OAI.KervaireRibbon.OuterRibbon

8. theorem OAI.KervaireRibbon.OuterRibbon.coefficient_eq_one line 261

   Source documentation

   The outside word of a planar relator ribbon can be a coefficient only when that coefficient is trivial. This is the complete inside-out cap induction.

   theorem OuterRibbon.coefficient_eq_one [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)
       {o : D} {l : List D} (r : OuterRibbon (V := V) ρ a s o l) (g : A)
   …

   Mentions: OAI.KervaireRibbon.OuterRibbon