Presheaf

📁 Source: Mathlib/Algebra/Category/ModuleCat/Presheaf.lean

Statistics

Metric	Count
Definitions PresheafOfModules, app, evaluation, forgetToPresheafModuleCat, forgetToPresheafModuleCatMap, forgetToPresheafModuleCatObj, forgetToPresheafModuleCatObjMap, forgetToPresheafModuleCatObjObj, homMk, instAddCommGroupHom, instAddHom, instCategory, instModuleCarrierObjOppositeRingCatCarrierAbPresheaf, instNegHom, instPreadditive, instSubHom, instZeroHom, isoMk, map, obj, ofPresheaf, presheaf, restriction, sections, eval, sectionsMap, sectionsMk, toPresheaf, unit, unitHomEquiv	30
Theorems ext, ext_iff, naturality, naturality_assoc, add_app, comp_app, congr_map_apply, evaluation_map, evaluation_obj, forgetToPresheafModuleCatObjMap_apply, forgetToPresheafModuleCatObjObj_coe, forgetToPresheafModuleCatObj_map, forgetToPresheafModuleCatObj_obj, forgetToPresheafModuleCat_map, forgetToPresheafModuleCat_obj, homMk_app, hom_ext, hom_ext_iff, id_app, instAdditiveFunctorOppositeAbToPresheaf, instAdditiveModuleCatCarrierObjOppositeRingCatEvaluation, instFaithfulFunctorOppositeAbToPresheaf, isoMk_hom_app, isoMk_inv_app, map_comp, map_comp_apply, map_comp_assoc, map_id, map_smul, naturality_apply, neg_app, ofPresheaf_map, ofPresheaf_obj_carrier, ofPresheaf_obj_isAddCommGroup, ofPresheaf_obj_isModule, ofPresheaf_presheaf, presheaf_map_apply_coe, presheaf_obj_coe, restriction_app, sectionsMap_coe, sectionsMap_comp, sectionsMap_id, sectionsMk_coe, sections_ext, sections_ext_iff, sections_property, sub_app, toPresheaf_map_app_apply, toPresheaf_obj_coe, unitHomEquiv_apply_coe, unit_map_one, zero_app, zsmul_app	53
Total	83

PresheafOfModules

Definitions

