OAI/NumberTheory/PiExponent/Cohomology/FreeCechResolution.lean
13 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.PiExponent.GeometrySupport.FreeCechResolution.tupleSimplexline 13 - def
OAI.PiExponent.GeometrySupport.FreeCechResolution.tupleAugmentedline 19 - def
OAI.PiExponent.GeometrySupport.FreeCechResolution.tupleExtraDegeneracyline 22 - def
OAI.PiExponent.GeometrySupport.FreeCechResolution.freeTupleComplexline 53 - theorem
OAI.PiExponent.GeometrySupport.FreeCechResolution.freeTupleComplex_exactline 56 - def
OAI.PiExponent.GeometrySupport.FreeCechResolution.coverVerticesline 73 - def
OAI.PiExponent.GeometrySupport.FreeCechResolution.tuplePresheafline 80 - def
OAI.PiExponent.GeometrySupport.FreeCechResolution.freePresheafComplexline 91 - theorem
OAI.PiExponent.GeometrySupport.FreeCechResolution.exact_of_objectwiseline 95 - theorem
OAI.PiExponent.GeometrySupport.FreeCechResolution.evaluation_freePresheafComplexline 104 - theorem
OAI.PiExponent.GeometrySupport.FreeCechResolution.freePresheafComplex_exactline 114 - def
OAI.PiExponent.GeometrySupport.FreeCechResolution.freeSheafComplexline 124 - theorem
OAI.PiExponent.GeometrySupport.FreeCechResolution.freeSheafComplex_exactline 130