OAI/AlgebraicGeometry/CharacterVarieties/Frames/GradeMaps.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IntegralCharacterVarieties.NamedBandGrades.gradeCoordinates line 10
2. def OAI.IntegralCharacterVarieties.NamedBandGrades.sumGrades line 23
3. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.grade_sumGrades line 28
4. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.prefix_sumGrades line 36
5. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.sumGrades_symm line 71
6. theorem OAI.IntegralCharacterVarieties.NamedBandGrades.namedFrame_holds line 79

   Source documentation

   Convert named grade maps to full seam frames by a block-diagonal correction over the coefficient ring.

   theorem namedFrame_holds (a : α → ℕ) (b : β → ℕ)
       (e : (α → R) ≃ₗ[R] V) (f : (β → R) ≃ₗ[R] V)
       (q : (k : ℕ) → ({i // a i=k} → R) ≃ₗ[R] ({i // b i=k} → R))
       (hp : ∀ k,framedPrefix a e k=framedPrefix b f k)
       (hg : ∀ k v,v∈framedPrefix a e (k+1) → q k (framedGrade a e k v)=framedGrade b f k v) :
       SameFramedFlag b ((sumGrades a b q).symm.trans e) f := by
   …

   Mentions: OAI.IntegralCharacterVarieties.framedPrefix, OAI.IntegralCharacterVarieties.framedGrade, OAI.IntegralCharacterVarieties.SameFramedFlag, OAI.IntegralCharacterVarieties.NamedBandGrades.sumGrades

7. def OAI.IntegralCharacterVarieties.NamedBandGrades.sectionGrade line 103
8. def OAI.IntegralCharacterVarieties.NamedBandGrades.gradeMap line 110

   Source documentation

   The induced map on a named graded quotient in the original coordinates.

   def gradeMap (a : α → ℕ) (b : β → ℕ)
       (e : (α → R) ≃ₗ[R] (β → R)) (k : ℕ) :
       ({i // a i=k} → R) →ₗ[R] ({i // b i=k} → R) :=
   …

9. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.grade_section line 123
10. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.section_prefix line 128
11. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.grade_prefix_zero line 134
12. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.subtract_section_prefix line 139
13. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.filtered_apply line 148
14. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.filtered_symm line 155
15. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.gradeMap_naturality line 162
16. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.gradeMap_left_inv line 172
17. def OAI.IntegralCharacterVarieties.NamedBandGrades.gradeEquiv line 184

    Source documentation

    Preservation of split prefixes makes the named row and column refinement maps invertible over the coefficient ring.

    def gradeEquiv (a : α → ℕ) (b : β → ℕ) (e : (α → R) ≃ₗ[R] (β → R))
        (h : ∀ k,(coordinatePrefix R a k).map e.toLinearMap=coordinatePrefix R b k)
        (k : ℕ) : ({i // a i=k} → R) ≃ₗ[R] ({i // b i=k} → R) :=
    …

    Mentions: OAI.IntegralCharacterVarieties.coordinatePrefix