Commit 2025-11-08 15:24 c5fdf193

View on Github →

feat(Algebra/Category/ModuleCat/Sheaf): O_S ⟶ f_* O_X and f^* O_S ≅ O_X (#30398)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Category/ModuleCat/Sheaf/Free.lean

added theorem SheafOfModules.freeCofan_inj

added theorem SheafOfModules.unitHomEquiv_symm_freeHomEquiv_apply

added theorem SheafOfModules.ιFree_freeMap

Modified Mathlib/Algebra/Category/ModuleCat/Sheaf/PullbackContinuous.lean

Created Mathlib/Algebra/Category/ModuleCat/Sheaf/PullbackFree.lean

added theorem SheafOfModules.bijective_pushforwardSections

added theorem SheafOfModules.pullbackObjFreeIso_hom_naturality

added theorem SheafOfModules.pullbackPushforwardAdjunction_homEquiv_pullbackObjUnitToUnit

added theorem SheafOfModules.pullbackPushforwardAdjunction_homEquiv_symm_unitToPushforwardObjUnit

added theorem SheafOfModules.pullback_map_ιFree_comp_pullbackObjFreeIso_hom

added def SheafOfModules.pushforwardSections

added theorem SheafOfModules.pushforwardSections_unitHomEquiv

added def SheafOfModules.unitToPushforwardObjUnit

added theorem SheafOfModules.unitToPushforwardObjUnit_val_app_apply

Modified Mathlib/CategoryTheory/Limits/Preserves/Shapes/Products.lean

added theorem CategoryTheory.Limits.inv_piComparison_comp_map_π

added theorem CategoryTheory.Limits.map_ι_comp_inv_sigmaComparison