Name	Category	Theorems
evaluation 📖	CompOp	13 math math: evaluation_preservesColimitsOfShape, instPreservesLimitsOfShapeModuleCatCarrierObjOppositeRingCatEvaluation, toFreeYonedaCoproduct_fromFreeYonedaCoproduct, instPreservesLimitsOfSizeModuleCatCarrierObjOppositeRingCatEvaluation, SheafOfModules.instSmallElemForallObjCompModuleCatCarrierOppositeRingCatValPresheafOfModulesForgetEvaluationForgetLinearMapIdCarrierSections, toFreeYonedaCoproduct_fromFreeYonedaCoproduct_assoc, evaluation_preservesColimitsOfSize, evaluation_preservesFiniteLimits, instAdditiveModuleCatCarrierObjOppositeRingCatEvaluation, restriction_app, Finite.evaluation_preservesFiniteColimits, evaluation_obj, evaluation_map
forgetToPresheafModuleCat 📖	CompOp	4 math math: forgetToPresheafModuleCat_obj, SheafOfModules.forgetToSheafModuleCat_map_val, SheafOfModules.forgetToSheafModuleCat_obj_val, forgetToPresheafModuleCat_map
forgetToPresheafModuleCatMap 📖	CompOp	1 math math: forgetToPresheafModuleCat_map
forgetToPresheafModuleCatObj 📖	CompOp	3 math math: forgetToPresheafModuleCatObj_map, forgetToPresheafModuleCat_obj, forgetToPresheafModuleCatObj_obj
forgetToPresheafModuleCatObjMap 📖	CompOp	2 math math: forgetToPresheafModuleCatObj_map, forgetToPresheafModuleCatObjMap_apply
forgetToPresheafModuleCatObjObj 📖	CompOp	3 math math: forgetToPresheafModuleCatObjMap_apply, forgetToPresheafModuleCatObjObj_coe, forgetToPresheafModuleCatObj_obj
homMk 📖	CompOp	3 math math: homEquivOfIsLocallyBijective_symm_apply, homMk_app, sheafifyMap_val
instAddCommGroupHom 📖	CompOp	1 math math: zsmul_app
instAddHom 📖	CompOp	2 math math: add_app, SheafOfModules.add_val
instCategory 📖	CompOp	126 math math: instAdditiveRestrictScalars, hasFiniteLimits, instIsRightAdjointPushforwardCompFunctorOppositeRingCatWhiskerLeftOp, AlgebraicGeometry.Scheme.Modules.instFaithfulPresheafOfModulesToPresheafOfModules, pullback_id_comp, instIsLocallySurjectiveToSheafify, add_app, toPresheaf_preservesFiniteLimits, restrictScalars_map_app, SheafOfModules.instFullPresheafOfModulesValRingCatForget, epi_iff_surjective, pullback_comp_id, Finite.hasFiniteColimits, evaluation_preservesColimitsOfShape, comp_app, homEquivOfIsLocallyBijective_symm_apply, pushforward_map_app_apply, toSheafify_app_apply', instPreservesLimitsOfShapeModuleCatCarrierObjOppositeRingCatEvaluation, toFreeYonedaCoproduct_fromFreeYonedaCoproduct, instIsLeftAdjointSheafOfModulesSheafification, sectionsMap_comp, free_map_app, ι_fromFreeYonedaCoproduct, freeYonedaEquiv_symm_app, id_app, toPresheaf_map_toSheafify, pushforward_map_app_apply', instFaithfulFunctorOppositeAbToPresheaf, zsmul_app, toPresheaf_obj_coe, isoMk_hom_app, instPreservesLimitsOfSizeModuleCatCarrierObjOppositeRingCatEvaluation, instIsNormalMonoCategory, freeYoneda.isSeparating, epi_of_surjective, SheafOfModules.restrictScalars_obj_val, mono_iff_surjective, SheafOfModules.instReflectsIsomorphismsPresheafOfModulesValRingCatForget, SheafOfModules.instFaithfulPresheafOfModulesValRingCatForget, SheafOfModules.toSheaf_map_val, pullback_assoc, SheafOfModules.instSmallElemForallObjCompModuleCatCarrierOppositeRingCatValPresheafOfModulesForgetEvaluationForgetLinearMapIdCarrierSections, sheafification_map, toFreeYonedaCoproduct_fromFreeYonedaCoproduct_assoc, toSheaf_map_sheafificationHomEquiv_symm, isoMk_inv_app, SheafOfModules.id_val, pushforward_obj_map_apply, homEquivOfIsLocallyBijective_apply, freeYoneda.isDetecting, unitHomEquiv_apply_coe, instIsNormalEpiCategory, ι_fromFreeYonedaCoproduct_assoc, SheafOfModules.fullyFaithfulForget_preimage_val, hasColimitsOfShape, SheafOfModules.restrictScalars_map_val, freeYoneda.instSmall, toPresheaf_map_app_apply, neg_app, instPreservesLimitsOfShapeFunctorOppositeAbToPresheaf, SheafOfModules.pushforward_map_val, evaluation_preservesColimitsOfSize, evaluation_preservesFiniteLimits, instPreservesLimitsOfSizeFunctorOppositeAbToPresheaf, sub_app, Elements.fromFreeYoneda_app_apply, mono_of_injective, pushforward_obj_obj, restrictScalars_obj, instFaithfulRestrictScalars, instAdditiveModuleCatCarrierObjOppositeRingCatEvaluation, SheafOfModules.add_val, comp_toPresheaf_map_sheafifyHomEquiv'_symm_hom, instEpiFromFreeYonedaCoproduct, restriction_app, free_obj, forgetToPresheafModuleCat_obj, Finite.toPresheaf_preservesFiniteColimits, SheafOfModules.forget_map, SheafOfModules.forgetPreservesLimitsOfSize, pullbackObjIsDefined_free_yoneda, toPresheaf_preservesColimitsOfShape, SheafOfModules.Finite.forgetPreservesFiniteLimits, SheafOfModules.forget_obj, SheafOfModules.comp_val_assoc, sectionsMap_id, hasLimitsOfSize, pushforward_assoc, AlgebraicGeometry.Scheme.Modules.instFullPresheafOfModulesToPresheafOfModules, pushforward_obj_map_apply', SheafOfModules.forgetToSheafModuleCat_map_val, hasLimitsOfShape, freeAdjunction_unit_app, freeYonedaEquiv_comp, sheafificationAdjunction_homEquiv_apply, hasColimitsOfSize, toPresheaf_preservesColimitsOfSize, SheafOfModules.forgetPreservesLimitsOfShape, wellPowered, Finite.evaluation_preservesFiniteColimits, SheafOfModules.comp_val, pullbackObjIsDefined_eq_top, toPresheaf_map_sheafificationAdjunction_unit_app, instIsRightAdjointPushforward, instIsLocallyInjectiveToSheafify, AlgebraicGeometry.Scheme.Modules.instIsRightAdjointPresheafOfModulesToPresheafOfModules, toPresheaf_map_sheafificationHomEquiv_def, instFullRestrictScalarsIdFunctorOppositeRingCat, fromFreeYonedaCoproduct_app_mk, toSheafify_app_apply, freeAdjunction_homEquiv, SheafOfModules.forgetToSheafModuleCat_obj_val, evaluation_obj, pushforward_id_comp, evaluation_map, SheafOfModules.pushforward_obj_val, instAdditiveFunctorOppositeAbToPresheaf, zero_app, forgetToPresheafModuleCat_map, toPresheaf_map_sheafificationHomEquiv, instIsRightAdjointPushforwardIdFunctorOppositeRingCat, SheafOfModules.instAdditivePresheafOfModulesValRingCatForget, pushforward_comp_id, instPreservesFiniteLimitsSheafOfModulesSheafification, instPreservesFiniteLimitsSheafAddCommGrpCatCompSheafOfModulesSheafificationToSheaf
instModuleCarrierObjOppositeRingCatCarrierAbPresheaf 📖	CompOp	—
instNegHom 📖	CompOp	1 math math: neg_app
instPreadditive 📖	CompOp	8 math math: instAdditiveRestrictScalars, toFreeYonedaCoproduct_fromFreeYonedaCoproduct, instIsNormalMonoCategory, toFreeYonedaCoproduct_fromFreeYonedaCoproduct_assoc, instIsNormalEpiCategory, instAdditiveModuleCatCarrierObjOppositeRingCatEvaluation, instAdditiveFunctorOppositeAbToPresheaf, SheafOfModules.instAdditivePresheafOfModulesValRingCatForget
instSubHom 📖	CompOp	1 math math: sub_app
instZeroHom 📖	CompOp	3 math math: toFreeYonedaCoproduct_fromFreeYonedaCoproduct, toFreeYonedaCoproduct_fromFreeYonedaCoproduct_assoc, zero_app
isoMk 📖	CompOp	2 math math: isoMk_hom_app, isoMk_inv_app
map 📖	CompOp	33 math math: limitPresheafOfModules_map, sections_property, Derivation.d_map, congr_map_apply, restrictScalarsObj_map, map_comp_apply, unit_map_one, map_smul, Monoidal.tensorObj_map_tmul, freeObj_map, presheaf_map_apply_coe, forgetToPresheafModuleCatObjMap_apply, pushforward_obj_map_apply, SheafOfModules.pushforwardPushforwardAdj_unit_app_val_app, map_comp, colimitPresheafOfModules_map, DifferentialsConstruction.relativeDifferentials'_map_d, Hom.naturality_assoc, restriction_app, DifferentialsConstruction.relativeDifferentials'_map, SheafOfModules.pushforwardNatTrans_app_val_app, map_id, SheafOfModules.pushforwardPushforwardEquivalence_unit_app_val_app, pushforward_obj_map_apply', Hom.naturality, SheafOfModules.pushforwardPushforwardAdj_counit_app_val_app, CategoryTheory.Presieve.FamilyOfElements.isCompatible_map_smul_aux, SheafOfModules.pushforwardNatTrans_app_val_app_apply, ofPresheaf_map, naturality_apply, SheafOfModules.pushforwardPushforwardEquivalence_counit_app_val_app, map_comp_assoc, pushforward₀_obj_map
obj 📖	CompOp	91 math math: Monoidal.tensorObj_obj, Sheafify.app_eq_of_isLocallyInjective, ofPresheaf_obj_isModule, add_app, restrictScalars_map_app, epi_iff_surjective, comp_app, pushforward_map_app_apply, sections_property, toSheafify_app_apply', Derivation.d_map, congr_map_apply, freeYonedaEquiv_symm_app, restrictScalarsObj_map, pushforward₀_obj_obj_carrier, id_app, restrictScalarsObj_obj, Derivation.postcomp_d_apply, Derivation.d_one, sectionsMap_coe, Sheafify.map_smul_eq, map_comp_apply, pushforward_map_app_apply', Derivation.d_mul, unit_map_one, zsmul_app, toPresheaf_obj_coe, isoMk_hom_app, map_smul, Monoidal.tensorObj_map_tmul, SheafOfModules.pushforwardComp_inv_app_val_app, pushforward₀_obj_obj_isAddCommGroup, mono_iff_surjective, instEpiModuleCatCarrierObjOppositeRingCatApp, presheaf_map_apply_coe, Derivation.congr_d, forgetToPresheafModuleCatObjMap_apply, SheafOfModules.pushforwardCongr_hom_app_val_app, surjective_of_epi, injective_of_mono, isoMk_inv_app, pushforward_obj_map_apply, forgetToPresheafModuleCatObjObj_coe, unitHomEquiv_apply_coe, freeObj_obj, SheafOfModules.pushforwardCongr_inv_app_val_app, SheafOfModules.pushforwardPushforwardAdj_unit_app_val_app, presheaf_obj_coe, toPresheaf_map_app_apply, Derivation'.d_app, neg_app, map_comp, SheafOfModules.pushforwardComp_hom_app_val_app, sub_app, DifferentialsConstruction.relativeDifferentials'_map_d, Elements.fromFreeYoneda_app_apply, pushforward_obj_obj, Hom.naturality_assoc, ofPresheaf_obj_carrier, ι_fromFreeYonedaCoproduct_apply, DifferentialsConstruction.relativeDifferentials'_obj, Derivation.d_app, SheafOfModules.unitToPushforwardObjUnit_val_app_apply, Monoidal.tensorHom_app, instMonoModuleCatCarrierObjOppositeRingCatApp, Derivation'.app_apply, SheafOfModules.pushforwardNatTrans_app_val_app, map_id, SheafOfModules.pushforwardPushforwardEquivalence_unit_app_val_app, pushforward_obj_map_apply', Hom.naturality, SheafOfModules.pushforwardPushforwardAdj_counit_app_val_app, CategoryTheory.Presieve.FamilyOfElements.isCompatible_map_smul_aux, freeYonedaEquiv_comp, SheafOfModules.pushforwardNatTrans_app_val_app_apply, colimitPresheafOfModules_obj, limitPresheafOfModules_obj, germ_ringCat_smul, naturality_apply, fromFreeYonedaCoproduct_app_mk, germ_smul, toSheafify_app_apply, pushforward₀_obj_obj_isModule, evaluation_obj, ofPresheaf_obj_isAddCommGroup, SheafOfModules.pushforwardPushforwardEquivalence_counit_app_val_app, freeObjDesc_app, zero_app, map_comp_assoc, Sheafify.SMulCandidate.h, SheafOfModules.unitHomEquiv_apply_coe
ofPresheaf 📖	CompOp	5 math math: ofPresheaf_obj_isModule, ofPresheaf_presheaf, ofPresheaf_obj_carrier, ofPresheaf_map, ofPresheaf_obj_isAddCommGroup
presheaf 📖	CompOp	26 math math: AlgebraicGeometry.StructureSheaf.instIsScalarTowerCarrierStalkCommRingCatStructurePresheafInCommRingCatCarrierAbPresheafOpensCarrierTopModuleStructurePresheaf, sections_property, toSheafify_app_apply', SheafOfModules.toSheaf_obj_val, sectionsMap_coe, SheafOfModules.isSheaf, presheaf_map_apply_coe, SheafOfModules.toSheaf_map_val, sheafification_map, toSheaf_map_sheafificationHomEquiv_symm, unitHomEquiv_apply_coe, freeAdjunctionUnit_app, presheaf_obj_coe, ofPresheaf_presheaf, sectionsMk_coe, AlgebraicGeometry.StructureSheaf.instIsLocalizedModuleCarrierStalkAbPresheafOpensCarrierTopModuleStructurePresheafPrimeComplAsIdealToStalkₗ, sections_ext_iff, toPresheaf_map_sheafificationAdjunction_unit_app, germ_ringCat_smul, toPresheaf_map_sheafificationHomEquiv_def, SheafOfModules.pushforwardSections_coe, germ_smul, toSheafify_app_apply, freeObjDesc_app, toPresheaf_map_sheafificationHomEquiv, SheafOfModules.unitHomEquiv_apply_coe
restriction 📖	CompOp	3 math math: limitPresheafOfModules_map, colimitPresheafOfModules_map, restriction_app
sections 📖	CompOp	1 math math: unitHomEquiv_apply_coe
sectionsMap 📖	CompOp	3 math math: sectionsMap_comp, sectionsMap_coe, sectionsMap_id
sectionsMk 📖	CompOp	1 math math: sectionsMk_coe
toPresheaf 📖	CompOp	25 math math: toPresheaf_preservesFiniteLimits, homEquivOfIsLocallyBijective_symm_apply, toPresheaf_map_toSheafify, instFaithfulFunctorOppositeAbToPresheaf, toPresheaf_preservesLimit, toPresheaf_obj_coe, SheafOfModules.toSheaf_map_val, sheafification_map, toSheaf_map_sheafificationHomEquiv_symm, toPresheaf_map_app_apply, instPreservesLimitsOfShapeFunctorOppositeAbToPresheaf, instPreservesLimitsOfSizeFunctorOppositeAbToPresheaf, Elements.fromFreeYoneda_app_apply, comp_toPresheaf_map_sheafifyHomEquiv'_symm_hom, Finite.toPresheaf_preservesFiniteColimits, toPresheaf_preservesColimitsOfShape, toPresheaf_preservesColimit, freeAdjunction_unit_app, toPresheaf_preservesColimitsOfSize, toPresheaf_map_sheafificationAdjunction_unit_app, toPresheaf_map_sheafificationHomEquiv_def, fromFreeYonedaCoproduct_app_mk, freeAdjunction_homEquiv, instAdditiveFunctorOppositeAbToPresheaf, toPresheaf_map_sheafificationHomEquiv
unit 📖	CompOp	3 math math: unit_map_one, unitHomEquiv_apply_coe, SheafOfModules.unit_val
unitHomEquiv 📖	CompOp	1 math math: unitHomEquiv_apply_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_app 📖	mathematical	—	Hom.app Quiver.Hom PresheafOfModules CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instAddHom ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory obj ModuleCat.instAddHom	—	—
comp_app 📖	mathematical	—	Hom.app CategoryTheory.CategoryStruct.comp PresheafOfModules CategoryTheory.Category.toCategoryStruct instCategory ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory obj	—	—
congr_map_apply 📖	mathematical	—	DFunLike.coe obj CategoryTheory.Functor.obj ModuleCat RingCat.carrier Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory ModuleCat.restrictScalars RingCat.Hom.hom CategoryTheory.Functor.map ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier map	—	—
evaluation_map 📖	mathematical	—	CategoryTheory.Functor.map PresheafOfModules instCategory ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory evaluation Hom.app	—	—
evaluation_obj 📖	mathematical	—	CategoryTheory.Functor.obj PresheafOfModules instCategory ModuleCat RingCat.carrier Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory evaluation obj	—	—
forgetToPresheafModuleCatObjMap_apply 📖	mathematical	—	DFunLike.coe LinearMap RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory Ring.toSemiring RingCat.ring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier forgetToPresheafModuleCatObjObj AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.Hom.hom forgetToPresheafModuleCatObjMap obj ModuleCat ModuleCat.moduleCategory ModuleCat.restrictScalars RingCat.Hom.hom CategoryTheory.Functor.map CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier map	—	—
forgetToPresheafModuleCatObjObj_coe 📖	mathematical	—	ModuleCat.carrier RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring forgetToPresheafModuleCatObjObj obj	—	—
forgetToPresheafModuleCatObj_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite ModuleCat RingCat.carrier CategoryTheory.Functor.obj RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory forgetToPresheafModuleCatObj forgetToPresheafModuleCatObjMap	—	—
forgetToPresheafModuleCatObj_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite ModuleCat RingCat.carrier RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory forgetToPresheafModuleCatObj forgetToPresheafModuleCatObjObj	—	—
forgetToPresheafModuleCat_map 📖	mathematical	—	CategoryTheory.Functor.map PresheafOfModules instCategory CategoryTheory.Functor Opposite CategoryTheory.Category.opposite ModuleCat RingCat.carrier CategoryTheory.Functor.obj RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory CategoryTheory.Functor.category forgetToPresheafModuleCat forgetToPresheafModuleCatMap	—	—
forgetToPresheafModuleCat_obj 📖	mathematical	—	CategoryTheory.Functor.obj PresheafOfModules instCategory CategoryTheory.Functor Opposite CategoryTheory.Category.opposite ModuleCat RingCat.carrier RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory CategoryTheory.Functor.category forgetToPresheafModuleCat forgetToPresheafModuleCatObj	—	—
homMk_app 📖	mathematical	DFunLike.coe CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Ab AddCommGrpCat.instCategory presheaf AddCommGrpCat.carrier CategoryTheory.ConcreteCategory.hom AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier CategoryTheory.NatTrans.app RingCat.carrier RingCat RingCat.instCategory ModuleCat.carrier RingCat.ring obj SMulZeroClass.toSMul AddZero.toZero ModuleCat.isAddCommGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid ModuleCat.isModule instModuleCarrierObjOppositeRingCatCarrierAbPresheaf	Hom.app homMk ModuleCat.ofHom RingHom.id Semiring.toNonAssocSemiring AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	—
hom_ext 📖	—	Hom.app	—	—	Hom.ext
hom_ext_iff 📖	mathematical	—	Hom.app	—	hom_ext
id_app 📖	mathematical	—	Hom.app CategoryTheory.CategoryStruct.id PresheafOfModules CategoryTheory.Category.toCategoryStruct instCategory ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory obj	—	—
instAdditiveFunctorOppositeAbToPresheaf 📖	mathematical	—	CategoryTheory.Functor.Additive PresheafOfModules CategoryTheory.Functor Opposite CategoryTheory.Category.opposite Ab AddCommGrpCat.instCategory instCategory CategoryTheory.Functor.category instPreadditive CategoryTheory.functorCategoryPreadditive AddCommGrpCat.instPreadditive toPresheaf	—	—
instAdditiveModuleCatCarrierObjOppositeRingCatEvaluation 📖	mathematical	—	CategoryTheory.Functor.Additive PresheafOfModules ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring instCategory ModuleCat.moduleCategory instPreadditive ModuleCat.instPreadditive evaluation	—	—
instFaithfulFunctorOppositeAbToPresheaf 📖	mathematical	—	CategoryTheory.Functor.Faithful PresheafOfModules instCategory CategoryTheory.Functor Opposite CategoryTheory.Category.opposite Ab AddCommGrpCat.instCategory CategoryTheory.Functor.category toPresheaf	—	hom_ext ModuleCat.hom_ext LinearMap.ext CategoryTheory.Functor.congr_map
isoMk_hom_app 📖	mathematical	—	Hom.app CategoryTheory.Iso.hom PresheafOfModules instCategory isoMk ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory obj	—	—
isoMk_inv_app 📖	mathematical	—	Hom.app CategoryTheory.Iso.inv PresheafOfModules instCategory isoMk ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory obj	—	—
map_comp 📖	mathematical	—	map CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct ModuleCat RingCat.carrier CategoryTheory.Functor.obj CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory obj ModuleCat.restrictScalars RingCat.Hom.hom CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category ModuleCat.restrictScalarsComp' RingCat.Hom RingHom Semiring.toNonAssocSemiring Ring.toSemiring MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass MulOne.toOne DFunLike.coe RingHom.instFunLike CategoryTheory.Functor.map_comp	—	—
map_comp_apply 📖	mathematical	—	DFunLike.coe obj CategoryTheory.Functor.obj ModuleCat RingCat.carrier Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory ModuleCat.restrictScalars RingCat.Hom.hom CategoryTheory.Functor.map CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier map	—	CategoryTheory.Functor.map_comp map_comp
map_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory obj ModuleCat.restrictScalars RingCat.Hom.hom CategoryTheory.Functor.map CategoryTheory.CategoryStruct.opposite map CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category ModuleCat.restrictScalarsComp' RingCat.Hom RingHom Semiring.toNonAssocSemiring Ring.toSemiring MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass MulOne.toOne DFunLike.coe RingHom.instFunLike CategoryTheory.Functor.map_comp	—	CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_comp
map_id 📖	mathematical	—	map CategoryTheory.CategoryStruct.id Opposite CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app ModuleCat RingCat.carrier CategoryTheory.Functor.obj CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory CategoryTheory.Functor.id ModuleCat.restrictScalars RingCat.Hom.hom CategoryTheory.Functor.map CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category ModuleCat.restrictScalarsId' RingCat.Hom RingHom Semiring.toNonAssocSemiring Ring.toSemiring MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass MulOne.toOne CategoryTheory.Functor.map_id obj	—	—
map_smul 📖	mathematical	—	DFunLike.coe obj CategoryTheory.Functor.obj ModuleCat RingCat.carrier Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory ModuleCat.restrictScalars RingCat.Hom.hom CategoryTheory.Functor.map ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier map SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction ModuleCat.instModuleCarrierObjRestrictScalars RingHom RingHom.instFunLike RingCat.instConcreteCategoryRingHomCarrier	—	map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass
naturality_apply 📖	mathematical	—	DFunLike.coe obj ModuleCat.carrier RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring CategoryTheory.ConcreteCategory.hom ModuleCat ModuleCat.moduleCategory LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier Hom.app ModuleCat.restrictScalars RingCat.Hom.hom CategoryTheory.Functor.map map	—	CategoryTheory.congr_fun Hom.naturality
neg_app 📖	mathematical	—	Hom.app Quiver.Hom PresheafOfModules CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instNegHom ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory obj ModuleCat.instNegHom	—	—
ofPresheaf_map 📖	mathematical	DFunLike.coe CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Ab AddCommGrpCat.instCategory 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 RingCat.carrier RingCat RingCat.instCategory SMulZeroClass.toSMul AddZero.toZero DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring RingCat.ring Module.toDistribMulAction AddCommGroup.toAddCommMonoid RingHom Semiring.toNonAssocSemiring RingHom.instFunLike RingCat.instConcreteCategoryRingHomCarrier	map ofPresheaf ModuleCat.ofHom ModuleCat.carrier ModuleCat ModuleCat.moduleCategory ModuleCat.restrictScalars RingCat.Hom.hom ModuleCat.of ModuleCat.isAddCommGroup Module.compHom ModuleCat.isModule RingHom.id AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	—
ofPresheaf_obj_carrier 📖	mathematical	DFunLike.coe CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Ab AddCommGrpCat.instCategory 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 RingCat.carrier RingCat RingCat.instCategory SMulZeroClass.toSMul AddZero.toZero DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring RingCat.ring Module.toDistribMulAction AddCommGroup.toAddCommMonoid RingHom Semiring.toNonAssocSemiring RingHom.instFunLike RingCat.instConcreteCategoryRingHomCarrier	ModuleCat.carrier obj ofPresheaf	—	—
ofPresheaf_obj_isAddCommGroup 📖	mathematical	DFunLike.coe CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Ab AddCommGrpCat.instCategory 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 RingCat.carrier RingCat RingCat.instCategory SMulZeroClass.toSMul AddZero.toZero DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring RingCat.ring Module.toDistribMulAction AddCommGroup.toAddCommMonoid RingHom Semiring.toNonAssocSemiring RingHom.instFunLike RingCat.instConcreteCategoryRingHomCarrier	ModuleCat.isAddCommGroup obj ofPresheaf	—	—
ofPresheaf_obj_isModule 📖	mathematical	DFunLike.coe CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Ab AddCommGrpCat.instCategory 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 RingCat.carrier RingCat RingCat.instCategory SMulZeroClass.toSMul AddZero.toZero DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring RingCat.ring Module.toDistribMulAction AddCommGroup.toAddCommMonoid RingHom Semiring.toNonAssocSemiring RingHom.instFunLike RingCat.instConcreteCategoryRingHomCarrier	ModuleCat.isModule obj ofPresheaf	—	—
ofPresheaf_presheaf 📖	mathematical	DFunLike.coe CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Ab AddCommGrpCat.instCategory 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 RingCat.carrier RingCat RingCat.instCategory SMulZeroClass.toSMul AddZero.toZero DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring RingCat.ring Module.toDistribMulAction AddCommGroup.toAddCommMonoid RingHom Semiring.toNonAssocSemiring RingHom.instFunLike RingCat.instConcreteCategoryRingHomCarrier	presheaf ofPresheaf	—	—
presheaf_map_apply_coe 📖	mathematical	—	DFunLike.coe AddMonoidHom AddCommGrpCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Ab AddCommGrpCat.instCategory presheaf AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str ModuleCat.carrier RingCat.carrier RingCat RingCat.instCategory RingCat.ring obj AddMonoidHom.instFunLike AddCommGrpCat.Hom.hom CategoryTheory.Functor.map ModuleCat ModuleCat.moduleCategory ModuleCat.restrictScalars RingCat.Hom.hom CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier map	—	—
presheaf_obj_coe 📖	mathematical	—	AddCommGrpCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Ab AddCommGrpCat.instCategory presheaf ModuleCat.carrier RingCat.carrier RingCat RingCat.instCategory RingCat.ring obj	—	—
restriction_app 📖	mathematical	—	CategoryTheory.NatTrans.app PresheafOfModules instCategory ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory evaluation CategoryTheory.Functor.comp ModuleCat.restrictScalars RingCat.Hom.hom CategoryTheory.Functor.map restriction map	—	—
sectionsMap_coe 📖	mathematical	—	Set Set.instMembership CategoryTheory.Functor.sections Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp Ab AddCommGrpCat.instCategory CategoryTheory.types presheaf CategoryTheory.forget AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier sectionsMap DFunLike.coe LinearMap RingCat.carrier CategoryTheory.Functor.obj RingCat RingCat.instCategory Ring.toSemiring RingCat.ring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier obj AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat ModuleCat.moduleCategory ModuleCat.instConcreteCategoryLinearMapIdCarrier Hom.app	—	—
sectionsMap_comp 📖	mathematical	—	sectionsMap CategoryTheory.CategoryStruct.comp PresheafOfModules CategoryTheory.Category.toCategoryStruct instCategory	—	—
sectionsMap_id 📖	mathematical	—	sectionsMap CategoryTheory.CategoryStruct.id PresheafOfModules CategoryTheory.Category.toCategoryStruct instCategory	—	—
sectionsMk_coe 📖	mathematical	DFunLike.coe obj CategoryTheory.Functor.obj ModuleCat RingCat.carrier Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory ModuleCat.restrictScalars RingCat.Hom.hom CategoryTheory.Functor.map ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier map	Set Set.instMembership CategoryTheory.Functor.sections CategoryTheory.Functor.comp Ab AddCommGrpCat.instCategory CategoryTheory.types presheaf CategoryTheory.forget AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier sectionsMk	—	—
sections_ext 📖	—	Set Set.instMembership CategoryTheory.Functor.sections Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp Ab AddCommGrpCat.instCategory CategoryTheory.types presheaf CategoryTheory.forget AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier	—	—	—
sections_ext_iff 📖	mathematical	—	Set Set.instMembership CategoryTheory.Functor.sections Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp Ab AddCommGrpCat.instCategory CategoryTheory.types presheaf CategoryTheory.forget AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier	—	sections_ext
sections_property 📖	mathematical	—	DFunLike.coe obj CategoryTheory.Functor.obj ModuleCat RingCat.carrier Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory ModuleCat.restrictScalars RingCat.Hom.hom CategoryTheory.Functor.map ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier map Set Set.instMembership CategoryTheory.Functor.sections CategoryTheory.Functor.comp Ab AddCommGrpCat.instCategory CategoryTheory.types presheaf CategoryTheory.forget AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier	—	—
sub_app 📖	mathematical	—	Hom.app Quiver.Hom PresheafOfModules CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instSubHom ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory obj ModuleCat.instSubHom	—	—
toPresheaf_map_app_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom AddCommGrpCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Ab AddCommGrpCat.instCategory PresheafOfModules instCategory CategoryTheory.Functor CategoryTheory.Functor.category toPresheaf AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str ModuleCat.carrier RingCat.carrier RingCat RingCat.instCategory RingCat.ring obj AddMonoidHom.instFunLike AddCommGrpCat.Hom.hom CategoryTheory.NatTrans.app CategoryTheory.Functor.map CategoryTheory.ConcreteCategory.hom ModuleCat ModuleCat.moduleCategory LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier Hom.app	—	—
toPresheaf_obj_coe 📖	mathematical	—	AddCommGrpCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Ab AddCommGrpCat.instCategory PresheafOfModules instCategory CategoryTheory.Functor CategoryTheory.Functor.category toPresheaf ModuleCat.carrier RingCat.carrier RingCat RingCat.instCategory RingCat.ring obj	—	—
unitHomEquiv_apply_coe 📖	mathematical	—	Set Set.instMembership CategoryTheory.Functor.sections Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp Ab AddCommGrpCat.instCategory CategoryTheory.types presheaf CategoryTheory.forget AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier DFunLike.coe Equiv Quiver.Hom PresheafOfModules CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory unit sections EquivLike.toFunLike Equiv.instEquivLike unitHomEquiv LinearMap RingCat.carrier CategoryTheory.Functor.obj RingCat RingCat.instCategory Ring.toSemiring RingCat.ring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier obj AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat ModuleCat.moduleCategory ModuleCat.instConcreteCategoryLinearMapIdCarrier Hom.app AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	—
unit_map_one 📖	mathematical	—	DFunLike.coe obj unit CategoryTheory.Functor.obj ModuleCat RingCat.carrier Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory ModuleCat.restrictScalars RingCat.Hom.hom CategoryTheory.Functor.map ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier map AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	RingHom.map_one
zero_app 📖	mathematical	—	Hom.app Quiver.Hom PresheafOfModules CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instZeroHom ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory obj ModuleCat.instZeroHom	—	—
zsmul_app 📖	mathematical	—	Hom.app Quiver.Hom PresheafOfModules CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroupHom ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory obj ModuleCat.instSMulIntHom	—	ModuleCat.hom_ext LinearMap.ext CategoryTheory.Functor.map_zsmul CategoryTheory.Functor.instAdditiveComp instAdditiveFunctorOppositeAbToPresheaf CategoryTheory.Functor.instAdditiveObjEvaluation

