OAI/AlgebraicGeometry/CharacterVarieties/Frames/Graded.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IntegralCharacterVarieties.TwoFlagBand.supportedCoordinates line 11
2. theorem OAI.IntegralCharacterVarieties.TwoFlagBand.supportedCoordinates_eq line 18
3. theorem OAI.IntegralCharacterVarieties.TwoFlagBand.boundedGrid_coordinate_mem line 42
4. abbrev OAI.IntegralCharacterVarieties.NamedBandGrades.Atoms line 59
5. def OAI.IntegralCharacterVarieties.NamedBandGrades.rowGrade line 62
6. def OAI.IntegralCharacterVarieties.NamedBandGrades.colGrade line 64
7. def OAI.IntegralCharacterVarieties.NamedBandGrades.curryCoordinates line 76
8. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.curry_row_prefix line 80
9. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.curry_col_prefix line 93
10. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.row_framedPrefix line 106
11. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.col_framedPrefix line 114
12. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.boundedGrid_map_support line 122
13. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.coordinatePrefix_top line 130
14. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.framedPrefix_top line 136
15. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.framedPrefix_mono line 142
16. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.framedPrefix_zero line 145
17. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.frameChange_filters line 159
18. def OAI.IntegralCharacterVarieties.NamedBandGrades.frameGradeEquiv line 170
19. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.frameGradeEquiv_naturality line 176
20. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.actual_band_common_prefixes line 198

    Source documentation

    A common atomic splitting of two endpoint flags preserves all prefixes.

    lemma actual_band_common_prefixes
        (a : α → Fin n) (b : β → Fin m)
        (f : (α → K) ≃ₗ[K] V) (h : (β → K) ≃ₗ[K] V) :
        ∃ (d : RankShape n m (Module.finrank K V)) (e : (Atoms d → K) ≃ₗ[K] V),
          (∀ k,framedPrefix (rowGrade d) e k=framedPrefix (fun i => (a i).val) f k)  ∧
          (∀ k,framedPrefix (colGrade d) e k=framedPrefix (fun i => (b i).val) h k) := by
    …

    Mentions: OAI.IntegralCharacterVarieties.NamedBandGrades.Atoms, OAI.IntegralCharacterVarieties.framedPrefix, OAI.IntegralCharacterVarieties.NamedBandGrades.rowGrade, OAI.IntegralCharacterVarieties.NamedBandGrades.colGrade

21. theorem OAI.IntegralCharacterVarieties.NamedBandGrades.actual_named_band_grades line 237

    Source documentation

    Simultaneous splitting of two framed endpoint flags into a finite rank array, with row and column quotient isomorphisms intertwining the named quotient projections on each prefix.

    theorem actual_named_band_grades
        (a : α → Fin n) (b : β → Fin m)
        (f : (α → K) ≃ₗ[K] V) (h : (β → K) ≃ₗ[K] V) :
        ∃ (d : RankShape n m (Module.finrank K V)) (e : (Atoms d → K) ≃ₗ[K] V)
          (row : (k : ℕ) → ({i // rowGrade d i=k} → K) ≃ₗ[K] ({i // (a i).val=k} → K))
          (col : (k : ℕ) → ({i // colGrade d i=k} → K) ≃ₗ[K] ({i // (b i).val=k} → K)),
          (∀ k,framedPrefix (rowGrade d) e k=framedPrefix (fun i => (a i).val) f k)  ∧
          (∀ k,framedPrefix (colGrade d) e k=framedPrefix (fun i => (b i).val) h k)  ∧
          (∀ k v,v∈framedPrefix (rowGrade d) e (k+1) →
            row k (framedGrade (rowGrade d) e k v)=framedGrade (fun i => (a i).val) f k v)  ∧
          (∀ k v,v∈framedPrefix (colGrade d) e (k+1) →
            col k (framedGrade (colGrade d) e k v)=framedGrade (fun i => (b i).val) h k v) := by
    …

    Mentions: OAI.IntegralCharacterVarieties.NamedBandGrades.Atoms, OAI.IntegralCharacterVarieties.NamedBandGrades.rowGrade, OAI.IntegralCharacterVarieties.NamedBandGrades.colGrade, OAI.IntegralCharacterVarieties.framedPrefix, OAI.IntegralCharacterVarieties.framedGrade