OAI/AlgebraicGeometry/CharacterVarieties/Foundation/ComplementaryPatches.lean

GitHub source file

83 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape line 15

   Source documentation

   Finite, exhaustive intersection-rank indexing set. Zero blocks and repeated flag terms are retained at this stage, rather than excluded by genericity.

   def RankShape (n m r : ℕ) :=
   …

2. instance OAI.IntegralCharacterVarieties.TwoFlagBand.(instance at line 18) line 18
3. abbrev OAI.IntegralCharacterVarieties.TwoFlagBand.BlockCoordinates line 22
4. def OAI.IntegralCharacterVarieties.TwoFlagBand.coordinateBlock line 25
5. def OAI.IntegralCharacterVarieties.TwoFlagBand.boundedGrid line 29
6. lemma OAI.IntegralCharacterVarieties.TwoFlagBand.boundedGrid_eq line 33
7. lemma OAI.IntegralCharacterVarieties.TwoFlagBand.finiteSubmoduleSum_single line 51
8. lemma OAI.IntegralCharacterVarieties.TwoFlagBand.piEquiv_single line 63
9. theorem OAI.IntegralCharacterVarieties.TwoFlagBand.finite_shape_frame_covers line 75

   Source documentation

   Every pair of finite flags is in one of these finitely many split matrix charts. There is no regularity, opposite-flags, or strict-rank premise.

   theorem finite_shape_frame_covers
       (F H : ℕ → Submodule K V) (hF : Monotone F) (hH : Monotone H)
       (hF0 : F 0=⊥) (hH0 : H 0=⊥) (n m : ℕ) (hFn : F n=⊤) (hHm : H m=⊤) :
       ∃ (d : RankShape n m (Module.finrank K V)) (e : BlockCoordinates K d ≃ₗ[K] V),
         ∀ i j, i ≤ n → j ≤ m →
           F i ⊓ H j=boundedGrid (fun p => (coordinateBlock d p).map e.toLinearMap) i j := by
   …

   Mentions: OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape, OAI.IntegralCharacterVarieties.TwoFlagBand.BlockCoordinates, OAI.IntegralCharacterVarieties.TwoFlagBand.boundedGrid, OAI.IntegralCharacterVarieties.TwoFlagBand.coordinateBlock

10. inductive OAI.IntegralCharacterVarieties.TwoFlagBand.BandColor line 122

    Source documentation

    Distinct occurrences survive even if two original graded spaces are isomorphic, zero, or come from the same repeatedly incident facet.

    inductive BandColor (n m : ℕ)
      | parent : BandColor n m
      | row : Fin n → BandColor n m
      | col : Fin m → BandColor n m
      | cell : Fin n → Fin m → BandColor n m
      deriving DecidableEq, Fintype
    
    namespace RankShape
    variable {n m r : ℕ} (d : RankShape n m r)

    Mentions: OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape

11. def OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.bandRank line 131
12. lemma OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.parent_row_rank line 137
13. def OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.band line 141

    Source documentation

    Canonically choose one finite allowed port band for each bounded rank shape. This producer does not take any affine-bundle hypothesis.

    noncomputable def band : RealizedBand (BandColor.parent : BandColor n m)
        (List.ofFn BandColor.row) (List.ofFn BandColor.col) :=
    …

    Mentions: OAI.IntegralCharacterVarieties.TwoFlagBand.BandColor

14. theorem OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.band_conservative line 146
15. abbrev OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.BandVertex line 151

    Source documentation

    The combined family is finite: lengths may vary with the intersection shape, but there are finitely many shapes and each band is finite.

    abbrev BandVertex := (d : RankShape n m r) × Fin (d.band.length+1)

    Mentions: OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape

16. instance OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.finiteBandVertex line 152
17. theorem OAI.IntegralCharacterVarieties.TwoFlagBand.actual_flags_in_produced_bands line 157

    Source documentation

    Exhaustive actual-flags linkage: the finite band family is indexed by the intersection pieces of every pair of flags, and every local allowed vertex has its rank identity. No opposite-flags or generic Jordan condition is introduced. Geometric reconstruction of the whole disk still has to attach these bands.

    theorem actual_flags_in_produced_bands
        (F H : ℕ → Submodule K V) (hF : Monotone F) (hH : Monotone H)
        (hF0 : F 0=⊥) (hH0 : H 0=⊥) (n m : ℕ) (hFn : F n=⊤) (hHm : H m=⊤) :
        ∃ (d : RankShape n m (Module.finrank K V)) (e : BlockCoordinates K d ≃ₗ[K] V),
          (∀ i j, i ≤ n → j ≤ m →
            F i ⊓ H j=boundedGrid (fun p => (coordinateBlock d p).map e.toLinearMap) i j) ∧
          (∀ v,(d.band.decoration v).Conservative d.bandRank) := by
    …

    Mentions: OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape, OAI.IntegralCharacterVarieties.TwoFlagBand.BlockCoordinates, OAI.IntegralCharacterVarieties.TwoFlagBand.boundedGrid, OAI.IntegralCharacterVarieties.TwoFlagBand.coordinateBlock

