OAI/Algebra/FrobeniusObstruction/SquareZero.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BoundaryOnly.FormalObstruction.SquareZero.Cycles line 13
  2. def OAI.BoundaryOnly.FormalObstruction.SquareZero.boundaryMap line 15
  3. def OAI.BoundaryOnly.FormalObstruction.SquareZero.boundaries line 18
  4. abbrev OAI.BoundaryOnly.FormalObstruction.SquareZero.Cohomology line 20
  5. def OAI.BoundaryOnly.FormalObstruction.SquareZero.classMap line 22
  6. theorem OAI.BoundaryOnly.FormalObstruction.SquareZero.class_boundary line 24
  7. theorem OAI.BoundaryOnly.FormalObstruction.SquareZero.class_eq_zero line 29
  8. theorem OAI.BoundaryOnly.FormalObstruction.SquareZero.classMap_surjective line 38
  9. def OAI.BoundaryOnly.FormalObstruction.SquareZero.cycleMap line 43
  10. theorem OAI.BoundaryOnly.FormalObstruction.SquareZero.cycleMap_val line 49
  11. def OAI.BoundaryOnly.FormalObstruction.SquareZero.induced line 52
  12. theorem OAI.BoundaryOnly.FormalObstruction.SquareZero.induced_class line 59
  13. theorem OAI.BoundaryOnly.FormalObstruction.SquareZero.induced_ext line 66
  14. theorem OAI.BoundaryOnly.FormalObstruction.SquareZero.induced_square_zero line 73
  15. def OAI.BoundaryOnly.FormalObstruction.SquareZero.oddInduced line 84
  16. theorem OAI.BoundaryOnly.FormalObstruction.SquareZero.oddInduced_class line 90
  17. theorem OAI.BoundaryOnly.FormalObstruction.SquareZero.oddInduced_square_zero line 95
  18. def OAI.BoundaryOnly.FormalObstruction.SquareZero.evenInduced line 101
  19. theorem OAI.BoundaryOnly.FormalObstruction.SquareZero.evenInduced_class line 105
  20. theorem OAI.BoundaryOnly.FormalObstruction.SquareZero.correction_of_kernel line 112
  21. theorem OAI.BoundaryOnly.FormalObstruction.SquareZero.generalized_inverse line 138
  22. theorem OAI.BoundaryOnly.FormalObstruction.SquareZero.cohomology_contraction line 150
  23. theorem OAI.BoundaryOnly.FormalObstruction.SquareZero.odd_generalized_inverse line 215
  24. theorem OAI.BoundaryOnly.FormalObstruction.SquareZero.odd_homotopy line 238
  25. theorem OAI.BoundaryOnly.FormalObstruction.SquareZero.equivariant_section line 277
  26. theorem OAI.BoundaryOnly.FormalObstruction.SquareZero.parity_cohomology_contraction line 299