OAI/Algebra/Cohomology/SemilinearCochains.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Degree exclusions, separated filtrations, kernel obstructions, and contraction of semilinear homogeneous cochains.

  1. theorem OAI.NamedPrimeFiveSupport.no_incoming_monomial line 9
  2. theorem OAI.NamedPrimeFiveSupport.incoming_congruence line 19
  3. theorem OAI.NamedPrimeFiveSupport.no_incoming_odd_degree line 23
  4. theorem OAI.NamedPrimeFiveSupport.filtration_zero_source_is_odd line 29
  5. theorem OAI.NamedPrimeFiveSupport.source_filtration_zero line 32
  6. theorem OAI.NamedPrimeFiveSupport.power_degrees line 37
  7. theorem OAI.NamedPrimeFiveSupport.tail_eq_bot line 46
  8. theorem OAI.NamedPrimeFiveSupport.later_eq_bot line 64
  9. theorem OAI.NamedPrimeFiveSupport.power_mem line 79
  10. theorem OAI.NamedPrimeFiveSupport.sixteenth_power_zero_of_filtration line 88
  11. theorem OAI.NamedPrimeFiveSupport.no_left_inverse line 106
  12. theorem OAI.NamedPrimeFiveSupport.kernel_from_factorization line 117
  13. theorem OAI.NamedPrimeFiveSupport.no_retraction_of_detected_kernel line 138
  14. abbrev OAI.SemilinearTraceSupport.Cochain line 160
  15. def OAI.SemilinearTraceSupport.delta line 162
  16. def OAI.SemilinearTraceSupport.Equivariant line 165
  17. def OAI.SemilinearTraceSupport.contract line 168
  18. lemma OAI.SemilinearTraceSupport.delta_cons line 172
  19. theorem OAI.SemilinearTraceSupport.delta_equivariant line 195
  20. theorem OAI.SemilinearTraceSupport.contract_equivariant line 205
  21. theorem OAI.SemilinearTraceSupport.contract_identity line 224
  22. theorem OAI.SemilinearTraceSupport.equivariant_cocycle_is_boundary line 241