18. abbrev OAI.IntegralCharacterVarieties.TwoFlagBand.CutShapes line 168

    Source documentation

    Multiple cuts are indexed simultaneously by a finite product of bounded rank arrays, not by an unbounded fresh family chosen for each old solution.

    abbrev CutShapes {Cut : Type} (rows cols size : Cut → ℕ) :=
    …

19. instance OAI.IntegralCharacterVarieties.TwoFlagBand.finiteCutShapes line 170
20. structure OAI.IntegralCharacterVarieties.TwoFlagBand.FlagPair line 173
21. theorem OAI.IntegralCharacterVarieties.TwoFlagBand.all_cuts_in_finite_band_family line 184

    Source documentation

    Exhaustivity holds simultaneously on any fixed finite incidence list of cuts, including several distinct occurrences of the same surface component.

    theorem all_cuts_in_finite_band_family {Cut : Type} [Fintype Cut]
        (rows cols : Cut → ℕ) (flags : (c : Cut) → FlagPair (K:=K) (V:=V) (rows c) (cols c)) :
    …

    Mentions: OAI.IntegralCharacterVarieties.TwoFlagBand.FlagPair

22. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.natColor line 208

    Source documentation

    The ordered list is extended by its parent off its finite domain. Using a natural numbered occurrence makes all reindexing by equality transparent.

    def natColor (p : LocalPort V kind) : Option ℕ → F
      | none => (d p.1).color ⟨p.2,none⟩
      | some i => if h : i < (kind p.1).arity p.2 then
          (d p.1).portColor p.2 (some ⟨i,h⟩) else (d p.1).color ⟨p.2,none⟩

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.LocalPort

23. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.natColor_local line 213
24. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.ColorCompatible line 224

    Source documentation

    Entire ordered lists, not merely multisets of ranks, agree at opposite ends.

    def ColorCompatible : Prop := ∀ (s : W.Seam),
    …

25. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.coloredFacet line 227
26. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.castFin_val line 230
27. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.sideOf_color line 233
28. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.fromDecoration line 255

    Source documentation

    Every corner-color equation follows from vertex tables and wiring.

    def fromDecoration (hd : W.ColorCompatible d) :
        PortAssembly F W.Seam V W.seamArity :=
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly

29. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.compatible_of_portColor line 263

    Source documentation

    Finite ordered port equality suffices; off-domain colors are the parents.

    lemma compatible_of_portColor
        (h : ∀ (s : W.Seam) (j : Option (Fin (W.seamArity s))),
          (d (W.wire s).val.1).portColor (W.wire s).val.2
            (j.map (finCongr (W.arity s).symm)) = (d s.val.1).portColor s.val.2 j) :
        W.ColorCompatible d := by
    …

30. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.sideNumber line 293

    Source documentation

    Numerical side labels are injective because the finite arity is retained by the seam itself. Used only to discharge dependent casts at sewing.

    def sideNumber {S : Type} {arity : S → ℕ} (z : Side S arity) : S × Option ℕ :=
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.Side

31. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.sideNumber_injective line 296
32. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.sideOf_number line 309
33. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.sideOf_eq line 315
34. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.finCongr_eq_cast line 323
35. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.realize_assemble line 327
36. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.boundaryNext_local line 344
37. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.familyKind line 375

    Source documentation

    Separate copies of every vertex and port are retained under replacement. Even two uses of the very same template have disjoint sigma-indexed vertices.

    def familyKind {T : Type} {V : T → Type} (k : (t : T) → V t → Kind) :
        ((t : T) × V t) → Kind := fun z => k z.1 z.2

38. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.familyPortEquiv line 378
39. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.family line 390

    Source documentation

    A finite collection of open templates, before interface sewing. Internal seams never acquire identifications between different copies.

    def family : PortPatch (familyKind k) ((t : T) × I t) ((t : T) × A t) ((t : T) × B t) where
    …

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

40. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.family_plus_internal line 397
41. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.family_minus_internal line 399
42. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.family_plus_external line 401
43. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.family_minus_external line 403
44. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.family_internal_unchanged line 407

    Source documentation

    Preservation of every internal seam under arbitrary legitimate external gluing, including self-incidence and repeated old facet names.

    theorem family_internal_unchanged (e : ((t : T) × A t) ≃ ((t : T) × B t))
        (he : ∀ a, (familyKind k ((family P).minus (.inr (e a))).val.1).arity
          ((family P).minus (.inr (e a))).val.2 =
          (familyKind k ((family P).plus (.inr a)).val.1).arity ((family P).plus (.inr a)).val.2)
        (t : T) (i : I t) :
        ((family P).complete e he).wire (familyPortEquiv k true ⟨t,(P t).plus (.inl i)⟩)=
          familyPortEquiv k false ⟨t,(P t).minus (.inl i)⟩ :=
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.familyKind, OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.family, OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.complete, OAI.IntegralCharacterVarieties.OccurrenceIncidence.familyPortEquiv

45. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.familyDecoration line 419

    Source documentation

    Old facet names may repeat while every new strip has its own copy.

    def familyDecoration {T F : Type} {V : T → Type} {k : (t : T) → V t → Kind}
        (d : (t : T) → (v : V t) → Decoration (k t v) F) :
        (z : (t : T) × V t) → Decoration (familyKind k z) F := fun z => d z.1 z.2
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.familyKind

46. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.familyEnd line 430

    Source documentation

    Inclusion of one occurrence-sensitive local patch into a disjoint family.

    def familyEnd {T : Type} {V : T → Type} (k : (t : T) → V t → Kind)
        (t : T) (x : LocalEnd (V t) (k t)) : LocalEnd ((t : T) × V t) (familyKind k) :=
    …

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

47. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.familyEnd_mate line 434
48. structure OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.InternalCycle line 442

    Source documentation

    Explicit internal oriented polygon. Every field is finite combinatorial source data; no flag lift or geometric bundle property is a field here.

    structure InternalCycle (P : PortPatch k I A B) (l : ℕ) where
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch

49. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.InternalCycle.plus_end line 464
50. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.InternalCycle.minus_end line 475
51. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.InternalCycle.sides_equal line 486
52. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.InternalCycle.side_seam line 494
53. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.InternalCycle.sides_injective line 498
54. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.InternalCycle.boundary_next line 508

    Source documentation

    Protected boundary polygon in an arbitrarily large sewn family, including every wrap and any repeated use of an old facet.

    theorem boundary_next {F : Type}
        (facet : Side ((family P).complete e he).Seam ((family P).complete e he).seamArity → F)
        (hc : ∀ x, facet (((family P).complete e he).sideOf (localMate x))=
          facet (((family P).complete e he).sideOf x)) (j : Fin l) :
        (((family P).complete e he).assemble facet hc).vertexAssembly.corners.boundaryNext
          (((family P).complete e he).sideOf (familyEnd k t (C.plusEnd j)))=
            ((family P).complete e he).sideOf
              (familyEnd k t (C.plusEnd ⟨(j.val+1)%l,Nat.mod_lt _ C.positive⟩)) := by
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.Side, OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.family, OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.complete, OAI.IntegralCharacterVarieties.OccurrenceIncidence.localMate, OAI.IntegralCharacterVarieties.OccurrenceIncidence.familyEnd

55. structure OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.ParentPath line 536

    Source documentation

    A finite parent route in a replacement, before any global sewing. The only fields are endpoint equalities in finite permitted-vertex tables.

    structure ParentPath (P : PortPatch k I A B) (n : ℕ) (a : A) (b : B) where
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch

56. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.ParentPath.along_sides line 558
57. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.ParentPath.first_side line 579
58. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.ParentPath.last_side line 592
59. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.ParentPath.boundary_step line 612
60. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.ParentPath.boundary_iterate line 623
61. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.ParentPath.boundary_exit line 634

    Source documentation

    The sewn boundary traverses the full parent route and exits on its designated exterior lane; exterior wiring was completely arbitrary.

    theorem boundary_exit :
        ((((family P).complete e he).assemble facet hc).vertexAssembly.corners.boundaryNext^[n+1])
          (((family P).complete e he).sideOf (familyEnd k t (C.node 0)))=
            ((family P).complete e he).sideOf (familyEnd k t (localMate (C.node (Fin.last n)))) := by
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.family, OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.complete, OAI.IntegralCharacterVarieties.OccurrenceIncidence.familyEnd, OAI.IntegralCharacterVarieties.OccurrenceIncidence.localMate

62. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.ParentPath.boundary_exterior line 650
63. inductive OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.Vertex line 666

    Source documentation

    The ten permitted vertices for the band reduction, complementary-swap replacement. U,Q follow old positive time; A,B follow the opposite orientation.

    inductive Vertex where
    …

64. inductive OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.Facet line 670
65. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.vertexEnum line 675
66. instance OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.(instance at line 676) line 676
67. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.facetEnum line 690
68. instance OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.(instance at line 691) line 691
69. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.kind line 708
70. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.plusList line 721

    Source documentation

    The first ten entries are internal seams; the last four are the exposed U,Q,A,B positive-endpoint ports. Each is a whole ordered seam list.

    def plusList : Fin 14 → PortAt kind true := ![
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAt, OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.kind

71. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.minusList line 730
72. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.plusIndex line 739
73. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.minusIndex line 749
74. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.plusEquiv line 759
75. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.minusEquiv line 767
76. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.patch line 776

    Source documentation

    Local incidence recipe. It contains all ten allowed vertices and all ten internal seams, with the eight boundary ports left exposed.

    def patch : PortPatch kind (Fin 10) (Fin 4) (Fin 4) where
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch, OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.kind

77. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.decoration line 782

    Source documentation

    The facet/strip names incident at every corner. A global use may map different A/B names to the same old facet without changing occurrences.

    def decoration : (v : Vertex) → Decoration (kind v) Facet
      | .uIn => splittingDecoration false .U .TB ![.a] ![.b,.h] ![]
      | .bIn => splittingDecoration true .B .TB ![] ![.b,.h] ![.y]
      | .qIn => splittingDecoration false .Q .HX ![] ![.h,.x] ![.y]
      | .aIn => splittingDecoration true .A .HX ![.a] ![.h,.x] ![]
      | .uSwap => passageDecoration (.interchange 0) .U ![.a,.b,.h]
      | .qSwap => passageDecoration (.interchange 1) .Q ![.h,.x,.y]
      | .uOut => splittingDecoration true .U .TA ![.b] ![.a,.h] ![]
      | .aOut => splittingDecoration false .A .TA ![] ![.a,.h] ![.x]
      | .qOut => splittingDecoration true .Q .HY ![] ![.h,.y] ![.x]
      | .bOut => splittingDecoration false .B .HY ![.b] ![.h,.y] ![]

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.Vertex, OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.kind, OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.Facet

78. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.rank line 795

    Source documentation

    The source's numerical rank array, before deletion of zero pieces.

    def rank (a b h x y : ℕ) : Facet → ℕ
      | .U => a+b+h | .Q => h+x+y | .A => a+h+x | .B => b+h+y
      | .TB => b+h | .HX => h+x | .TA => a+h | .HY => h+y
      | .a => a | .b => b | .h => h | .x => x | .y => y
    
    end IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch
    
    namespace IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch
    open scoped Classical
    open VertexTable
    
    /-- U route: split tilde-b, interchange a,b, merge a,h. -/

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.Facet, OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable

79. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.uParentPath line 807

    Source documentation

    U route: split tilde-b, interchange a,b, merge a,h.

    def uParentPath : PortPatch.ParentPath patch 2 (0 : Fin 4) 0 where
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.ParentPath, OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.patch

80. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.qParentPath line 819

    Source documentation

    Q route, through the complementary interchange x,y.

    def qParentPath : PortPatch.ParentPath patch 2 (1 : Fin 4) 1 where
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.ParentPath, OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.patch

81. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.aParentPath line 831

    Source documentation

    A keeps its old surface orientation; time on it is opposite to U,Q.

    def aParentPath : PortPatch.ParentPath patch 1 (2 : Fin 4) 2 where
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.ParentPath, OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.patch

82. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.bParentPath line 842
83. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.parent_path_colors line 854

    Source documentation

    All parent route nodes preserve the named surface, not only ranks.

    theorem parent_path_colors :
        (∀ j,(decoration (uParentPath.node j).1).color (uParentPath.node j).2=.U) ∧
        (∀ j,(decoration (qParentPath.node j).1).color (qParentPath.node j).2=.Q) ∧
        (∀ j,(decoration (aParentPath.node j).1).color (aParentPath.node j).2=.A) ∧
        (∀ j,(decoration (bParentPath.node j).1).color (bParentPath.node j).2=.B) := by
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.decoration