OAI/Geometry/BundleTests/Twisted.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

Twisted hyperplane bundles, zeros, graph coordinates, and frame sections.

  1. def OAI.Kaplansky.twistedProjectiveDimensions line 19

    Source documentation

    The auxiliary factor for the stable obstruction has dimension h.

    def twistedProjectiveDimensions : Option ι → ℕ
  | none => h
  | some i => K i
  2. abbrev OAI.Kaplansky.TwistedHyperplaneSlot line 23
  3. def OAI.Kaplansky.twistedOldLabel line 25
  4. def OAI.Kaplansky.twistedHyperplaneLineCore line 31

    Source documentation

    The summands of (trivial(h) ⊕ H) tensored with the hyperplane line from the auxiliary factor. This is an explicit vector-bundle core.

    def twistedHyperplaneLineCore (s : TwistedHyperplaneSlot K h) :=
…

    Mentions: OAI.Kaplansky.TwistedHyperplaneSlot

  5. def OAI.Kaplansky.twistedHyperplaneSumCore line 36
  6. theorem OAI.Kaplansky.twistedHyperplaneSum_finrank line 38
  7. theorem OAI.Kaplansky.twistedHyperplaneLines_unitary line 43
  8. def OAI.Kaplansky.twistedCoordinateSection line 48
  9. theorem OAI.Kaplansky.continuous_twistedCoordinateSection line 56
  10. def OAI.Kaplansky.twistedOldSection line 66
  11. def OAI.Kaplansky.twistedNewSection line 73
  12. theorem OAI.Kaplansky.continuous_twistedOldSection line 81
  13. theorem OAI.Kaplansky.continuous_twistedNewSection line 92
  14. def OAI.Kaplansky.twistedHyperplaneSection line 99

    Source documentation

    A concrete section: auxiliary positive coordinates on the h trivial summands, and old positive coordinates multiplied by auxiliary coordinate 0 on the other summands. Its topological nonvanishing remains to be proved.

    def twistedHyperplaneSection (P : ProjectiveProduct (twistedProjectiveDimensions K h)) :
    (twistedHyperplaneSumCore K h).Fiber P :=
…

    Mentions: OAI.Kaplansky.twistedProjectiveDimensions, OAI.Kaplansky.twistedHyperplaneSumCore

  15. theorem OAI.Kaplansky.continuous_twistedHyperplaneSection line 103
  16. theorem OAI.Kaplansky.hyperplaneFirstCoordinateSection_ne_zero line 115
  17. theorem OAI.Kaplansky.twistedCoordinateSection_positive_zero_iff line 129
  18. theorem OAI.Kaplansky.twistedHyperplaneSection_eq_zero_iff line 147

    Source documentation

    The explicit twisted section has exactly one zero on the actual augmented projective product. This is geometry, not a nonzero Euler map.

    theorem twistedHyperplaneSection_eq_zero_iff
    (P : ProjectiveProduct (twistedProjectiveDimensions K h)) :
    twistedHyperplaneSection K h P = 0 ↔
      P = firstCoordinateProduct (twistedProjectiveDimensions K h) := by
…

    Mentions: OAI.Kaplansky.twistedProjectiveDimensions, OAI.Kaplansky.twistedHyperplaneSection, OAI.Kaplansky.firstCoordinateProduct

  19. def OAI.Kaplansky.productGraphLineProjection line 218
  20. def OAI.Kaplansky.productGraphLineVector line 223
  21. theorem OAI.Kaplansky.productGraphLineVector_mem line 227
  22. theorem OAI.Kaplansky.productGraphLineVector_ne_zero line 240
  23. theorem OAI.Kaplansky.continuous_productGraphLineVector line 244
  24. def OAI.Kaplansky.productGraphLineEvaluation line 252
  25. def OAI.Kaplansky.productGraphLineUnit line 259

    Source documentation

    The graph evaluation unit also covers zero-dimensional factors.

    def productGraphLineUnit (i : Option ι) (a : A) :
    (pullbackLineCore (productLineCore K i) (chartBaseMap U e)).Fiber a :=
