OAI/NumberTheory/PiExponent/Cohomology/FreeCechSections.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponent.GeometrySupport.FreeCechSections.canonicalTuple line 18
2. def OAI.PiExponent.GeometrySupport.FreeCechSections.tupleNatEquiv line 22
3. def OAI.PiExponent.GeometrySupport.FreeCechSections.freeTerm line 55
4. def OAI.PiExponent.GeometrySupport.FreeCechSections.sectionValuesEquiv line 59
5. def OAI.PiExponent.GeometrySupport.FreeCechSections.sectionsEquiv line 64
6. def OAI.PiExponent.GeometrySupport.FreeCechSections.tupleEmbedding line 68
7. def OAI.PiExponent.GeometrySupport.FreeCechSections.generator line 72
8. theorem OAI.PiExponent.GeometrySupport.FreeCechSections.sectionsEquiv_apply line 77
9. theorem OAI.PiExponent.GeometrySupport.FreeCechSections.tupleEmbedding_face line 96
10. def OAI.PiExponent.GeometrySupport.FreeCechSections.freeFace line 105
11. theorem OAI.PiExponent.GeometrySupport.FreeCechSections.generator_face line 109
12. def OAI.PiExponent.GeometrySupport.FreeCechSections.boundary line 120
13. theorem OAI.PiExponent.GeometrySupport.FreeCechSections.boundary_eq_sum line 124
14. theorem OAI.PiExponent.GeometrySupport.FreeCechSections.boundary_squared line 136
15. def OAI.PiExponent.GeometrySupport.FreeCechSections.termShortComplex line 142
16. theorem OAI.PiExponent.GeometrySupport.FreeCechSections.sectionsEquiv_boundary line 145
17. theorem OAI.PiExponent.GeometrySupport.FreeCechSections.hasPrimitives_of_exact line 154
18. theorem OAI.PiExponent.GeometrySupport.FreeCechSections.injective_hasPrimitives line 174
19. theorem OAI.PiExponent.GeometrySupport.FreeCechSections.ext_succ_eq_zero line 181
20. abbrev OAI.PiExponent.GeometrySupport.FreeCechSections.schemeFreeOpen line 191
21. theorem OAI.PiExponent.GeometrySupport.FreeCechSections.affine_ext_succ_eq_zero line 196