Sheaf

📁 Source: Mathlib/AlgebraicGeometry/Modules/Sheaf.lean

Statistics

Metric	Count
Definitions Modules, app, mapPresheaf, fullyFaithfulToPresheafOfModules, instAbelian, instCategory, instModuleCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensCarrierAbPresheaf, presheaf, pseudofunctor, pullback, pullbackComp, pullbackCongr, pullbackId, pullbackPushforwardAdjunction, pushforward, pushforwardComp, pushforwardCongr, pushforwardId, restrict, restrictAdjunction, restrictFunctor, restrictFunctorAdjCounitIso, restrictFunctorComp, restrictFunctorCongr, restrictFunctorId, restrictFunctorIsoPullback, restrictStalkNatIso, toPresheaf, toPresheafOfModules, «termΓ(_,_)_1»_1»)	30
Theorems add_app, app_smul, comp_app, id_app, isIso_iff_isIso_app, sub_app, zero_app, conjugateEquiv_pullbackComp_inv, conjugateEquiv_pullbackId_hom, germ_restrictStalkNatIso_hom_app, germ_restrictStalkNatIso_inv_app, hom_ext, hom_ext_iff, instAdditivePullback, instAdditivePushforward, instFaithfulPresheafAbCarrierCommRingCatToPresheaf, instFaithfulPresheafOfModulesToPresheafOfModules, instFaithfulPushforward, instFullPresheafOfModulesToPresheafOfModules, instFullPushforward, instHasColimits, instHasLimits, instIsIsoAbApp, instIsIsoFunctorCounitRestrictAdjunction, instIsLeftAdjointPullback, instIsLeftAdjointRestrictFunctor, instIsRightAdjointPresheafOfModulesToPresheafOfModules, instIsRightAdjointPushforward, instPreservesLimitsPresheafAbCarrierCommRingCatToPresheaf, instReflectsIsomorphismsPresheafAbCarrierCommRingCatToPresheaf, inv_app, isSheaf, mapPresheaf_app, map_smul, pseudofunctor_associativity, pseudofunctor_associativity_assoc, pseudofunctor_left_unitality, pseudofunctor_left_unitality_assoc, pseudofunctor_mapComp_hom_τl, pseudofunctor_mapComp_hom_τr, pseudofunctor_mapComp_inv_τl, pseudofunctor_mapComp_inv_τr, pseudofunctor_mapId_hom_τl, pseudofunctor_mapId_hom_τr, pseudofunctor_mapId_inv_τl, pseudofunctor_mapId_inv_τr, pseudofunctor_map_adj, pseudofunctor_map_l, pseudofunctor_map_r, pseudofunctor_obj_obj, pseudofunctor_right_unitality, pseudofunctor_right_unitality_assoc, pushforwardComp_hom_app_app, pushforwardComp_inv_app_app, pushforwardCongr_hom_app_app, pushforwardCongr_inv_app_app, pushforwardId_hom_app_app, pushforwardId_inv_app_app, pushforward_map_app, pushforward_obj_obj, pushforward_obj_presheaf_map, restrictAdjunction_counit_app_app, restrictAdjunction_unit_app_app, restrictFunctorComp_hom_app_app, restrictFunctorComp_inv_app_app, restrictFunctorCongr_hom_app_app, restrictFunctorCongr_inv_app_app, restrictFunctorId_hom_app_app, restrictFunctorId_inv_app_app, restrict_map, restrict_obj, toPresheaf_map, toPresheaf_obj	73
Total	103

AlgebraicGeometry

Definitions

Name	Category	Theorems
«termΓ(_,_)_1» 📖_1» "API Documentation")	CompOp	—

AlgebraicGeometry.Scheme

Definitions

Name	Category	Theorems
Modules 📖	CompOp	93 math math: Modules.pushforward_obj_presheaf_map, Modules.pseudofunctor_map_adj, Modules.pushforwardId_inv_app_app, Modules.instFaithfulPresheafOfModulesToPresheafOfModules, Modules.restrictAdjunction_counit_app_app, Modules.pushforwardCongr_hom_app_app, Modules.pushforward_obj_obj, Modules.instPreservesLimitsPresheafAbCarrierCommRingCatToPresheaf, Modules.instAdditivePullback, Modules.germ_restrictStalkNatIso_inv_app, AlgebraicGeometry.instIsLeftAdjointModuleCatCarrierModulesSpecOfFunctor, AlgebraicGeometry.tilde.map_id, Modules.Hom.zero_app, AlgebraicGeometry.tilde.map_sub, Modules.pseudofunctor_map_l, Modules.toOpen_fromTildeΓ_app, Modules.pseudofunctor_right_unitality_assoc, Modules.instIsIsoFunctorCounitRestrictAdjunction, Modules.pushforwardComp_inv_app_app, AlgebraicGeometry.instAdditiveModuleCatCarrierModulesSpecOfFunctor, Modules.instHasLimits, Modules.germ_restrictStalkNatIso_hom_app, AlgebraicGeometry.instFullModuleCatCarrierModulesSpecOfFunctor, Modules.toPresheaf_obj, Modules.instFaithfulPresheafAbCarrierCommRingCatToPresheaf, Modules.instIsLeftAdjointPullback, Modules.instFullPushforward, AlgebraicGeometry.tilde.isoTop_hom, ModuleCat.Tilde.toOpen_res, Modules.restrictFunctorComp_hom_app_app, Modules.restrictFunctorComp_inv_app_app, AlgebraicGeometry.tilde.functor_map, Modules.toPresheaf_map, Modules.restrictFunctorCongr_inv_app_app, Modules.pseudofunctor_right_unitality, Modules.pseudofunctor_mapComp_hom_τl, AlgebraicGeometry.tilde.map_comp_assoc, Modules.toOpen_fromTildeΓ_app_assoc, Modules.instFaithfulPushforward, AlgebraicGeometry.tilde.isIso_toOpen_top, Modules.restrictFunctorCongr_hom_app_app, Modules.pseudofunctor_mapComp_hom_τr, Modules.restrictFunctorId_inv_app_app, Modules.pushforwardComp_hom_app_app, Modules.Hom.id_app, Modules.Hom.isIso_iff_isIso_app, Modules.Hom.comp_app, Modules.pseudofunctor_mapId_hom_τr, Modules.pseudofunctor_obj_obj, Modules.Hom.sub_app, Modules.instHasColimits, Modules.pushforwardId_hom_app_app, Modules.restrictAdjunction_unit_app_app, Modules.Hom.add_app, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓUnitOpensCarrierCarrierCommRingCatRingCatSheaf, AlgebraicGeometry.instFaithfulModuleCatCarrierModulesSpecOfFunctor, AlgebraicGeometry.tilde.map_add, AlgebraicGeometry.tilde.toOpen_res, AlgebraicGeometry.tilde.toOpen_res_assoc, AlgebraicGeometry.tilde.isUnit_algebraMap_end_basicOpen, Modules.conjugateEquiv_pullbackId_hom, Modules.instIsLeftAdjointRestrictFunctor, Modules.conjugateEquiv_pullbackComp_inv, Modules.pseudofunctor_left_unitality, Modules.pseudofunctor_associativity_assoc, Modules.instFullPresheafOfModulesToPresheafOfModules, Modules.pseudofunctor_mapComp_inv_τl, AlgebraicGeometry.tilde.map_zero, Modules.pseudofunctor_left_unitality_assoc, Modules.pseudofunctor_mapId_hom_τl, AlgebraicGeometry.tilde.functor_obj, AlgebraicGeometry.tilde.toOpen_map_app_assoc, Modules.pushforwardCongr_inv_app_app, AlgebraicGeometry.tilde.map_comp, Modules.instReflectsIsomorphismsPresheafAbCarrierCommRingCatToPresheaf, Modules.instIsRightAdjointPushforward, Modules.pseudofunctor_map_r, AlgebraicGeometry.instIsIsoFunctorModuleCatCarrierUnitModulesSpecOfAdjunction, AlgebraicGeometry.tilde.map_neg, Modules.instIsRightAdjointPresheafOfModulesToPresheafOfModules, Modules.restrictFunctorId_hom_app_app, Modules.pseudofunctor_mapComp_inv_τr, AlgebraicGeometry.isIso_fromTildeΓ_iff, AlgebraicGeometry.tilde.map_id_assoc, Modules.pushforward_map_app, Modules.inv_app, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓFreeOpensCarrierCarrierCommRingCat, Modules.pseudofunctor_mapId_inv_τl, Modules.pseudofunctor_associativity, Modules.instAdditivePushforward, Modules.pseudofunctor_mapId_inv_τr, AlgebraicGeometry.tilde.instIsLocalizedModuleCarrierCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecModuleCatPresheafModulesSheafModulesSpecToSheafOpBasicOpenPowersHomToOpen, AlgebraicGeometry.tilde.toOpen_map_app

