Commit 2026-01-22 10:30 e5a5da15

View on Github →

chore(AlgebraicGeometry): API for 𝒪ₓ-modules (#31854)

Estimated changes

Modified Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

added def ModuleCat.restrictScalarsCongr

added theorem ModuleCat.restrictScalarsCongr_hom_app

added theorem ModuleCat.restrictScalarsCongr_inv_app

added theorem ModuleCat.restrictScalarsCongr_symm

Modified Mathlib/Algebra/Category/ModuleCat/Presheaf/Colimits.lean

Modified Mathlib/Algebra/Category/ModuleCat/Presheaf/Limits.lean

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

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

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

added theorem SheafOfModules.pushforwardComp_hom_app_val_app

added theorem SheafOfModules.pushforwardComp_inv_app_val_app

added def SheafOfModules.pushforwardCongr

added theorem SheafOfModules.pushforwardCongr_hom_app_val_app

added theorem SheafOfModules.pushforwardCongr_inv_app_val_app

added theorem SheafOfModules.pushforwardCongr_symm

added def SheafOfModules.pushforwardNatTrans

added theorem SheafOfModules.pushforwardNatTrans_app_val_app

added theorem SheafOfModules.pushforwardNatTrans_app_val_app_apply

added theorem SheafOfModules.pushforwardNatTrans_comp

added theorem SheafOfModules.pushforwardNatTrans_id

added def SheafOfModules.pushforwardPushforwardAdj

added theorem SheafOfModules.pushforwardPushforwardAdj_counit_app_val_app

added theorem SheafOfModules.pushforwardPushforwardAdj_unit_app_val_app

Modified Mathlib/AlgebraicGeometry/Modules/Sheaf.lean

added theorem AlgebraicGeometry.Scheme.Modules.Hom.add_app

added def AlgebraicGeometry.Scheme.Modules.Hom.app

added theorem AlgebraicGeometry.Scheme.Modules.Hom.app_smul

added theorem AlgebraicGeometry.Scheme.Modules.Hom.comp_app

added theorem AlgebraicGeometry.Scheme.Modules.Hom.id_app

added theorem AlgebraicGeometry.Scheme.Modules.Hom.isIso_iff_isIso_app

added theorem AlgebraicGeometry.Scheme.Modules.Hom.sub_app

added theorem AlgebraicGeometry.Scheme.Modules.Hom.zero_app

added def AlgebraicGeometry.Scheme.Modules.fullyFaithfulToPresheafOfModules

added theorem AlgebraicGeometry.Scheme.Modules.germ_restrictStalkNatIso_hom_app

added theorem AlgebraicGeometry.Scheme.Modules.germ_restrictStalkNatIso_inv_app

added theorem AlgebraicGeometry.Scheme.Modules.hom_ext

added theorem AlgebraicGeometry.Scheme.Modules.inv_app

added theorem AlgebraicGeometry.Scheme.Modules.isSheaf

added theorem AlgebraicGeometry.Scheme.Modules.mapPresheaf_app

added theorem AlgebraicGeometry.Scheme.Modules.map_smul

added def AlgebraicGeometry.Scheme.Modules.pseudofunctor

added def AlgebraicGeometry.Scheme.Modules.pullback

added def AlgebraicGeometry.Scheme.Modules.pullbackComp

added def AlgebraicGeometry.Scheme.Modules.pullbackCongr

added def AlgebraicGeometry.Scheme.Modules.pullbackId

added def AlgebraicGeometry.Scheme.Modules.pullbackPushforwardAdjunction

added def AlgebraicGeometry.Scheme.Modules.pushforward

added def AlgebraicGeometry.Scheme.Modules.pushforwardComp

added theorem AlgebraicGeometry.Scheme.Modules.pushforwardComp_hom_app_app

added theorem AlgebraicGeometry.Scheme.Modules.pushforwardComp_inv_app_app

added def AlgebraicGeometry.Scheme.Modules.pushforwardCongr

added theorem AlgebraicGeometry.Scheme.Modules.pushforwardCongr_hom_app_app

added theorem AlgebraicGeometry.Scheme.Modules.pushforwardCongr_inv_app_app

added def AlgebraicGeometry.Scheme.Modules.pushforwardId

added theorem AlgebraicGeometry.Scheme.Modules.pushforwardId_hom_app_app

added theorem AlgebraicGeometry.Scheme.Modules.pushforwardId_inv_app_app

added theorem AlgebraicGeometry.Scheme.Modules.pushforward_map_app

added theorem AlgebraicGeometry.Scheme.Modules.pushforward_obj_obj

added theorem AlgebraicGeometry.Scheme.Modules.pushforward_obj_presheaf_map

added def AlgebraicGeometry.Scheme.Modules.restrictAdjunction

added theorem AlgebraicGeometry.Scheme.Modules.restrictAdjunction_counit_app_app

added theorem AlgebraicGeometry.Scheme.Modules.restrictAdjunction_unit_app_app

added def AlgebraicGeometry.Scheme.Modules.restrictFunctor

added def AlgebraicGeometry.Scheme.Modules.restrictFunctorAdjCounitIso

added def AlgebraicGeometry.Scheme.Modules.restrictFunctorComp

added theorem AlgebraicGeometry.Scheme.Modules.restrictFunctorComp_hom_app_app

added theorem AlgebraicGeometry.Scheme.Modules.restrictFunctorComp_inv_app_app

added def AlgebraicGeometry.Scheme.Modules.restrictFunctorCongr

added theorem AlgebraicGeometry.Scheme.Modules.restrictFunctorCongr_hom_app_app

added theorem AlgebraicGeometry.Scheme.Modules.restrictFunctorCongr_inv_app_app

added def AlgebraicGeometry.Scheme.Modules.restrictFunctorId

added theorem AlgebraicGeometry.Scheme.Modules.restrictFunctorId_hom_app_app

added theorem AlgebraicGeometry.Scheme.Modules.restrictFunctorId_inv_app_app

added def AlgebraicGeometry.Scheme.Modules.restrictFunctorIsoPullback

added def AlgebraicGeometry.Scheme.Modules.restrictStalkNatIso

added theorem AlgebraicGeometry.Scheme.Modules.restrict_map

added theorem AlgebraicGeometry.Scheme.Modules.restrict_obj

added def AlgebraicGeometry.Scheme.Modules.toPresheafOfModules

added theorem AlgebraicGeometry.Scheme.Modules.toPresheaf_map

added theorem AlgebraicGeometry.Scheme.Modules.toPresheaf_obj

Modified Mathlib/AlgebraicGeometry/OpenImmersion.lean

added theorem AlgebraicGeometry.Scheme.Hom.appIso_inv_app_presheafMap

added theorem AlgebraicGeometry.Scheme.Hom.comp_appIso

added theorem AlgebraicGeometry.Scheme.Hom.id_appIso