OAI/Geometry/BundleTests/Base.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

The compact bundle-test base, prefix dimensions, and retained multiplicities.

  1. def OAI.Kaplansky.testProjectiveDimension line 14
  2. theorem OAI.Kaplansky.testProjectiveDimension_pos line 17
  3. def OAI.Kaplansky.coordinateLineProjection line 27

    Source documentation

    A concrete basepoint in every projective factor.

    def coordinateLineProjection (k : ℕ) : projectionSpace (k+1) 1 := by
…

    Mentions: OAI.Kaplansky.projectionSpace

  4. abbrev OAI.Kaplansky.BundleTestBase line 39
  5. instance OAI.Kaplansky.(instance at line 42) line 42
  6. def OAI.Kaplansky.bundleTestBasePoint line 44
  7. instance OAI.Kaplansky.(instance at line 47) line 47
  8. def OAI.Kaplansky.bundleTestProjection line 49
  9. abbrev OAI.Kaplansky.TestTautologicalLine line 53
  10. instance OAI.Kaplansky.(instance at line 56) line 56
  11. instance OAI.Kaplansky.(instance at line 57) line 57
  12. theorem OAI.Kaplansky.testTautologicalLine_finrank line 59
  13. abbrev OAI.Kaplansky.TestHyperplaneLine line 65

    Source documentation

    The actual dual hyperplane-line candidate on the projection product.

    abbrev TestHyperplaneLine (m R : ℕ) (i : Fin R) :=
…
  14. instance OAI.Kaplansky.(instance at line 68) line 68
  15. instance OAI.Kaplansky.(instance at line 69) line 69
  16. theorem OAI.Kaplansky.testHyperplaneLine_finrank line 71
  17. theorem OAI.Kaplansky.three_sum_pow_four line 83
  18. theorem OAI.Kaplansky.testProjectiveDimension_bound line 91
  19. def OAI.Kaplansky.testPrefixDimension line 102

    Source documentation

    Exact prefix dimensions, retaining every later occurrence through R.

    def testPrefixDimension (m R j : ℕ) (hj : j<R) : ℕ :=
…
  20. theorem OAI.Kaplansky.testPrefixDimension_margin line 105
  21. def OAI.Kaplansky.retainedHyperplaneMultiplicity line 124

    Source documentation

    Count all copies of L_(i+1) in m copies of E_0⊕...⊕E_R. The stages are enumerated in descending order.

    def retainedHyperplaneMultiplicity (m R : ℕ) (i : Fin R) : ℕ :=
…
  22. theorem OAI.Kaplansky.retainedHyperplaneMultiplicity_eq line 127
  23. def OAI.Kaplansky.retainedTrivialMultiplicity line 150

    Source documentation

    The exact rank of the retained trivial block, in descending stage order.

    def retainedTrivialMultiplicity (m R : ℕ) : ℕ :=
…
  24. theorem OAI.Kaplansky.retainedTrivialMultiplicity_eq line 153
  25. theorem OAI.Kaplansky.retainedTrivialMultiplicity_bound line 165