OAI/Geometry/HypersurfaceGerms/RelativeChains.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Relative singular chains and naturality of the oriented prism.

  1. abbrev OAI.AmbientMultiplicity.RelativeSingular.integralChains line 11
  2. def OAI.AmbientMultiplicity.RelativeSingular.inclusion line 17
  3. instance OAI.AmbientMultiplicity.RelativeSingular.inclusion_mono line 20
  4. abbrev OAI.AmbientMultiplicity.RelativeSingular.relativeChains line 24
  5. abbrev OAI.AmbientMultiplicity.RelativeSingular.RelativeHomology line 28
  6. def OAI.AmbientMultiplicity.RelativeSingular.pairSequence line 31
  7. lemma OAI.AmbientMultiplicity.RelativeSingular.pairSequence_shortExact line 35
  8. def OAI.AmbientMultiplicity.RelativeSingular.toRelativeHomology line 40
  9. def OAI.AmbientMultiplicity.RelativeSingular.boundary line 45
  10. lemma OAI.AmbientMultiplicity.RelativeSingular.boundary_comp_inclusion line 49
  11. lemma OAI.AmbientMultiplicity.RelativeSingular.relative_comp_boundary line 53
  12. lemma OAI.AmbientMultiplicity.RelativeSingular.exact_at_subspace line 59
  13. lemma OAI.AmbientMultiplicity.RelativeSingular.exact_at_space line 66
  14. lemma OAI.AmbientMultiplicity.RelativeSingular.exact_at_relative line 75
  15. def OAI.AmbientMultiplicity.RelativeSingular.relativeDegreeDesc line 81
  16. lemma OAI.AmbientMultiplicity.RelativeSingular.quotient_comp_relativeDegreeDesc line 89
  17. lemma OAI.AmbientMultiplicity.PrismNaturality.simplicial_components line 109
  18. lemma OAI.AmbientMultiplicity.PrismNaturality.simplicial_prism line 122
  19. lemma OAI.AmbientMultiplicity.PrismNaturality.topological_square line 150
  20. lemma OAI.AmbientMultiplicity.PrismNaturality.topological_prism line 159
  21. lemma OAI.AmbientMultiplicity.PrismNaturality.topological_prism_all line 171