OAI/AlgebraicGeometry/CharacterVarieties/Foundation/Incidence.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.Side line 11

   Source documentation

   A side is an occurrence, not a facet: none denotes the parent and some j the j-th ordered child. The same facet may appear arbitrarily often.

   abbrev Side (S : Type*) (arity : S → ℕ) := (s : S) × Option (Fin (arity s))

2. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.Germ line 12
3. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.positive line 15

   Source documentation

   The positive boundary orientation follows the seam parameter on the parent and goes against it on every child.

   def positive {S : Type*} {arity : S → ℕ} (a : Side S arity) : Bool := a.2.isNone

   Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.Side

4. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.start line 17
5. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.finish line 18
6. structure OAI.IntegralCharacterVarieties.OccurrenceIncidence.Corners line 21

   Source documentation

   Frame-independent incidence data before imposing the allowed vertex tables. Facets and germs stay separate. Corner maps cannot accidentally identify two occurrences merely because they sit on the same facet.

   structure Corners (F S : Type*) (arity : S → ℕ) where
   …

7. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.Corners.mate_finish line 31
8. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.Corners.mate_start line 40
9. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.Corners.mate_ne line 47
10. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.Corners.boundaryNext line 56

    Source documentation

    The next-side permutation of the oriented facet boundaries. All finite cycles, in particular self-incidences and one-side circles, are retained.

    def boundaryNext : Equiv.Perm (Side S arity) where
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.Side

11. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.Corners.boundaryNext_facet line 68
12. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.Corners.boundaryPrev_facet line 71
13. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.Corners.boundaryNext_iterate_facet line 74
14. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.Corners.occurrence_preserved line 82

    Source documentation

    Distinct side-germ occurrences never collapse under the boundary successor, even when all of their facets coincide.

    theorem occurrence_preserved (a b : Side S arity) :
        D.boundaryNext a=D.boundaryNext b ↔ a=b := D.boundaryNext.injective.eq_iff
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.Side

15. structure OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable line 91

    Source documentation

    One local vertex table. Every endpoint port has its own full ordered side list. A mate is a pairing of occurrences, not an identification of facets.

    structure VertexTable where
    …

16. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.passage line 102

    Source documentation

    A continuation or interchange has precisely two ports.

    def passage {C : Type} (σ : Equiv.Perm C) : VertexTable where
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable

17. inductive OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Passage line 115

    Source documentation

    Only these two passage permutations are allowed in a surface diagram. An arbitrary permutation is factored into several vertices, never one vertex.

    inductive Passage (m : ℕ) where
    …

18. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Passage.permutation line 121
19. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Passage.table line 125
20. inductive OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.SplitPort line 128
21. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.splitChild line 132

    Source documentation

    Ordered child lists: prefix, the split block, suffix; and then prefix, its ordered subblocks, suffix. The third seam carries just those subblocks.

    def splitChild (A B C : Type) : SplitPort → Type
      | .before => A ⊕ (Unit ⊕ C)
      | .after => A ⊕ (B ⊕ C)
      | .branch => B
    
    /-- Germ matching at a split. In particular the child W and the parent W are different occurrences; each subblock is also used twice, not collapsed. -/

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.SplitPort, OAI.IntegralCharacterVarieties.OccurrenceIncidence.Germ

22. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.splitMate line 138

    Source documentation

    Germ matching at a split. In particular the child W and the parent W are different occurrences; each subblock is also used twice, not collapsed.

    def splitMate {A B C : Type} : ((p : SplitPort) × Option (splitChild A B C p)) →
        ((p : SplitPort) × Option (splitChild A B C p))
      | ⟨.before,none⟩ => ⟨.after,none⟩
      | ⟨.after,none⟩ => ⟨.before,none⟩
      | ⟨.before,some (.inl a)⟩ => ⟨.after,some (.inl a)⟩
      | ⟨.after,some (.inl a)⟩ => ⟨.before,some (.inl a)⟩
      | ⟨.before,some (.inr (.inl _))⟩ => ⟨.branch,none⟩
      | ⟨.branch,none⟩ => ⟨.before,some (.inr (.inl ()))⟩
      | ⟨.before,some (.inr (.inr c))⟩ => ⟨.after,some (.inr (.inr c))⟩
      | ⟨.after,some (.inr (.inr c))⟩ => ⟨.before,some (.inr (.inr c))⟩
      | ⟨.after,some (.inr (.inl b))⟩ => ⟨.branch,some b⟩
      | ⟨.branch,some b⟩ => ⟨.after,some (.inr (.inl b))⟩

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.SplitPort, OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.splitChild

23. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.splitEndpoint line 151
24. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.splitMate_involutive line 153
25. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.splitMate_orientation line 160
26. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.split line 171

    Source documentation

    A split or its orientation-reversed merge, with all three port lists.

    def split (A B C : Type) : VertexTable where
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable

27. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.reverse line 180

    Source documentation

    Reversal changes every seam endpoint, and nothing in the occurrence table.

    def reverse (t : VertexTable) : VertexTable where
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable

28. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.mate_ne line 194

    Source documentation

    Every local table is fixed-point free for occurrences, even when a facet is attached to several of the ports.

    lemma mate_ne (t : VertexTable) (s : (p : t.Port) × Option (t.Child p)) : t.mate s ≠ s := by
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable

29. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.splitPortEquiv line 208
30. instance OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.(instance at line 214) line 214
31. inductive OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind line 217

    Source documentation

    Exactly the allowed vertex list, including reversal of splitting. The nonnegative numbers include every zero block before normalization.

    inductive Kind where
    …

32. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind.table line 221
33. instance OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.finitePort line 226
34. instance OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.finiteChild line 232
35. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.LocalEnd line 240

    Source documentation

    Local endpoint occurrences at permitted vertices.

    abbrev LocalEnd (V : Type) (kind : V → VertexTable.Kind) :=
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind

36. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.localMate line 243
37. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.localMate_involutive line 246
38. structure OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexAssembly line 253

    Source documentation

    A finite incidence diagram is specified by a bijection from local ports to global side-germ occurrences.

    structure VertexAssembly (F S V : Type) (arity : S → ℕ) where
    …

39. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexAssembly.localOrientation line 264
40. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexAssembly.corners line 271

    Source documentation

    The global corner involution is constructed from the source vertex tables.

    def corners : Corners F S arity where
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.Corners

41. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexAssembly.corner_local line 284

    Source documentation

    Every corner of the constructed diagram is one of the permitted local occurrences, even if all its adjacent sides share the same facet name.

    lemma corner_local (g : Germ S arity) :
        A.realize.symm (A.corners.mate g)=localMate (A.realize.symm g) :=
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.Germ, OAI.IntegralCharacterVarieties.OccurrenceIncidence.localMate

42. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexAssembly.boundary_next_injective line 288
43. instance OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexAssembly.finiteLocalEnd line 292
44. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind.arity line 302
45. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.unitFin line 311
46. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.beforeEnum line 312
47. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.afterEnum line 315
48. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind.childEnumeration line 319

    Source documentation

    The source order on each child list: prefix, split block/subblocks, suffix. This is not an arbitrary finite enumeration or an unconstrained germ bijection.

    def Kind.childEnumeration : (k : Kind) → (p : k.table.Port) →
        k.table.Child p ≃ Fin (k.arity p)
      | .passage _ _, _ => Equiv.refl _
      | .splitting a _ c false, .before => beforeEnum a c
      | .splitting a b c false, .after => afterEnum a b c
      | .splitting _ _ _ false, .branch => Equiv.refl _
      | .splitting a _ c true, .before => beforeEnum a c
      | .splitting a b c true, .after => afterEnum a b c
      | .splitting _ _ _ true, .branch => Equiv.refl _
    end VertexTable

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind, OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.passage, OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.beforeEnum, OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.afterEnum, OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable

49. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.LocalPort line 330
50. structure OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly line 333

    Source documentation

    Whole ordered ports, rather than unrelated side germs, attach to seam endpoints. This is the finite incidence condition for surface diagrams.

    structure PortAssembly (F S V : Type) (arity : S → ℕ) where
    …

51. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.childEquiv line 349
52. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.localBundleEquiv line 352
53. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bundleGermEquiv line 359
54. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.realize line 366

    Source documentation

    Every germ follows its own port, retaining all repeated facet uses.

    def realize : LocalEnd V A.kind ≃ Germ S arity :=
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.LocalEnd, OAI.IntegralCharacterVarieties.OccurrenceIncidence.Germ

55. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.realize_apply line 370
56. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.realize_endpoint line 374
57. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.realize_parent line 377
58. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.vertexAssembly line 383

    Source documentation

    The original corner construction can now be used WITHOUT accidentally scattering a seam's children between unrelated endpoints.

    def vertexAssembly : VertexAssembly F S V arity where
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexAssembly

59. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.port_integrity line 398

    Source documentation

    Port integrity: even the parent and every child of the same port lie at the same global seam endpoint.

    theorem port_integrity (p : LocalPort V A.kind) (c : Option ((A.kind p.1).table.Child p.2)) :
        ((A.realize ⟨p.1,p.2,c⟩).1.1,(A.realize ⟨p.1,p.2,c⟩).2)=A.attach p := rfl
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.LocalPort