OAI/AlgebraicGeometry/CharacterVarieties/Foundation/VertexFrames.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.rank_sum line 14

    Source documentation

    The rank identities on all three ports of every split/merge and on both ports of both interchanges. There is no unverified seam-rank premise.

    theorem rank_sum (a b h x y : ℕ) (v : Vertex) (p : (kind v).table.Port) :
    rank a b h x y ((decoration v).color ⟨p,none⟩)=
      ∑ j, rank a b h x y ((decoration v).color ⟨p,some j⟩) := by
…

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.Vertex, OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.kind, OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.rank, OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.decoration

  2. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.vertexRanks line 31
  3. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.rank_strict line 37

    Source documentation

    All auxiliary strips/disks are at most one of A,B. Thus the patch lowers rank whenever the four replaced parents are already below the original n.

    theorem rank_strict {a b h x y n : ℕ}
    (hU : a+b+h<n) (hQ : h+x+y<n) (hA : a+h+x<n) (hB : b+h+y<n) (f : Facet) :
    rank a b h x y f<n := by
…

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

  4. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.RankArray line 43

    Source documentation

    Finite numerical choices for the local replacement. In a global family every vertex uses an independent occurrence of this bounded array.

    def RankArray (n : ℕ) :=
…
  5. instance OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.(instance at line 47) line 47
  6. lemma OAI.IntegralCharacterVarieties.MatrixIso.congr_trans line 56
  7. lemma OAI.IntegralCharacterVarieties.MatrixIso.congr_reindex line 62
  8. lemma OAI.IntegralCharacterVarieties.MatrixIso.congr_sum line 69
  9. lemma OAI.IntegralCharacterVarieties.MatrixIso.holds_self line 75
  10. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.passageComparison_congr line 90
  11. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.splitRefinementEquiv line 105
  12. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.splitRefinement_congr line 112
  13. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.splitComparison_congr line 119
  14. lemma OAI.IntegralCharacterVarieties.MatrixIso.trans_assoc line 137
  15. lemma OAI.IntegralCharacterVarieties.MatrixIso.reindex_trans line 142
  16. lemma OAI.IntegralCharacterVarieties.MatrixIso.reindex_refl_eq line 148
  17. def OAI.IntegralCharacterVarieties.MatrixIso.diagonal line 152

    Source documentation

    Unit-valued diagonal, valid over the full coefficient ring.

    def diagonal (u : α → Rˣ) : MatrixIso R α α where
…

    Mentions: OAI.IntegralCharacterVarieties.MatrixIso

  18. lemma OAI.IntegralCharacterVarieties.MatrixIso.diagonal_naturality line 164
  19. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.changeSplitParent line 183

    Source documentation

    Change the common parent frame, keeping the named third-seam frame.

    def changeSplitParent (f : ∀ p, MatrixIso R (d.Columns p) (d.Parent p))
    (z : MatrixIso R (d.Parent .before) (d.Parent .before)) :
    ∀ p, MatrixIso R (d.Columns p) (d.Parent p)
  | .before => (f .before).trans z
  | .after => (f .after).trans (z.reindex d.splitParent d.splitParent)
  | .branch => f .branch

    Mentions: OAI.IntegralCharacterVarieties.MatrixIso

  20. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.changeSplitParent_comparison_eq line 190
  21. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.atoms line 209

    Source documentation

    The five genuinely named small fibers in the manuscript normal form. These are names, not extra geometric constraints on an old subspace.

    def atoms : Facet → Finset (Fin 5)
  | .U => {0,1,2} | .Q => {2,3,4} | .A => {0,2,3} | .B => {1,2,4}
  | .TB => {1,2} | .HX => {2,3} | .TA => {0,2} | .HY => {2,4}
  | .a => {0} | .b => {1} | .h => {2} | .x => {3} | .y => {4}

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.Facet

  22. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.Fiber line 214
  23. instance OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.(instance at line 216) line 216
  24. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.fiberSigma line 219
  25. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.card_fiber line 226
  26. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.fiberEnum line 233
  27. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.atom_partition line 238

    Source documentation

    Every ordered port partitions the named atom coordinates. The assertion is verified for the ten-vertex table.

    lemma atom_partition (v : Vertex) (p : (kind v).table.Port) (t : Fin 5) :
    (∃! c, t ∈ atoms ((decoration v).color ⟨p,some c⟩)) ↔
      t ∈ atoms ((decoration v).color ⟨p,none⟩) := by
…

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.Vertex, OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.kind, OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.atoms, OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.decoration

  28. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.child_containment line 244
  29. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.flattenFun line 254
  30. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.flattenFun_bijective line 259
  31. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.flatten line 274
  32. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.portEquiv line 281

    Source documentation

    Ordered seam columns, not an unlabelled flag: first expand each named child into its atoms and then identify with the parent named atoms.

    def portEquiv : (vertexRanks (r 0) (r 1) (r 2) (r 3) (r 4) v).Columns p ≃
    (vertexRanks (r 0) (r 1) (r 2) (r 3) (r 4) v).Parent p :=
…

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.vertexRanks

  33. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.positiveFrame line 289
  34. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.fiber_enum_cancel line 295
  35. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.ComplementaryPatch.positive_comparison_eq line 300