Sheaf

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

Statistics

Metric	Count
Definitions IsLocallyInjective, IsLocallySurjective, homEquivOfIsLocallyBijective, SheafOfModules, val, evaluation, forget, forgetToSheafModuleCat, fullyFaithfulForget, instAddCommGroupHom, instCategory, instPreadditive, sections, sectionsFunctor, sectionsMap, toSheaf, toSheafCompSheafToPresheafIso, unit, unitHomEquiv, val	20
Theorems homEquivOfIsLocallyBijective_apply, homEquivOfIsLocallyBijective_symm_apply, ext, ext_iff, add_val, comp_val, comp_val_assoc, forgetToSheafModuleCat_map_hom, forgetToSheafModuleCat_obj_obj, forget_map, forget_obj, fullyFaithfulForget_preimage_val, hom_ext, hom_ext_iff, id_val, instAdditivePresheafOfModulesObjFunctorOppositeRingCatIsSheafForget, instAdditiveSheafAddCommGrpCatToSheaf, instFaithfulPresheafOfModulesObjFunctorOppositeRingCatIsSheafForget, instFaithfulSheafAddCommGrpCatToSheaf, instFullPresheafOfModulesObjFunctorOppositeRingCatIsSheafForget, instReflectsIsomorphismsPresheafOfModulesObjFunctorOppositeRingCatIsSheafForget, isSheaf, sectionsFunctor_map, sectionsFunctor_obj, sectionsMap_comp, sectionsMap_id, toSheaf_map_hom, toSheaf_obj_obj, unitHomEquiv_apply_coe, unitHomEquiv_comp_apply, unitHomEquiv_symm_comp, unit_val	32
Total	52

PresheafOfModules

Definitions

Name	Category	Theorems
IsLocallyInjective 📖	MathDef	1 math math: instIsLocallyInjectiveToSheafify
IsLocallySurjective 📖	MathDef	1 math math: instIsLocallySurjectiveToSheafify
homEquivOfIsLocallyBijective 📖	CompOp	2 math math: homEquivOfIsLocallyBijective_symm_apply, homEquivOfIsLocallyBijective_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
homEquivOfIsLocallyBijective_apply 📖	mathematical	CategoryTheory.Presheaf.IsSheaf Ab AddCommGrpCat.instCategory presheaf	DFunLike.coe Equiv Quiver.Hom PresheafOfModules CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory EquivLike.toFunLike Equiv.instEquivLike homEquivOfIsLocallyBijective CategoryTheory.CategoryStruct.comp	—	—
homEquivOfIsLocallyBijective_symm_apply 📖	mathematical	CategoryTheory.Presheaf.IsSheaf Ab AddCommGrpCat.instCategory presheaf	DFunLike.coe Equiv Quiver.Hom PresheafOfModules CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory EquivLike.toFunLike Equiv.instEquivLike Equiv.symm homEquivOfIsLocallyBijective homMk CategoryTheory.Functor Opposite CategoryTheory.Category.opposite Ab AddCommGrpCat.instCategory CategoryTheory.Functor.category CategoryTheory.Functor.obj toPresheaf presheaf CategoryTheory.ObjectProperty.isLocal.homEquiv CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.map	—	—

SheafOfModules

Definitions