AlgebraicGeometry.Scheme.Modules

Definitions

Name	Category	Theorems
fullyFaithfulToPresheafOfModules 📖	CompOp	—
instAbelian 📖	CompOp	10 math math: instAdditivePullback, Hom.zero_app, AlgebraicGeometry.tilde.map_sub, AlgebraicGeometry.instAdditiveModuleCatCarrierModulesSpecOfFunctor, Hom.sub_app, Hom.add_app, AlgebraicGeometry.tilde.map_add, AlgebraicGeometry.tilde.map_zero, AlgebraicGeometry.tilde.map_neg, instAdditivePushforward
instCategory 📖	CompOp	93 math math: pushforward_obj_presheaf_map, pseudofunctor_map_adj, pushforwardId_inv_app_app, instFaithfulPresheafOfModulesToPresheafOfModules, restrictAdjunction_counit_app_app, pushforwardCongr_hom_app_app, pushforward_obj_obj, instPreservesLimitsPresheafAbCarrierCommRingCatToPresheaf, instAdditivePullback, germ_restrictStalkNatIso_inv_app, AlgebraicGeometry.instIsLeftAdjointModuleCatCarrierModulesSpecOfFunctor, AlgebraicGeometry.tilde.map_id, Hom.zero_app, AlgebraicGeometry.tilde.map_sub, pseudofunctor_map_l, toOpen_fromTildeΓ_app, pseudofunctor_right_unitality_assoc, instIsIsoFunctorCounitRestrictAdjunction, pushforwardComp_inv_app_app, AlgebraicGeometry.instAdditiveModuleCatCarrierModulesSpecOfFunctor, instHasLimits, germ_restrictStalkNatIso_hom_app, AlgebraicGeometry.instFullModuleCatCarrierModulesSpecOfFunctor, toPresheaf_obj, instFaithfulPresheafAbCarrierCommRingCatToPresheaf, instIsLeftAdjointPullback, instFullPushforward, AlgebraicGeometry.tilde.isoTop_hom, ModuleCat.Tilde.toOpen_res, restrictFunctorComp_hom_app_app, restrictFunctorComp_inv_app_app, AlgebraicGeometry.tilde.functor_map, toPresheaf_map, restrictFunctorCongr_inv_app_app, pseudofunctor_right_unitality, pseudofunctor_mapComp_hom_τl, AlgebraicGeometry.tilde.map_comp_assoc, toOpen_fromTildeΓ_app_assoc, instFaithfulPushforward, AlgebraicGeometry.tilde.isIso_toOpen_top, restrictFunctorCongr_hom_app_app, pseudofunctor_mapComp_hom_τr, restrictFunctorId_inv_app_app, pushforwardComp_hom_app_app, Hom.id_app, Hom.isIso_iff_isIso_app, Hom.comp_app, pseudofunctor_mapId_hom_τr, pseudofunctor_obj_obj, Hom.sub_app, instHasColimits, pushforwardId_hom_app_app, restrictAdjunction_unit_app_app, Hom.add_app, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓUnitOpensCarrierCarrierCommRingCatRingCatSheaf, AlgebraicGeometry.instFaithfulModuleCatCarrierModulesSpecOfFunctor, AlgebraicGeometry.tilde.map_add, AlgebraicGeometry.tilde.toOpen_res, AlgebraicGeometry.tilde.toOpen_res_assoc, AlgebraicGeometry.tilde.isUnit_algebraMap_end_basicOpen, conjugateEquiv_pullbackId_hom, instIsLeftAdjointRestrictFunctor, conjugateEquiv_pullbackComp_inv, pseudofunctor_left_unitality, pseudofunctor_associativity_assoc, instFullPresheafOfModulesToPresheafOfModules, pseudofunctor_mapComp_inv_τl, AlgebraicGeometry.tilde.map_zero, pseudofunctor_left_unitality_assoc, pseudofunctor_mapId_hom_τl, AlgebraicGeometry.tilde.functor_obj, AlgebraicGeometry.tilde.toOpen_map_app_assoc, pushforwardCongr_inv_app_app, AlgebraicGeometry.tilde.map_comp, instReflectsIsomorphismsPresheafAbCarrierCommRingCatToPresheaf, instIsRightAdjointPushforward, pseudofunctor_map_r, AlgebraicGeometry.instIsIsoFunctorModuleCatCarrierUnitModulesSpecOfAdjunction, AlgebraicGeometry.tilde.map_neg, instIsRightAdjointPresheafOfModulesToPresheafOfModules, restrictFunctorId_hom_app_app, pseudofunctor_mapComp_inv_τr, AlgebraicGeometry.isIso_fromTildeΓ_iff, AlgebraicGeometry.tilde.map_id_assoc, pushforward_map_app, inv_app, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓFreeOpensCarrierCarrierCommRingCat, pseudofunctor_mapId_inv_τl, pseudofunctor_associativity, instAdditivePushforward, pseudofunctor_mapId_inv_τr, AlgebraicGeometry.tilde.instIsLocalizedModuleCarrierCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecModuleCatPresheafModulesSheafModulesSpecToSheafOpBasicOpenPowersHomToOpen, AlgebraicGeometry.tilde.toOpen_map_app
instModuleCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensCarrierAbPresheaf 📖	CompOp	2 math math: Hom.app_smul, map_smul
presheaf 📖	CompOp	34 math math: pushforward_obj_presheaf_map, pushforwardId_inv_app_app, restrictAdjunction_counit_app_app, pushforwardCongr_hom_app_app, pushforward_obj_obj, germ_restrictStalkNatIso_inv_app, Hom.zero_app, pushforwardComp_inv_app_app, germ_restrictStalkNatIso_hom_app, toPresheaf_obj, isSheaf, restrictFunctorComp_hom_app_app, restrictFunctorComp_inv_app_app, restrict_map, restrictFunctorCongr_inv_app_app, restrictFunctorCongr_hom_app_app, restrictFunctorId_inv_app_app, pushforwardComp_hom_app_app, mapPresheaf_app, AlgebraicGeometry.tilde.instIsLocalizedModuleCarrierCarrierOfCarrierStalkAbPresheafPrimeComplAsIdealHomToStalk, Hom.id_app, Hom.isIso_iff_isIso_app, Hom.comp_app, instIsIsoAbApp, Hom.sub_app, pushforwardId_hom_app_app, restrict_obj, restrictAdjunction_unit_app_app, Hom.add_app, pushforwardCongr_inv_app_app, restrictFunctorId_hom_app_app, Hom.app_smul, inv_app, map_smul
pseudofunctor 📖	CompOp	12 math math: pseudofunctor_map_adj, pseudofunctor_map_l, pseudofunctor_mapComp_hom_τl, pseudofunctor_mapComp_hom_τr, pseudofunctor_mapId_hom_τr, pseudofunctor_obj_obj, pseudofunctor_mapComp_inv_τl, pseudofunctor_mapId_hom_τl, pseudofunctor_map_r, pseudofunctor_mapComp_inv_τr, pseudofunctor_mapId_inv_τl, pseudofunctor_mapId_inv_τr
pullback 📖	CompOp	16 math math: pseudofunctor_map_adj, instAdditivePullback, pseudofunctor_map_l, pseudofunctor_right_unitality_assoc, instIsLeftAdjointPullback, pseudofunctor_right_unitality, pseudofunctor_mapComp_hom_τl, conjugateEquiv_pullbackId_hom, conjugateEquiv_pullbackComp_inv, pseudofunctor_left_unitality, pseudofunctor_associativity_assoc, pseudofunctor_mapComp_inv_τl, pseudofunctor_left_unitality_assoc, pseudofunctor_mapId_hom_τl, pseudofunctor_mapId_inv_τl, pseudofunctor_associativity
pullbackComp 📖	CompOp	9 math math: pseudofunctor_right_unitality_assoc, pseudofunctor_right_unitality, pseudofunctor_mapComp_hom_τl, conjugateEquiv_pullbackComp_inv, pseudofunctor_left_unitality, pseudofunctor_associativity_assoc, pseudofunctor_mapComp_inv_τl, pseudofunctor_left_unitality_assoc, pseudofunctor_associativity
pullbackCongr 📖	CompOp	—
pullbackId 📖	CompOp	7 math math: pseudofunctor_right_unitality_assoc, pseudofunctor_right_unitality, conjugateEquiv_pullbackId_hom, pseudofunctor_left_unitality, pseudofunctor_left_unitality_assoc, pseudofunctor_mapId_hom_τl, pseudofunctor_mapId_inv_τl
pullbackPushforwardAdjunction 📖	CompOp	3 math math: pseudofunctor_map_adj, conjugateEquiv_pullbackId_hom, conjugateEquiv_pullbackComp_inv
pushforward 📖	CompOp	24 math math: pushforward_obj_presheaf_map, pseudofunctor_map_adj, pushforwardId_inv_app_app, restrictAdjunction_counit_app_app, pushforwardCongr_hom_app_app, pushforward_obj_obj, instIsIsoFunctorCounitRestrictAdjunction, pushforwardComp_inv_app_app, instFullPushforward, instFaithfulPushforward, pseudofunctor_mapComp_hom_τr, pushforwardComp_hom_app_app, pseudofunctor_mapId_hom_τr, pushforwardId_hom_app_app, restrictAdjunction_unit_app_app, conjugateEquiv_pullbackId_hom, conjugateEquiv_pullbackComp_inv, pushforwardCongr_inv_app_app, instIsRightAdjointPushforward, pseudofunctor_map_r, pseudofunctor_mapComp_inv_τr, pushforward_map_app, instAdditivePushforward, pseudofunctor_mapId_inv_τr
pushforwardComp 📖	CompOp	5 math math: pushforwardComp_inv_app_app, pseudofunctor_mapComp_hom_τr, pushforwardComp_hom_app_app, conjugateEquiv_pullbackComp_inv, pseudofunctor_mapComp_inv_τr
pushforwardCongr 📖	CompOp	2 math math: pushforwardCongr_hom_app_app, pushforwardCongr_inv_app_app
pushforwardId 📖	CompOp	5 math math: pushforwardId_inv_app_app, pseudofunctor_mapId_hom_τr, pushforwardId_hom_app_app, conjugateEquiv_pullbackId_hom, pseudofunctor_mapId_inv_τr
restrict 📖	CompOp	2 math math: restrict_map, restrict_obj
restrictAdjunction 📖	CompOp	3 math math: restrictAdjunction_counit_app_app, instIsIsoFunctorCounitRestrictAdjunction, restrictAdjunction_unit_app_app
restrictFunctor 📖	CompOp	12 math math: restrictAdjunction_counit_app_app, germ_restrictStalkNatIso_inv_app, instIsIsoFunctorCounitRestrictAdjunction, germ_restrictStalkNatIso_hom_app, restrictFunctorComp_hom_app_app, restrictFunctorComp_inv_app_app, restrictFunctorCongr_inv_app_app, restrictFunctorCongr_hom_app_app, restrictFunctorId_inv_app_app, restrictAdjunction_unit_app_app, instIsLeftAdjointRestrictFunctor, restrictFunctorId_hom_app_app
restrictFunctorAdjCounitIso 📖	CompOp	—
restrictFunctorComp 📖	CompOp	2 math math: restrictFunctorComp_hom_app_app, restrictFunctorComp_inv_app_app
restrictFunctorCongr 📖	CompOp	2 math math: restrictFunctorCongr_inv_app_app, restrictFunctorCongr_hom_app_app
restrictFunctorId 📖	CompOp	2 math math: restrictFunctorId_inv_app_app, restrictFunctorId_hom_app_app
restrictFunctorIsoPullback 📖	CompOp	—
restrictStalkNatIso 📖	CompOp	2 math math: germ_restrictStalkNatIso_inv_app, germ_restrictStalkNatIso_hom_app
toPresheaf 📖	CompOp	7 math math: instPreservesLimitsPresheafAbCarrierCommRingCatToPresheaf, germ_restrictStalkNatIso_inv_app, germ_restrictStalkNatIso_hom_app, toPresheaf_obj, instFaithfulPresheafAbCarrierCommRingCatToPresheaf, toPresheaf_map, instReflectsIsomorphismsPresheafAbCarrierCommRingCatToPresheaf
toPresheafOfModules 📖	CompOp	3 math math: instFaithfulPresheafOfModulesToPresheafOfModules, instFullPresheafOfModulesToPresheafOfModules, instIsRightAdjointPresheafOfModulesToPresheafOfModules

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
conjugateEquiv_pullbackComp_inv 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.Functor AlgebraicGeometry.Scheme.Modules instCategory CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category pullback CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Functor.comp pushforward EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.conjugateEquiv CategoryTheory.Adjunction.comp pullbackPushforwardAdjunction CategoryTheory.Iso.inv pullbackComp CategoryTheory.Iso.hom pushforwardComp	—	SheafOfModules.conjugateEquiv_pullbackComp_inv
conjugateEquiv_pullbackId_hom 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.Functor AlgebraicGeometry.Scheme.Modules instCategory CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category pullback CategoryTheory.CategoryStruct.id AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Functor.id pushforward EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.conjugateEquiv CategoryTheory.Adjunction.id pullbackPushforwardAdjunction CategoryTheory.Iso.hom pullbackId CategoryTheory.Iso.inv pushforwardId	—	SheafOfModules.conjugateEquiv_pullbackId_hom
germ_restrictStalkNatIso_hom_app 📖	mathematical	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.Scheme.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	CategoryTheory.CategoryStruct.comp Ab CategoryTheory.Category.toCategoryStruct AddCommGrpCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder presheaf AlgebraicGeometry.Scheme.Modules instCategory restrictFunctor Opposite.op TopCat.Presheaf.stalk AddCommGrpCat.hasColimitsOfSize UnivLE.self CategoryTheory.Functor.comp TopCat.Presheaf TopCat.instCategoryPresheaf toPresheaf TopCat.Presheaf.stalkFunctor DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' TopCat.Presheaf.germ CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category restrictStalkNatIso AlgebraicGeometry.Scheme.Hom.opensFunctor Opposite.unop	—	CategoryTheory.Functor.Final.ι_colimitIso_hom Topology.IsOpenEmbedding.isOpenMap AlgebraicGeometry.Scheme.Hom.isOpenEmbedding CategoryTheory.Functor.final_op_of_initial CategoryTheory.Functor.initial_of_adjunction AddCommGrpCat.hasColimit Opposite.small UnivLE.small UnivLE.self
germ_restrictStalkNatIso_inv_app 📖	mathematical	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.Scheme.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	CategoryTheory.CategoryStruct.comp Ab CategoryTheory.Category.toCategoryStruct AddCommGrpCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder presheaf Opposite.op AlgebraicGeometry.Scheme.Hom.opensFunctor Opposite.unop TopCat.Presheaf.stalk AddCommGrpCat.hasColimitsOfSize UnivLE.self DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' AlgebraicGeometry.Scheme.Modules instCategory CategoryTheory.Functor.comp restrictFunctor TopCat.Presheaf TopCat.instCategoryPresheaf toPresheaf TopCat.Presheaf.stalkFunctor TopCat.Presheaf.germ CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category restrictStalkNatIso	—	AddCommGrpCat.hasColimitsOfSize UnivLE.self germ_restrictStalkNatIso_hom_app CategoryTheory.Category.assoc CategoryTheory.NatTrans.comp_app CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id
hom_ext 📖	—	Hom.app	—	—	SheafOfModules.hom_ext PresheafOfModules.hom_ext ModuleCat.hom_ext LinearMap.ext
hom_ext_iff 📖	mathematical	—	Hom.app	—	hom_ext
instAdditivePullback 📖	mathematical	—	CategoryTheory.Functor.Additive AlgebraicGeometry.Scheme.Modules instCategory CategoryTheory.Abelian.toPreadditive instAbelian pullback	—	CategoryTheory.Functor.additive_of_preservesBinaryBiproducts CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Functor.preservesZeroMorphisms_of_preserves_initial_object CategoryTheory.Abelian.hasZeroObject CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint instIsLeftAdjointPullback CategoryTheory.Limits.preservesBinaryBiproducts_of_preservesBinaryCoproducts
instAdditivePushforward 📖	mathematical	—	CategoryTheory.Functor.Additive AlgebraicGeometry.Scheme.Modules instCategory CategoryTheory.Abelian.toPreadditive instAbelian pushforward	—	CategoryTheory.Functor.additive_of_preservesBinaryBiproducts CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Functor.preservesZeroMorphisms_of_preserves_terminal_object CategoryTheory.Abelian.hasZeroObject CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint instIsRightAdjointPushforward CategoryTheory.Limits.preservesBinaryBiproducts_of_preservesBinaryProducts
instFaithfulPresheafAbCarrierCommRingCatToPresheaf 📖	mathematical	—	CategoryTheory.Functor.Faithful AlgebraicGeometry.Scheme.Modules instCategory TopCat.Presheaf Ab AddCommGrpCat.instCategory AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.instCategoryPresheaf toPresheaf	—	CategoryTheory.Functor.Faithful.comp instFaithfulPresheafOfModulesToPresheafOfModules PresheafOfModules.instFaithfulFunctorOppositeAbToPresheaf
instFaithfulPresheafOfModulesToPresheafOfModules 📖	mathematical	—	CategoryTheory.Functor.Faithful AlgebraicGeometry.Scheme.Modules instCategory AlgebraicGeometry.Scheme.PresheafOfModules PresheafOfModules.instCategory TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Sheaf.val Opens.grothendieckTopology RingCat RingCat.instCategory AlgebraicGeometry.Scheme.ringCatSheaf toPresheafOfModules	—	CategoryTheory.Functor.FullyFaithful.faithful
instFaithfulPushforward 📖	mathematical	—	CategoryTheory.Functor.Faithful AlgebraicGeometry.Scheme.Modules instCategory pushforward	—	CategoryTheory.Functor.FullyFaithful.faithful instIsIsoFunctorCounitRestrictAdjunction
instFullPresheafOfModulesToPresheafOfModules 📖	mathematical	—	CategoryTheory.Functor.Full AlgebraicGeometry.Scheme.Modules instCategory AlgebraicGeometry.Scheme.PresheafOfModules PresheafOfModules.instCategory TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Sheaf.val Opens.grothendieckTopology RingCat RingCat.instCategory AlgebraicGeometry.Scheme.ringCatSheaf toPresheafOfModules	—	CategoryTheory.Functor.FullyFaithful.full
instFullPushforward 📖	mathematical	—	CategoryTheory.Functor.Full AlgebraicGeometry.Scheme.Modules instCategory pushforward	—	CategoryTheory.Functor.FullyFaithful.full instIsIsoFunctorCounitRestrictAdjunction
instHasColimits 📖	mathematical	—	CategoryTheory.Limits.HasColimits AlgebraicGeometry.Scheme.Modules instCategory	—	SheafOfModules.instHasColimitsOfSizeOfPresheafOfModulesValRingCat CategoryTheory.instHasWeakSheafifyOfHasSheafify CategoryTheory.instHasSheafifyOfPreservesLimitsForgetOfHasFiniteLimitsOfSmallOppositeCover AddCommGrpCat.hasLimit small_subtype small_Pi UnivLE.small univLE_of_max UnivLE.self AddCommGrpCat.hasColimitsOfShape Opposite.small CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits AddCommGrpCat.FilteredColimits.forget_preservesFilteredColimits CategoryTheory.isFiltered_op_of_isCofiltered CategoryTheory.isCofiltered_of_directed_ge_nonempty SemilatticeInf.instIsCodirectedOrder AddCommGrpCat.forget_reflects_isos AddCommGrpCat.forget_preservesLimitsOfShape AddCommGrpCat.forget_preservesLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits AddCommGrpCat.hasLimits CategoryTheory.GrothendieckTopology.instWEqualsLocallyBijectiveOfHasWeakSheafifyOfHasSheafComposeOfPreservesSheafificationOfReflectsIsomorphismsForget CategoryTheory.hasSheafCompose_of_preservesMulticospan CategoryTheory.Functor.corepresentable_preservesLimit AddCommGrpCat.forget_isCorepresentable CategoryTheory.GrothendieckTopology.instPreservesSheafificationForgetOfPreservesLimitsOfHasColimitsOfShapeOfPreservesColimitsOfShapeOppositeCoverOfHasLimitsOfShapeWalkingMulticospanOfReflectsIsomorphisms AddCommGrpCat.hasLimitsOfShape PresheafOfModules.hasColimitsOfSize AddCommGrpCat.hasColimitsOfSize
instHasLimits 📖	mathematical	—	CategoryTheory.Limits.HasLimits AlgebraicGeometry.Scheme.Modules instCategory	—	SheafOfModules.hasLimitsOfSize
instIsIsoAbApp 📖	mathematical	—	CategoryTheory.IsIso Ab AddCommGrpCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder presheaf Opposite.op Hom.app	—	Hom.isIso_iff_isIso_app
instIsIsoFunctorCounitRestrictAdjunction 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor AlgebraicGeometry.Scheme.Modules instCategory CategoryTheory.Functor.category CategoryTheory.Functor.comp pushforward restrictFunctor CategoryTheory.Functor.id CategoryTheory.Adjunction.counit restrictAdjunction	—	CategoryTheory.Iso.isIso_hom
instIsLeftAdjointPullback 📖	mathematical	—	CategoryTheory.Functor.IsLeftAdjoint AlgebraicGeometry.Scheme.Modules instCategory pullback	—	CategoryTheory.Adjunction.isLeftAdjoint
instIsLeftAdjointRestrictFunctor 📖	mathematical	—	CategoryTheory.Functor.IsLeftAdjoint AlgebraicGeometry.Scheme.Modules instCategory restrictFunctor	—	CategoryTheory.Adjunction.isLeftAdjoint
instIsRightAdjointPresheafOfModulesToPresheafOfModules 📖	mathematical	—	CategoryTheory.Functor.IsRightAdjoint AlgebraicGeometry.Scheme.PresheafOfModules PresheafOfModules.instCategory TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Sheaf.val Opens.grothendieckTopology RingCat RingCat.instCategory AlgebraicGeometry.Scheme.ringCatSheaf AlgebraicGeometry.Scheme.Modules instCategory toPresheafOfModules	—	CategoryTheory.Adjunction.isRightAdjoint CategoryTheory.Presheaf.instIsLocallyInjectiveOfIsIsoFunctorOpposite CategoryTheory.IsIso.id CategoryTheory.Presheaf.isLocallySurjective_of_iso CategoryTheory.GrothendieckTopology.instWEqualsLocallyBijectiveOfHasWeakSheafifyOfHasSheafComposeOfPreservesSheafificationOfReflectsIsomorphismsForget CategoryTheory.instHasWeakSheafifyOfHasSheafify CategoryTheory.instHasSheafifyOfPreservesLimitsForgetOfHasFiniteLimitsOfSmallOppositeCover AddCommGrpCat.hasLimit small_subtype small_Pi UnivLE.small UnivLE.self AddCommGrpCat.hasColimitsOfShape Opposite.small CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits AddCommGrpCat.FilteredColimits.forget_preservesFilteredColimits CategoryTheory.isFiltered_op_of_isCofiltered CategoryTheory.isCofiltered_of_directed_ge_nonempty SemilatticeInf.instIsCodirectedOrder AddCommGrpCat.forget_reflects_isos AddCommGrpCat.forget_preservesLimitsOfShape AddCommGrpCat.forget_preservesLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits AddCommGrpCat.hasLimits CategoryTheory.hasSheafCompose_of_preservesMulticospan CategoryTheory.Functor.corepresentable_preservesLimit AddCommGrpCat.forget_isCorepresentable CategoryTheory.GrothendieckTopology.instPreservesSheafificationForgetOfPreservesLimitsOfHasColimitsOfShapeOfPreservesColimitsOfShapeOppositeCoverOfHasLimitsOfShapeWalkingMulticospanOfReflectsIsomorphisms AddCommGrpCat.hasLimitsOfShape
instIsRightAdjointPushforward 📖	mathematical	—	CategoryTheory.Functor.IsRightAdjoint AlgebraicGeometry.Scheme.Modules instCategory pushforward	—	CategoryTheory.Adjunction.isRightAdjoint
instPreservesLimitsPresheafAbCarrierCommRingCatToPresheaf 📖	mathematical	—	CategoryTheory.Limits.PreservesLimits AlgebraicGeometry.Scheme.Modules instCategory TopCat.Presheaf Ab AddCommGrpCat.instCategory AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.instCategoryPresheaf toPresheaf	—	CategoryTheory.Limits.comp_preservesLimits CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint instIsRightAdjointPresheafOfModulesToPresheafOfModules PresheafOfModules.instPreservesLimitsOfSizeFunctorOppositeAbToPresheaf
instReflectsIsomorphismsPresheafAbCarrierCommRingCatToPresheaf 📖	mathematical	—	CategoryTheory.Functor.ReflectsIsomorphisms AlgebraicGeometry.Scheme.Modules instCategory TopCat.Presheaf Ab AddCommGrpCat.instCategory AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.instCategoryPresheaf toPresheaf	—	CategoryTheory.reflectsIsomorphisms_comp CategoryTheory.reflectsIsomorphisms_of_reflectsMonomorphisms_of_reflectsEpimorphisms CategoryTheory.balanced_of_strongMonoCategory CategoryTheory.strongMonoCategory_of_regularMonoCategory CategoryTheory.regularMonoCategoryOfNormalMonoCategory CategoryTheory.Abelian.toIsNormalMonoCategory CategoryTheory.reflectsMonomorphisms_of_reflectsLimitsOfShape CategoryTheory.Limits.ReflectsFiniteLimits.reflects CategoryTheory.Limits.instReflectsFiniteLimitsOfReflectsLimits CategoryTheory.Limits.fullyFaithful_reflectsLimits instFullPresheafOfModulesToPresheafOfModules instFaithfulPresheafOfModulesToPresheafOfModules CategoryTheory.reflectsEpimorphisms_of_reflectsColimitsOfShape CategoryTheory.Limits.ReflectsFiniteColimits.reflects CategoryTheory.Limits.instReflectsFiniteColimitsOfReflectsColimits CategoryTheory.Limits.fullyFaithful_reflectsColimits PresheafOfModules.instIsNormalMonoCategory CategoryTheory.Functor.reflectsMonomorphisms_of_faithful PresheafOfModules.instFaithfulFunctorOppositeAbToPresheaf CategoryTheory.Functor.reflectsEpimorphisms_of_faithful
inv_app 📖	mathematical	—	Hom.app CategoryTheory.inv AlgebraicGeometry.Scheme.Modules instCategory Ab AddCommGrpCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder presheaf Opposite.op instIsIsoAbApp	—	CategoryTheory.IsIso.eq_inv_of_hom_inv_id instIsIsoAbApp CategoryTheory.IsIso.hom_inv_id
isSheaf 📖	mathematical	—	TopCat.Presheaf.IsSheaf Ab AddCommGrpCat.instCategory AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace presheaf	—	SheafOfModules.isSheaf
mapPresheaf_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Ab AddCommGrpCat.instCategory presheaf Hom.mapPresheaf Hom.app Opposite.unop	—	—
map_smul 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Ab AddCommGrpCat.instCategory presheaf Opposite.op AlgebraicGeometry.Scheme.Opens AddCommGrpCat.carrier CategoryTheory.ConcreteCategory.hom AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier CommRingCat.carrier AlgebraicGeometry.PresheafedSpace.presheaf SMulZeroClass.toSMul AddZero.toZero DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid instModuleCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensCarrierAbPresheaf RingHom Semiring.toNonAssocSemiring RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier	—	PresheafOfModules.map_smul
pseudofunctor_associativity 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor AlgebraicGeometry.Scheme.Modules instCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Functor.comp CategoryTheory.Iso.inv pullbackComp CategoryTheory.Functor.whiskerRight CategoryTheory.Iso.hom CategoryTheory.Functor.associator CategoryTheory.Functor.whiskerLeft CategoryTheory.eqToHom	—	instIsContinuousOpensCarrierMapGrothendieckTopology SheafOfModules.instIsRightAdjointPushforward PresheafOfModules.instIsRightAdjointPushforward CategoryTheory.instHasWeakSheafifyOfHasSheafify CategoryTheory.instHasSheafifyOfPreservesLimitsForgetOfHasFiniteLimitsOfSmallOppositeCover AddCommGrpCat.hasLimit small_subtype small_Pi UnivLE.small UnivLE.self AddCommGrpCat.hasColimitsOfShape Opposite.small CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits AddCommGrpCat.FilteredColimits.forget_preservesFilteredColimits CategoryTheory.isFiltered_op_of_isCofiltered CategoryTheory.isCofiltered_of_directed_ge_nonempty SemilatticeInf.instIsCodirectedOrder AddCommGrpCat.forget_reflects_isos AddCommGrpCat.forget_preservesLimitsOfShape AddCommGrpCat.forget_preservesLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits AddCommGrpCat.hasLimits CategoryTheory.GrothendieckTopology.instWEqualsLocallyBijectiveOfHasWeakSheafifyOfHasSheafComposeOfPreservesSheafificationOfReflectsIsomorphismsForget CategoryTheory.hasSheafCompose_of_preservesMulticospan CategoryTheory.Functor.corepresentable_preservesLimit AddCommGrpCat.forget_isCorepresentable CategoryTheory.GrothendieckTopology.instPreservesSheafificationForgetOfPreservesLimitsOfHasColimitsOfShapeOfPreservesColimitsOfShapeOppositeCoverOfHasLimitsOfShapeWalkingMulticospanOfReflectsIsomorphisms AddCommGrpCat.hasLimitsOfShape TopologicalSpace.Opens.instIsContinuousCompGrothendieckTopology SheafOfModules.instIsRightAdjointPushforwardCompSheafRingCatMapSheafPushforwardContinuous SheafOfModules.pullback_assoc CategoryTheory.Iso.hom_inv_id_assoc CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.Iso.inv_hom_id
pseudofunctor_associativity_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor AlgebraicGeometry.Scheme.Modules instCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Functor.comp CategoryTheory.Iso.inv pullbackComp CategoryTheory.Functor.whiskerRight CategoryTheory.Iso.hom CategoryTheory.Functor.associator CategoryTheory.Functor.whiskerLeft CategoryTheory.eqToHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pseudofunctor_associativity
pseudofunctor_left_unitality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor AlgebraicGeometry.Scheme.Modules instCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.CategoryStruct.id CategoryTheory.Functor.comp CategoryTheory.Iso.inv pullbackComp CategoryTheory.Functor.id CategoryTheory.Functor.whiskerRight CategoryTheory.Iso.hom pullbackId CategoryTheory.Functor.leftUnitor CategoryTheory.eqToHom	—	CategoryTheory.Functor.isContinuous_id SheafOfModules.instIsRightAdjointPushforwardIdSheafRingCat instIsContinuousOpensCarrierMapGrothendieckTopology SheafOfModules.instIsRightAdjointPushforward PresheafOfModules.instIsRightAdjointPushforward CategoryTheory.instHasWeakSheafifyOfHasSheafify CategoryTheory.instHasSheafifyOfPreservesLimitsForgetOfHasFiniteLimitsOfSmallOppositeCover AddCommGrpCat.hasLimit small_subtype small_Pi UnivLE.small UnivLE.self AddCommGrpCat.hasColimitsOfShape Opposite.small CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits AddCommGrpCat.FilteredColimits.forget_preservesFilteredColimits CategoryTheory.isFiltered_op_of_isCofiltered CategoryTheory.isCofiltered_of_directed_ge_nonempty SemilatticeInf.instIsCodirectedOrder AddCommGrpCat.forget_reflects_isos AddCommGrpCat.forget_preservesLimitsOfShape AddCommGrpCat.forget_preservesLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits AddCommGrpCat.hasLimits CategoryTheory.GrothendieckTopology.instWEqualsLocallyBijectiveOfHasWeakSheafifyOfHasSheafComposeOfPreservesSheafificationOfReflectsIsomorphismsForget CategoryTheory.hasSheafCompose_of_preservesMulticospan CategoryTheory.Functor.corepresentable_preservesLimit AddCommGrpCat.forget_isCorepresentable CategoryTheory.GrothendieckTopology.instPreservesSheafificationForgetOfPreservesLimitsOfHasColimitsOfShapeOfPreservesColimitsOfShapeOppositeCoverOfHasLimitsOfShapeWalkingMulticospanOfReflectsIsomorphisms AddCommGrpCat.hasLimitsOfShape CategoryTheory.Functor.instIsContinuousCompId_1 SheafOfModules.instIsRightAdjointPushforwardCompSheafRingCatMapSheafPushforwardContinuous SheafOfModules.pullback_id_comp CategoryTheory.Iso.inv_hom_id
pseudofunctor_left_unitality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor AlgebraicGeometry.Scheme.Modules instCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.CategoryStruct.id CategoryTheory.Functor.comp CategoryTheory.Iso.inv pullbackComp CategoryTheory.Functor.id CategoryTheory.Functor.whiskerRight CategoryTheory.Iso.hom pullbackId CategoryTheory.Functor.leftUnitor CategoryTheory.eqToHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pseudofunctor_left_unitality
pseudofunctor_mapComp_hom_τl 📖	mathematical	—	CategoryTheory.Bicategory.Adj.Hom₂.τl CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.LocallyDiscrete.as Opposite AlgebraicGeometry.Scheme CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite AlgebraicGeometry.Scheme.instCategory CategoryTheory.Discrete.as Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.Adj CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Bicategory.Adj.inst CategoryTheory.Iso.hom CategoryTheory.Bicategory.Adj.instCategoryStruct CategoryTheory.Bicategory.Adj.instCategoryHom CategoryTheory.Pseudofunctor.mapComp CategoryTheory.LocallyDiscrete CategoryTheory.locallyDiscreteBicategory pseudofunctor CategoryTheory.NatTrans.toCatHom₂ AlgebraicGeometry.Scheme.Modules Opposite.unop instCategory pullback Quiver.Hom.unop CategoryTheory.Functor.comp CategoryTheory.Cat.str CategoryTheory.Cat.of CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category pullbackComp	—	—
pseudofunctor_mapComp_hom_τr 📖	mathematical	—	CategoryTheory.Bicategory.Adj.Hom₂.τr CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.LocallyDiscrete.as Opposite AlgebraicGeometry.Scheme CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite AlgebraicGeometry.Scheme.instCategory CategoryTheory.Discrete.as Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.Adj CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Bicategory.Adj.inst CategoryTheory.Iso.hom CategoryTheory.Bicategory.Adj.instCategoryStruct CategoryTheory.Bicategory.Adj.instCategoryHom CategoryTheory.Pseudofunctor.mapComp CategoryTheory.LocallyDiscrete CategoryTheory.locallyDiscreteBicategory pseudofunctor CategoryTheory.NatTrans.toCatHom₂ AlgebraicGeometry.Scheme.Modules Opposite.unop CategoryTheory.Cat.str CategoryTheory.Cat.of instCategory CategoryTheory.Functor.comp pushforward Quiver.Hom.unop CategoryTheory.Functor CategoryTheory.Functor.category pushforwardComp	—	—
pseudofunctor_mapComp_inv_τl 📖	mathematical	—	CategoryTheory.Bicategory.Adj.Hom₂.τl CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.LocallyDiscrete.as Opposite AlgebraicGeometry.Scheme CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.Adj CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Bicategory.Adj.inst CategoryTheory.Discrete.as Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite AlgebraicGeometry.Scheme.instCategory CategoryTheory.Iso.inv CategoryTheory.Bicategory.Adj.instCategoryStruct CategoryTheory.Bicategory.Adj.instCategoryHom CategoryTheory.Pseudofunctor.mapComp CategoryTheory.LocallyDiscrete CategoryTheory.locallyDiscreteBicategory pseudofunctor CategoryTheory.NatTrans.toCatHom₂ AlgebraicGeometry.Scheme.Modules Opposite.unop instCategory CategoryTheory.Functor.comp CategoryTheory.Cat.str CategoryTheory.Cat.of pullback Quiver.Hom.unop CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category pullbackComp	—	—
pseudofunctor_mapComp_inv_τr 📖	mathematical	—	CategoryTheory.Bicategory.Adj.Hom₂.τr CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.LocallyDiscrete.as Opposite AlgebraicGeometry.Scheme CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.Adj CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Bicategory.Adj.inst CategoryTheory.Discrete.as Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite AlgebraicGeometry.Scheme.instCategory CategoryTheory.Iso.inv CategoryTheory.Bicategory.Adj.instCategoryStruct CategoryTheory.Bicategory.Adj.instCategoryHom CategoryTheory.Pseudofunctor.mapComp CategoryTheory.LocallyDiscrete CategoryTheory.locallyDiscreteBicategory pseudofunctor CategoryTheory.NatTrans.toCatHom₂ AlgebraicGeometry.Scheme.Modules Opposite.unop CategoryTheory.Cat.str CategoryTheory.Cat.of instCategory pushforward Quiver.Hom.unop CategoryTheory.Functor.comp CategoryTheory.Functor CategoryTheory.Functor.category pushforwardComp	—	—
pseudofunctor_mapId_hom_τl 📖	mathematical	—	CategoryTheory.Bicategory.Adj.Hom₂.τl CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.LocallyDiscrete.as Opposite AlgebraicGeometry.Scheme CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite AlgebraicGeometry.Scheme.instCategory CategoryTheory.Bicategory.Adj CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Bicategory.Adj.inst CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.Adj.instCategoryStruct CategoryTheory.Bicategory.Adj.instCategoryHom CategoryTheory.Pseudofunctor.mapId CategoryTheory.LocallyDiscrete CategoryTheory.locallyDiscreteBicategory pseudofunctor CategoryTheory.NatTrans.toCatHom₂ AlgebraicGeometry.Scheme.Modules Opposite.unop instCategory pullback CategoryTheory.Functor.id CategoryTheory.Cat.str CategoryTheory.Cat.of CategoryTheory.Functor CategoryTheory.Functor.category pullbackId	—	—
pseudofunctor_mapId_hom_τr 📖	mathematical	—	CategoryTheory.Bicategory.Adj.Hom₂.τr CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.LocallyDiscrete.as Opposite AlgebraicGeometry.Scheme CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite AlgebraicGeometry.Scheme.instCategory CategoryTheory.Bicategory.Adj CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Bicategory.Adj.inst CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.Adj.instCategoryStruct CategoryTheory.Bicategory.Adj.instCategoryHom CategoryTheory.Pseudofunctor.mapId CategoryTheory.LocallyDiscrete CategoryTheory.locallyDiscreteBicategory pseudofunctor CategoryTheory.NatTrans.toCatHom₂ AlgebraicGeometry.Scheme.Modules Opposite.unop CategoryTheory.Cat.str CategoryTheory.Cat.of instCategory CategoryTheory.Functor.id pushforward CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category pushforwardId	—	—
pseudofunctor_mapId_inv_τl 📖	mathematical	—	CategoryTheory.Bicategory.Adj.Hom₂.τl CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.LocallyDiscrete.as Opposite AlgebraicGeometry.Scheme CategoryTheory.CategoryStruct.id CategoryTheory.Bicategory.Adj CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Bicategory.Adj.inst CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite AlgebraicGeometry.Scheme.instCategory CategoryTheory.Iso.inv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.Adj.instCategoryStruct CategoryTheory.Bicategory.Adj.instCategoryHom CategoryTheory.Pseudofunctor.mapId CategoryTheory.LocallyDiscrete CategoryTheory.locallyDiscreteBicategory pseudofunctor CategoryTheory.NatTrans.toCatHom₂ AlgebraicGeometry.Scheme.Modules Opposite.unop instCategory CategoryTheory.Functor.id CategoryTheory.Cat.str CategoryTheory.Cat.of pullback CategoryTheory.Functor CategoryTheory.Functor.category pullbackId	—	—
pseudofunctor_mapId_inv_τr 📖	mathematical	—	CategoryTheory.Bicategory.Adj.Hom₂.τr CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.LocallyDiscrete.as Opposite AlgebraicGeometry.Scheme CategoryTheory.CategoryStruct.id CategoryTheory.Bicategory.Adj CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Bicategory.Adj.inst CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite AlgebraicGeometry.Scheme.instCategory CategoryTheory.Iso.inv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.Adj.instCategoryStruct CategoryTheory.Bicategory.Adj.instCategoryHom CategoryTheory.Pseudofunctor.mapId CategoryTheory.LocallyDiscrete CategoryTheory.locallyDiscreteBicategory pseudofunctor CategoryTheory.NatTrans.toCatHom₂ AlgebraicGeometry.Scheme.Modules Opposite.unop CategoryTheory.Cat.str CategoryTheory.Cat.of instCategory pushforward CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category pushforwardId	—	—
pseudofunctor_map_adj 📖	mathematical	—	CategoryTheory.Bicategory.Adj.Hom.adj CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.Bicategory.Adj.obj CategoryTheory.LocallyDiscrete.as Opposite AlgebraicGeometry.Scheme Prefunctor.map CategoryTheory.LocallyDiscrete CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite AlgebraicGeometry.Scheme.instCategory CategoryTheory.Bicategory.Adj CategoryTheory.Bicategory.Adj.inst CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor pseudofunctor CategoryTheory.Adjunction.toCat AlgebraicGeometry.Scheme.Modules Opposite.unop instCategory pullback Quiver.Hom.unop CategoryTheory.Discrete.as pushforward pullbackPushforwardAdjunction	—	—
pseudofunctor_map_l 📖	mathematical	—	CategoryTheory.Bicategory.Adj.Hom.l CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.Bicategory.Adj.obj CategoryTheory.LocallyDiscrete.as Opposite AlgebraicGeometry.Scheme Prefunctor.map CategoryTheory.LocallyDiscrete CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite AlgebraicGeometry.Scheme.instCategory CategoryTheory.Bicategory.Adj CategoryTheory.Bicategory.Adj.inst CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor pseudofunctor CategoryTheory.Functor.toCatHom AlgebraicGeometry.Scheme.Modules Opposite.unop instCategory pullback Quiver.Hom.unop CategoryTheory.Discrete.as	—	—
pseudofunctor_map_r 📖	mathematical	—	CategoryTheory.Bicategory.Adj.Hom.r CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.Bicategory.Adj.obj CategoryTheory.LocallyDiscrete.as Opposite AlgebraicGeometry.Scheme Prefunctor.map CategoryTheory.LocallyDiscrete CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite AlgebraicGeometry.Scheme.instCategory CategoryTheory.Bicategory.Adj CategoryTheory.Bicategory.Adj.inst CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor pseudofunctor CategoryTheory.Functor.toCatHom AlgebraicGeometry.Scheme.Modules Opposite.unop instCategory pushforward Quiver.Hom.unop CategoryTheory.Discrete.as	—	—
pseudofunctor_obj_obj 📖	mathematical	—	CategoryTheory.Bicategory.Adj.obj CategoryTheory.Cat CategoryTheory.Cat.bicategory Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite AlgebraicGeometry.Scheme CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite AlgebraicGeometry.Scheme.instCategory CategoryTheory.Bicategory.Adj CategoryTheory.Bicategory.Adj.inst CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor pseudofunctor CategoryTheory.Cat.of AlgebraicGeometry.Scheme.Modules Opposite.unop CategoryTheory.LocallyDiscrete.as instCategory	—	—
pseudofunctor_right_unitality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor AlgebraicGeometry.Scheme.Modules instCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.CategoryStruct.id CategoryTheory.Functor.comp CategoryTheory.Iso.inv pullbackComp CategoryTheory.Functor.id CategoryTheory.Functor.whiskerLeft CategoryTheory.Iso.hom pullbackId CategoryTheory.Functor.rightUnitor CategoryTheory.eqToHom	—	instIsContinuousOpensCarrierMapGrothendieckTopology SheafOfModules.instIsRightAdjointPushforward PresheafOfModules.instIsRightAdjointPushforward CategoryTheory.instHasWeakSheafifyOfHasSheafify CategoryTheory.instHasSheafifyOfPreservesLimitsForgetOfHasFiniteLimitsOfSmallOppositeCover AddCommGrpCat.hasLimit small_subtype small_Pi UnivLE.small UnivLE.self AddCommGrpCat.hasColimitsOfShape Opposite.small CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits AddCommGrpCat.FilteredColimits.forget_preservesFilteredColimits CategoryTheory.isFiltered_op_of_isCofiltered CategoryTheory.isCofiltered_of_directed_ge_nonempty SemilatticeInf.instIsCodirectedOrder AddCommGrpCat.forget_reflects_isos AddCommGrpCat.forget_preservesLimitsOfShape AddCommGrpCat.forget_preservesLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits AddCommGrpCat.hasLimits CategoryTheory.GrothendieckTopology.instWEqualsLocallyBijectiveOfHasWeakSheafifyOfHasSheafComposeOfPreservesSheafificationOfReflectsIsomorphismsForget CategoryTheory.hasSheafCompose_of_preservesMulticospan CategoryTheory.Functor.corepresentable_preservesLimit AddCommGrpCat.forget_isCorepresentable CategoryTheory.GrothendieckTopology.instPreservesSheafificationForgetOfPreservesLimitsOfHasColimitsOfShapeOfPreservesColimitsOfShapeOppositeCoverOfHasLimitsOfShapeWalkingMulticospanOfReflectsIsomorphisms AddCommGrpCat.hasLimitsOfShape CategoryTheory.Functor.isContinuous_id SheafOfModules.instIsRightAdjointPushforwardIdSheafRingCat CategoryTheory.Functor.instIsContinuousCompId SheafOfModules.instIsRightAdjointPushforwardCompSheafRingCatMapSheafPushforwardContinuous SheafOfModules.pullback_comp_id CategoryTheory.Iso.inv_hom_id
pseudofunctor_right_unitality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor AlgebraicGeometry.Scheme.Modules instCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.CategoryStruct.id CategoryTheory.Functor.comp CategoryTheory.Iso.inv pullbackComp CategoryTheory.Functor.id CategoryTheory.Functor.whiskerLeft CategoryTheory.Iso.hom pullbackId CategoryTheory.Functor.rightUnitor CategoryTheory.eqToHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pseudofunctor_right_unitality
pushforwardComp_hom_app_app 📖	mathematical	—	Hom.app CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Modules instCategory CategoryTheory.Functor.comp pushforward CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category pushforwardComp CategoryTheory.CategoryStruct.id Ab AddCommGrpCat.instCategory Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder presheaf Opposite.op	—	—
pushforwardComp_inv_app_app 📖	mathematical	—	Hom.app CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Modules instCategory pushforward CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.Functor.comp CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category pushforwardComp CategoryTheory.CategoryStruct.id Ab AddCommGrpCat.instCategory Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder presheaf Opposite.op	—	—
pushforwardCongr_hom_app_app 📖	mathematical	—	Hom.app CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Modules instCategory pushforward CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category pushforwardCongr CategoryTheory.Functor.map Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Ab AddCommGrpCat.instCategory presheaf Opposite.op TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom Quiver.Hom AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory	—	—
pushforwardCongr_inv_app_app 📖	mathematical	—	Hom.app CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Modules instCategory pushforward CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category pushforwardCongr CategoryTheory.Functor.map Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Ab AddCommGrpCat.instCategory presheaf Opposite.op TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom Quiver.Hom AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory	—	—
pushforwardId_hom_app_app 📖	mathematical	—	Hom.app CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Modules instCategory pushforward CategoryTheory.CategoryStruct.id AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category pushforwardId Ab AddCommGrpCat.instCategory Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder presheaf Opposite.op	—	—
pushforwardId_inv_app_app 📖	mathematical	—	Hom.app CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Modules instCategory CategoryTheory.Functor.id pushforward CategoryTheory.CategoryStruct.id AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category pushforwardId Ab AddCommGrpCat.instCategory Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder presheaf Opposite.op	—	—
pushforward_map_app 📖	mathematical	—	Hom.app CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Modules instCategory pushforward CategoryTheory.Functor.map AlgebraicGeometry.Scheme.Opens Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom'	—	—
pushforward_obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Ab AddCommGrpCat.instCategory presheaf AlgebraicGeometry.Scheme.Modules instCategory pushforward Opposite.op AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom'	—	—
pushforward_obj_presheaf_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Ab AddCommGrpCat.instCategory presheaf CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Modules instCategory pushforward Opposite.op AlgebraicGeometry.Scheme.Opens Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom'	—	—
restrictAdjunction_counit_app_app 📖	mathematical	—	Hom.app CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Modules instCategory CategoryTheory.Functor.comp pushforward restrictFunctor CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Adjunction.counit restrictAdjunction CategoryTheory.Functor.map Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Ab AddCommGrpCat.instCategory presheaf Opposite.op AlgebraicGeometry.Scheme.Opens TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier AlgebraicGeometry.Scheme.Hom.opensFunctor Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom AlgebraicGeometry.Scheme.Hom.preimage_image_eq	—	—
restrictAdjunction_unit_app_app 📖	mathematical	—	Hom.app CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Modules instCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp restrictFunctor pushforward CategoryTheory.NatTrans.app CategoryTheory.Adjunction.unit restrictAdjunction CategoryTheory.Functor.map Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Ab AddCommGrpCat.instCategory presheaf Opposite.op AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier AlgebraicGeometry.Scheme.Hom.opensFunctor TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.homOfLE AlgebraicGeometry.Scheme.Hom.image_preimage_le	—	—
restrictFunctorComp_hom_app_app 📖	mathematical	—	Hom.app CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Modules instCategory restrictFunctor CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.IsOpenImmersion.comp CategoryTheory.Functor.comp CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category restrictFunctorComp CategoryTheory.Functor.map Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Ab AddCommGrpCat.instCategory presheaf Opposite.op AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier AlgebraicGeometry.Scheme.Hom.opensFunctor Opposite.unop CategoryTheory.Functor.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.eqToHom	—	AlgebraicGeometry.IsOpenImmersion.comp
restrictFunctorComp_inv_app_app 📖	mathematical	—	Hom.app CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Modules instCategory CategoryTheory.Functor.comp restrictFunctor CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.IsOpenImmersion.comp CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category restrictFunctorComp CategoryTheory.Functor.map Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Ab AddCommGrpCat.instCategory presheaf Opposite.op AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier AlgebraicGeometry.Scheme.Hom.opensFunctor Opposite.unop CategoryTheory.Functor.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.eqToHom	—	AlgebraicGeometry.IsOpenImmersion.comp
restrictFunctorCongr_hom_app_app 📖	mathematical	—	Hom.app CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Modules instCategory restrictFunctor CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category restrictFunctorCongr CategoryTheory.Functor.map Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Ab AddCommGrpCat.instCategory presheaf Opposite.op AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier AlgebraicGeometry.Scheme.Hom.opensFunctor Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom	—	—
restrictFunctorCongr_inv_app_app 📖	mathematical	—	Hom.app CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Modules instCategory restrictFunctor CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category restrictFunctorCongr CategoryTheory.Functor.map Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Ab AddCommGrpCat.instCategory presheaf Opposite.op AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier AlgebraicGeometry.Scheme.Hom.opensFunctor Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom	—	—
restrictFunctorId_hom_app_app 📖	mathematical	—	Hom.app CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Modules instCategory restrictFunctor CategoryTheory.CategoryStruct.id AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.IsIso.id CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category restrictFunctorId CategoryTheory.Functor.map Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Ab AddCommGrpCat.instCategory presheaf Opposite.op AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier AlgebraicGeometry.Scheme.Hom.opensFunctor Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.eqToHom	—	AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.IsIso.id
restrictFunctorId_inv_app_app 📖	mathematical	—	Hom.app CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Modules instCategory CategoryTheory.Functor.id restrictFunctor CategoryTheory.CategoryStruct.id AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.IsIso.id CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category restrictFunctorId CategoryTheory.Functor.map Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Ab AddCommGrpCat.instCategory presheaf Opposite.op AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier AlgebraicGeometry.Scheme.Hom.opensFunctor Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.eqToHom	—	AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.IsIso.id
restrict_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Ab AddCommGrpCat.instCategory presheaf restrict Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.Opens CategoryTheory.Functor.obj AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier AlgebraicGeometry.Scheme.Hom.opensFunctor	—	—
restrict_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Ab AddCommGrpCat.instCategory presheaf restrict Opposite.op AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier AlgebraicGeometry.Scheme.Hom.opensFunctor	—	—
toPresheaf_map 📖	mathematical	—	CategoryTheory.Functor.map AlgebraicGeometry.Scheme.Modules instCategory TopCat.Presheaf Ab AddCommGrpCat.instCategory AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.instCategoryPresheaf toPresheaf Hom.mapPresheaf	—	—
toPresheaf_obj 📖	mathematical	—	CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Modules instCategory TopCat.Presheaf Ab AddCommGrpCat.instCategory AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.instCategoryPresheaf toPresheaf presheaf	—	—

