OAI/Geometry/HypersurfaceGerms/Meridian.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

Meridian sweeps, split section pairs and their homology maps.

  1. def OAI.AmbientMultiplicity.InnerCircleSection.collapseProjection line 14
  2. def OAI.AmbientMultiplicity.InnerCircleSection.collapseSection line 19
  3. lemma OAI.AmbientMultiplicity.InnerCircleSection.projection_section line 23
  4. lemma OAI.AmbientMultiplicity.InnerCircleSection.section_isEmbedding line 26
  5. lemma OAI.AmbientMultiplicity.InnerCircleSection.homology_projection_section line 31
  6. def OAI.AmbientMultiplicity.InnerCircleSection.homologyProjection line 40
  7. def OAI.AmbientMultiplicity.InnerCircleSection.homologySection line 43
  8. lemma OAI.AmbientMultiplicity.InnerCircleSection.homology_projection_section_apply line 46
  9. def OAI.AmbientMultiplicity.InnerCircleSection.sectionHomologyAddSplitting line 53
  10. def OAI.AmbientMultiplicity.InnerCircleSection.sectionHomologySplitting line 81
  11. def OAI.AmbientMultiplicity.InnerCircleSection.sectionSetoid line 87
  12. abbrev OAI.AmbientMultiplicity.InnerCircleSection.SectionQuotient line 101
  13. def OAI.AmbientMultiplicity.InnerCircleSection.meridianSet line 104
  14. abbrev OAI.AmbientMultiplicity.InnerCircleSection.RelativeCircleQuotient line 107
  15. lemma OAI.AmbientMultiplicity.InnerCircleSection.mk_mem_section_iff line 109
  16. def OAI.AmbientMultiplicity.InnerCircleSection.toRelative line 124
  17. lemma OAI.AmbientMultiplicity.InnerCircleSection.continuous_toRelative line 132
  18. lemma OAI.AmbientMultiplicity.InnerCircleSection.toRelative_section_eq line 135
  19. def OAI.AmbientMultiplicity.InnerCircleSection.sectionQuotientToRelative line 141
  20. lemma OAI.AmbientMultiplicity.InnerCircleSection.continuous_sectionQuotientToRelative line 148
  21. def OAI.AmbientMultiplicity.InnerCircleSection.relativeToSectionQuotient line 152
  22. lemma OAI.AmbientMultiplicity.InnerCircleSection.continuous_relativeToSectionQuotient line 161
  23. def OAI.AmbientMultiplicity.InnerCircleSection.sectionQuotientHomeomorph line 170
  24. def OAI.AmbientMultiplicity.SourceInnerPage.rootSet line 196
  25. abbrev OAI.AmbientMultiplicity.SourceInnerPage.RootRelativeHomology line 200
  26. def OAI.AmbientMultiplicity.SourceInnerPage.rootBoundary line 205
  27. def OAI.AmbientMultiplicity.SourceInnerPage.rootPushforward line 211
  28. lemma OAI.AmbientMultiplicity.SourceInnerPage.root_inclusion_projection line 216
  29. lemma OAI.AmbientMultiplicity.SourceInnerPage.root_projection_kernel line 231
  30. lemma OAI.AmbientMultiplicity.SourceInnerPage.rootBoundary_range_eq_kernel line 249
  31. def OAI.AmbientMultiplicity.InnerCircleSection.meridianHomotopy line 267
  32. lemma OAI.AmbientMultiplicity.InnerCircleSection.meridianHomotopy_on_root line 279
  33. lemma OAI.AmbientMultiplicity.InnerCircleSection.meridianHomotopy_over_base line 284
  34. def OAI.AmbientMultiplicity.InnerCircleSection.meridianChainHomotopy line 289
  35. def OAI.AmbientMultiplicity.InnerCircleSection.meridianPrism line 296
  36. lemma OAI.AmbientMultiplicity.InnerCircleSection.meridianPrism_dNext_prevD line 301
  37. def OAI.AmbientMultiplicity.InnerCircleSection.zeroSet line 313
  38. def OAI.AmbientMultiplicity.InnerCircleSection.rootToSection line 316
  39. lemma OAI.AmbientMultiplicity.InnerCircleSection.root_meridian_square line 320
  40. lemma OAI.AmbientMultiplicity.InnerCircleSection.meridianPrism_root_zero line 330
  41. def OAI.AmbientMultiplicity.InnerCircleSection.relativeMeridianPrism line 361
  42. lemma OAI.AmbientMultiplicity.InnerCircleSection.quotient_comp_relativeMeridianPrism line 371
  43. lemma OAI.AmbientMultiplicity.InnerCircleSection.relativeMeridianPrism_dNext_prevD line 380
  44. lemma OAI.AmbientMultiplicity.InnerCircleSection.relativeMeridianPrism_shape line 395
  45. lemma OAI.AmbientMultiplicity.InnerCircleSection.relativeMeridianPrism_boundary line 403
  46. def OAI.AmbientMultiplicity.InnerCircleSection.meridianShortComplexMap line 414
  47. def OAI.AmbientMultiplicity.InnerCircleSection.relativeMeridianHomology line 435
  48. def OAI.AmbientMultiplicity.InnerCircleSection.sectionRangeRetraction line 453
  49. lemma OAI.AmbientMultiplicity.InnerCircleSection.inclusion_sectionRangeRetraction line 460
  50. def OAI.AmbientMultiplicity.InnerCircleSection.sectionPairChainSplitting line 471
  51. def OAI.AmbientMultiplicity.InnerCircleSection.sectionRelativeLift line 484
  52. lemma OAI.AmbientMultiplicity.InnerCircleSection.sectionRelativeLift_toRelative line 489
  53. def OAI.AmbientMultiplicity.InnerCircleSection.meridianHomology line 502
  54. lemma OAI.AmbientMultiplicity.InnerCircleSection.meridianHomology_toRelative line 506
  55. def OAI.AmbientMultiplicity.InnerCircleSection.sectionBaseProjection line 518
  56. lemma OAI.AmbientMultiplicity.InnerCircleSection.sectionRetraction_base line 522
  57. lemma OAI.AmbientMultiplicity.InnerCircleSection.sectionRelativeLift_projection line 528
  58. lemma OAI.AmbientMultiplicity.InnerCircleSection.meridianHomology_projection line 544
  59. def OAI.AmbientMultiplicity.InnerCircleSection.meridianKernelAddHom line 556
  60. def OAI.AmbientMultiplicity.InnerCircleSection.meridianKernelHomology line 566