OAI/AlgebraicTopology/IntegralHomology/ProjectivePuncture.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

Punctures, collapse, and hyperplane retraction in projective space.

  1. def OAI.Kaplansky.ComplexGrassmann.oppositeLineFrame line 18

    Source documentation

    Interchange the two one-dimensional factors of a projective-line chart.

    def oppositeLineFrame (F : GraphFrame 1 1) : GraphFrame 1 1 :=
…

    Mentions: OAI.Kaplansky.ComplexGrassmann.GraphFrame

  2. theorem OAI.Kaplansky.ComplexGrassmann.oppositeLineFrame_source line 23

    Source documentation

    In complex dimension one the opposite affine chart omits exactly the origin of the original chart. This uses actual lines in the ambient space.

    theorem oppositeLineFrame_source (F : GraphFrame 1 1) :
    (grassmannChart (oppositeLineFrame F)).source =
      ({graphPoint F 0}ᶜ : Set (Grassmann 1 1)) := by
…

    Mentions: OAI.Kaplansky.ComplexGrassmann.GraphFrame, OAI.Kaplansky.ComplexGrassmann.grassmannChart, OAI.Kaplansky.ComplexGrassmann.oppositeLineFrame, OAI.Kaplansky.ComplexGrassmann.graphPoint, OAI.Kaplansky.ComplexGrassmann.Grassmann

  3. def OAI.Kaplansky.ComplexGrassmann.projectiveLinePunctureHomeomorph line 60

    Source documentation

    The projective line minus any point is the entire affine complex model.

    def projectiveLinePunctureHomeomorph (P : Grassmann 1 1) :
    ({P}ᶜ : Set (Grassmann 1 1)) ≃ₜ GraphSlope 1 1 := by
…

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

  4. theorem OAI.Kaplansky.ComplexGrassmann.projectiveLinePuncture_contractible line 71
  5. def OAI.Kaplansky.ComplexGrassmann.projectiveLinearImage line 87

    Source documentation

    The actual image line, when the linear map is injective on that line.

    def projectiveLinearImage (L : Components 1 k →L[ℂ] Components 1 l)
    (P : Grassmann 1 k) (h : Function.Injective (L.toLinearMap.comp P.val.subtype)) :
    Grassmann 1 l :=
…

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

  6. def OAI.Kaplansky.ComplexGrassmann.graphLineFrame line 96

    Source documentation

    A continuously varying independent frame for a graph-chart line.

    def graphLineFrame (F : GraphFrame 1 k) (A : GraphSlope 1 k) : PlaneFrameMap 1 k :=
…

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

  7. theorem OAI.Kaplansky.ComplexGrassmann.graphLineFrame_injective line 100
  8. theorem OAI.Kaplansky.ComplexGrassmann.graphLineFrame_point line 105
  9. theorem OAI.Kaplansky.ComplexGrassmann.continuous_graphLineFrame line 120
  10. theorem OAI.Kaplansky.ComplexGrassmann.continuous_projectiveLinearImage line 128

    Source documentation

    Linear images vary continuously even if the ambient map is singular; only injectivity on the input line is needed.

    theorem continuous_projectiveLinearImage {X : Type*} [TopologicalSpace X]
    (L : X → Components 1 k →L[ℂ] Components 1 l) (P : X → Grassmann 1 k)
    (h : ∀ x, Function.Injective ((L x).toLinearMap.comp (P x).val.subtype))
    (hL : Continuous L) (hP : Continuous P) :
    Continuous (fun x => projectiveLinearImage (L x) (P x) (h x)) := by
…

    Mentions: OAI.Kaplansky.ComplexGrassmann.Components, OAI.Kaplansky.ComplexGrassmann.Grassmann, OAI.Kaplansky.ComplexGrassmann.projectiveLinearImage

  11. theorem OAI.Kaplansky.ComplexGrassmann.verticalProjection_injective_iff line 174

    Source documentation

    Projection along the removed line is injective on every other line.

    theorem verticalProjection_injective_iff (F : GraphFrame 1 k) (P : Grassmann 1 k) :
    Function.Injective (fun z : P.val => (F z.val).2) ↔ P ≠ graphPoint F 0 := by
