OAI/AlgebraicGeometry/CharacterVarieties/Foundation/BandIncidence.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.BandCutSeam line 13

    Source documentation

    Three old subintervals and one transverse identity connection. This is the intermediate inverse handle cut, before the two-flag gallery replaces the identity connection by proper lower strips. No fresh facet is introduced.

    abbrev BandCutSeam (S : Type) := (S × Fin 3) ⊕ Unit
  2. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.BandCutVertex line 14
  3. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCutArity line 15
  4. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCutKind line 21
  5. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCutSplitPort line 26
  6. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCutInteriorPort line 30
  7. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCutAttachTo line 34
  8. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCutAttachFrom line 47
  9. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCutFacet line 61

    Source documentation

    The two sides of the inverse band belong to the SAME original parent surface. All child occurrences, including repeated old facets, remain literal.

    def bandCutFacet : Side (BandCutSeam S) (bandCutArity arity) → F
  | ⟨.inl (s,_),c⟩ => A.facet ⟨s,c⟩
  | ⟨.inr (),_⟩ => A.facet ⟨q,none⟩
end IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly

namespace IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly
open scoped Classical
open VertexTable
variable {F S V : Type} {arity : S → ℕ} (A : PortAssembly F S V arity) (q : S)

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.Side, OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.BandCutSeam, OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCutArity, OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly, OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable

  10. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCutAttach_interior line 71
  11. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCutAttach_outer line 81
  12. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCutAttach_left line 85
  13. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCutAttach_right line 107
  14. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCutAttach line 116
  15. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCutEndpoint line 129
  16. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCutCount line 137
  17. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCut_fin_transport line 146
  18. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCutPorts line 149
  19. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.inverse_band_port_assembly line 193

    Source documentation

    Required inverse arc incidence, with no scattering of an old port and no lost old endpoint or repeated child occurrence.

    theorem inverse_band_port_assembly : ∃ B : PortAssembly F (BandCutSeam S) (BandCutVertex V S q) (bandCutArity arity),
    B.kind=A.bandCutKind q ∧ B.facet=A.bandCutFacet q ∧
      (∀ (v : V) (p : (A.kind v).table.Port),
        ∃ u : LocalPort (BandCutVertex V S q) B.kind,
          u.1=.inl v ∧ B.attach u=A.bandCutAttachTo q ⟨.inl v,p⟩) := by
…

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly, OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.BandCutSeam, OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.BandCutVertex, OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCutArity, OAI.IntegralCharacterVarieties.OccurrenceIncidence.LocalPort

  20. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCutLong line 208

    Source documentation

    The oriented old boundary traverses three pieces. Only the middle parent piece at q is replaced by the child side of the inverse band.

    def bandCutLong : Side S arity × Fin 3 → Side (BandCutSeam S) (bandCutArity arity)
  | (⟨s,none⟩,k) => if s=q ∧ k=1 then ⟨.inr (),some (0 : Fin 1)⟩ else ⟨.inl (s,k),none⟩
  | (⟨s,some c⟩,k) => ⟨.inl (s,k.rev),some c⟩

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.Side, OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.BandCutSeam, OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCutArity

  21. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCutShort line 212
  22. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCutSideFrom line 215
  23. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCutSideEquiv line 222

    Source documentation

    Exhaustive side occurrence bijection. The new short boundary is additional, rather than a chosen list that might omit fresh-parent germs.

    def bandCutSideEquiv : ((Side S arity × Fin 3) ⊕ Fin 2) ≃ Side (BandCutSeam S) (bandCutArity arity) where
…

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.Side, OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.BandCutSeam, OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCutArity

  24. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCutLong_facet line 255
  25. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCutShort_facet line 266
  26. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCutBeforeEnd line 277
  27. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCutAfterEnd line 280
  28. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCutBranchEnd line 283
  29. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCut_realize_old line 287
  30. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCut_realize_continuation line 291
  31. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCut_realize_before line 296
  32. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCut_realize_after line 312
  33. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCut_realize_branch line 331
  34. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCut_mate_realize line 336
  35. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCut_mate_middle line 343
  36. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCut_mate_outer_piece line 358
  37. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCut_mate_band line 373
  38. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCutOuter line 400
  39. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCut_mate_outer line 403
  40. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCut_mate_continuation line 413
  41. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCut_mate_continuation_back line 423
  42. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCutLong_start line 432
  43. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCutLong_finish line 438
  44. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCut_next_last line 444
  45. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCut_next_first line 452
  46. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCut_next_second line 473
  47. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandCut_next_short line 494