OAI/AlgebraicGeometry/CharacterVarieties/Foundation/BoundaryCycles.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.IntegralCharacterVarieties.FiniteCycles.Component line 12
2. def OAI.IntegralCharacterVarieties.FiniteCycles.representative line 14
3. def OAI.IntegralCharacterVarieties.FiniteCycles.length line 16
4. lemma OAI.IntegralCharacterVarieties.FiniteCycles.length_pos line 18
5. def OAI.IntegralCharacterVarieties.FiniteCycles.entry line 21
6. lemma OAI.IntegralCharacterVarieties.FiniteCycles.component_at line 24
7. lemma OAI.IntegralCharacterVarieties.FiniteCycles.at_next line 32
8. lemma OAI.IntegralCharacterVarieties.FiniteCycles.at_injective line 39
9. lemma OAI.IntegralCharacterVarieties.FiniteCycles.at_surjective line 44
10. def OAI.IntegralCharacterVarieties.FiniteCycles.enumeration line 54

    Source documentation

    Every side occurrence appears once, even in self-incidence cycles.

    def enumeration : ((c : Component p) × Fin (length p c)) ≃ α :=
    …

    Mentions: OAI.IntegralCharacterVarieties.FiniteCycles.Component, OAI.IntegralCharacterVarieties.FiniteCycles.length

11. lemma OAI.IntegralCharacterVarieties.FiniteCycles.iterate_facet line 68
12. def OAI.IntegralCharacterVarieties.FiniteCycles.componentFacet line 73
13. lemma OAI.IntegralCharacterVarieties.FiniteCycles.at_facet line 77
14. abbrev OAI.IntegralCharacterVarieties.FiniteCycles.FacetComponents line 80
15. instance OAI.IntegralCharacterVarieties.FiniteCycles.finiteComponents line 82
16. instance OAI.IntegralCharacterVarieties.FiniteCycles.finiteFacetComponents line 83
17. def OAI.IntegralCharacterVarieties.FiniteCycles.componentCount line 85
18. def OAI.IntegralCharacterVarieties.FiniteCycles.componentIndex line 86
19. def OAI.IntegralCharacterVarieties.FiniteCycles.boundaryLength line 89
20. lemma OAI.IntegralCharacterVarieties.FiniteCycles.boundaryLength_pos line 92
21. def OAI.IntegralCharacterVarieties.FiniteCycles.facetEnumeration line 96

    Source documentation

    Historical facet labels survive grouping: several cycles may belong to one surface, and a side on that surface can occur any number of times.

    def facetEnumeration :
        ((f : F) × (b : Fin (componentCount p facet f)) × Fin (boundaryLength p facet f b)) ≃ α :=
    …

    Mentions: OAI.IntegralCharacterVarieties.FiniteCycles.componentCount, OAI.IntegralCharacterVarieties.FiniteCycles.boundaryLength

22. lemma OAI.IntegralCharacterVarieties.FiniteCycles.facetEnumeration_apply line 104
23. lemma OAI.IntegralCharacterVarieties.FiniteCycles.facetEnumeration_facet line 109
24. lemma OAI.IntegralCharacterVarieties.FiniteCycles.facetEnumeration_next line 115
25. def OAI.IntegralCharacterVarieties.SurfacePresentation.fromPorts line 127

    Source documentation

    Construct every boundary circle from the oriented corner involution. In particular no boundary-coverage or cyclic-closure premise is imposed on a new rank-reduction diagram. Facet labels may repeat, and closed facets have zero cycles.

    def fromPorts {F S V : Type} [Finite S] {arity : S → ℕ}
        (A : PortAssembly F S V arity) (rank genus : F → ℕ)
        (h : ∀ s, rank (A.facet ⟨s,none⟩)=∑ j,rank (A.facet ⟨s,some j⟩)) : Diagram F S V arity where
    …

    Mentions: OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram

26. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.fromPorts_retains line 143

    Source documentation

    The constructor alters no facet labels, numerical ranks, seam ranks or handles.

    lemma fromPorts_retains {F S V : Type} [Finite S] {arity : S → ℕ}
        (A : PortAssembly F S V arity) (rank genus : F → ℕ)
        (h : ∀ s, rank (A.facet ⟨s,none⟩)=∑ j,rank (A.facet ⟨s,some j⟩)) :
        (fromPorts A rank genus h).ports=A ∧ (fromPorts A rank genus h).rank=rank ∧
          (fromPorts A rank genus h).genus=genus := ⟨rfl,rfl,rfl⟩

    Mentions: OAI.IntegralCharacterVarieties.SurfacePresentation.fromPorts

27. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.fromPorts_boundary_unique line 150

    Source documentation

    Strong occurrence-sensitive coverage, including all self-incidences.

    lemma fromPorts_boundary_unique {F S V : Type} [Finite S] {arity : S → ℕ}
        (A : PortAssembly F S V arity) (rank genus : F → ℕ)
        (h : ∀ s, rank (A.facet ⟨s,none⟩)=∑ j,rank (A.facet ⟨s,some j⟩)) (a : Side S arity) :
        ∃! z, (fromPorts A rank genus h).boundarySide z=a :=
    …

    Mentions: OAI.IntegralCharacterVarieties.SurfacePresentation.fromPorts

28. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAt line 161
29. structure OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring line 164

    Source documentation

    A wiring joins whole ordered ports of equal arity with opposite endpoint orientations. No side-germ is allowed to migrate to another seam on its own.

    structure PortWiring where
    …

30. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.Seam line 170
31. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.seamArity line 172
32. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.portAt line 175

    Source documentation

    Both ends of each newly assembled seam, with their original local ports.

    def portAt : W.Seam × Bool → LocalPort V kind
      | (s,true) => s.val
      | (s,false) => (W.wire s).val

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.LocalPort

33. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.endOf line 179
34. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.portAt_endOf line 183
35. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.endOf_portAt line 190
36. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.attach line 201
37. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.endpoint line 207
38. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.count line 214
39. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.sideOf line 224

    Source documentation

    The side belonging to one local germ after whole-port wiring.

    def sideOf (x : LocalEnd V kind) : Side W.Seam W.seamArity :=
    …

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

40. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.assemble line 229

    Source documentation

    Gluing constructor.

    def assemble {F : Type} (facet : Side W.Seam W.seamArity → F)
        (h : ∀ x, facet (W.sideOf (localMate x))=facet (W.sideOf x)) :
        PortAssembly F W.Seam V W.seamArity where
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.Side, OAI.IntegralCharacterVarieties.OccurrenceIncidence.localMate, OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly

41. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.assemble_facet line 239
42. instance OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.finiteSeam line 243
43. structure OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.Proper line 252

    Source documentation

    Exactly the source normalization: delete zero facets/children and sew identity seams BEFORE closed factors are separated.

    structure Proper : Prop where
    …

44. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.proper_child_lt line 258
45. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.maximal_side_parent line 276

    Source documentation

    Every maximal-rank occurrence is a parent. Repeated occurrences of the same facet are not collapsed: this assertion is made separately for each side.

    lemma maximal_side_parent {n : ℕ} (hn : ∀ f, D.rank f ≤ n) (a : Side S arity)
        (ha : D.rank (D.ports.facet a)=n) : a.2=none := by
    …

46. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.maximal_boundary_parent line 286
47. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.maximal_local_parent line 291
48. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.maximal_corner_parents line 297

    Source documentation

    At the paired corner of a maximal side the other side is also a parent. Thus branch-child corners cannot occur on the maximal disk boundary.

    lemma maximal_corner_parents {n : ℕ} (hn : ∀ f, D.rank f ≤ n) (x : LocalEnd V D.ports.kind)
        (hx : D.rank (D.ports.facet (D.portSide ⟨x.1,x.2.1⟩ x.2.2))=n) :
        x.2.2=none ∧ (localMate x).2.2=none := by
    …

49. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind.principalIn line 309

    Source documentation

    Along a maximal oriented facet this is the incoming parent port. A branch parent at a split is paired to a CHILD, so cannot lie on such a facet.

    def Kind.principalIn : (k : Kind) → k.table.Port
      | .passage _ _ => false
      | .splitting _ _ _ false => .before
      | .splitting _ _ _ true => .after

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

50. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind.principalOut line 314
51. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind.principal_endpoint line 319
52. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind.principal_mate line 325
53. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind.principal_unique line 331
54. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.localFinish line 350
55. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.localStart line 351
56. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.realize_localFinish line 353
57. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.realize_localStart line 355
58. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.localFinish_mate line 358
59. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.maximal_finish_ports line 365
60. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.eventVertex line 385

    Source documentation

    Vertex visited after the named interval occurrence.

    def eventVertex (f : F) (b : Fin (D.boundaryCount f)) (i : Fin (D.boundaryLength f b)) : V :=
    …

61. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.nextBoundaryIndex line 388
62. theorem OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.maximal_event_germs line 392

    Source documentation

    Both principal parent germs of the event are the ORIGINAL boundary germs. The second equality includes the last-to-first corner of the disk exactly.

    theorem maximal_event_germs (h : D.Proper) {n : ℕ} (hn : ∀ f, D.rank f ≤ n)
        (f : F) (hf : D.rank f=n) (b : Fin (D.boundaryCount f)) (i : Fin (D.boundaryLength f b)) :
        D.ports.realize ⟨D.eventVertex f b i,(D.ports.kind (D.eventVertex f b i)).principalIn,none⟩ =
          finish (D.boundarySide ⟨f,b,i⟩) ∧
        D.ports.realize ⟨D.eventVertex f b i,(D.ports.kind (D.eventVertex f b i)).principalOut,none⟩ =
          start (D.boundarySide ⟨f,b,D.nextBoundaryIndex f b i⟩) := by
    …

63. structure OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Decoration line 421

    Source documentation

    Facet names are attached to EACH local germ, even when their values repeat.

    structure Decoration (k : Kind) (F : Type) where
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind

64. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.passageDecoration line 427
65. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.splitColor line 439
66. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.splitColor_corner line 453
67. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.splittingDecoration line 462
68. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Decoration.map line 469

    Source documentation

    Replacing names uniformly preserves all corner incidences, so a local recipe may be used when several of its named old facets coincide globally.

    def Decoration.map {k : Kind} {G : Type} (d : Decoration k F) (f : F → G) : Decoration k G where
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind, OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Decoration