BandCut.lean`

55 declarations, 0 contain sorry, 0 declared as axioms

Generator coordinates for a nonseparating cut

The cut sides and endpoint frames determine the new generator coordinates. Their seam and vertex equations follow from the full-block refinement identities.

lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutIdentityRank line 22
def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutIdentityColumns line 28
Source documentation
The coordinate equivalence for the singleton child of the identity seam.
```
def bandCutIdentityColumns : Fin ((D.bandCutDiagram q).seamDim (.inr ())) ≃ Fin (D.seamDim q) :=
…
```
Mentions: OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.seamDim
abbrev OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.BandCutUnit line 33
def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutP line 39
Source documentation
The old positive parent-side matrix, in the simultaneous child basis.
```
def bandCutP : D.BandCutUnit (A:=A) q := rebaseUnit (D.seamRank q) (g (.side ⟨q,none⟩))
```
Mentions: OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.rebaseUnit
def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutF line 41

def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutSideValues line 44

Source documentation

Transports on the cut sides, retaining the old child transports.

def bandCutSideValues : (a : Side (BandCutSeam S) (bandCutArity arity)) →
    (Matrix (Fin (D.rank ((D.ports.bandCutPorts q).facet a)))
      (Fin (D.rank ((D.ports.bandCutPorts q).facet a))) A)ˣ
  | ⟨.inl (s,k),none⟩ =>
      if hs : s=q then by
        subst s
        exact if k=1 then rebaseUnit (D.seamRank q).symm
          (T⁻¹*J⁻¹*D.bandCutP q g*T) else 1
      else if k=2 then g (.side ⟨s,none⟩) else 1
  | ⟨.inl (s,k),some i⟩ => if k=2 then g (.side ⟨s,some i⟩) else 1
  | ⟨.inr (),none⟩ => 1
  | ⟨.inr (),some _⟩ => rebaseUnit (D.seamRank q).symm J

Mentions: OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.rebaseUnit

def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutFrameValues line 58

Source documentation

Endpoint frames realizing both new splits as refinements of the old flags.

def bandCutFrameValues : (s : BandCutSeam S) → Bool →
    (Matrix (Fin ((D.bandCutDiagram q).seamDim s))
      (Fin ((D.bandCutDiagram q).seamDim s)) A)ˣ
  | .inl (s,k),e =>
      if hs : s=q then by
        subst s
        exact if k=0 then g (.frame q false)
          else if k=1 then
            if e then T⁻¹*J⁻¹*D.bandCutP q g*D.bandCutF q g false
              else T⁻¹*D.bandCutF q g false
          else if e then g (.frame q true) else D.bandCutP q g*D.bandCutF q g false
      else if k=2 ∧ e=true then g (.frame s true) else g (.frame s false)
…

Mentions: OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.seamDim

def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutPunctures line 73
def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutValues line 79
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.rebaseUnit_refl line 94
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.rebaseUnit_trans line 96
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.rebaseUnit_iso line 100
lemma OAI.IntegralCharacterVarieties.MatrixExpression.Term.eval_cast_unit line 110
lemma OAI.IntegralCharacterVarieties.MatrixExpression.blockUnit_one line 116
lemma OAI.IntegralCharacterVarieties.MatrixExpression.uniqueSigma_const_apply line 124

lemma OAI.IntegralCharacterVarieties.MatrixExpression.blockUnit_single line 132

Source documentation

A one-child seam retains its specified block ordering.

lemma blockUnit_single {n : ℕ} (x : (Matrix (Fin n) (Fin n) A)ˣ) :
    MatrixIso.unit (blockUnit (fun _ : Fin 1 => n) (fun _ => x))=
      (MatrixIso.unit x).reindex
        ((blockIndex (fun _ : Fin 1 => n)).trans (Equiv.uniqueSigma (fun _ => Fin n)))
        ((blockIndex (fun _ : Fin 1 => n)).trans (Equiv.uniqueSigma (fun _ => Fin n))) := by
…

Mentions: OAI.IntegralCharacterVarieties.MatrixIso.unit, OAI.IntegralCharacterVarieties.MatrixExpression.blockUnit, OAI.IntegralCharacterVarieties.MatrixExpression.blockIndex

lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCut_parent_inl line 155
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCut_parent_identity line 161
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCut_seam_last line 167
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCut_seam_first line 219
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCut_seam_middle line 249
lemma OAI.IntegralCharacterVarieties.MatrixIso.reindex_reindex line 301
lemma OAI.IntegralCharacterVarieties.MatrixIso.unit_injective_general line 305
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCut_identity_block line 319
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCut_seam_identity line 328
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCut_vertexRanks_old line 353
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutFrameValues_outer line 356
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCut_portFrame_old line 362
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCut_vertexComparison_old line 372
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCut_vertexComparison_continuation line 391
def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.fullSplitAfter line 416
def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.fullSplitBefore line 422
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.splitRefinement_full line 429
Source documentation
Refinement of the sole block at the inverse-band vertices.
```
lemma splitRefinement_full (w : MatrixIso R (d.Columns .branch) (d.Parent .branch)) :
    d.splitRefinement w=(w.reindex d.splitBranchChildren d.splitBranchParent).reindex
      d.fullSplitAfter d.fullSplitBefore := by
…
```
Mentions: OAI.IntegralCharacterVarieties.MatrixIso
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.rank_ext line 453
abbrev OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutSplitRanks line 462
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutSplitRanks_reverse line 465
def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutSplitChildIndex line 472
Source documentation
After and branch fiber indices in the full-block split.
```
def bandCutSplitChildIndex : (D.bandCutSplitRanks q).Columns .branch ≃ Fin (D.seamDim q) :=
…
```
def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutSplitRowIndex line 475
def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutSplitParentIndex line 478
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutSplitChild_compat line 481
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutSplitBefore_compat line 506
abbrev OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutSplitFrame line 539
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutSplitFrame_exact line 549
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCut_portFrame_first line 579
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCut_vertexComparison_first line 598
abbrev OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutSplitRanksLast line 615
def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutSplitChildIndexLast line 619
Source documentation
After and branch fiber indices in the full-block split.
```
def bandCutSplitChildIndexLast : (D.bandCutSplitRanksLast q).Columns .branch ≃ Fin (D.seamDim q) :=
…
```
def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutSplitRowIndexLast line 622
def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutSplitParentIndexLast line 625
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutSplitChild_compatLast line 628
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutSplitBefore_compatLast line 653
abbrev OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutSplitFrameLast line 686
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCutSplitFrameLast_exact line 696
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCut_portFrame_last line 726
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandCut_vertexComparison_last line 746