OAI/AlgebraicGeometry/CharacterVarieties/Frames/BandBases.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IntegralCharacterVarieties.MatrixIso.ofLinearEquiv line 11
2. lemma OAI.IntegralCharacterVarieties.MatrixIso.linearEquiv_ofLinearEquiv line 20
3. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.AtomicData.mirror line 30
4. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.AtomicData.mirror_atoms line 57
5. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.ext_rank line 61
6. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.AtomicData.ranks_eq line 68
7. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.AtomicData.framesAtRanks line 69
8. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.AtomicData.framesAtRanks_holds line 72
9. def OAI.IntegralCharacterVarieties.NamedBandGrades.sigmaGradeEquiv line 88
10. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.rowGrade_card line 98
11. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.colGrade_card line 104
12. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.row_rank line 110
13. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.col_rank line 118
14. structure OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand line 134

    Source documentation

    A named simultaneous splitting of two frames.

    structure IdentifiedBand
        (f h : (((i : Fin n) × Fin (s i)) → K) ≃ₗ[K] (Fin r → K)) where
    …

15. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.identifiedBand_nonempty line 150
16. def OAI.IntegralCharacterVarieties.NamedBandGrades.identifiedBand line 160
17. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.rowRanks line 167
18. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.colRanks line 168
19. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.namedSeamFrame line 179
20. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.bandFromOldFrames line 184
21. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.colorBases_aux line 198
22. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.colorBases line 209

    Source documentation

    Bases on named secondary labels satisfy corner coherence at every allowed vertex.

    def colorBases : d.CoherentBases (R:=R) where
    …