Name	Category	Theorems
evaluation 📖	CompOp	10 math math: evaluationPreservesLimit, evaluationPreservesLimitsOfShape, evaluationPreservesLimitsOfSize, Presentation.map_relations_I, Presentation.mapRelations_mapGenerators, relationsOfIsCokernelFree_I, Presentation.mapRelations_mapGenerators_assoc, relationsOfIsCokernelFree_s, Presentation.IsFinite.finite_relations, Finite.evaluationPreservesFiniteLimits
forget 📖	CompOp	21 math math: instAdditivePresheafOfModulesObjFunctorOppositeRingCatIsSheafForget, PresheafOfModules.instFullSheafOfModulesCompObjFunctorOppositeRingCatIsSheafForgetRestrictScalars, PresheafOfModules.toSheaf_map_sheafificationAdjunction_counit_app, instSmallElemForallObjCompModuleCatCarrierOppositeRingCatObjFunctorIsSheafPresheafOfModulesForgetEvaluationForgetLinearMapIdCarrierSections, PresheafOfModules.toSheaf_map_sheafificationHomEquiv_symm, PresheafOfModules.instIsIsoFunctorSheafOfModulesCounitSheafificationAdjunction, fullyFaithfulForget_preimage_val, PresheafOfModules.instFaithfulSheafOfModulesCompObjFunctorOppositeRingCatIsSheafForgetRestrictScalars, forget_map, forgetPreservesLimitsOfSize, instFaithfulPresheafOfModulesObjFunctorOppositeRingCatIsSheafForget, Finite.forgetPreservesFiniteLimits, forget_obj, toSheaf_map_hom, instReflectsIsomorphismsPresheafOfModulesObjFunctorOppositeRingCatIsSheafForget, PresheafOfModules.sheafificationAdjunction_homEquiv_apply, forgetPreservesLimitsOfShape, PresheafOfModules.toPresheaf_map_sheafificationAdjunction_unit_app, PresheafOfModules.toPresheaf_map_sheafificationHomEquiv_def, instFullPresheafOfModulesObjFunctorOppositeRingCatIsSheafForget, PresheafOfModules.toPresheaf_map_sheafificationHomEquiv
forgetToSheafModuleCat 📖	CompOp	2 math math: forgetToSheafModuleCat_map_hom, forgetToSheafModuleCat_obj_obj
fullyFaithfulForget 📖	CompOp	1 math math: fullyFaithfulForget_preimage_val
instAddCommGroupHom 📖	CompOp	1 math math: add_val
instCategory 📖	CompOp	138 math math: pushforward_assoc, instAdditivePresheafOfModulesObjFunctorOppositeRingCatIsSheafForget, hasLimitsOfSize, pushforwardNatIso_inv, sectionsMap_id, instAdditiveRestrictScalars, pullbackPushforwardAdjunction_homEquiv_pullbackObjUnitToUnit, evaluationPreservesLimit, instPreservesColimitsOfSizeFreeFunctor, forgetToSheafModuleCat_map_hom, inl_freeSumIso_hom, unitHomEquiv_symm_comp, PresheafOfModules.instIsLeftAdjointSheafOfModulesSheafification, freeHomEquiv_freeMap, inr_freeSumIso_hom, instHasColimitsOfShapeOfPresheafOfModulesObjFunctorOppositeRingCatIsSheaf, instIsRightAdjointPushforwardCompSheafRingCatMapSheafPushforwardContinuous, evaluationPreservesLimitsOfShape, unitHomEquiv_symm_freeHomEquiv_apply, GeneratingSections.epi, GeneratingSections.opEpi_comp, instIsLeftAdjointPullback, PresheafOfModules.instFullSheafOfModulesCompObjFunctorOppositeRingCatIsSheafForgetRestrictScalars, ιFree_mapFree_inv_assoc, pullback_map_ιFree_comp_pullbackObjFreeIso_hom_assoc, evaluationPreservesLimitsOfSize, pushforwardComp_inv_app_val_app, PresheafOfModules.toSheaf_map_sheafificationAdjunction_counit_app, pushforwardNatTrans_id, restrictScalars_obj_val, instSmallElemForallObjCompModuleCatCarrierOppositeRingCatObjFunctorIsSheafPresheafOfModulesForgetEvaluationForgetLinearMapIdCarrierSections, instAdditiveSheafAddCommGrpCatToSheaf, sectionsFunctor_obj, PresheafOfModules.instReflectsIsomorphismsSheafOfModulesSheafAddCommGrpCatToSheaf_1, sectionsFunctor_map, freeHomEquiv_symm_comp, Presentation.quasicoherentData_presentation, pushforwardCongr_hom_app_val_app, pullbackObjFreeIso_hom_naturality_assoc, PresheafOfModules.sheafification_map, pullback_comp_id, instPreservesFiniteLimitsFunctorOppositeAddCommGrpCatCompSheafToSheafSheafToPresheaf, freeHomEquiv_comp_apply, PresheafOfModules.toSheaf_map_sheafificationHomEquiv_symm, instPreservesColimitsOfSize, id_val, PresheafOfModules.instIsIsoFunctorSheafOfModulesCounitSheafificationAdjunction, ιFree_freeMap, PresheafOfModules.inverseImage_W_toPresheaf_eq_inverseImage_isomorphisms, toSheaf_obj_obj, pushforwardCongr_inv_app_val_app, freeFunctor_obj, freeFunctor_map, conjugateEquiv_pullbackComp_inv, inl_freeSumIso_hom_assoc, pushforwardPushforwardAdj_unit_app_val_app, fullyFaithfulForget_preimage_val, PresheafOfModules.instReflectsIsomorphismsSheafOfModulesSheafAddCommGrpCatToSheaf, pullback_id_comp, restrictScalars_map_val, ιFree_freeMap_assoc, inr_freeSumIso_hom_assoc, pushforward_map_val, pushforwardComp_hom_app_val_app, Presentation.map_relations_I, freeHomEquiv_apply, instIsLeftAdjointOverOverRingCatPushforwardIdSheafOver, ιFree_mapFree_inv, Presentation.mapRelations_mapGenerators, PresheafOfModules.instFaithfulSheafOfModulesCompObjFunctorOppositeRingCatIsSheafForgetRestrictScalars, relationsOfIsCokernelFree_I, instHasColimitsOfSizeOfPresheafOfModulesObjFunctorOppositeRingCatIsSheaf, hasLimitsOfShape, sectionsMap_comp, pushforwardCongr_symm, add_val, instFaithfulSheafAddCommGrpCatToSheaf, unitHomEquiv_comp_apply, unitToPushforwardObjUnit_val_app_apply, pullback_assoc, forget_map, Presentation.of_isIso_relations, forgetPreservesLimitsOfSize, instFaithfulPresheafOfModulesObjFunctorOppositeRingCatIsSheafForget, Finite.forgetPreservesFiniteLimits, Presentation.mapRelations_mapGenerators_assoc, forget_obj, GeneratingSections.ofEpi_π, comp_val_assoc, map_ιFree_mapFree_hom, toSheaf_map_hom, instIsIsoPullbackObjUnitToUnitOfFinal, pushforwardNatTrans_app_val_app, Finite.hasFiniteLimits, PresheafOfModules.instIsLocalizationSheafOfModulesSheafificationInverseImageFunctorOppositeAbWToPresheaf, pullbackPushforwardAdjunction_homEquiv_symm_unitToPushforwardObjUnit, instReflectsIsomorphismsPresheafOfModulesObjFunctorOppositeRingCatIsSheafForget, instIsRightAdjointPushforward, pushforwardPushforwardEquivalence_unit_app_val_app, pushforward_comp_id, relationsOfIsCokernelFree_s, forgetToSheafModuleCat_obj_obj, bijective_pushforwardSections, pullbackObjFreeIso_hom_naturality, pushforwardPushforwardAdj_counit_app_val_app, conjugateEquiv_pullbackId_hom, Presentation.map_generators_I, pullback_map_ιFree_comp_pullbackObjFreeIso_hom, PresheafOfModules.sheafificationAdjunction_homEquiv_apply, instPreservesFiniteLimitsSheafAddCommGrpCatToSheaf, map_ιFree_mapFree_hom_assoc, forgetPreservesLimitsOfShape, Presentation.IsFinite.finite_relations, pushforwardNatTrans_app_val_app_apply, sectionsMap_freeHomEquiv_symm_freeSection, comp_val, PresheafOfModules.instReflectsFiniteLimitsSheafOfModulesSheafAddCommGrpCatToSheaf, PresheafOfModules.toPresheaf_map_sheafificationAdjunction_unit_app, pushforward_id_comp, hasLimit, PresheafOfModules.toPresheaf_map_sheafificationHomEquiv_def, pushforwardSections_coe, pushforwardSections_unitHomEquiv, instIsRightAdjointPushforwardIdSheafRingCat, instFullPresheafOfModulesObjFunctorOppositeRingCatIsSheafForget, generatorsOfIsCokernelFree_s, pushforwardNatIso_hom, pushforwardPushforwardEquivalence_counit_app_val_app, pushforward_obj_val, GeneratingSections.opEpi_id, PresheafOfModules.toPresheaf_map_sheafificationHomEquiv, Presentation.map_π_eq, Finite.evaluationPreservesFiniteLimits, freeCofan_inj, pushforwardNatTrans_comp, PresheafOfModules.instPreservesFiniteLimitsSheafOfModulesSheafification, PresheafOfModules.instPreservesFiniteLimitsSheafAddCommGrpCatCompSheafOfModulesSheafificationToSheaf, unitHomEquiv_apply_coe
instPreadditive 📖	CompOp	10 math math: instAdditivePresheafOfModulesObjFunctorOppositeRingCatIsSheafForget, instAdditiveRestrictScalars, instAdditiveSheafAddCommGrpCatToSheaf, Presentation.map_relations_I, Presentation.mapRelations_mapGenerators, relationsOfIsCokernelFree_I, Presentation.of_isIso_relations, Presentation.mapRelations_mapGenerators_assoc, relationsOfIsCokernelFree_s, Presentation.IsFinite.finite_relations
sections 📖	CompOp	8 math math: unitHomEquiv_symm_comp, freeHomEquiv_freeMap, unitHomEquiv_symm_freeHomEquiv_apply, sectionsFunctor_obj, unitHomEquiv_comp_apply, bijective_pushforwardSections, pushforwardSections_unitHomEquiv, unitHomEquiv_apply_coe
sectionsFunctor 📖	CompOp	2 math math: sectionsFunctor_obj, sectionsFunctor_map
sectionsMap 📖	CompOp	11 math math: sectionsMap_id, unitHomEquiv_symm_comp, sectionsFunctor_map, freeHomEquiv_symm_comp, sectionMap_freeMap_freeSection, freeHomEquiv_comp_apply, freeHomEquiv_apply, sectionsMap_comp, unitHomEquiv_comp_apply, GeneratingSections.ofEpi_s, sectionsMap_freeHomEquiv_symm_freeSection
toSheaf 📖	CompOp	13 math math: PresheafOfModules.toSheaf_map_sheafificationAdjunction_counit_app, instAdditiveSheafAddCommGrpCatToSheaf, PresheafOfModules.instReflectsIsomorphismsSheafOfModulesSheafAddCommGrpCatToSheaf_1, instPreservesFiniteLimitsFunctorOppositeAddCommGrpCatCompSheafToSheafSheafToPresheaf, PresheafOfModules.toSheaf_map_sheafificationHomEquiv_symm, toSheaf_obj_obj, PresheafOfModules.instReflectsIsomorphismsSheafOfModulesSheafAddCommGrpCatToSheaf, instFaithfulSheafAddCommGrpCatToSheaf, toSheaf_map_hom, instPreservesFiniteLimitsSheafAddCommGrpCatToSheaf, PresheafOfModules.instReflectsFiniteLimitsSheafOfModulesSheafAddCommGrpCatToSheaf, PresheafOfModules.toPresheaf_map_sheafificationHomEquiv, PresheafOfModules.instPreservesFiniteLimitsSheafAddCommGrpCatCompSheafOfModulesSheafificationToSheaf
toSheafCompSheafToPresheafIso 📖	CompOp	—
unit 📖	CompOp	21 math math: pullbackPushforwardAdjunction_homEquiv_pullbackObjUnitToUnit, unitHomEquiv_symm_comp, unitHomEquiv_symm_freeHomEquiv_apply, ιFree_mapFree_inv_assoc, pullback_map_ιFree_comp_pullbackObjFreeIso_hom_assoc, Presentation.quasicoherentData_presentation, ιFree_freeMap, ιFree_freeMap_assoc, unit_val, ιFree_mapFree_inv, unitHomEquiv_comp_apply, unitToPushforwardObjUnit_val_app_apply, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓUnitOpensCarrierCarrierCommRingCatRingCatSheaf, map_ιFree_mapFree_hom, instIsIsoPullbackObjUnitToUnitOfFinal, pullbackPushforwardAdjunction_homEquiv_symm_unitToPushforwardObjUnit, pullback_map_ιFree_comp_pullbackObjFreeIso_hom, map_ιFree_mapFree_hom_assoc, pushforwardSections_unitHomEquiv, freeCofan_inj, unitHomEquiv_apply_coe
unitHomEquiv 📖	CompOp	5 math math: unitHomEquiv_symm_comp, unitHomEquiv_symm_freeHomEquiv_apply, unitHomEquiv_comp_apply, pushforwardSections_unitHomEquiv, unitHomEquiv_apply_coe
val 📖	CompOp	36 math math: PresheafOfModules.instIsLocallySurjectiveToSheafify, forgetToSheafModuleCat_map_hom, PresheafOfModules.toSheafify_app_apply', PresheafOfModules.toPresheaf_map_toSheafify, isSheaf, pushforwardComp_inv_app_val_app, restrictScalars_obj_val, pushforwardCongr_hom_app_val_app, id_val, toSheaf_obj_obj, pushforwardCongr_inv_app_val_app, pushforwardPushforwardAdj_unit_app_val_app, restrictScalars_map_val, pushforward_map_val, pushforwardComp_hom_app_val_app, unit_val, add_val, PresheafOfModules.sheafifyMap_val, PresheafOfModules.comp_toPresheaf_map_sheafifyHomEquiv'_symm_hom, unitToPushforwardObjUnit_val_app_apply, forget_obj, comp_val_assoc, toSheaf_map_hom, pushforwardNatTrans_app_val_app, pushforwardPushforwardEquivalence_unit_app_val_app, forgetToSheafModuleCat_obj_obj, pushforwardPushforwardAdj_counit_app_val_app, pushforwardNatTrans_app_val_app_apply, comp_val, PresheafOfModules.instIsLocallyInjectiveToSheafify, PresheafOfModules.toPresheaf_map_sheafificationHomEquiv_def, pushforwardSections_coe, PresheafOfModules.toSheafify_app_apply, pushforwardPushforwardEquivalence_counit_app_val_app, pushforward_obj_val, unitHomEquiv_apply_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_val 📖	mathematical	—	Hom.val Quiver.Hom SheafOfModules CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid instAddCommGroupHom PresheafOfModules CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf PresheafOfModules.instCategory val PresheafOfModules.instAddHom	—	—
comp_val 📖	mathematical	—	Hom.val CategoryTheory.CategoryStruct.comp SheafOfModules CategoryTheory.Category.toCategoryStruct instCategory PresheafOfModules CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf PresheafOfModules.instCategory val	—	—
comp_val_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp PresheafOfModules CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Category.toCategoryStruct PresheafOfModules.instCategory val Hom.val SheafOfModules instCategory	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_val
forgetToSheafModuleCat_map_hom 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Functor Opposite CategoryTheory.Category.opposite ModuleCat RingCat.carrier CategoryTheory.Functor.obj RingCat RingCat.instCategory CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf RingCat.ring ModuleCat.moduleCategory PresheafOfModules PresheafOfModules.instCategory PresheafOfModules.forgetToPresheafModuleCat val CategoryTheory.Functor.map SheafOfModules instCategory CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category forgetToSheafModuleCat Hom.val	—	—
forgetToSheafModuleCat_obj_obj 📖	mathematical	—	CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite ModuleCat RingCat.carrier CategoryTheory.Functor.obj RingCat RingCat.instCategory CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf RingCat.ring ModuleCat.moduleCategory SheafOfModules instCategory CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category forgetToSheafModuleCat PresheafOfModules PresheafOfModules.instCategory PresheafOfModules.forgetToPresheafModuleCat val	—	—
forget_map 📖	mathematical	—	CategoryTheory.Functor.map SheafOfModules instCategory PresheafOfModules CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf PresheafOfModules.instCategory forget Hom.val	—	—
forget_obj 📖	mathematical	—	CategoryTheory.Functor.obj SheafOfModules instCategory PresheafOfModules CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf PresheafOfModules.instCategory forget val	—	—
fullyFaithfulForget_preimage_val 📖	mathematical	—	Hom.val CategoryTheory.Functor.FullyFaithful.preimage SheafOfModules instCategory PresheafOfModules CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf PresheafOfModules.instCategory forget fullyFaithfulForget	—	—
hom_ext 📖	—	Hom.val	—	—	Hom.ext
hom_ext_iff 📖	mathematical	—	Hom.val	—	hom_ext
id_val 📖	mathematical	—	Hom.val CategoryTheory.CategoryStruct.id SheafOfModules CategoryTheory.Category.toCategoryStruct instCategory PresheafOfModules CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf PresheafOfModules.instCategory val	—	—
instAdditivePresheafOfModulesObjFunctorOppositeRingCatIsSheafForget 📖	mathematical	—	CategoryTheory.Functor.Additive SheafOfModules PresheafOfModules CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf instCategory PresheafOfModules.instCategory instPreadditive PresheafOfModules.instPreadditive forget	—	—
instAdditiveSheafAddCommGrpCatToSheaf 📖	mathematical	—	CategoryTheory.Functor.Additive SheafOfModules CategoryTheory.Sheaf AddCommGrpCat AddCommGrpCat.instCategory instCategory CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf instPreadditive CategoryTheory.Preadditive.fullSubcategory CategoryTheory.functorCategoryPreadditive AddCommGrpCat.instPreadditive toSheaf	—	—
instFaithfulPresheafOfModulesObjFunctorOppositeRingCatIsSheafForget 📖	mathematical	—	CategoryTheory.Functor.Faithful SheafOfModules instCategory PresheafOfModules CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf PresheafOfModules.instCategory forget	—	CategoryTheory.Functor.FullyFaithful.faithful
instFaithfulSheafAddCommGrpCatToSheaf 📖	mathematical	—	CategoryTheory.Functor.Faithful SheafOfModules instCategory CategoryTheory.Sheaf AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf toSheaf	—	CategoryTheory.Functor.Faithful.of_comp_iso CategoryTheory.Functor.Faithful.comp instFaithfulPresheafOfModulesObjFunctorOppositeRingCatIsSheafForget PresheafOfModules.instFaithfulFunctorOppositeAbToPresheaf
instFullPresheafOfModulesObjFunctorOppositeRingCatIsSheafForget 📖	mathematical	—	CategoryTheory.Functor.Full SheafOfModules instCategory PresheafOfModules CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf PresheafOfModules.instCategory forget	—	CategoryTheory.Functor.FullyFaithful.full
instReflectsIsomorphismsPresheafOfModulesObjFunctorOppositeRingCatIsSheafForget 📖	mathematical	—	CategoryTheory.Functor.ReflectsIsomorphisms SheafOfModules instCategory PresheafOfModules CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf PresheafOfModules.instCategory forget	—	CategoryTheory.Functor.FullyFaithful.reflectsIsomorphisms
isSheaf 📖	mathematical	—	CategoryTheory.Presheaf.IsSheaf Ab AddCommGrpCat.instCategory PresheafOfModules.presheaf CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Functor.category val	—	—
sectionsFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map SheafOfModules instCategory CategoryTheory.types sectionsFunctor sectionsMap	—	—
sectionsFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj SheafOfModules instCategory CategoryTheory.types sectionsFunctor sections	—	—
sectionsMap_comp 📖	mathematical	—	sectionsMap CategoryTheory.CategoryStruct.comp SheafOfModules CategoryTheory.Category.toCategoryStruct instCategory	—	—
sectionsMap_id 📖	mathematical	—	sectionsMap CategoryTheory.CategoryStruct.id SheafOfModules CategoryTheory.Category.toCategoryStruct instCategory	—	—
toSheaf_map_hom 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Functor Opposite CategoryTheory.Category.opposite AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.ObjectProperty.FullSubcategory.obj PresheafOfModules.presheaf RingCat RingCat.instCategory val isSheaf CategoryTheory.Functor.map SheafOfModules instCategory CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category toSheaf Ab CategoryTheory.Functor.comp PresheafOfModules PresheafOfModules.instCategory forget PresheafOfModules.toPresheaf	—	isSheaf
toSheaf_obj_obj 📖	mathematical	—	CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.obj SheafOfModules instCategory CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category toSheaf PresheafOfModules.presheaf RingCat RingCat.instCategory val	—	—
unitHomEquiv_apply_coe 📖	mathematical	—	Set Set.instMembership CategoryTheory.Functor.sections Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp Ab AddCommGrpCat.instCategory CategoryTheory.types PresheafOfModules.presheaf CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor RingCat RingCat.instCategory CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf val 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 SheafOfModules CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory unit sections EquivLike.toFunLike Equiv.instEquivLike unitHomEquiv PresheafOfModules.obj ModuleCat.carrier RingCat.carrier CategoryTheory.Functor.obj 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 PresheafOfModules.Hom.app Hom.val AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	—
unitHomEquiv_comp_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom SheafOfModules CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory unit sections EquivLike.toFunLike Equiv.instEquivLike unitHomEquiv CategoryTheory.CategoryStruct.comp sectionsMap	—	—
unitHomEquiv_symm_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SheafOfModules CategoryTheory.Category.toCategoryStruct instCategory unit DFunLike.coe Equiv sections Quiver.Hom CategoryTheory.CategoryStruct.toQuiver EquivLike.toFunLike Equiv.instEquivLike Equiv.symm unitHomEquiv sectionsMap	—	Equiv.injective Equiv.apply_symm_apply
unit_val 📖	mathematical	—	val unit PresheafOfModules.unit CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf	—	—

