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_val, forgetToSheafModuleCat_obj_val, forget_map, forget_obj, fullyFaithfulForget_preimage_val, hom_ext, hom_ext_iff, id_val, instAdditivePresheafOfModulesValRingCatForget, instAdditiveSheafAddCommGrpCatToSheaf, instFaithfulPresheafOfModulesValRingCatForget, instFaithfulSheafAddCommGrpCatToSheaf, instFullPresheafOfModulesValRingCatForget, instReflectsIsomorphismsPresheafOfModulesValRingCatForget, isSheaf, sectionsFunctor_map, sectionsFunctor_obj, sectionsMap_comp, sectionsMap_id, toSheaf_map_val, toSheaf_obj_val, 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 CategoryTheory.Functor.category CategoryTheory.Functor.obj toPresheaf CategoryTheory.ObjectProperty.isLocal.homEquiv CategoryTheory.Functor.map	—	—

SheafOfModules

Definitions

Name	Category	Theorems
evaluation 📖	CompOp	9 math math: 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	17 math math: instFullPresheafOfModulesValRingCatForget, instReflectsIsomorphismsPresheafOfModulesValRingCatForget, instFaithfulPresheafOfModulesValRingCatForget, toSheaf_map_val, instSmallElemForallObjCompModuleCatCarrierOppositeRingCatValPresheafOfModulesForgetEvaluationForgetLinearMapIdCarrierSections, PresheafOfModules.toSheaf_map_sheafificationHomEquiv_symm, fullyFaithfulForget_preimage_val, forget_map, forgetPreservesLimitsOfSize, Finite.forgetPreservesFiniteLimits, forget_obj, PresheafOfModules.sheafificationAdjunction_homEquiv_apply, forgetPreservesLimitsOfShape, PresheafOfModules.toPresheaf_map_sheafificationAdjunction_unit_app, PresheafOfModules.toPresheaf_map_sheafificationHomEquiv_def, PresheafOfModules.toPresheaf_map_sheafificationHomEquiv, instAdditivePresheafOfModulesValRingCatForget
forgetToSheafModuleCat 📖	CompOp	2 math math: forgetToSheafModuleCat_map_val, forgetToSheafModuleCat_obj_val
fullyFaithfulForget 📖	CompOp	1 math math: fullyFaithfulForget_preimage_val
instAddCommGroupHom 📖	CompOp	1 math math: add_val
instCategory 📖	CompOp	119 math math: pushforward_assoc, hasLimitsOfSize, pushforwardNatIso_inv, instFullPresheafOfModulesValRingCatForget, sectionsMap_id, instAdditiveRestrictScalars, pullbackPushforwardAdjunction_homEquiv_pullbackObjUnitToUnit, unitHomEquiv_symm_comp, PresheafOfModules.instIsLeftAdjointSheafOfModulesSheafification, freeHomEquiv_freeMap, instIsRightAdjointPushforwardCompSheafRingCatMapSheafPushforwardContinuous, evaluationPreservesLimitsOfShape, toSheaf_obj_val, unitHomEquiv_symm_freeHomEquiv_apply, GeneratingSections.epi, GeneratingSections.opEpi_comp, instIsLeftAdjointPullback, ιFree_mapFree_inv_assoc, pullback_map_ιFree_comp_pullbackObjFreeIso_hom_assoc, evaluationPreservesLimitsOfSize, pushforwardComp_inv_app_val_app, pushforwardNatTrans_id, restrictScalars_obj_val, instReflectsIsomorphismsPresheafOfModulesValRingCatForget, instAdditiveSheafAddCommGrpCatToSheaf, sectionsFunctor_obj, instFaithfulPresheafOfModulesValRingCatForget, sectionsFunctor_map, freeHomEquiv_symm_comp, Presentation.quasicoherentData_presentation, pushforwardCongr_hom_app_val_app, toSheaf_map_val, pullbackObjFreeIso_hom_naturality_assoc, PresheafOfModules.sheafification_map, pullback_comp_id, instPreservesFiniteLimitsFunctorOppositeAddCommGrpCatCompSheafToSheafSheafToPresheaf, freeHomEquiv_comp_apply, PresheafOfModules.toSheaf_map_sheafificationHomEquiv_symm, instPreservesColimitsOfSize, id_val, ιFree_freeMap, pushforwardCongr_inv_app_val_app, freeFunctor_obj, freeFunctor_map, instHasColimitsOfSizeOfPresheafOfModulesValRingCat, conjugateEquiv_pullbackComp_inv, pushforwardPushforwardAdj_unit_app_val_app, fullyFaithfulForget_preimage_val, PresheafOfModules.instReflectsIsomorphismsSheafOfModulesSheafAddCommGrpCatToSheaf, pullback_id_comp, restrictScalars_map_val, ιFree_freeMap_assoc, pushforward_map_val, pushforwardComp_hom_app_val_app, Presentation.map_relations_I, instIsLeftAdjointOverOverRingCatPushforwardIdSheafOver, ιFree_mapFree_inv, Presentation.mapRelations_mapGenerators, hasLimitsOfShape, sectionsMap_comp, pushforwardCongr_symm, add_val, instHasColimitsOfShapeOfPresheafOfModulesValRingCat, instFaithfulSheafAddCommGrpCatToSheaf, unitHomEquiv_comp_apply, unitToPushforwardObjUnit_val_app_apply, pullback_assoc, forget_map, Presentation.of_isIso_relations, forgetPreservesLimitsOfSize, Finite.forgetPreservesFiniteLimits, Presentation.mapRelations_mapGenerators_assoc, forget_obj, GeneratingSections.ofEpi_π, comp_val_assoc, map_ιFree_mapFree_hom, instIsIsoPullbackObjUnitToUnitOfFinal, pushforwardNatTrans_app_val_app, Finite.hasFiniteLimits, pullbackPushforwardAdjunction_homEquiv_symm_unitToPushforwardObjUnit, instIsRightAdjointPushforward, pushforwardPushforwardEquivalence_unit_app_val_app, pushforward_comp_id, bijective_pushforwardSections, forgetToSheafModuleCat_map_val, pullbackObjFreeIso_hom_naturality, PresheafOfModules.instReflectsIsomorphismsSheafOfModulesFunctorOppositeAddCommGrpCatCompSheafToSheafSheafToPresheaf, 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, comp_val, PresheafOfModules.instReflectsFiniteLimitsSheafOfModulesSheafAddCommGrpCatToSheaf, PresheafOfModules.toPresheaf_map_sheafificationAdjunction_unit_app, pushforward_id_comp, PresheafOfModules.toPresheaf_map_sheafificationHomEquiv_def, pushforwardSections_coe, pushforwardSections_unitHomEquiv, instIsRightAdjointPushforwardIdSheafRingCat, forgetToSheafModuleCat_obj_val, pushforwardNatIso_hom, pushforwardPushforwardEquivalence_counit_app_val_app, pushforward_obj_val, GeneratingSections.opEpi_id, PresheafOfModules.toPresheaf_map_sheafificationHomEquiv, Presentation.map_π_eq, Finite.evaluationPreservesFiniteLimits, instAdditivePresheafOfModulesValRingCatForget, freeCofan_inj, pushforwardNatTrans_comp, PresheafOfModules.instPreservesFiniteLimitsSheafOfModulesSheafification, PresheafOfModules.instPreservesFiniteLimitsSheafAddCommGrpCatCompSheafOfModulesSheafificationToSheaf, unitHomEquiv_apply_coe
instPreadditive 📖	CompOp	8 math math: instAdditiveRestrictScalars, instAdditiveSheafAddCommGrpCatToSheaf, Presentation.map_relations_I, Presentation.mapRelations_mapGenerators, Presentation.of_isIso_relations, Presentation.mapRelations_mapGenerators_assoc, Presentation.IsFinite.finite_relations, instAdditivePresheafOfModulesValRingCatForget
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	9 math math: sectionsMap_id, unitHomEquiv_symm_comp, sectionsFunctor_map, freeHomEquiv_symm_comp, sectionMap_freeMap_freeSection, freeHomEquiv_comp_apply, sectionsMap_comp, unitHomEquiv_comp_apply, GeneratingSections.ofEpi_s
toSheaf 📖	CompOp	12 math math: toSheaf_obj_val, instAdditiveSheafAddCommGrpCatToSheaf, toSheaf_map_val, instPreservesFiniteLimitsFunctorOppositeAddCommGrpCatCompSheafToSheafSheafToPresheaf, PresheafOfModules.toSheaf_map_sheafificationHomEquiv_symm, PresheafOfModules.instReflectsIsomorphismsSheafOfModulesSheafAddCommGrpCatToSheaf, instFaithfulSheafAddCommGrpCatToSheaf, PresheafOfModules.instReflectsIsomorphismsSheafOfModulesFunctorOppositeAddCommGrpCatCompSheafToSheafSheafToPresheaf, 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, PresheafOfModules.toSheafify_app_apply', toSheaf_obj_val, PresheafOfModules.toPresheaf_map_toSheafify, isSheaf, pushforwardComp_inv_app_val_app, restrictScalars_obj_val, pushforwardCongr_hom_app_val_app, toSheaf_map_val, id_val, 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, pushforwardNatTrans_app_val_app, pushforwardPushforwardEquivalence_unit_app_val_app, forgetToSheafModuleCat_map_val, 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, forgetToSheafModuleCat_obj_val, 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.Sheaf.val RingCat RingCat.instCategory PresheafOfModules.instCategory val PresheafOfModules.instAddHom	—	—
comp_val 📖	mathematical	—	Hom.val CategoryTheory.CategoryStruct.comp SheafOfModules CategoryTheory.Category.toCategoryStruct instCategory PresheafOfModules CategoryTheory.Sheaf.val RingCat RingCat.instCategory PresheafOfModules.instCategory val	—	—
comp_val_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp PresheafOfModules CategoryTheory.Sheaf.val RingCat RingCat.instCategory CategoryTheory.Category.toCategoryStruct PresheafOfModules.instCategory val Hom.val SheafOfModules instCategory	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_val
forgetToSheafModuleCat_map_val 📖	mathematical	—	CategoryTheory.Sheaf.Hom.val ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Sheaf.val RingCat.ring ModuleCat.moduleCategory PresheafOfModules PresheafOfModules.instCategory CategoryTheory.Functor CategoryTheory.Functor.category PresheafOfModules.forgetToPresheafModuleCat val CategoryTheory.Functor.map SheafOfModules instCategory CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf forgetToSheafModuleCat Hom.val	—	—
forgetToSheafModuleCat_obj_val 📖	mathematical	—	CategoryTheory.Sheaf.val ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory SheafOfModules instCategory CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf forgetToSheafModuleCat PresheafOfModules PresheafOfModules.instCategory CategoryTheory.Functor CategoryTheory.Functor.category PresheafOfModules.forgetToPresheafModuleCat val	—	—
forget_map 📖	mathematical	—	CategoryTheory.Functor.map SheafOfModules instCategory PresheafOfModules CategoryTheory.Sheaf.val RingCat RingCat.instCategory PresheafOfModules.instCategory forget Hom.val	—	—
forget_obj 📖	mathematical	—	CategoryTheory.Functor.obj SheafOfModules instCategory PresheafOfModules CategoryTheory.Sheaf.val RingCat RingCat.instCategory PresheafOfModules.instCategory forget val	—	—
fullyFaithfulForget_preimage_val 📖	mathematical	—	Hom.val CategoryTheory.Functor.FullyFaithful.preimage SheafOfModules instCategory PresheafOfModules CategoryTheory.Sheaf.val RingCat RingCat.instCategory 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.Sheaf.val RingCat RingCat.instCategory PresheafOfModules.instCategory val	—	—
instAdditivePresheafOfModulesValRingCatForget 📖	mathematical	—	CategoryTheory.Functor.Additive SheafOfModules PresheafOfModules CategoryTheory.Sheaf.val RingCat RingCat.instCategory instCategory PresheafOfModules.instCategory instPreadditive PresheafOfModules.instPreadditive forget	—	—
instAdditiveSheafAddCommGrpCatToSheaf 📖	mathematical	—	CategoryTheory.Functor.Additive SheafOfModules CategoryTheory.Sheaf AddCommGrpCat AddCommGrpCat.instCategory instCategory CategoryTheory.Sheaf.instCategorySheaf instPreadditive CategoryTheory.instPreadditiveSheaf AddCommGrpCat.instPreadditive toSheaf	—	—
instFaithfulPresheafOfModulesValRingCatForget 📖	mathematical	—	CategoryTheory.Functor.Faithful SheafOfModules instCategory PresheafOfModules CategoryTheory.Sheaf.val RingCat RingCat.instCategory PresheafOfModules.instCategory forget	—	CategoryTheory.Functor.FullyFaithful.faithful
instFaithfulSheafAddCommGrpCatToSheaf 📖	mathematical	—	CategoryTheory.Functor.Faithful SheafOfModules instCategory CategoryTheory.Sheaf AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.Sheaf.instCategorySheaf toSheaf	—	CategoryTheory.Functor.Faithful.of_comp_iso CategoryTheory.Functor.Faithful.comp instFaithfulPresheafOfModulesValRingCatForget PresheafOfModules.instFaithfulFunctorOppositeAbToPresheaf
instFullPresheafOfModulesValRingCatForget 📖	mathematical	—	CategoryTheory.Functor.Full SheafOfModules instCategory PresheafOfModules CategoryTheory.Sheaf.val RingCat RingCat.instCategory PresheafOfModules.instCategory forget	—	CategoryTheory.Functor.FullyFaithful.full
instReflectsIsomorphismsPresheafOfModulesValRingCatForget 📖	mathematical	—	CategoryTheory.Functor.ReflectsIsomorphisms SheafOfModules instCategory PresheafOfModules CategoryTheory.Sheaf.val RingCat RingCat.instCategory PresheafOfModules.instCategory forget	—	CategoryTheory.Functor.FullyFaithful.reflectsIsomorphisms
isSheaf 📖	mathematical	—	CategoryTheory.Presheaf.IsSheaf Ab AddCommGrpCat.instCategory PresheafOfModules.presheaf CategoryTheory.Sheaf.val RingCat RingCat.instCategory 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_val 📖	mathematical	—	CategoryTheory.Sheaf.Hom.val AddCommGrpCat AddCommGrpCat.instCategory PresheafOfModules.presheaf CategoryTheory.Sheaf.val RingCat RingCat.instCategory val isSheaf CategoryTheory.Functor.map SheafOfModules instCategory CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf toSheaf CategoryTheory.Functor Opposite CategoryTheory.Category.opposite Ab CategoryTheory.Functor.category CategoryTheory.Functor.comp PresheafOfModules PresheafOfModules.instCategory forget PresheafOfModules.toPresheaf	—	isSheaf
toSheaf_obj_val 📖	mathematical	—	CategoryTheory.Sheaf.val AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.Functor.obj SheafOfModules instCategory CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf 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.Sheaf.val RingCat RingCat.instCategory 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.Sheaf.val RingCat RingCat.instCategory	—	—