AlgebraicGeometry.Scheme.Modules.Hom

Definitions

Name	Category	Theorems
app 📖	CompOp	26 math math: AlgebraicGeometry.Scheme.Modules.pushforwardId_inv_app_app, AlgebraicGeometry.Scheme.Modules.restrictAdjunction_counit_app_app, AlgebraicGeometry.Scheme.Modules.pushforwardCongr_hom_app_app, zero_app, AlgebraicGeometry.Scheme.Modules.pushforwardComp_inv_app_app, AlgebraicGeometry.Scheme.Modules.restrictFunctorComp_hom_app_app, AlgebraicGeometry.Scheme.Modules.restrictFunctorComp_inv_app_app, AlgebraicGeometry.Scheme.Modules.restrictFunctorCongr_inv_app_app, AlgebraicGeometry.Scheme.Modules.restrictFunctorCongr_hom_app_app, AlgebraicGeometry.Scheme.Modules.restrictFunctorId_inv_app_app, AlgebraicGeometry.Scheme.Modules.pushforwardComp_hom_app_app, AlgebraicGeometry.Scheme.Modules.mapPresheaf_app, id_app, isIso_iff_isIso_app, comp_app, AlgebraicGeometry.Scheme.Modules.hom_ext_iff, AlgebraicGeometry.Scheme.Modules.instIsIsoAbApp, sub_app, AlgebraicGeometry.Scheme.Modules.pushforwardId_hom_app_app, AlgebraicGeometry.Scheme.Modules.restrictAdjunction_unit_app_app, add_app, AlgebraicGeometry.Scheme.Modules.pushforwardCongr_inv_app_app, AlgebraicGeometry.Scheme.Modules.restrictFunctorId_hom_app_app, app_smul, AlgebraicGeometry.Scheme.Modules.pushforward_map_app, AlgebraicGeometry.Scheme.Modules.inv_app
mapPresheaf 📖	CompOp	2 math math: AlgebraicGeometry.Scheme.Modules.toPresheaf_map, AlgebraicGeometry.Scheme.Modules.mapPresheaf_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_app 📖	mathematical	—	app Quiver.Hom AlgebraicGeometry.Scheme.Modules CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.Modules.instCategory AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.Abelian.toPreadditive AlgebraicGeometry.Scheme.Modules.instAbelian Ab AddCommGrpCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.Scheme.Modules.presheaf Opposite.op AddCommGrpCat.instAddHom	—	—
app_smul 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Ab AddCommGrpCat.instCategory AlgebraicGeometry.Scheme.Modules.presheaf Opposite.op AddCommGrpCat.carrier CategoryTheory.ConcreteCategory.hom AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier app CommRingCat.carrier AlgebraicGeometry.PresheafedSpace.presheaf AlgebraicGeometry.Scheme.Opens SMulZeroClass.toSMul AddZero.toZero DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid AlgebraicGeometry.Scheme.Modules.instModuleCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensCarrierAbPresheaf	—	LinearMap.map_smul
comp_app 📖	mathematical	—	app CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme.Modules CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.Modules.instCategory Ab AddCommGrpCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.Scheme.Modules.presheaf Opposite.op	—	—
id_app 📖	mathematical	—	app CategoryTheory.CategoryStruct.id AlgebraicGeometry.Scheme.Modules CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.Modules.instCategory Ab AddCommGrpCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.Scheme.Modules.presheaf Opposite.op	—	—
isIso_iff_isIso_app 📖	mathematical	—	CategoryTheory.IsIso AlgebraicGeometry.Scheme.Modules AlgebraicGeometry.Scheme.Modules.instCategory Ab AddCommGrpCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.Scheme.Modules.presheaf Opposite.op app	—	CategoryTheory.isIso_iff_of_reflects_iso AlgebraicGeometry.Scheme.Modules.instReflectsIsomorphismsPresheafAbCarrierCommRingCatToPresheaf CategoryTheory.NatTrans.isIso_iff_isIso_app Function.Surjective.forall Opposite.op_surjective
sub_app 📖	mathematical	—	app Quiver.Hom AlgebraicGeometry.Scheme.Modules CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.Modules.instCategory SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup CategoryTheory.Abelian.toPreadditive AlgebraicGeometry.Scheme.Modules.instAbelian Ab AddCommGrpCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.Scheme.Modules.presheaf Opposite.op AddCommGrpCat.instSubHom	—	—
zero_app 📖	mathematical	—	app Quiver.Hom AlgebraicGeometry.Scheme.Modules CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.Modules.instCategory CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AlgebraicGeometry.Scheme.Modules.instAbelian Ab AddCommGrpCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.Scheme.Modules.presheaf Opposite.op AddCommGrpCat.instZeroHom_1	—	—

---

← Back to Index