OAI/Geometry/BundleTests/Smooth.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Smooth bases and test bundles with replacement maps.

  1. abbrev OAI.Kaplansky.SmoothTestBase line 16
  2. abbrev OAI.Kaplansky.SmoothTestModel line 17
  3. def OAI.Kaplansky.testFactorProjectiveHomeomorph line 19
  4. def OAI.Kaplansky.testBaseProjectiveHomeomorph line 26
  5. instance OAI.Kaplansky.(instance at line 29) line 29
  6. instance OAI.Kaplansky.(instance at line 30) line 30
  7. instance OAI.Kaplansky.(instance at line 31) line 31
  8. abbrev OAI.Kaplansky.SmoothPrefixBase line 33
  9. abbrev OAI.Kaplansky.SmoothPrefixModel line 35
  10. theorem OAI.Kaplansky.smoothPrefix_incidence_margin line 38
  11. abbrev OAI.Kaplansky.stageProjectiveDimensions line 56
  12. def OAI.Kaplansky.smoothTestBundleCore line 60

    Source documentation

    E_n on the first b projective factors, retaining the full-R K_i.

    def smoothTestBundleCore (m R b n : ℕ) (hb : b≤R) (hn : n≤b) :=
…
  13. abbrev OAI.Kaplansky.SmoothTestBundle line 64
  14. instance OAI.Kaplansky.smoothTestBundle_norm line 67
  15. instance OAI.Kaplansky.smoothTestBundle_inner line 70
  16. instance OAI.Kaplansky.smoothTestBundle_smooth line 73
  17. theorem OAI.Kaplansky.smoothTestBundle_finrank line 79
  18. def OAI.Kaplansky.smoothFreshCore line 87

    Source documentation

    The fresh block on Y_{j+1}, consisting of exactly a_{j+1,j+1} occurrences of the hyperplane line of its last factor.

    def smoothFreshCore (m R j : ℕ) (hj : j<R) :=
…
  19. def OAI.Kaplansky.testReplacementMultiplicity line 99
  20. def OAI.Kaplansky.testReplacementCore line 102
  21. abbrev OAI.Kaplansky.TestReplacementModel line 106
  22. theorem OAI.Kaplansky.exists_testBundle_replacements line 108
  23. def OAI.Kaplansky.smoothReplacementCore line 142
  24. theorem OAI.Kaplansky.exists_smoothTest_replacements line 147