Theorem SheafOfModules.unitToPushforwardObjUnit_val_app_apply

Modification history

2026-03-06 08:34
Mathlib/Algebra/Category/ModuleCat/Sheaf/PullbackFree.lean
refactor(CategoryTheory/Sites): redefine the category of sheaves using `ObjectProperty.FullSubcategory` (#36081) …
Modified SheafOfModules.unitToPushforwardObjUnit_val_app_applyView on Github →
2025-11-08 15:24
Mathlib/Algebra/Category/ModuleCat/Sheaf/PullbackFree.lean
feat(Algebra/Category/ModuleCat/Sheaf): `O_S ⟶ f_* O_X` and `f^* O_S ≅ O_X` (#30398)
Added SheafOfModules.unitToPushforwardObjUnit_val_app_applyView on Github →