OAI/AlgebraicGeometry/CharacterVarieties/Frames/BandGauges.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.fiberEnum line 14
2. def OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.rowFiberEquiv line 18
3. def OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.colFiberEquiv line 23
4. def OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.parentGauge line 28
5. def OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.rowGauge line 32
6. def OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.colGauge line 41
7. def OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.colorGauge line 51

   Source documentation

   Row and column contacts have separate named gauges, including when their facet labels coincide.

   def colorGauge (c : Option (Secondary n n)) :
       MatrixIso K (Fin (freshRank r w.shape.secondaryRank c))
         (Fin (freshRank r w.shape.secondaryRank c)) := by
   …

   Mentions: OAI.IntegralCharacterVarieties.MatrixIso

8. def OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.vertexBases line 60
9. def OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.vertexFrames line 65
10. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.vertexFrames_holds line 71
11. def OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.mirrorColorGauge line 77

    Source documentation

    The mirror gauge changes only the principal rank fiber; lower strip fibers retain their named gauges.

    def mirrorColorGauge (T : MatrixIso K (Fin r) (Fin r)) (c : Option (Secondary n n)) :
        MatrixIso K (Fin (freshRank r w.shape.secondaryRank c))
          (Fin (freshRank r w.shape.secondaryRank c)) := by
    …

    Mentions: OAI.IntegralCharacterVarieties.MatrixIso

12. def OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.mirrorVertexBases line 84
13. def OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.mirrorVertexFrames line 92
14. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.mirrorVertexFrames_holds line 99
15. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.AtomicData.rank_of_atoms line 113
16. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.AtomicData.atom_cast_other line 116
17. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.AtomicData.seamColumns line 127
18. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.AtomicData.portEquiv_seam line 133
19. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.AtomicData.frame_seam line 147

    Source documentation

    Ordered atomic block frames agree under named parent and child identifications.

    lemma frame_seam {R : Type} [CommRing R] (p : k.table.Port) (q : l.table.Port)
        (c : k.table.Child p ≃ l.table.Child q)
        (hp : D.atoms ⟨p,none⟩=E.atoms ⟨q,none⟩)
        (hc : ∀ a,D.atoms ⟨p,some a⟩=E.atoms ⟨q,some (c a)⟩) :
        ((D.frame p (R:=R)).trans (MatrixIso.congr (finCongr (D.rank_of_atoms E hp))))=
    …

    Mentions: OAI.IntegralCharacterVarieties.MatrixIso.congr

20. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.AtomicData.frame_reindex line 164
21. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.AtomicData.reframe_seam line 181

    Source documentation

    Gauge-compatible named atomic seams give frame equalities under the parent and child identifications.

    lemma reframe_seam (G : D.localRanks.CoherentBases (R:=R))
    …

22. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.vertex_frame_seam line 212
23. def OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.interiorChild line 231
24. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.interior_parent line 238
25. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.interior_child line 245
26. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.interior_frame_seam line 257

    Source documentation

    Internal original-gallery seams are satisfied by the named root bases with identity side transports.

    lemma interior_frame_seam (j : Fin w.shape.atomicBand.length) :
        (w.vertexFrames j.succ (w.shape.atomicBand.kind j.succ).input).reindex
          ((w.shape.vertexAtoms j.castSucc).seamColumns (w.shape.vertexAtoms j.succ)
            _ _ (w.interiorChild j)
            (fun a => congrArg w.shape.facetAtoms (w.interior_child j a)))
          (finCongr ((w.shape.vertexAtoms j.castSucc).rank_of_atoms (w.shape.vertexAtoms j.succ)
            (congrArg w.shape.facetAtoms (w.interior_parent j))))=
          w.vertexFrames j.castSucc (w.shape.atomicBand.kind j.castSucc).output :=
    …