OAI/AlgebraicGeometry/CharacterVarieties/Foundation/PortPatches.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch line 13

   Source documentation

   A finite open template is given by explicit enumerations of all vertex ports. Internal wires match equal indices; the remaining ports are the interface.

   structure PortPatch (kind : V → VertexTable.Kind) (I A B : Type) where
   …

   Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind

2. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.complete line 23

   Source documentation

   Closing the interface uses only an whole-port matching, never a matching of independent child germs.

   def complete (e : A ≃ B)
       (h : ∀ a, (kind (P.minus (.inr (e a))).val.1).arity (P.minus (.inr (e a))).val.2 =
         (kind (P.plus (.inr a)).val.1).arity (P.plus (.inr a)).val.2) : PortWiring kind where
   …

   Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring

3. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.complete_internal line 36
4. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.complete_external line 42
5. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.port_exhaustive line 49

   Source documentation

   Every port is accounted for exactly once already in the template.

   theorem port_exhaustive (p : PortAt kind true) :
       (∃ i, P.plus (.inl i)=p) ∨ (∃ a, P.plus (.inr a)=p) := by
   …

   Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAt

6. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Decoration.portColor line 63

   Source documentation

   Ordered list form of a local decoration; none is still the parent.

   def Decoration.portColor (d : Decoration k F) (p : k.table.Port)
       (j : Option (Fin (k.arity p))) : F := d.color ⟨p,j.map (k.childEnumeration p).symm⟩

   Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Decoration

7. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Decoration.portColor_child line 66
8. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.includeComplement line 76

   Source documentation

   An embedding, together with all unconsumed objects, is an exact disjoint partition. This is used on whole ports, never on independent child germs.

   noncomputable def includeComplement {I P : Type} (f : I ↪ P) :
       I ⊕ {p : P // p∉Set.range f} ≃ P :=
   …

9. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.includeComplement_inl line 81
10. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.includeComplement_inr line 83
11. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.ofPartial line 89

    Source documentation

    A partial sewing, with every unused port left exposed exactly once. Injectivity prevents accidental multiple use of a repeated occurrence.

    noncomputable def ofPartial (plus : I ↪ PortAt k true) (minus : I ↪ PortAt k false)
        (h : ∀ i, (k (minus i).val.1).arity (minus i).val.2=
          (k (plus i).val.1).arity (plus i).val.2) :
        PortPatch k I {p : PortAt k true // p∉Set.range plus}
          {p : PortAt k false // p∉Set.range minus} where
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAt, OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch

12. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind.input line 101

    Source documentation

    The incoming/outgoing main ports at one allowed event. Every remaining port (the split branch) is still present in the original table.

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

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

13. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind.output line 106
14. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind.input_endpoint line 111
15. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind.output_endpoint line 115
16. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind.principal_corner line 120
17. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VariableGallery.input line 130
18. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VariableGallery.output line 132
19. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VariableGallery.internalPlus line 135
20. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VariableGallery.internalMinus line 138
21. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VariableGallery.patch line 145

    Source documentation

    Variable-length path of split/merge/adjacent events. All side branches are part of its explicit interface, not discarded by the path.

    noncomputable def patch := PortPatch.ofPartial (internalPlus kind) (internalMinus kind) ha

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.ofPartial, OAI.IntegralCharacterVarieties.OccurrenceIncidence.VariableGallery.internalPlus, OAI.IntegralCharacterVarieties.OccurrenceIncidence.VariableGallery.internalMinus

22. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VariableGallery.first_exposed line 147
23. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VariableGallery.last_exposed line 152
24. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VariableGallery.parent_corner line 159

    Source documentation

    Parent corners concatenate with the original orientation.

    lemma parent_corner (v : Fin (l+1)) :
        localMate (⟨v,(kind v).input,none⟩ : LocalEnd _ kind)=⟨v,(kind v).output,none⟩ := by
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.localMate, OAI.IntegralCharacterVarieties.OccurrenceIncidence.VariableGallery.input, OAI.IntegralCharacterVarieties.OccurrenceIncidence.LocalEnd, OAI.IntegralCharacterVarieties.OccurrenceIncidence.VariableGallery.output

25. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VariableGallery.ColorChain line 164

    Source documentation

    Lists must match in their order, including repetitions.

    def ColorChain {F : Type} (d : (v : Fin (l+1)) → Decoration (kind v) F) : Prop :=
    …

26. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Decoration.children line 176
27. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Decoration.children_length line 179
28. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.splitting_after_color_false line 182
29. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.splitting_before_color_false line 197
30. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.splitting_after_children_false line 212
31. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.splitting_before_children_false line 221
32. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.splitting_branch_children_false line 230
33. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.splitting_after_color_true line 235
34. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.splitting_before_color_true line 250
35. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.splitting_after_children_true line 265
36. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.splitting_before_children_true line 274
37. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.splitting_branch_children_true line 283
38. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.splitLists line 289

    Source documentation

    One split/merge slot in the source's ordered flag gallery.

    def splitLists (rev : Bool) (main big : F) (left mid right : List F) :
        Decoration (.splitting left.length mid.length right.length rev) F :=
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Decoration

39. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.splitLists_input line 293
40. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.splitLists_output line 299
41. structure OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.OrderedStep line 312

    Source documentation

    A step records the permitted vertex and all of its ports; the two lists only designate the main band through that vertex. Branch ports are not removed or identified.

    structure OrderedStep (parent : F) (before after : List F) where
    …

42. inductive OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.OrderedChain line 320
43. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.OrderedChain.single line 327
44. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.OrderedChain.trans line 328
45. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.OrderedStep.split line 334

    Source documentation

    An split vertex, retaining its branch with its fine ordered grades.

    def OrderedStep.split (parent big : F) (left mid right : List F) :
        OrderedStep parent (left++big::right) (left++(mid++right)) where
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.OrderedStep

46. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.OrderedStep.merge line 344

    Source documentation

    Reversal retains the same three whole ports, with all their orientations reversed according to the source merge convention.

    def OrderedStep.merge (parent big : F) (left mid right : List F) :
        OrderedStep parent (left++(mid++right)) (left++big::right) where
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.OrderedStep

47. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.OrderedStep.passage line 353
48. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.refine_rows line 363

    Source documentation

    The finite row refinement is produced one split at a time. Each named row branch stays in the template interface. No flag-factorization or geometric-bundle premise occurs in this construction.

    theorem refine_rows (parent : F) (rows : List (F × List F)) (left right : List F) :
        Nonempty (OrderedChain parent (left++(rows.map Prod.fst++right))
          (left++(rows.flatMap Prod.snd++right))) ∧
        Nonempty (OrderedChain parent (left++(rows.flatMap Prod.snd++right))
          (left++(rows.map Prod.fst++right))) := by
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.OrderedChain

49. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.permutation_chain line 382

    Source documentation

    Every finite permutation of the common fine grades is produced entirely by the source's adjacent interchanges. Zero grades and repeated facet names are allowed; no distinctness condition is imposed on f.

    theorem permutation_chain (parent : F) {m : ℕ} (σ : Equiv.Perm (Fin m)) :
        ∀ f : Fin m → F, Nonempty (OrderedChain parent (List.ofFn f)
          (List.ofFn (f ∘ σ.symm))) := by
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.OrderedChain