SheafOfModules.Hom

Definitions

Name	Category	Theorems
val 📖	CompOp	25 math math: SheafOfModules.forgetToSheafModuleCat_map_hom, SheafOfModules.pushforwardComp_inv_app_val_app, SheafOfModules.pushforwardCongr_hom_app_val_app, SheafOfModules.id_val, SheafOfModules.pushforwardCongr_inv_app_val_app, SheafOfModules.pushforwardPushforwardAdj_unit_app_val_app, SheafOfModules.fullyFaithfulForget_preimage_val, SheafOfModules.restrictScalars_map_val, SheafOfModules.pushforward_map_val, SheafOfModules.pushforwardComp_hom_app_val_app, SheafOfModules.add_val, PresheafOfModules.sheafifyMap_val, SheafOfModules.unitToPushforwardObjUnit_val_app_apply, SheafOfModules.forget_map, SheafOfModules.comp_val_assoc, SheafOfModules.hom_ext_iff, SheafOfModules.pushforwardNatTrans_app_val_app, SheafOfModules.pushforwardPushforwardEquivalence_unit_app_val_app, SheafOfModules.pushforwardPushforwardAdj_counit_app_val_app, SheafOfModules.pushforwardNatTrans_app_val_app_apply, SheafOfModules.comp_val, PresheafOfModules.toPresheaf_map_sheafificationHomEquiv_def, ext_iff, SheafOfModules.pushforwardPushforwardEquivalence_counit_app_val_app, SheafOfModules.unitHomEquiv_apply_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	val	—	—	—
ext_iff 📖	mathematical	—	val	—	ext

