OAI/RingTheory/DirectFiniteness/OpenDiagrams.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.KaplanskyCounterexample.Planar.ZeroBalanced line 17

   Source documentation

   An auxiliary balanced component, without an exceptional white vertex.

   structure ZeroBalanced (R : Ribbon α) (Inc : V → F → Prop)
       (ι : V → F → (A →+ B)) where
   …

   Mentions: OAI.KaplanskyCounterexample.Planar.Ribbon

2. def OAI.KaplanskyCounterexample.Planar.WeakBalanced.sumZero line 31
3. def OAI.KaplanskyCounterexample.Planar.augInc line 81

   Source documentation

   The temporary boundary is an unlabelled black vertex.

   def augInc (Inc : V → F → Prop) : Option V → F → Prop
     | none, _ => True
     | some v, f => Inc v f

4. def OAI.KaplanskyCounterexample.Planar.augMap line 85
5. structure OAI.KaplanskyCounterexample.Planar.OpenDiagram line 91

   Source documentation

   A planar partially exposed lifetime diagram. The anchor has zero weight and merely keeps a distinguished boundary rotation available at the empty word.

   structure OpenDiagram (Inc : V → F → Prop) (ι : V → F → (A →+ B))
       (f₀ : F) (w : List (F × A)) where
   …