OAI/NumberTheory/PiExponent/Cohomology/CechH1Transfer.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PiExponent.GeometrySupport.CechH1Transfer.schemeFreeOpen line 14
2. abbrev OAI.PiExponent.GeometrySupport.CechH1Transfer.schemeUnit line 17
3. def OAI.PiExponent.GeometrySupport.CechH1Transfer.freeOpenHomAddCommGroup line 20
4. def OAI.PiExponent.GeometrySupport.CechH1Transfer.higherCochainAddCommGroup line 25
5. structure OAI.PiExponent.GeometrySupport.CechH1Transfer.SectionComparison line 34
6. def OAI.PiExponent.GeometrySupport.CechH1Transfer.SectionComparison.cochainZero line 57
7. def OAI.PiExponent.GeometrySupport.CechH1Transfer.SectionComparison.cochainOne line 65
8. def OAI.PiExponent.GeometrySupport.CechH1Transfer.SectionComparison.cochainTwo line 71
9. theorem OAI.PiExponent.GeometrySupport.CechH1Transfer.SectionComparison.cochainOne_injective line 77
10. theorem OAI.PiExponent.GeometrySupport.CechH1Transfer.SectionComparison.map_differential_zero line 82
11. theorem OAI.PiExponent.GeometrySupport.CechH1Transfer.SectionComparison.map_differential_one line 94
12. theorem OAI.PiExponent.GeometrySupport.CechH1Transfer.SectionComparison.hasPrimitives line 108
13. theorem OAI.PiExponent.GeometrySupport.CechH1Transfer.SectionComparison.cohomology_one_zero line 119