…

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

  12. def OAI.Kaplansky.ComplexGrassmann.punctureCollapseLinear line 203

    Source documentation

    Scale the removed-line coordinate and leave the complementary coordinates fixed.

    def punctureCollapseLinear (F : GraphFrame 1 k) (c : ℂ) :
    Components 1 k →L[ℂ] Components 1 k :=
…

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

  13. theorem OAI.Kaplansky.ComplexGrassmann.punctureCollapseLinear_coordinates line 210
  14. theorem OAI.Kaplansky.ComplexGrassmann.continuous_punctureCollapseLinear line 215
  15. theorem OAI.Kaplansky.ComplexGrassmann.punctureCollapseLinear_injective line 222
  16. def OAI.Kaplansky.ComplexGrassmann.punctureCollapse line 232

    Source documentation

    Collapse within the punctured projective space, including at c=0.

    def punctureCollapse (F : GraphFrame 1 k) (c : ℂ)
    (P : ({graphPoint F 0}ᶜ : Set (Grassmann 1 k))) : Grassmann 1 k :=
…

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

  17. theorem OAI.Kaplansky.ComplexGrassmann.punctureCollapse_ne_center line 237
  18. theorem OAI.Kaplansky.ComplexGrassmann.continuous_punctureCollapse line 254
  19. theorem OAI.Kaplansky.ComplexGrassmann.punctureCollapse_one line 261
  20. theorem OAI.Kaplansky.ComplexGrassmann.punctureCollapse_zero_horizontal line 273

    Source documentation

    The endpoint lies entirely in the complementary projective hyperplane.

    theorem punctureCollapse_zero_horizontal (F : GraphFrame 1 k)
    (P : ({graphPoint F 0}ᶜ : Set (Grassmann 1 k)))
    (z : (punctureCollapse F 0 P).val) : (F z.val).1 = 0 := by
…

    Mentions: OAI.Kaplansky.ComplexGrassmann.GraphFrame, OAI.Kaplansky.ComplexGrassmann.graphPoint, OAI.Kaplansky.ComplexGrassmann.Grassmann, OAI.Kaplansky.ComplexGrassmann.punctureCollapse

  21. theorem OAI.Kaplansky.ComplexGrassmann.punctureCollapse_fixed line 281

    Source documentation

    Every point already in the complementary hyperplane stays fixed.

    theorem punctureCollapse_fixed (F : GraphFrame 1 k) (c : ℂ)
    (P : ({graphPoint F 0}ᶜ : Set (Grassmann 1 k)))
    (hP : ∀ z : P.val.val, (F z.val).1 = 0) : punctureCollapse F c P = P.val := by
…

    Mentions: OAI.Kaplansky.ComplexGrassmann.GraphFrame, OAI.Kaplansky.ComplexGrassmann.graphPoint, OAI.Kaplansky.ComplexGrassmann.Grassmann, OAI.Kaplansky.ComplexGrassmann.punctureCollapse

  22. abbrev OAI.Kaplansky.ComplexGrassmann.ProjectivePuncture line 308
  23. def OAI.Kaplansky.ComplexGrassmann.PunctureHyperplane line 312

    Source documentation

    The actual complementary projective hyperplane, as a subspace of the puncture.

    def PunctureHyperplane (F : GraphFrame 1 k) :=
…

    Mentions: OAI.Kaplansky.ComplexGrassmann.GraphFrame

  24. instance OAI.Kaplansky.ComplexGrassmann.(instance at line 315) line 315
  25. def OAI.Kaplansky.ComplexGrassmann.punctureHyperplaneInclusion line 319
  26. def OAI.Kaplansky.ComplexGrassmann.punctureHyperplaneRetraction line 322
  27. theorem OAI.Kaplansky.ComplexGrassmann.punctureHyperplaneRetraction_inclusion line 329
  28. def OAI.Kaplansky.ComplexGrassmann.punctureDeformation line 338

    Source documentation

    The deformation scales [a:v] to [(1-t)a:v]; it stays outside the removed point and fixes the entire complementary hyperplane.

    def punctureDeformation (F : GraphFrame 1 k) :
    (ContinuousMap.id (ProjectivePuncture F)).Homotopy
      ((punctureHyperplaneInclusion F).comp (punctureHyperplaneRetraction F)) where
