Specialized results for sheaves of modules over topological spaces

noncomputable def TopologicalSpace.Opens.sheafOfModulesEquivOver {X : TopCat} (U : Opens ↑X) (R : TopCat.Sheaf RingCat X) : SheafOfModules (CategoryTheory.Sheaf.over R U) ≌ SheafOfModules (U.sheafRestrict.obj R)

Sheaves of modules over R.over U are equivalent to sheaves of modules over R |_ U.

Equations

• U.sheafOfModulesEquivOver R = SheafOfModules.pushforwardPushforwardEquivalence U.overEquivalence.symm (U.overPullbackSheafEquivOver.app R).inv (U.sheafRestrictSheafEquivOver.app R).inv ⋯ ⋯

noncomputable def TopologicalSpace.Opens.sheafOfModulesEquivOverUnit {X : TopCat} (U : Opens ↑X) (R : TopCat.Sheaf RingCat X) : (U.sheafOfModulesEquivOver R).functor.obj (SheafOfModules.unit (CategoryTheory.Sheaf.over R U)) ≅ SheafOfModules.unit (U.sheafRestrict.obj R)

sheafOfModulesEquivOver takes R.over U to R |_ U.

Equations

• U.sheafOfModulesEquivOverUnit R = CategoryTheory.Iso.refl ((U.sheafOfModulesEquivOver R).functor.obj (SheafOfModules.unit (CategoryTheory.Sheaf.over R U)))

noncomputable def TopologicalSpace.Opens.sheafOfModulesEquivOverInverseUnit {X : TopCat} (U : Opens ↑X) (R : TopCat.Sheaf RingCat X) : (U.sheafOfModulesEquivOver R).inverse.obj (SheafOfModules.unit (U.sheafRestrict.obj R)) ≅ SheafOfModules.unit (CategoryTheory.Sheaf.over R U)

sheafOfModulesEquivOver.inverse takes R |_ U to R.over U.

Equations

• One or more equations did not get rendered due to their size.