OAI/Geometry/ComplexBundle/Projective.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Projection models of complex projective space and products.

  1. def OAI.Kaplansky.ComplexGrassmann.projectionToGrassmann line 18
  2. def OAI.Kaplansky.ComplexGrassmann.columnFrame line 22
  3. theorem OAI.Kaplansky.ComplexGrassmann.columnFrame_injective line 26
  4. theorem OAI.Kaplansky.ComplexGrassmann.columnFrame_point line 43
  5. theorem OAI.Kaplansky.ComplexGrassmann.continuousOn_columnFrame line 58
  6. theorem OAI.Kaplansky.ComplexGrassmann.continuous_projectionToGrassmann line 66
  7. theorem OAI.Kaplansky.ComplexGrassmann.projectionToGrassmann_injective line 78
  8. def OAI.Kaplansky.ComplexGrassmann.graphLineVector line 95

    Source documentation

    A nonvanishing representative of a line in a graph chart.

    def graphLineVector (F : GraphFrame 1 k) (A : GraphSlope 1 k) : EuclideanSpace ℂ (Fin (1+k)) :=
…

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

  9. theorem OAI.Kaplansky.ComplexGrassmann.graphLineVector_coordinates line 98
  10. theorem OAI.Kaplansky.ComplexGrassmann.graphLineVector_ne_zero line 102
  11. theorem OAI.Kaplansky.ComplexGrassmann.continuous_graphLineVector line 110
  12. def OAI.Kaplansky.ComplexGrassmann.graphLineProjection line 115
  13. theorem OAI.Kaplansky.ComplexGrassmann.continuous_graphLineProjection line 118
  14. theorem OAI.Kaplansky.ComplexGrassmann.graphLineProjection_point line 124
  15. theorem OAI.Kaplansky.ComplexGrassmann.projectionToGrassmann_surjective line 139
  16. def OAI.Kaplansky.ComplexGrassmann.projectiveProjectionEquiv line 147

    Source documentation

    Projection and graph-atlas models of complex projective space agree as sets of actual complex lines.

    def projectiveProjectionEquiv (k : ℕ) : projectionSpace (1+k) 1 ≃ Grassmann 1 k :=
…

    Mentions: OAI.Kaplansky.projectionSpace, OAI.Kaplansky.ComplexGrassmann.Grassmann

  17. theorem OAI.Kaplansky.ComplexGrassmann.projectiveProjectionEquiv_symm_slopePoint line 159
  18. theorem OAI.Kaplansky.ComplexGrassmann.continuous_projectiveProjectionEquiv_symm line 165
  19. def OAI.Kaplansky.ComplexGrassmann.projectiveProjectionHomeomorph line 178

    Source documentation

    Identification of the compact orthogonal-projection model with the ordinary smooth graph-chart model of complex projective space.

    def projectiveProjectionHomeomorph (k : ℕ) : projectionSpace (1+k) 1 ≃ₜ Grassmann 1 k where
…

    Mentions: OAI.Kaplansky.projectionSpace, OAI.Kaplansky.ComplexGrassmann.Grassmann

  20. instance OAI.Kaplansky.ComplexGrassmann.projectiveGrassmannT2 line 183
  21. instance OAI.Kaplansky.ComplexGrassmann.projectiveGrassmannCompact line 186
  22. abbrev OAI.Kaplansky.ComplexGrassmann.ProjectiveProduct line 196
  23. abbrev OAI.Kaplansky.ComplexGrassmann.ProjectiveProductModel line 197
  24. instance OAI.Kaplansky.ComplexGrassmann.projectiveProductChartedSpace line 199
  25. instance OAI.Kaplansky.ComplexGrassmann.projectiveProductRealManifold line 203
  26. instance OAI.Kaplansky.ComplexGrassmann.projectiveProductCompact line 226
  27. instance OAI.Kaplansky.ComplexGrassmann.projectiveProductT2 line 227
  28. theorem OAI.Kaplansky.ComplexGrassmann.projectiveProduct_real_finrank line 229
  29. theorem OAI.Kaplansky.ComplexGrassmann.contMDiff_projectiveProduct_apply line 245

    Source documentation

    Coordinate projections of the actual finite projective product are smooth.

    theorem contMDiff_projectiveProduct_apply (i : ι) :
    ContMDiff 𝓘(ℝ,ProjectiveProductModel K) 𝓘(ℝ,GraphSlope 1 (K i)) ∞
      (fun P : ProjectiveProduct K => P i) := by
…

    Mentions: OAI.Kaplansky.ComplexGrassmann.ProjectiveProductModel, OAI.Kaplansky.ComplexGrassmann.GraphSlope, OAI.Kaplansky.ComplexGrassmann.ProjectiveProduct