SheafOfModules.Hom

Definitions

Name	Category	Theorems
val 📖	CompOp	25 math math: 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.forgetToSheafModuleCat_map_val, 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	119 math math: SheafOfModules.pushforward_assoc, SheafOfModules.hasLimitsOfSize, SheafOfModules.pushforwardNatIso_inv, SheafOfModules.instFullPresheafOfModulesValRingCatForget, SheafOfModules.sectionsMap_id, SheafOfModules.instAdditiveRestrictScalars, SheafOfModules.pullbackPushforwardAdjunction_homEquiv_pullbackObjUnitToUnit, SheafOfModules.unitHomEquiv_symm_comp, PresheafOfModules.instIsLeftAdjointSheafOfModulesSheafification, SheafOfModules.freeHomEquiv_freeMap, SheafOfModules.instIsRightAdjointPushforwardCompSheafRingCatMapSheafPushforwardContinuous, SheafOfModules.evaluationPreservesLimitsOfShape, SheafOfModules.toSheaf_obj_val, SheafOfModules.unitHomEquiv_symm_freeHomEquiv_apply, SheafOfModules.GeneratingSections.epi, SheafOfModules.GeneratingSections.opEpi_comp, SheafOfModules.instIsLeftAdjointPullback, SheafOfModules.ιFree_mapFree_inv_assoc, SheafOfModules.pullback_map_ιFree_comp_pullbackObjFreeIso_hom_assoc, SheafOfModules.evaluationPreservesLimitsOfSize, SheafOfModules.pushforwardComp_inv_app_val_app, SheafOfModules.pushforwardNatTrans_id, SheafOfModules.restrictScalars_obj_val, SheafOfModules.instReflectsIsomorphismsPresheafOfModulesValRingCatForget, SheafOfModules.instAdditiveSheafAddCommGrpCatToSheaf, SheafOfModules.sectionsFunctor_obj, SheafOfModules.instFaithfulPresheafOfModulesValRingCatForget, SheafOfModules.sectionsFunctor_map, SheafOfModules.freeHomEquiv_symm_comp, SheafOfModules.Presentation.quasicoherentData_presentation, SheafOfModules.pushforwardCongr_hom_app_val_app, SheafOfModules.toSheaf_map_val, 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, SheafOfModules.ιFree_freeMap, SheafOfModules.pushforwardCongr_inv_app_val_app, SheafOfModules.freeFunctor_obj, SheafOfModules.freeFunctor_map, SheafOfModules.instHasColimitsOfSizeOfPresheafOfModulesValRingCat, SheafOfModules.conjugateEquiv_pullbackComp_inv, 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.pushforward_map_val, SheafOfModules.pushforwardComp_hom_app_val_app, SheafOfModules.Presentation.map_relations_I, SheafOfModules.instIsLeftAdjointOverOverRingCatPushforwardIdSheafOver, SheafOfModules.ιFree_mapFree_inv, SheafOfModules.Presentation.mapRelations_mapGenerators, SheafOfModules.hasLimitsOfShape, SheafOfModules.sectionsMap_comp, SheafOfModules.pushforwardCongr_symm, SheafOfModules.add_val, SheafOfModules.instHasColimitsOfShapeOfPresheafOfModulesValRingCat, 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.Finite.forgetPreservesFiniteLimits, SheafOfModules.Presentation.mapRelations_mapGenerators_assoc, SheafOfModules.forget_obj, SheafOfModules.GeneratingSections.ofEpi_π, SheafOfModules.comp_val_assoc, SheafOfModules.map_ιFree_mapFree_hom, SheafOfModules.instIsIsoPullbackObjUnitToUnitOfFinal, SheafOfModules.pushforwardNatTrans_app_val_app, SheafOfModules.Finite.hasFiniteLimits, SheafOfModules.pullbackPushforwardAdjunction_homEquiv_symm_unitToPushforwardObjUnit, SheafOfModules.instIsRightAdjointPushforward, SheafOfModules.pushforwardPushforwardEquivalence_unit_app_val_app, SheafOfModules.pushforward_comp_id, SheafOfModules.bijective_pushforwardSections, SheafOfModules.forgetToSheafModuleCat_map_val, SheafOfModules.pullbackObjFreeIso_hom_naturality, PresheafOfModules.instReflectsIsomorphismsSheafOfModulesFunctorOppositeAddCommGrpCatCompSheafToSheafSheafToPresheaf, 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.comp_val, PresheafOfModules.instReflectsFiniteLimitsSheafOfModulesSheafAddCommGrpCatToSheaf, PresheafOfModules.toPresheaf_map_sheafificationAdjunction_unit_app, SheafOfModules.pushforward_id_comp, PresheafOfModules.toPresheaf_map_sheafificationHomEquiv_def, SheafOfModules.pushforwardSections_coe, SheafOfModules.pushforwardSections_unitHomEquiv, SheafOfModules.instIsRightAdjointPushforwardIdSheafRingCat, SheafOfModules.forgetToSheafModuleCat_obj_val, 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.instAdditivePresheafOfModulesValRingCatForget, SheafOfModules.freeCofan_inj, SheafOfModules.pushforwardNatTrans_comp, PresheafOfModules.instPreservesFiniteLimitsSheafOfModulesSheafification, PresheafOfModules.instPreservesFiniteLimitsSheafAddCommGrpCatCompSheafOfModulesSheafificationToSheaf, SheafOfModules.unitHomEquiv_apply_coe

---

← Back to Index