PresheafOfModules.Hom

Definitions

Name	Category	Theorems
app 📖	CompOp	53 math math: PresheafOfModules.add_app, PresheafOfModules.restrictScalars_map_app, PresheafOfModules.epi_iff_surjective, PresheafOfModules.comp_app, PresheafOfModules.pushforward_map_app_apply, PresheafOfModules.toSheafify_app_apply', PresheafOfModules.free_map_app, PresheafOfModules.freeYonedaEquiv_symm_app, PresheafOfModules.id_app, PresheafOfModules.Derivation.postcomp_d_apply, PresheafOfModules.sectionsMap_coe, PresheafOfModules.pushforward_map_app_apply', PresheafOfModules.zsmul_app, PresheafOfModules.isoMk_hom_app, SheafOfModules.pushforwardComp_inv_app_val_app, PresheafOfModules.mono_iff_surjective, PresheafOfModules.limitCone_π_app_app, PresheafOfModules.instEpiModuleCatCarrierObjOppositeRingCatApp, SheafOfModules.pushforwardCongr_hom_app_val_app, PresheafOfModules.surjective_of_epi, PresheafOfModules.injective_of_mono, PresheafOfModules.isoMk_inv_app, PresheafOfModules.unitHomEquiv_apply_coe, SheafOfModules.pushforwardCongr_inv_app_val_app, SheafOfModules.pushforwardPushforwardAdj_unit_app_val_app, PresheafOfModules.homMk_app, PresheafOfModules.toPresheaf_map_app_apply, PresheafOfModules.neg_app, SheafOfModules.pushforwardComp_hom_app_val_app, PresheafOfModules.sub_app, PresheafOfModules.Elements.fromFreeYoneda_app_apply, naturality_assoc, PresheafOfModules.ι_fromFreeYonedaCoproduct_apply, SheafOfModules.unitToPushforwardObjUnit_val_app_apply, PresheafOfModules.Monoidal.tensorHom_app, PresheafOfModules.instMonoModuleCatCarrierObjOppositeRingCatApp, SheafOfModules.pushforwardNatTrans_app_val_app, PresheafOfModules.hom_ext_iff, SheafOfModules.pushforwardPushforwardEquivalence_unit_app_val_app, naturality, SheafOfModules.pushforwardPushforwardAdj_counit_app_val_app, PresheafOfModules.freeYonedaEquiv_comp, ext_iff, SheafOfModules.pushforwardNatTrans_app_val_app_apply, PresheafOfModules.colimitCocone_ι_app_app, PresheafOfModules.naturality_apply, PresheafOfModules.fromFreeYonedaCoproduct_app_mk, PresheafOfModules.toSheafify_app_apply, SheafOfModules.pushforwardPushforwardEquivalence_counit_app_val_app, PresheafOfModules.evaluation_map, PresheafOfModules.freeObjDesc_app, PresheafOfModules.zero_app, SheafOfModules.unitHomEquiv_apply_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	app	—	—	—
ext_iff 📖	mathematical	—	app	—	ext
naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory PresheafOfModules.obj ModuleCat.restrictScalars RingCat.Hom.hom CategoryTheory.Functor.map PresheafOfModules.map app	—	—
naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory PresheafOfModules.obj ModuleCat.restrictScalars RingCat.Hom.hom CategoryTheory.Functor.map PresheafOfModules.map app	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' naturality