(root)

Definitions

Name	Category	Theorems
SheafOfModules 📖	CompData	138 math math: SheafOfModules.pushforward_assoc, SheafOfModules.instAdditivePresheafOfModulesObjFunctorOppositeRingCatIsSheafForget, SheafOfModules.hasLimitsOfSize, SheafOfModules.pushforwardNatIso_inv, SheafOfModules.sectionsMap_id, SheafOfModules.instAdditiveRestrictScalars, SheafOfModules.pullbackPushforwardAdjunction_homEquiv_pullbackObjUnitToUnit, SheafOfModules.evaluationPreservesLimit, SheafOfModules.instPreservesColimitsOfSizeFreeFunctor, SheafOfModules.forgetToSheafModuleCat_map_hom, SheafOfModules.inl_freeSumIso_hom, SheafOfModules.unitHomEquiv_symm_comp, PresheafOfModules.instIsLeftAdjointSheafOfModulesSheafification, SheafOfModules.freeHomEquiv_freeMap, SheafOfModules.inr_freeSumIso_hom, SheafOfModules.instHasColimitsOfShapeOfPresheafOfModulesObjFunctorOppositeRingCatIsSheaf, SheafOfModules.instIsRightAdjointPushforwardCompSheafRingCatMapSheafPushforwardContinuous, SheafOfModules.evaluationPreservesLimitsOfShape, SheafOfModules.unitHomEquiv_symm_freeHomEquiv_apply, SheafOfModules.GeneratingSections.epi, SheafOfModules.GeneratingSections.opEpi_comp, SheafOfModules.instIsLeftAdjointPullback, PresheafOfModules.instFullSheafOfModulesCompObjFunctorOppositeRingCatIsSheafForgetRestrictScalars, SheafOfModules.ιFree_mapFree_inv_assoc, SheafOfModules.pullback_map_ιFree_comp_pullbackObjFreeIso_hom_assoc, SheafOfModules.evaluationPreservesLimitsOfSize, SheafOfModules.pushforwardComp_inv_app_val_app, PresheafOfModules.toSheaf_map_sheafificationAdjunction_counit_app, SheafOfModules.pushforwardNatTrans_id, SheafOfModules.restrictScalars_obj_val, SheafOfModules.instSmallElemForallObjCompModuleCatCarrierOppositeRingCatObjFunctorIsSheafPresheafOfModulesForgetEvaluationForgetLinearMapIdCarrierSections, SheafOfModules.instAdditiveSheafAddCommGrpCatToSheaf, SheafOfModules.sectionsFunctor_obj, PresheafOfModules.instReflectsIsomorphismsSheafOfModulesSheafAddCommGrpCatToSheaf_1, SheafOfModules.sectionsFunctor_map, SheafOfModules.freeHomEquiv_symm_comp, SheafOfModules.Presentation.quasicoherentData_presentation, SheafOfModules.pushforwardCongr_hom_app_val_app, SheafOfModules.pullbackObjFreeIso_hom_naturality_assoc, PresheafOfModules.sheafification_map, SheafOfModules.pullback_comp_id, SheafOfModules.instPreservesFiniteLimitsFunctorOppositeAddCommGrpCatCompSheafToSheafSheafToPresheaf, SheafOfModules.freeHomEquiv_comp_apply, PresheafOfModules.toSheaf_map_sheafificationHomEquiv_symm, SheafOfModules.instPreservesColimitsOfSize, SheafOfModules.id_val, PresheafOfModules.instIsIsoFunctorSheafOfModulesCounitSheafificationAdjunction, SheafOfModules.ιFree_freeMap, PresheafOfModules.inverseImage_W_toPresheaf_eq_inverseImage_isomorphisms, SheafOfModules.toSheaf_obj_obj, SheafOfModules.pushforwardCongr_inv_app_val_app, SheafOfModules.freeFunctor_obj, SheafOfModules.freeFunctor_map, SheafOfModules.conjugateEquiv_pullbackComp_inv, SheafOfModules.inl_freeSumIso_hom_assoc, SheafOfModules.pushforwardPushforwardAdj_unit_app_val_app, SheafOfModules.fullyFaithfulForget_preimage_val, PresheafOfModules.instReflectsIsomorphismsSheafOfModulesSheafAddCommGrpCatToSheaf, SheafOfModules.pullback_id_comp, SheafOfModules.restrictScalars_map_val, SheafOfModules.ιFree_freeMap_assoc, SheafOfModules.inr_freeSumIso_hom_assoc, SheafOfModules.pushforward_map_val, SheafOfModules.pushforwardComp_hom_app_val_app, SheafOfModules.Presentation.map_relations_I, SheafOfModules.freeHomEquiv_apply, SheafOfModules.instIsLeftAdjointOverOverRingCatPushforwardIdSheafOver, SheafOfModules.ιFree_mapFree_inv, SheafOfModules.Presentation.mapRelations_mapGenerators, PresheafOfModules.instFaithfulSheafOfModulesCompObjFunctorOppositeRingCatIsSheafForgetRestrictScalars, SheafOfModules.relationsOfIsCokernelFree_I, SheafOfModules.instHasColimitsOfSizeOfPresheafOfModulesObjFunctorOppositeRingCatIsSheaf, SheafOfModules.hasLimitsOfShape, SheafOfModules.sectionsMap_comp, SheafOfModules.pushforwardCongr_symm, SheafOfModules.add_val, SheafOfModules.instFaithfulSheafAddCommGrpCatToSheaf, SheafOfModules.unitHomEquiv_comp_apply, SheafOfModules.unitToPushforwardObjUnit_val_app_apply, SheafOfModules.pullback_assoc, SheafOfModules.forget_map, SheafOfModules.Presentation.of_isIso_relations, SheafOfModules.forgetPreservesLimitsOfSize, SheafOfModules.instFaithfulPresheafOfModulesObjFunctorOppositeRingCatIsSheafForget, SheafOfModules.Finite.forgetPreservesFiniteLimits, SheafOfModules.Presentation.mapRelations_mapGenerators_assoc, SheafOfModules.forget_obj, SheafOfModules.GeneratingSections.ofEpi_π, SheafOfModules.comp_val_assoc, SheafOfModules.map_ιFree_mapFree_hom, SheafOfModules.toSheaf_map_hom, SheafOfModules.instIsIsoPullbackObjUnitToUnitOfFinal, SheafOfModules.pushforwardNatTrans_app_val_app, SheafOfModules.Finite.hasFiniteLimits, PresheafOfModules.instIsLocalizationSheafOfModulesSheafificationInverseImageFunctorOppositeAbWToPresheaf, SheafOfModules.pullbackPushforwardAdjunction_homEquiv_symm_unitToPushforwardObjUnit, SheafOfModules.instReflectsIsomorphismsPresheafOfModulesObjFunctorOppositeRingCatIsSheafForget, SheafOfModules.instIsRightAdjointPushforward, SheafOfModules.pushforwardPushforwardEquivalence_unit_app_val_app, SheafOfModules.pushforward_comp_id, SheafOfModules.relationsOfIsCokernelFree_s, SheafOfModules.forgetToSheafModuleCat_obj_obj, SheafOfModules.bijective_pushforwardSections, SheafOfModules.pullbackObjFreeIso_hom_naturality, SheafOfModules.pushforwardPushforwardAdj_counit_app_val_app, SheafOfModules.conjugateEquiv_pullbackId_hom, SheafOfModules.Presentation.map_generators_I, SheafOfModules.pullback_map_ιFree_comp_pullbackObjFreeIso_hom, PresheafOfModules.sheafificationAdjunction_homEquiv_apply, SheafOfModules.instPreservesFiniteLimitsSheafAddCommGrpCatToSheaf, SheafOfModules.map_ιFree_mapFree_hom_assoc, SheafOfModules.forgetPreservesLimitsOfShape, SheafOfModules.Presentation.IsFinite.finite_relations, SheafOfModules.pushforwardNatTrans_app_val_app_apply, SheafOfModules.sectionsMap_freeHomEquiv_symm_freeSection, SheafOfModules.comp_val, PresheafOfModules.instReflectsFiniteLimitsSheafOfModulesSheafAddCommGrpCatToSheaf, PresheafOfModules.toPresheaf_map_sheafificationAdjunction_unit_app, SheafOfModules.pushforward_id_comp, SheafOfModules.hasLimit, PresheafOfModules.toPresheaf_map_sheafificationHomEquiv_def, SheafOfModules.pushforwardSections_coe, SheafOfModules.pushforwardSections_unitHomEquiv, SheafOfModules.instIsRightAdjointPushforwardIdSheafRingCat, SheafOfModules.instFullPresheafOfModulesObjFunctorOppositeRingCatIsSheafForget, SheafOfModules.generatorsOfIsCokernelFree_s, SheafOfModules.pushforwardNatIso_hom, SheafOfModules.pushforwardPushforwardEquivalence_counit_app_val_app, SheafOfModules.pushforward_obj_val, SheafOfModules.GeneratingSections.opEpi_id, PresheafOfModules.toPresheaf_map_sheafificationHomEquiv, SheafOfModules.Presentation.map_π_eq, SheafOfModules.Finite.evaluationPreservesFiniteLimits, SheafOfModules.freeCofan_inj, SheafOfModules.pushforwardNatTrans_comp, PresheafOfModules.instPreservesFiniteLimitsSheafOfModulesSheafification, PresheafOfModules.instPreservesFiniteLimitsSheafAddCommGrpCatCompSheafOfModulesSheafificationToSheaf, SheafOfModules.unitHomEquiv_apply_coe

---

← Back to Index