Main results

The main results that the formalization.yaml of FormalFrontier/sheaf-cohomology lists under status.main_results at commit 85cf087f, each that the scan finds declared in the file the yaml gives, with its line. They are listed here, not made articles: in several Formal Frontier libraries this list is close to the whole API. The notes are the yaml's.

The scan does not find 1 of them; the library's page names it.

Declaration	Kind	Where	Note
SheafCohomology.CompactOpenSections.preservesColimit_sections	theorem	SheafCohomology/CompactOpenSections.lean, line 783
TopCat.Sheaf.IsQuasiFlasque.subsingleton_H_succ	theorem	SheafCohomology/QuasiFlasqueAcyclicity.lean, line 260
SheafCohomology.HigherDirectImageFilteredColimit.rightDerivedPushforward_colimitPost_isIso	theorem	SheafCohomology/HigherDirectImageFilteredColimit.lean, line 332
AlgebraicGeometry.SheafedSpace.AbelianForget.preservesCofilteredLimit	theorem	SheafCohomology/AbelianForget/LimitPreservation.lean, line 103
AlgebraicGeometry.SheafedSpace.CommRingForget.preservesCofilteredLimit	theorem	SheafCohomology/CommRingForget/LimitPreservation.lean, line 112
AlgebraicGeometry.SheafedSpace.isIso_nativeCommRingGlobalSectionsComparison	theorem	SheafCohomology/NativeCommRingGlobalSections.lean, line 104
AlgebraicGeometry.SheafedSpace.NativeCylinderLimit.isIso_nativeCommRingCylinderSectionsComparison	theorem	SheafCohomology/NativeCommRingCylinderSections.lean, line 106
AlgebraicGeometry.SheafedSpace.NativeCylinderLimit.cylinderSectionsNaturality	def	SheafCohomology/NativeCylinderOpenNaturality.lean, line 331
AlgebraicGeometry.SheafedSpace.NativeCylinderLimit.cylinderSectionsComparison_betweenTail	theorem	SheafCohomology/NativeCylinderTailChange.lean, line 253

Quoted from the main results in formalization.yaml of FormalFrontier/sheaf-cohomology at commit 85cf087f, Apache-2.0.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.