…

    Mentions: OAI.Kaplansky.ComplexGrassmann.GraphFrame, OAI.Kaplansky.ComplexGrassmann.ProjectivePuncture, OAI.Kaplansky.ComplexGrassmann.punctureHyperplaneInclusion, OAI.Kaplansky.ComplexGrassmann.punctureHyperplaneRetraction

  29. theorem OAI.Kaplansky.ComplexGrassmann.punctureDeformation_fixes line 355
  30. def OAI.Kaplansky.ComplexGrassmann.punctureHyperplaneHomotopyEquiv line 363

    Source documentation

    A proved homotopy equivalence, not a deformation-retraction premise.

    def punctureHyperplaneHomotopyEquiv (F : GraphFrame 1 k) :
    ProjectivePuncture F ≃ₕ PunctureHyperplane F where
…

    Mentions: OAI.Kaplansky.ComplexGrassmann.GraphFrame, OAI.Kaplansky.ComplexGrassmann.ProjectivePuncture, OAI.Kaplansky.ComplexGrassmann.PunctureHyperplane

  31. def OAI.Kaplansky.ComplexGrassmann.verticalAmbientEquiv line 381
  32. def OAI.Kaplansky.ComplexGrassmann.hyperplaneEmbedLinear line 385
  33. def OAI.Kaplansky.ComplexGrassmann.hyperplaneProjectLinear line 391
  34. theorem OAI.Kaplansky.ComplexGrassmann.hyperplaneEmbedLinear_coordinates line 397
  35. theorem OAI.Kaplansky.ComplexGrassmann.hyperplaneProjectLinear_embed line 401
  36. theorem OAI.Kaplansky.ComplexGrassmann.hyperplaneEmbedLinear_project line 406
  37. theorem OAI.Kaplansky.ComplexGrassmann.hyperplaneEmbedLinear_injective line 414
  38. def OAI.Kaplansky.ComplexGrassmann.hyperplaneEmbedPoint line 418
  39. theorem OAI.Kaplansky.ComplexGrassmann.hyperplaneEmbedPoint_ne_center line 423
  40. theorem OAI.Kaplansky.ComplexGrassmann.hyperplaneEmbedPoint_horizontal line 436
  41. def OAI.Kaplansky.ComplexGrassmann.hyperplaneEmbed line 442
  42. theorem OAI.Kaplansky.ComplexGrassmann.hyperplaneProjectLinear_injective line 452
  43. def OAI.Kaplansky.ComplexGrassmann.hyperplaneProject line 459
  44. theorem OAI.Kaplansky.ComplexGrassmann.hyperplaneProject_embed line 466
  45. theorem OAI.Kaplansky.ComplexGrassmann.hyperplaneEmbed_project line 477
  46. def OAI.Kaplansky.ComplexGrassmann.projectiveHyperplaneHomeomorph line 495

    Source documentation

    The complementary hyperplane carries exactly the topology of CP^k.

    def projectiveHyperplaneHomeomorph (F : GraphFrame 1 (k+1)) :
    PunctureHyperplane F ≃ₜ Grassmann 1 k where
…

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

  47. def OAI.Kaplansky.ComplexGrassmann.projectivePunctureLowerHomotopyEquiv line 505

    Source documentation

    CP^(k+1) minus a chart center is homotopy equivalent to CP^k.

    def projectivePunctureLowerHomotopyEquiv (F : GraphFrame 1 (k+1)) :
    ProjectivePuncture F ≃ₕ Grassmann 1 k :=
…

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

  48. def OAI.Kaplansky.ComplexGrassmann.projectivePointPunctureLowerHomotopyEquiv line 510

    Source documentation

    The puncture retraction theorem holds at any actual projective point.

    def projectivePointPunctureLowerHomotopyEquiv (P : Grassmann 1 (k+1)) :
    ({P}ᶜ : Set (Grassmann 1 (k+1))) ≃ₕ Grassmann 1 k := by
…

    Mentions: OAI.Kaplansky.ComplexGrassmann.Grassmann