OAI/Geometry/ComplexBundle/GrassmannManifold.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Grassmannian frames, smooth manifold structure, and countability.

  1. abbrev OAI.Kaplansky.ComplexGrassmann.PlaneFrameMap line 19
  2. abbrev OAI.Kaplansky.ComplexGrassmann.IndependentFrame line 20
  3. def OAI.Kaplansky.ComplexGrassmann.framePoint line 22
  4. def OAI.Kaplansky.ComplexGrassmann.frameTop line 27
  5. def OAI.Kaplansky.ComplexGrassmann.frameBottom line 31
  6. def OAI.Kaplansky.ComplexGrassmann.frameSlope line 35
  7. theorem OAI.Kaplansky.ComplexGrassmann.frameTop_apply line 38
  8. theorem OAI.Kaplansky.ComplexGrassmann.frameBottom_apply line 41
  9. theorem OAI.Kaplansky.ComplexGrassmann.frameTop_contDiff line 44
  10. theorem OAI.Kaplansky.ComplexGrassmann.frameSlope_contDiffAt line 47
  11. theorem OAI.Kaplansky.ComplexGrassmann.frameSlope_plane line 57
  12. theorem OAI.Kaplansky.ComplexGrassmann.frameTop_unit line 74
  13. theorem OAI.Kaplansky.ComplexGrassmann.framePoint_continuous line 82

    Source documentation

    Sending an arbitrary independent frame to its actual span is continuous for the graph topology; this connects the atlas to geometric frame families.

    theorem framePoint_continuous : Continuous (framePoint (s := s) (k := k)) := by
…

    Mentions: OAI.Kaplansky.ComplexGrassmann.framePoint

  14. instance OAI.Kaplansky.ComplexGrassmann.grassmannChartedSpace line 109
  15. theorem OAI.Kaplansky.ComplexGrassmann.grassmann_overlap_source line 115
  16. instance OAI.Kaplansky.ComplexGrassmann.grassmannComplexManifold line 125
  17. instance OAI.Kaplansky.ComplexGrassmann.grassmannRealManifold line 133
  18. theorem OAI.Kaplansky.ComplexGrassmann.graph_slope_complex_finrank line 141
  19. theorem OAI.Kaplansky.ComplexGrassmann.graph_slope_real_finrank line 145
  20. theorem OAI.Kaplansky.ComplexGrassmann.framePoint_surjective line 157

    Source documentation

    Every actual plane is the span of an independent frame.

    theorem framePoint_surjective : Function.Surjective (framePoint (s := s) (k := k)) := by
…

    Mentions: OAI.Kaplansky.ComplexGrassmann.framePoint

  21. instance OAI.Kaplansky.ComplexGrassmann.independentFrameLocallyCompact line 180
  22. instance OAI.Kaplansky.ComplexGrassmann.grassmannSigmaCompact line 184
  23. instance OAI.Kaplansky.ComplexGrassmann.grassmannSecondCountable line 189
  24. theorem OAI.Kaplansky.ComplexGrassmann.exists_countable_graph_cover line 194

    Source documentation

    The graph atlas has a countable subcover of actual planes, providing the countability needed for the lower-dimensional image argument.

    theorem exists_countable_graph_cover : ∃ c : Set (GraphFrame s k), c.Countable ∧
    ∀ P : Grassmann s k, ∃ F ∈ c, InGraphChart F P.val := by
…

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