OAI/AlgebraicGeometry/CharacterVarieties/Foundation/IntervalTransport.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.IntegralCharacterVarieties.IntrinsicInterval.Data line 12

    Source documentation

    The adjacent old flag terms and chosen subsystem. No splitting or exact-sequence data is an input.

    structure Data (R V : Type*) [CommRing R] [AddCommGroup V] [Module R V] where
…
  2. abbrev OAI.IntegralCharacterVarieties.IntrinsicInterval.Data.p line 20
  3. abbrev OAI.IntegralCharacterVarieties.IntrinsicInterval.Data.n line 21
  4. abbrev OAI.IntegralCharacterVarieties.IntrinsicInterval.Data.G line 22
  5. abbrev OAI.IntegralCharacterVarieties.IntrinsicInterval.Data.up line 23
  6. abbrev OAI.IntegralCharacterVarieties.IntrinsicInterval.Data.UG line 24
  7. abbrev OAI.IntegralCharacterVarieties.IntrinsicInterval.Data.qi line 25
  8. abbrev OAI.IntegralCharacterVarieties.IntrinsicInterval.Data.qp line 26
  9. abbrev OAI.IntegralCharacterVarieties.IntrinsicInterval.Data.QG line 28
  10. abbrev OAI.IntegralCharacterVarieties.IntrinsicInterval.Data.S line 29
  11. def OAI.IntegralCharacterVarieties.IntrinsicInterval.Data.includeU line 32

    Source documentation

    Inclusion of the induced intersection grade into the old grade.

    def includeU : D.UG →ₗ[R] D.G :=
…
  12. theorem OAI.IntegralCharacterVarieties.IntrinsicInterval.Data.includeU_mk line 35
  13. theorem OAI.IntegralCharacterVarieties.IntrinsicInterval.Data.includeU_injective line 38
  14. theorem OAI.IntegralCharacterVarieties.IntrinsicInterval.Data.includeU_range line 43
  15. def OAI.IntegralCharacterVarieties.IntrinsicInterval.Data.toImage line 48

    Source documentation

    Send an old flag vector to its class in the quotient subsystem, retaining its membership in the induced image flag.

    def toImage : D.current →ₗ[R] D.qi where
…
  16. theorem OAI.IntegralCharacterVarieties.IntrinsicInterval.Data.toImage_val line 53
  17. theorem OAI.IntegralCharacterVarieties.IntrinsicInterval.Data.toImage_surjective line 56
  18. theorem OAI.IntegralCharacterVarieties.IntrinsicInterval.Data.p_toImage line 61
  19. def OAI.IntegralCharacterVarieties.IntrinsicInterval.Data.projectQ line 66

    Source documentation

    Projection to the successive quotient of the image flag on V/U.

    def projectQ : D.G →ₗ[R] D.QG := D.p.mapQ D.qp D.toImage D.p_toImage
  20. theorem OAI.IntegralCharacterVarieties.IntrinsicInterval.Data.projectQ_mk line 68
  21. theorem OAI.IntegralCharacterVarieties.IntrinsicInterval.Data.projectQ_surjective line 71
  22. theorem OAI.IntegralCharacterVarieties.IntrinsicInterval.Data.projectQ_kernel line 78

    Source documentation

    Exactness follows from x having the same U-quotient as an element of the previous old flag iff their difference lies in U. This uses the old subspaces; compatibility is not an extra hypothesis.

    theorem projectQ_kernel : D.projectQ.ker = D.S := by
…
  23. theorem OAI.IntegralCharacterVarieties.IntrinsicInterval.Data.exact_at_grade line 105
  24. def OAI.IntegralCharacterVarieties.IntrinsicInterval.Data.uGradeEquiv line 109

    Source documentation

    The induced U-graded space is the subspace of the old grade.

    def uGradeEquiv : D.UG ≃ₗ[R] D.S :=
…
  25. theorem OAI.IntegralCharacterVarieties.IntrinsicInterval.Data.uGradeEquiv_val line 113
  26. def OAI.IntegralCharacterVarieties.IntrinsicInterval.Data.qGradeEquiv line 117

    Source documentation

    The quotient by that subspace is exactly the induced Q grade.

    def qGradeEquiv : (D.G ⧸ D.S) ≃ₗ[R] D.QG :=