PresheafOfModules.sections

Definitions

Name	Category	Theorems
eval 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
PresheafOfModules 📖	CompData	123 math math: PresheafOfModules.instAdditiveRestrictScalars, PresheafOfModules.hasFiniteLimits, PresheafOfModules.instIsRightAdjointPushforwardCompFunctorOppositeRingCatWhiskerLeftOp, PresheafOfModules.pullback_id_comp, PresheafOfModules.instIsLocallySurjectiveToSheafify, PresheafOfModules.add_app, PresheafOfModules.toPresheaf_preservesFiniteLimits, PresheafOfModules.restrictScalars_map_app, SheafOfModules.instFullPresheafOfModulesValRingCatForget, PresheafOfModules.epi_iff_surjective, PresheafOfModules.pullback_comp_id, PresheafOfModules.Finite.hasFiniteColimits, PresheafOfModules.evaluation_preservesColimitsOfShape, PresheafOfModules.comp_app, PresheafOfModules.homEquivOfIsLocallyBijective_symm_apply, PresheafOfModules.pushforward_map_app_apply, PresheafOfModules.toSheafify_app_apply', PresheafOfModules.instPreservesLimitsOfShapeModuleCatCarrierObjOppositeRingCatEvaluation, PresheafOfModules.toFreeYonedaCoproduct_fromFreeYonedaCoproduct, PresheafOfModules.instIsLeftAdjointSheafOfModulesSheafification, PresheafOfModules.sectionsMap_comp, PresheafOfModules.free_map_app, PresheafOfModules.ι_fromFreeYonedaCoproduct, PresheafOfModules.freeYonedaEquiv_symm_app, PresheafOfModules.id_app, PresheafOfModules.toPresheaf_map_toSheafify, PresheafOfModules.pushforward_map_app_apply', PresheafOfModules.instFaithfulFunctorOppositeAbToPresheaf, PresheafOfModules.zsmul_app, PresheafOfModules.toPresheaf_obj_coe, PresheafOfModules.isoMk_hom_app, PresheafOfModules.instPreservesLimitsOfSizeModuleCatCarrierObjOppositeRingCatEvaluation, PresheafOfModules.instIsNormalMonoCategory, PresheafOfModules.freeYoneda.isSeparating, PresheafOfModules.epi_of_surjective, SheafOfModules.restrictScalars_obj_val, PresheafOfModules.mono_iff_surjective, SheafOfModules.instReflectsIsomorphismsPresheafOfModulesValRingCatForget, SheafOfModules.instFaithfulPresheafOfModulesValRingCatForget, SheafOfModules.toSheaf_map_val, PresheafOfModules.pullback_assoc, SheafOfModules.instSmallElemForallObjCompModuleCatCarrierOppositeRingCatValPresheafOfModulesForgetEvaluationForgetLinearMapIdCarrierSections, PresheafOfModules.sheafification_map, PresheafOfModules.toFreeYonedaCoproduct_fromFreeYonedaCoproduct_assoc, PresheafOfModules.toSheaf_map_sheafificationHomEquiv_symm, PresheafOfModules.isoMk_inv_app, SheafOfModules.id_val, PresheafOfModules.pushforward_obj_map_apply, PresheafOfModules.homEquivOfIsLocallyBijective_apply, PresheafOfModules.freeYoneda.isDetecting, PresheafOfModules.unitHomEquiv_apply_coe, PresheafOfModules.instIsNormalEpiCategory, PresheafOfModules.ι_fromFreeYonedaCoproduct_assoc, SheafOfModules.fullyFaithfulForget_preimage_val, PresheafOfModules.hasColimitsOfShape, SheafOfModules.restrictScalars_map_val, PresheafOfModules.freeYoneda.instSmall, PresheafOfModules.toPresheaf_map_app_apply, PresheafOfModules.neg_app, PresheafOfModules.instPreservesLimitsOfShapeFunctorOppositeAbToPresheaf, SheafOfModules.pushforward_map_val, PresheafOfModules.evaluation_preservesColimitsOfSize, PresheafOfModules.evaluation_preservesFiniteLimits, PresheafOfModules.instPreservesLimitsOfSizeFunctorOppositeAbToPresheaf, PresheafOfModules.sub_app, PresheafOfModules.Elements.fromFreeYoneda_app_apply, PresheafOfModules.mono_of_injective, PresheafOfModules.pushforward_obj_obj, PresheafOfModules.restrictScalars_obj, PresheafOfModules.instFaithfulRestrictScalars, PresheafOfModules.instAdditiveModuleCatCarrierObjOppositeRingCatEvaluation, SheafOfModules.add_val, PresheafOfModules.comp_toPresheaf_map_sheafifyHomEquiv'_symm_hom, PresheafOfModules.instEpiFromFreeYonedaCoproduct, PresheafOfModules.restriction_app, PresheafOfModules.free_obj, PresheafOfModules.forgetToPresheafModuleCat_obj, PresheafOfModules.Finite.toPresheaf_preservesFiniteColimits, SheafOfModules.forget_map, SheafOfModules.forgetPreservesLimitsOfSize, PresheafOfModules.pullbackObjIsDefined_free_yoneda, PresheafOfModules.toPresheaf_preservesColimitsOfShape, SheafOfModules.Finite.forgetPreservesFiniteLimits, SheafOfModules.forget_obj, SheafOfModules.comp_val_assoc, PresheafOfModules.sectionsMap_id, PresheafOfModules.hasLimitsOfSize, PresheafOfModules.pushforward_assoc, PresheafOfModules.pushforward_obj_map_apply', SheafOfModules.forgetToSheafModuleCat_map_val, PresheafOfModules.hasLimitsOfShape, PresheafOfModules.freeAdjunction_unit_app, PresheafOfModules.freeYonedaEquiv_comp, PresheafOfModules.sheafificationAdjunction_homEquiv_apply, PresheafOfModules.hasColimitsOfSize, PresheafOfModules.toPresheaf_preservesColimitsOfSize, SheafOfModules.forgetPreservesLimitsOfShape, PresheafOfModules.wellPowered, PresheafOfModules.Finite.evaluation_preservesFiniteColimits, SheafOfModules.comp_val, PresheafOfModules.pullbackObjIsDefined_eq_top, PresheafOfModules.toPresheaf_map_sheafificationAdjunction_unit_app, PresheafOfModules.instIsRightAdjointPushforward, PresheafOfModules.instIsLocallyInjectiveToSheafify, PresheafOfModules.toPresheaf_map_sheafificationHomEquiv_def, PresheafOfModules.instFullRestrictScalarsIdFunctorOppositeRingCat, PresheafOfModules.fromFreeYonedaCoproduct_app_mk, PresheafOfModules.toSheafify_app_apply, PresheafOfModules.freeAdjunction_homEquiv, SheafOfModules.forgetToSheafModuleCat_obj_val, PresheafOfModules.evaluation_obj, PresheafOfModules.pushforward_id_comp, PresheafOfModules.evaluation_map, SheafOfModules.pushforward_obj_val, PresheafOfModules.instAdditiveFunctorOppositeAbToPresheaf, PresheafOfModules.zero_app, PresheafOfModules.forgetToPresheafModuleCat_map, PresheafOfModules.toPresheaf_map_sheafificationHomEquiv, PresheafOfModules.instIsRightAdjointPushforwardIdFunctorOppositeRingCat, SheafOfModules.instAdditivePresheafOfModulesValRingCatForget, PresheafOfModules.pushforward_comp_id, PresheafOfModules.instPreservesFiniteLimitsSheafOfModulesSheafification, PresheafOfModules.instPreservesFiniteLimitsSheafAddCommGrpCatCompSheafOfModulesSheafificationToSheaf

---

← Back to Index