…

    Mentions: OAI.Kaplansky.pullbackLineCore, OAI.Kaplansky.chartBaseMap

  26. theorem OAI.Kaplansky.productGraphLineUnit_ne_zero line 265
  27. theorem OAI.Kaplansky.continuous_productGraphLineUnit line 271
  28. instance OAI.Kaplansky.twistedHyperplaneFiberNormedAddCommGroup line 298
  29. instance OAI.Kaplansky.twistedHyperplaneFiberInnerProductSpace line 303
  30. abbrev OAI.Kaplansky.twistedGraphBundleDomain line 308
  31. def OAI.Kaplansky.twistedGraphLineUnit line 312
  32. theorem OAI.Kaplansky.twistedGraphLineUnit_ne_zero line 320
  33. theorem OAI.Kaplansky.continuous_twistedGraphLineUnit line 325
  34. def OAI.Kaplansky.twistedGraphBundleCoordinates line 332

    Source documentation

    Genuine linear coordinates for the original twisted bundle, over any subset of any product graph chart.

    def twistedGraphBundleCoordinates : twistedGraphBundleDomain K h U ≃ₜ
    A × (TwistedHyperplaneSlot K h → ℂ) :=
…

    Mentions: OAI.Kaplansky.twistedGraphBundleDomain, OAI.Kaplansky.TwistedHyperplaneSlot

  35. theorem OAI.Kaplansky.twistedGraphBundleCoordinates_base line 340
  36. theorem OAI.Kaplansky.twistedGraphBundleCoordinates_zero_iff line 343
  37. def OAI.Kaplansky.twistedGraphBundleRelativeIso line 348
  38. def OAI.Kaplansky.twistedGraphBundleNormalization line 354
  39. theorem OAI.Kaplansky.div_linearEquiv_inverse_one line 367
  40. def OAI.Kaplansky.twistedSlotEquiv line 377
  41. def OAI.Kaplansky.twistedSlopeEvaluationEquiv line 388
  42. def OAI.Kaplansky.twistedStandardFrames line 393
  43. abbrev OAI.Kaplansky.twistedStandardChart line 395
  44. abbrev OAI.Kaplansky.twistedStandardChartHomeomorph line 396
  45. def OAI.Kaplansky.twistedStandardLineUnit line 398
  46. def OAI.Kaplansky.twistedStandardSectionCoordinates line 404

    Source documentation

    Actual section coordinates in the proved tensor graph trivialization.

    def twistedStandardSectionCoordinates
    (A : ProjectiveProductModel (twistedProjectiveDimensions K h)) : TwistedHyperplaneSlot K h → ℂ :=
…

    Mentions: OAI.Kaplansky.twistedProjectiveDimensions, OAI.Kaplansky.TwistedHyperplaneSlot

  47. theorem OAI.Kaplansky.twistedStandard_coordinate_evaluation line 410
  48. theorem OAI.Kaplansky.twistedStandardSectionCoordinates_eq line 434
  49. theorem OAI.Kaplansky.twistedStandardSection_regular_zero line 473
  50. def OAI.Kaplansky.twistedSourceLabel line 492
  51. def OAI.Kaplansky.twistedSourceStage line 496
  52. def OAI.Kaplansky.twistedOldBase line 499
  53. theorem OAI.Kaplansky.continuous_twistedOldComponent line 502
  54. def OAI.Kaplansky.twistedSectionFromVector line 522

    Source documentation

    Tensor an arbitrary old section with a homogeneous auxiliary coordinate, preserving the original bundle topologies.

    def twistedSectionFromVector (v : ∀ y, (twistedSourceStage K h).Fiber y)
    (j : Fin (1+h)) (P : ProjectiveProduct (twistedProjectiveDimensions K h)) :
    (twistedHyperplaneSumCore K h).Fiber P :=
…

    Mentions: OAI.Kaplansky.twistedSourceStage, OAI.Kaplansky.twistedProjectiveDimensions, OAI.Kaplansky.twistedHyperplaneSumCore

  55. theorem OAI.Kaplansky.continuous_twistedSectionFromVector line 530
  56. theorem OAI.Kaplansky.twistedCoordinateSections_not_all_zero line 542
  57. def OAI.Kaplansky.twistedFrameSection line 559
  58. theorem OAI.Kaplansky.continuous_twistedFrameSection line 565
  59. theorem OAI.Kaplansky.twistedFrameSection_ne_zero line 574