…
  27. theorem OAI.IntegralCharacterVarieties.IntrinsicInterval.Data.qGradeEquiv_mk line 121
  28. theorem OAI.IntegralCharacterVarieties.IntrinsicInterval.Data.boundary_exact_sequence line 125

    Source documentation

    Every old interval canonically produces its required short exact sequence.

    theorem boundary_exact_sequence :
    Function.Injective D.includeU ∧ D.includeU.range=D.projectQ.ker ∧
      Function.Surjective D.projectQ :=
…
  29. structure OAI.IntegralCharacterVarieties.IntrinsicInterval.Transport line 137

    Source documentation

    Old parallel transport preserving the subsystem and old flag.

    structure Transport (D : Data R V) (E : Data R V') where
…

    Mentions: OAI.IntegralCharacterVarieties.IntrinsicInterval.Data

  30. def OAI.IntegralCharacterVarieties.IntrinsicInterval.Transport.onCurrent line 147
  31. def OAI.IntegralCharacterVarieties.IntrinsicInterval.Transport.onQuotient line 150
  32. theorem OAI.IntegralCharacterVarieties.IntrinsicInterval.Transport.p_map line 153
  33. theorem OAI.IntegralCharacterVarieties.IntrinsicInterval.Transport.n_map line 159
  34. def OAI.IntegralCharacterVarieties.IntrinsicInterval.Transport.onGrade line 165
  35. def OAI.IntegralCharacterVarieties.IntrinsicInterval.Transport.onIntersection line 168
  36. theorem OAI.IntegralCharacterVarieties.IntrinsicInterval.Transport.up_map line 171
  37. def OAI.IntegralCharacterVarieties.IntrinsicInterval.Transport.onUGrade line 177
  38. theorem OAI.IntegralCharacterVarieties.IntrinsicInterval.Transport.quotient_naturality line 180
  39. theorem OAI.IntegralCharacterVarieties.IntrinsicInterval.Transport.qi_map line 186
  40. theorem OAI.IntegralCharacterVarieties.IntrinsicInterval.Transport.prev_image_map line 191
  41. def OAI.IntegralCharacterVarieties.IntrinsicInterval.Transport.onImage line 196
  42. theorem OAI.IntegralCharacterVarieties.IntrinsicInterval.Transport.qp_map line 199
  43. def OAI.IntegralCharacterVarieties.IntrinsicInterval.Transport.onQGrade line 206
  44. theorem OAI.IntegralCharacterVarieties.IntrinsicInterval.Transport.grade_mk line 209
  45. theorem OAI.IntegralCharacterVarieties.IntrinsicInterval.Transport.uGrade_mk line 212
  46. theorem OAI.IntegralCharacterVarieties.IntrinsicInterval.Transport.qGrade_mk line 215
  47. theorem OAI.IntegralCharacterVarieties.IntrinsicInterval.Transport.inclusion_naturality line 219

    Source documentation

    Inclusion contact commutes with the old parallel transport.

    theorem inclusion_naturality (x : D.UG) :
    g.onGrade (D.includeU x)=E.includeU (g.onUGrade x) := by
…
  48. theorem OAI.IntegralCharacterVarieties.IntrinsicInterval.Transport.projection_naturality line 225

    Source documentation

    Image/quotient contact commutes with old parallel transport.

    theorem projection_naturality (x : D.G) :
    g.onQGrade (D.projectQ x)=E.projectQ (g.onGrade x) := by
…
  49. theorem OAI.IntegralCharacterVarieties.IntrinsicInterval.Transport.S_map line 230
  50. def OAI.IntegralCharacterVarieties.IntrinsicInterval.Transport.identity line 236
  51. def OAI.IntegralCharacterVarieties.IntrinsicInterval.Transport.followedBy line 242
  52. theorem OAI.IntegralCharacterVarieties.IntrinsicInterval.Transport.identity_grade line 254
  53. theorem OAI.IntegralCharacterVarieties.IntrinsicInterval.Transport.identity_uGrade line 257
  54. theorem OAI.IntegralCharacterVarieties.IntrinsicInterval.Transport.identity_qGrade line 260
  55. theorem OAI.IntegralCharacterVarieties.IntrinsicInterval.Transport.followedBy_grade line 269
  56. theorem OAI.IntegralCharacterVarieties.IntrinsicInterval.Transport.followedBy_uGrade line 273
  57. theorem OAI.IntegralCharacterVarieties.IntrinsicInterval.Transport.followedBy_qGrade line 277