OAI/AlgebraicGeometry/CharacterVarieties/Foundation/PatchCycles.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.IntegralCharacterVarieties.FiniteCycles.Polygon line 13

   Source documentation

   A cyclicly ordered embedded boundary polygon.

   structure Polygon (l : ℕ) where
   …

2. def OAI.IntegralCharacterVarieties.FiniteCycles.Polygon.Support line 20
3. lemma OAI.IntegralCharacterVarieties.FiniteCycles.Polygon.next_in_support line 22
4. def OAI.IntegralCharacterVarieties.FiniteCycles.Polygon.separate line 37

   Source documentation

   Separate this new disk from any old label shared by its working strip coordinates. No occurrence or existing corner transport is changed.

   noncomputable def separate {F : Type*} (f : α → F) (a : α) : Option F :=
   …

5. lemma OAI.IntegralCharacterVarieties.FiniteCycles.Polygon.separate_none_iff line 40
6. lemma OAI.IntegralCharacterVarieties.FiniteCycles.Polygon.separate_side line 44
7. lemma OAI.IntegralCharacterVarieties.FiniteCycles.Polygon.separate_old line 49
8. lemma OAI.IntegralCharacterVarieties.FiniteCycles.Polygon.separate_next line 52
9. def OAI.IntegralCharacterVarieties.FiniteCycles.Polygon.newSides line 57

   Source documentation

   The new facet's entire boundary side set, not just an embedded subset, is exactly the given polygon. This makes its unique boundary equation available.

   noncomputable def newSides {F : Type*} (f : α → F) :
       Fin l ≃ {a // C.separate f a=none} where
   …

10. def OAI.IntegralCharacterVarieties.FiniteCycles.blockPolygon line 73

    Source documentation

    Lexicographic subdivision of a cyclic polygon by routed blocks.

    def blockPolygon {m n : ℕ} (hm : 0 < m) (f : (Fin m × Fin (n+1)) ↪ α)
        (step : ∀ t (i : Fin n), σ (f (t,i.castSucc))=f (t,i.succ))
        (wrap : ∀ t, σ (f (t,Fin.last n))=f (⟨(t.val+1)% m,Nat.mod_lt _ hm⟩,0)) :
        Polygon σ (m*(n+1)) where
    …

    Mentions: OAI.IntegralCharacterVarieties.FiniteCycles.Polygon

11. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.ParentPath.inner_side line 116
12. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.routeSeam line 134
13. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.routeSeam_injective line 138
14. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.ParentPath.route_side line 166
15. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.ParentPath.route_sides_injective line 173
16. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.ParentPath.cyclicPolygon line 188

    Source documentation

    A cycle of patch routes is an embedded polygon for the boundary permutation. There is no extra topological closure hypothesis.

    def cyclicPolygon (hm : 0 < m) (hs : ∀ t, Function.Injective (C t).seam)
        (route : ∀ t, e.symm ⟨t,b t⟩=⟨⟨(t.val+1)%m,Nat.mod_lt _ hm⟩,
          a ⟨(t.val+1)%m,Nat.mod_lt _ hm⟩⟩) :
        IntegralCharacterVarieties.FiniteCycles.Polygon
          (((family P).complete e he).assemble facet hc).vertexAssembly.corners.boundaryNext
          (m*(n+1)) :=
    …

    Mentions: OAI.IntegralCharacterVarieties.FiniteCycles.Polygon, OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.family, OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.complete

17. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.uParentPath_seam_injective line 216
18. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.qParentPath_seam_injective line 219
19. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.u_parent_exhaustive line 224

    Source documentation

    Exhaustive local topological description of the U boundary. No child of a whole port can be confused with its parent even at a self-incidence.

    lemma u_parent_exhaustive (x : LocalEnd Vertex kind)
        (hx : (decoration x.1).color x.2=.U) :
        ∃ j : Fin 3, x=uParentPath.node j ∨ x=localMate (uParentPath.node j) := by
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.LocalEnd, OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.Vertex, OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.kind, OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.decoration, OAI.IntegralCharacterVarieties.OccurrenceIncidence.localMate

20. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.q_parent_exhaustive line 241
21. def OAI.IntegralCharacterVarieties.FiniteCycles.Polygon.start line 266
22. lemma OAI.IntegralCharacterVarieties.FiniteCycles.Polygon.iterate_side line 269
23. lemma OAI.IntegralCharacterVarieties.FiniteCycles.Polygon.side_sameCycle line 280
24. def OAI.IntegralCharacterVarieties.FiniteCycles.Polygon.newComponent line 291

    Source documentation

    Its separated new-facet label has only one orbit; this identifies the ENTIRE new facet boundary, in an arbitrary sewn global occurrence diagram.

    noncomputable def newComponent {F : Type} (f : α → F) :
        FacetComponents σ (C.separate f) none :=
    …

    Mentions: OAI.IntegralCharacterVarieties.FiniteCycles.FacetComponents

25. lemma OAI.IntegralCharacterVarieties.FiniteCycles.Polygon.newComponent_unique line 303
26. def OAI.IntegralCharacterVarieties.FiniteCycles.Polygon.newComponents line 316
27. theorem OAI.IntegralCharacterVarieties.FiniteCycles.Polygon.new_boundary_count line 323
28. theorem OAI.IntegralCharacterVarieties.FiniteCycles.Polygon.componentCount_of_support line 337

    Source documentation

    An exhaustive polygon determines the entire named facet boundary, not merely a cycle inside it. This does not change any original side label.

    theorem componentCount_of_support {F : Type} (f : α → F) (u : F)
        (h : ∀ z, z∈C.Support ↔ f z=u) : componentCount σ f u=1 := by
    …

    Mentions: OAI.IntegralCharacterVarieties.FiniteCycles.componentCount

29. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.sideOf_surjective line 352
30. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.Cyclic.patches line 370
31. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.Cyclic.colors line 371
32. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.Cyclic.wiring line 377
33. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.Cyclic.assembly line 379
34. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.Cyclic.color_mate line 382
35. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.Cyclic.uPolygon line 391
36. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.Cyclic.u_side line 397
37. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.Cyclic.u_node_mem line 404
38. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.Cyclic.u_support_color line 409
39. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.Cyclic.u_boundary_count line 438

    Source documentation

    The named U facet has exactly one boundary component, with no separation of labels and no unproved disk-topology interface.

    theorem u_boundary_count : IntegralCharacterVarieties.FiniteCycles.componentCount
        (assembly e he hd).vertexAssembly.corners.boundaryNext
        ((wiring e he).coloredFacet colors) .U=1 :=
    …

    Mentions: OAI.IntegralCharacterVarieties.FiniteCycles.componentCount, OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.Cyclic.assembly, OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.Cyclic.wiring, OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.Cyclic.colors

40. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.Cyclic.qPolygon line 445
41. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.Cyclic.q_side line 451
42. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.Cyclic.q_node_mem line 458
43. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.Cyclic.q_support_color line 463
44. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.Cyclic.q_boundary_count line 492

    Source documentation

    The named Q facet has exactly one boundary component, with no separation of labels and no unproved disk-topology interface.

    theorem q_boundary_count : IntegralCharacterVarieties.FiniteCycles.componentCount
        (assembly e he hd).vertexAssembly.corners.boundaryNext
        ((wiring e he).coloredFacet colors) .Q=1 :=
    …

    Mentions: OAI.IntegralCharacterVarieties.FiniteCycles.componentCount, OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.Cyclic.assembly, OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.Cyclic.wiring, OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.Cyclic.colors

45. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VariableGallery.parentPath line 510

    Source documentation

    Every gallery, including arbitrary splitting/merging and adjacent passages, has its input-to-output parent boundary route. All unconsumed branch ports remain exposed by patch; no branch is deleted here.

    noncomputable def parentPath : PortPatch.ParentPath (patch kind ha) l
        ⟨input kind 0, first_exposed kind⟩
        ⟨output kind (Fin.last l), last_exposed kind⟩ where
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.ParentPath, OAI.IntegralCharacterVarieties.OccurrenceIncidence.VariableGallery.patch, OAI.IntegralCharacterVarieties.OccurrenceIncidence.VariableGallery.input, OAI.IntegralCharacterVarieties.OccurrenceIncidence.VariableGallery.first_exposed, OAI.IntegralCharacterVarieties.OccurrenceIncidence.VariableGallery.output, OAI.IntegralCharacterVarieties.OccurrenceIncidence.VariableGallery.last_exposed

46. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VariableGallery.parentPath_seam_injective line 523
47. theorem OAI.IntegralCharacterVarieties.FiniteCycles.variableCyclic_sameCycle line 532

    Source documentation

    Unequal-length rows of a cyclic boundary are one permutation orbit. Length is not padded by fictitious vertices or zero-rank blocks.

    theorem variableCyclic_sameCycle {α : Type} (σ : Equiv.Perm α) {m : ℕ}
        (n : Fin (m+1) → ℕ) (node : (t : Fin (m+1)) → Fin (n t+1) → α)
        (step : ∀ t (j : Fin (n t)), σ (node t j.castSucc)=node t j.succ)
        (wrap : ∀ t, σ (node t (Fin.last (n t)))=
          node ⟨(t.val+1)%(m+1),Nat.mod_lt _ (Nat.succ_pos _)⟩ 0)
        (t : Fin (m+1)) (j : Fin (n t+1)) : σ.SameCycle (node 0 0) (node t j) := by
    …

48. theorem OAI.IntegralCharacterVarieties.FiniteCycles.componentCount_of_connected line 567

    Source documentation

    A named facet has one boundary precisely when all its sides belong to the orbit of one of its sides. No new separated labeling is introduced.

    theorem componentCount_of_connected {α F : Type} [Finite α] (σ : Equiv.Perm α)
        (facet : α → F) (hc : ∀ x, facet (σ x)=facet x) (u : F)
        (x : α) (hx : facet x=u)
        (connected : ∀ y, facet y=u → σ.SameCycle x y) :
        componentCount σ facet u=1 := by
    …

    Mentions: OAI.IntegralCharacterVarieties.FiniteCycles.componentCount