OAI/NumberTheory/PiExponent/Cohomology/ProjectiveMonomialCohomology.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponent.ProjectiveMonomialCohomology.differentialLinear line 12
2. def OAI.PiExponent.ProjectiveMonomialCohomology.regularCochains line 25
3. def OAI.PiExponent.ProjectiveMonomialCohomology.cycles line 41
4. theorem OAI.PiExponent.ProjectiveMonomialCohomology.degreeZero_coeff_eq line 44
5. theorem OAI.PiExponent.ProjectiveMonomialCohomology.degreeZero_nonnegative line 62
6. def OAI.PiExponent.ProjectiveMonomialCohomology.degreeZeroCoefficients line 79
7. theorem OAI.PiExponent.ProjectiveMonomialCohomology.degreeZeroCoefficients_injective line 86
8. instance OAI.PiExponent.ProjectiveMonomialCohomology.degreeZero_finite line 115
9. def OAI.PiExponent.ProjectiveMonomialCohomology.boundaryMap line 124
10. def OAI.PiExponent.ProjectiveMonomialCohomology.negativeCycles line 130
11. def OAI.PiExponent.ProjectiveMonomialCohomology.negativeCoefficients line 144
12. theorem OAI.PiExponent.ProjectiveMonomialCohomology.negativeCoefficients_injective line 151
13. instance OAI.PiExponent.ProjectiveMonomialCohomology.negativeCycles_finite line 162
14. theorem OAI.PiExponent.ProjectiveMonomialCohomology.exists_negative_representative line 166
15. theorem OAI.PiExponent.ProjectiveMonomialCohomology.finite_of_boundary_annihilating_surjective line 183