OAI/Geometry/ComplexBundle/Grassmann.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

Graph charts and atlas of the complex Grassmannian.

  1. abbrev OAI.Kaplansky.ComplexGrassmann.GraphHorizontal line 21
  2. abbrev OAI.Kaplansky.ComplexGrassmann.GraphVertical line 22
  3. abbrev OAI.Kaplansky.ComplexGrassmann.GraphAmbient line 23
  4. abbrev OAI.Kaplansky.ComplexGrassmann.GraphMap line 24
  5. abbrev OAI.Kaplansky.ComplexGrassmann.Components line 25
  6. abbrev OAI.Kaplansky.ComplexGrassmann.GraphFrame line 26
  7. def OAI.Kaplansky.ComplexGrassmann.Grassmann line 29

    Source documentation

    Actual complex s-planes in complex dimension s+k.

    def Grassmann (s k : ℕ) := {P : Submodule ℂ (Components s k) // Module.finrank ℂ P=s}
…

    Mentions: OAI.Kaplansky.ComplexGrassmann.Components

  8. def OAI.Kaplansky.ComplexGrassmann.graphPlane line 34

    Source documentation

    The usual graph chart, transported by an arbitrary linear splitting.

    def graphPlane (F : (GraphFrame s k)) (A : (GraphMap s k)) : Submodule ℂ (Components s k) :=
…

    Mentions: OAI.Kaplansky.ComplexGrassmann.GraphFrame, OAI.Kaplansky.ComplexGrassmann.GraphMap, OAI.Kaplansky.ComplexGrassmann.Components

  9. theorem OAI.Kaplansky.ComplexGrassmann.mem_graphPlane line 37
  10. def OAI.Kaplansky.ComplexGrassmann.graphPlaneEquiv line 40
  11. theorem OAI.Kaplansky.ComplexGrassmann.graphPlane_finrank line 61
  12. def OAI.Kaplansky.ComplexGrassmann.graphPoint line 65
  13. theorem OAI.Kaplansky.ComplexGrassmann.graphPlane_injective line 67
  14. def OAI.Kaplansky.ComplexGrassmann.InGraphChart line 78

    Source documentation

    A plane is in a splitting's graph domain exactly when its projection to the horizontal factor is bijective. This is independent of its chosen basis.

    def InGraphChart (F : (GraphFrame s k)) (P : Submodule ℂ (Components s k)) : Prop :=
…

    Mentions: OAI.Kaplansky.ComplexGrassmann.GraphFrame, OAI.Kaplansky.ComplexGrassmann.Components

  15. theorem OAI.Kaplansky.ComplexGrassmann.graphPlane_inChart line 81
  16. def OAI.Kaplansky.ComplexGrassmann.graphProjection line 84
  17. def OAI.Kaplansky.ComplexGrassmann.graphCoordinate line 87
  18. theorem OAI.Kaplansky.ComplexGrassmann.graphCoordinate_plane line 91
  19. theorem OAI.Kaplansky.ComplexGrassmann.inGraphChart_iff line 109
  20. theorem OAI.Kaplansky.ComplexGrassmann.graph_charts_cover line 118

    Source documentation

    Every actual s-plane is the center of a graph chart.

    theorem graph_charts_cover (P : Submodule ℂ (Components s k)) (hP : Module.finrank ℂ P=s) :
    ∃ F : (GraphFrame s k), graphPlane F 0=P := by
…

    Mentions: OAI.Kaplansky.ComplexGrassmann.Components, OAI.Kaplansky.ComplexGrassmann.GraphFrame, OAI.Kaplansky.ComplexGrassmann.graphPlane

  21. theorem OAI.Kaplansky.ComplexGrassmann.graph_model_finrank line 148
  22. abbrev OAI.Kaplansky.ComplexGrassmann.GraphSlope line 160
  23. def OAI.Kaplansky.ComplexGrassmann.graphInclusion line 162
  24. theorem OAI.Kaplansky.ComplexGrassmann.graphInclusion_apply line 166
  25. def OAI.Kaplansky.ComplexGrassmann.graphTransport line 169
  26. def OAI.Kaplansky.ComplexGrassmann.graphTop line 172
  27. def OAI.Kaplansky.ComplexGrassmann.graphBottom line 175
  28. theorem OAI.Kaplansky.ComplexGrassmann.graphTop_apply line 178
  29. theorem OAI.Kaplansky.ComplexGrassmann.graphBottom_apply line 181
  30. def OAI.Kaplansky.ComplexGrassmann.graphTransition line 185

    Source documentation

    The exact change of graph slope: bottom block times inverse top block.

    def graphTransition (F G : (GraphFrame s k)) (A : (GraphSlope s k)) : (GraphSlope s k) :=
…

    Mentions: OAI.Kaplansky.ComplexGrassmann.GraphFrame, OAI.Kaplansky.ComplexGrassmann.GraphSlope

  31. theorem OAI.Kaplansky.ComplexGrassmann.graphTop_contDiff line 188
  32. theorem OAI.Kaplansky.ComplexGrassmann.graphBottom_contDiff line 192
  33. theorem OAI.Kaplansky.ComplexGrassmann.graphOverlap_open line 196
  34. theorem OAI.Kaplansky.ComplexGrassmann.graphTransition_contDiffAt line 199
  35. theorem OAI.Kaplansky.ComplexGrassmann.graphTop_inverse_apply line 207
  36. theorem OAI.Kaplansky.ComplexGrassmann.graphTop_inverse_apply' line 214
  37. theorem OAI.Kaplansky.ComplexGrassmann.graphTransition_plane line 222

    Source documentation

    On overlap, the rational transition describes the identical actual plane.

    theorem graphTransition_plane (F G : (GraphFrame s k)) (A : (GraphSlope s k)) (hA : IsUnit (graphTop F G A)) :
    graphPlane G (graphTransition F G A).toLinearMap=graphPlane F A.toLinearMap := by
…

    Mentions: OAI.Kaplansky.ComplexGrassmann.GraphFrame, OAI.Kaplansky.ComplexGrassmann.GraphSlope, OAI.Kaplansky.ComplexGrassmann.graphTop, OAI.Kaplansky.ComplexGrassmann.graphPlane, OAI.Kaplansky.ComplexGrassmann.graphTransition

  38. theorem OAI.Kaplansky.ComplexGrassmann.inGraphChart_iff_unit line 245
  39. def OAI.Kaplansky.ComplexGrassmann.slopePoint line 274
  40. theorem OAI.Kaplansky.ComplexGrassmann.slopePoint_injective line 276
  41. def OAI.Kaplansky.ComplexGrassmann.slopeCoordinate line 281
  42. theorem OAI.Kaplansky.ComplexGrassmann.slopePoint_coordinate line 285
  43. theorem OAI.Kaplansky.ComplexGrassmann.slopeCoordinate_point line 291
  44. instance OAI.Kaplansky.ComplexGrassmann.grassmannTopology line 298

    Source documentation

    The (Grassmann s k) topology is specified by its full graph atlas on actual subspaces. The following theorems verify that these maps are open charts.

    instance grassmannTopology : TopologicalSpace (Grassmann s k) where
…

    Mentions: OAI.Kaplansky.ComplexGrassmann.Grassmann

  45. theorem OAI.Kaplansky.ComplexGrassmann.slopePoint_continuous line 310
  46. theorem OAI.Kaplansky.ComplexGrassmann.slopePoint_image_preimage line 315
  47. theorem OAI.Kaplansky.ComplexGrassmann.slopePoint_isOpenMap line 339
  48. def OAI.Kaplansky.ComplexGrassmann.graphPartialEquiv line 346
  49. def OAI.Kaplansky.ComplexGrassmann.grassmannChart line 357

    Source documentation

    A genuine open chart, with all s*k complex graph coordinates as its target.

    def grassmannChart (F : (GraphFrame s k)) : OpenPartialHomeomorph (Grassmann s k) (GraphSlope s k) :=
…

    Mentions: OAI.Kaplansky.ComplexGrassmann.GraphFrame, OAI.Kaplansky.ComplexGrassmann.Grassmann, OAI.Kaplansky.ComplexGrassmann.GraphSlope

  50. theorem OAI.Kaplansky.ComplexGrassmann.grassmannChart_source line 361
  51. theorem OAI.Kaplansky.ComplexGrassmann.grassmannChart_target line 364
  52. theorem OAI.Kaplansky.ComplexGrassmann.grassmannChart_apply line 366
  53. theorem OAI.Kaplansky.ComplexGrassmann.grassmannChart_symm_apply line 369
  54. theorem OAI.Kaplansky.ComplexGrassmann.grassmann_atlas_covers line 372
  55. theorem OAI.Kaplansky.ComplexGrassmann.grassmann_chart_transition line 379
  56. theorem OAI.Kaplansky.ComplexGrassmann.grassmann_chart_transition_smooth line 389

    Source documentation

    Smoothness on every actual chart overlap, with no assumed transition law.

    theorem grassmann_chart_transition_smooth (F G : (GraphFrame s k)) :
    ContDiffOn ℂ ∞ (fun A => grassmannChart G ((grassmannChart F).symm A))
      {A | IsUnit (graphTop F G A)} := by
…

    Mentions: OAI.Kaplansky.ComplexGrassmann.GraphFrame, OAI.Kaplansky.ComplexGrassmann.grassmannChart, OAI.Kaplansky.ComplexGrassmann.graphTop