OAI/AlgebraicGeometry/CharacterVarieties/Foundation/BoundaryFrames.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IntegralCharacterVarieties.MatrixIso.GradeDiagonal line 14

    Source documentation

    Change of bases on the named graded fibers.

    def GradeDiagonal (a : α → ℕ) (M : Matrix α α R) : Prop :=
…
  2. lemma OAI.IntegralCharacterVarieties.MatrixIso.conjugate_flag_entries line 17
  3. lemma OAI.IntegralCharacterVarieties.MatrixIso.sameFramedFlag_bases line 40

    Source documentation

    Common block changes on the source and common ambient changes on the TARGET preserve both flags and their specified grade maps.

    lemma sameFramedFlag_bases (a : α → ℕ) (x y : MatrixIso R α β)
    (w : MatrixIso R α α) (z : MatrixIso R β β)
    (hw : GradeDiagonal a w.val) (hi : GradeDiagonal a w.inv)
    (h : SameFramedFlag a x.linearEquiv y.linearEquiv) :
    SameFramedFlag a ((w.trans x).trans z).linearEquiv
      ((w.trans y).trans z).linearEquiv := by
…

    Mentions: OAI.IntegralCharacterVarieties.MatrixIso, OAI.IntegralCharacterVarieties.MatrixIso.GradeDiagonal, OAI.IntegralCharacterVarieties.SameFramedFlag, OAI.IntegralCharacterVarieties.MatrixIso.trans, OAI.IntegralCharacterVarieties.MatrixIso.linearEquiv

  4. lemma OAI.IntegralCharacterVarieties.MatrixIso.block_GradeDiagonal line 57
  5. theorem OAI.IntegralCharacterVarieties.MatrixIso.trans_symm_self line 74
  6. theorem OAI.IntegralCharacterVarieties.MatrixIso.symm_trans_self line 76
  7. theorem OAI.IntegralCharacterVarieties.MatrixIso.refl_trans line 78
  8. theorem OAI.IntegralCharacterVarieties.MatrixIso.trans_refl line 80
  9. theorem OAI.IntegralCharacterVarieties.MatrixIso.reindex_symm_eq line 82
  10. theorem OAI.IntegralCharacterVarieties.MatrixIso.sum_trans line 86
  11. theorem OAI.IntegralCharacterVarieties.MatrixIso.sum_symm line 92
  12. theorem OAI.IntegralCharacterVarieties.MatrixIso.congr_gauge line 96
  13. theorem OAI.IntegralCharacterVarieties.MatrixIso.reindex_reindex_eq line 121
  14. lemma OAI.IntegralCharacterVarieties.MatrixIso.bases_reindex line 126
  15. lemma OAI.IntegralCharacterVarieties.MatrixIso.GradeDiagonal_reindex line 134
  16. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.changePassageBases line 152

    Source documentation

    Rebase every named fiber continued through a passage, with the exact permutation and rank equalities of the original vertex.

    def changePassageBases (f : ∀ p, MatrixIso R (d.Columns p) (d.Parent p))
    (C : MatrixIso R (d.Columns false) (d.Columns false))
    (P : MatrixIso R (d.Parent false) (d.Parent false)) :
    ∀ p, MatrixIso R (d.Columns p) (d.Parent p)
  | false => (C.symm.trans (f false)).trans P
  | true => ((C.reindex d.passageColumns.symm d.passageColumns.symm).symm.trans
      (f true)).trans (P.reindex d.passageParent.symm d.passageParent.symm)

    Mentions: OAI.IntegralCharacterVarieties.MatrixIso

  17. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.changePassageBases_holds line 160
  18. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.changePassageBlockBases_holds line 176
  19. lemma OAI.IntegralCharacterVarieties.MatrixIso.congr_pull line 193
  20. lemma OAI.IntegralCharacterVarieties.MatrixIso.congr_bases_cancel line 198
  21. lemma OAI.IntegralCharacterVarieties.MatrixIso.split_refinement_natural line 204

    Source documentation

    Every untouched prefix/suffix strand cancels its two common basis changes; only the prescribed branch frame remains.

    lemma split_refinement_natural (e : A' ≃ A) (f : C' ≃ C)
    (v : MatrixIso R B W) (GA : MatrixIso R A A) (GB : MatrixIso R B B)
    (GW : MatrixIso R W W) (GC : MatrixIso R C C) :
    (congr e).sum (((GB.symm.trans v).trans GW).sum (congr f))=
      (((GA.reindex e e).sum (GB.sum (GC.reindex f f))).symm.trans
        ((congr e).sum (v.sum (congr f)))).trans (GA.sum (GW.sum GC)) := by
…

    Mentions: OAI.IntegralCharacterVarieties.MatrixIso, OAI.IntegralCharacterVarieties.MatrixIso.congr, OAI.IntegralCharacterVarieties.MatrixIso.sum, OAI.IntegralCharacterVarieties.MatrixIso.trans

  22. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.splitBeforeBasis line 225

    Source documentation

    Coherent changes in the six fiber types of a split, transported through the exact named corner equalities rather than through rank alone.

    def splitBeforeBasis (GA : MatrixIso R (d.SplitA false) (d.SplitA false))
    (GW : MatrixIso R d.SplitW d.SplitW)
    (GC : MatrixIso R (d.SplitC false) (d.SplitC false)) :=
…

    Mentions: OAI.IntegralCharacterVarieties.MatrixIso

  23. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.splitAfterBasis line 230
  24. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.splitBranchBasis line 236
  25. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.splitMiddleBasis line 239
  26. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.splitRefinement_bases line 242
  27. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.changeSplitBases line 262
  28. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.changeSplitBases_holds line 274
  29. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.splitAfterBasis_blocks_diagonal line 313
  30. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.changeSplitBlockBases_holds line 338