AddCommGrpCat

📁 Source: Mathlib/Topology/Sheaves/AddCommGrpCat.lean

Statistics

Metric	Count
Definitions AddCommGrpCat	1
Theorems restrict_sum, sections_exact_of_exact, sections_exact_of_left_exact	3
Total	4

TopCat.Presheaf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
restrict_sum 📖	mathematical	TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder	restrictOpen AddCommGrpCat AddCommGrpCat.instCategory AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.ToType	—	map_add AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass
sections_exact_of_exact 📖	mathematical	CategoryTheory.ShortComplex.Exact TopCat.Presheaf AddCommGrpCat AddCommGrpCat.instCategory TopCat.instCategoryPresheaf CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive TopCat.instAbelianPresheaf AddCommGrpCat.instAbelian DFunLike.coe CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.ShortComplex.X₂ Opposite.op CategoryTheory.ShortComplex.X₃ 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 CategoryTheory.ShortComplex.g NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	AddCommGrpCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.ShortComplex.X₁ TopCat.Presheaf TopCat.instCategoryPresheaf CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive TopCat.instAbelianPresheaf AddCommGrpCat.instAbelian Opposite.op DFunLike.coe CategoryTheory.ShortComplex.X₂ CategoryTheory.ConcreteCategory.hom AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier CategoryTheory.NatTrans.app CategoryTheory.ShortComplex.f	—	CategoryTheory.Functor.preservesZeroMorphisms_evaluation_obj CategoryTheory.ShortComplex.ab_exact_iff CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Functor.instAdditiveObjEvaluation List.TFAE.out CategoryTheory.Functor.exact_tfae CategoryTheory.Limits.instPreservesFiniteLimitsFunctorObjEvaluationOfHasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasCountableLimits CategoryTheory.Limits.hasCountableLimits_of_hasLimits AddCommGrpCat.hasLimits CategoryTheory.Limits.instPreservesFiniteColimitsFunctorObjEvaluationOfHasFiniteColimits CategoryTheory.Limits.hasFiniteColimits_of_hasCountableColimits CategoryTheory.Limits.hasCountableColimits_of_hasColimits AddCommGrpCat.hasColimitsOfSize UnivLE.self

TopCat.Sheaf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sections_exact_of_left_exact 📖	mathematical	CategoryTheory.ShortComplex.Exact TopCat.Sheaf AddCommGrpCat AddCommGrpCat.instCategory TopCat.instCategorySheaf CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive instAbelian CategoryTheory.instHasSheafifyOfPreservesLimitsForgetOfHasFiniteLimitsOfSmallOppositeCover TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opens.grothendieckTopology AddCommGrpCat.hasLimit CategoryTheory.Limits.WalkingMulticospan CategoryTheory.GrothendieckTopology.Cover.shape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.MulticospanIndex.multicospan CategoryTheory.GrothendieckTopology.Cover.index small_subtype small_Pi CategoryTheory.Functor.obj CategoryTheory.types CategoryTheory.Functor.comp CategoryTheory.forget AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier UnivLE.small univLE_of_max UnivLE.self Set Set.instMembership CategoryTheory.Functor.sections AddCommGrpCat.hasColimitsOfShape Opposite CategoryTheory.GrothendieckTopology.Cover CategoryTheory.Category.opposite CategoryTheory.GrothendieckTopology.instPreorderCover Opposite.small CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits AddCommGrpCat.FilteredColimits.forget_preservesFilteredColimits CategoryTheory.isFiltered_op_of_isCofiltered CategoryTheory.isCofiltered_of_directed_ge_nonempty SemilatticeInf.instIsCodirectedOrder CategoryTheory.GrothendieckTopology.Cover.instSemilatticeInf CategoryTheory.GrothendieckTopology.Cover.instInhabited AddCommGrpCat.forget_reflects_isos AddCommGrpCat.forget_preservesLimitsOfShape AddCommGrpCat.forget_preservesLimits CategoryTheory.Limits.hasFiniteLimits_of_hasCountableLimits CategoryTheory.Limits.hasCountableLimits_of_hasLimits AddCommGrpCat.hasLimits AddCommGrpCat.instAbelian DFunLike.coe CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.ShortComplex.X₂ Opposite.op CategoryTheory.ShortComplex.X₃ CategoryTheory.ConcreteCategory.hom CategoryTheory.NatTrans.app CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ShortComplex.g NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	AddCommGrpCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf Opens.grothendieckTopology CategoryTheory.ShortComplex.X₁ TopCat.Sheaf TopCat.instCategorySheaf CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive instAbelian CategoryTheory.instHasSheafifyOfPreservesLimitsForgetOfHasFiniteLimitsOfSmallOppositeCover AddCommGrpCat.hasLimit CategoryTheory.Limits.WalkingMulticospan CategoryTheory.GrothendieckTopology.Cover.shape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.MulticospanIndex.multicospan CategoryTheory.GrothendieckTopology.Cover.index small_subtype small_Pi CategoryTheory.types CategoryTheory.Functor.comp CategoryTheory.forget AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier UnivLE.small univLE_of_max UnivLE.self Set Set.instMembership CategoryTheory.Functor.sections AddCommGrpCat.hasColimitsOfShape CategoryTheory.GrothendieckTopology.Cover CategoryTheory.GrothendieckTopology.instPreorderCover Opposite.small CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits AddCommGrpCat.FilteredColimits.forget_preservesFilteredColimits CategoryTheory.isFiltered_op_of_isCofiltered CategoryTheory.isCofiltered_of_directed_ge_nonempty SemilatticeInf.instIsCodirectedOrder CategoryTheory.GrothendieckTopology.Cover.instSemilatticeInf CategoryTheory.GrothendieckTopology.Cover.instInhabited AddCommGrpCat.forget_reflects_isos AddCommGrpCat.forget_preservesLimitsOfShape AddCommGrpCat.forget_preservesLimits CategoryTheory.Limits.hasFiniteLimits_of_hasCountableLimits CategoryTheory.Limits.hasCountableLimits_of_hasLimits AddCommGrpCat.hasLimits AddCommGrpCat.instAbelian Opposite.op DFunLike.coe CategoryTheory.ShortComplex.X₂ CategoryTheory.ConcreteCategory.hom CategoryTheory.NatTrans.app CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ShortComplex.f	—	CategoryTheory.instHasSheafifyOfPreservesLimitsForgetOfHasFiniteLimitsOfSmallOppositeCover AddCommGrpCat.hasLimit small_subtype small_Pi UnivLE.small univLE_of_max UnivLE.self AddCommGrpCat.hasColimitsOfShape Opposite.small CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits AddCommGrpCat.FilteredColimits.forget_preservesFilteredColimits CategoryTheory.isFiltered_op_of_isCofiltered CategoryTheory.isCofiltered_of_directed_ge_nonempty SemilatticeInf.instIsCodirectedOrder AddCommGrpCat.forget_reflects_isos AddCommGrpCat.forget_preservesLimitsOfShape AddCommGrpCat.forget_preservesLimits CategoryTheory.Limits.hasFiniteLimits_of_hasCountableLimits CategoryTheory.Limits.hasCountableLimits_of_hasLimits AddCommGrpCat.hasLimits TopCat.Presheaf.sections_exact_of_exact CategoryTheory.Functor.preservesZeroMorphisms_of_additive instAdditivePresheafForget List.TFAE.out CategoryTheory.Functor.preservesFiniteLimits_tfae CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits CategoryTheory.preservesLimits_of_createsLimits_and_hasLimits TopCat.instHasLimitsPresheaf

(root)

Definitions

Name	Category	Theorems
AddCommGrpCat 📖	CompData	325 math math: ModuleCat.HasColimit.colimitCocone_pt_isAddCommGroup, AddCommGrpCat.forget₂AddGroup_preservesLimitsOfShape, AddCommGrpCat.image.lift_fac, AddCommGrpCat.coyoneda_obj_obj_coe, AddCommGrpCat.isZero_iff_subsingleton, AddCommGrpCat.binaryProductLimitCone_cone_pt, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_X₃, ModuleCat.forget₂_reflectsLimitsOfSize, SheafOfModules.presentationOfIsCokernelFree_generators, AddCommGrpCat.biproductIsoPi_inv_comp_π_apply, CategoryTheory.isSeparator_iff_faithful_preadditiveCoyoneda, AddCommGrpCat.comp_apply, RingCat.FilteredColimits.instPreservesFilteredColimitsAddCommGrpCatForget₂RingHomCarrierAddMonoidHomCarrier, ModuleCat.forget₂PreservesColimitsOfSize, commGroupAddCommGroupEquivalence_functor, AddCommGrpCat.hom_add, AddCommGrpCat.instPreservesMonomorphismsFree, AddCommGrpCat.ofHom_comp, AddCommGrpCat.FilteredColimits.forget_preservesFilteredColimits, ModuleCat.forget₂AddCommGroup_preservesLimitsOfSize, ModuleCat.mkOfSMul'_smul, PresheafOfModules.Sheafify.add_smul, CategoryTheory.isCoseparator_iff_faithful_preadditiveYoneda, AddCommGrpCat.hasLimit, AddCommGrpCat.injective_of_divisible, CategoryTheory.Abelian.Ext.preadditiveYoneda_homologySequenceδ_singleTriangle_apply, AddCommGrpCat.hasZeroObject, AddCommGrpCat.hasLimitsOfSize, CategoryTheory.Abelian.Ext.contravariant_sequence_exact₁', CategoryTheory.Abelian.extFunctorObj_obj_coe, AddCommGrpCat.hom_zero, SheafOfModules.Presentation.isQuasicoherent, AddCommGrpCat.hasLimitsOfShape, instAB4AddCommGrpCat, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_X₁, RingCat.forget₂AddCommGroup_preservesLimits, PresheafOfModules.toSheafify_app_apply', AddCommGrpCat.hasColimit_of_small_quot, CochainComplex.HomComplex.leftHomologyData_K_coe, AddCommGrpCat.isColimit_iff_bijective_desc, commGroupAddCommGroupEquivalence_counitIso, ModuleCat.forget₂_addCommGrp_essSurj, AddCommGrpCat.hasLimits, CochainComplex.HomComplex.leftHomologyData'_i, AddCommGrpCat.neg_hom_apply, AddCommGrpCat.forget_preservesLimits, ModuleCat.forget₂AddCommGroup_reflectsLimitOfShape, AddCommGrpCat.forget_preservesLimitsOfShape, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply, AddCommGrpCat.coe_comp, instHasFilteredColimitsAddCommGrpCat, AddCommGrpCat.forget₂_map, ModuleCat.HasColimit.colimitCocone_ι_app, AddCommGrpCat.Colimits.colimitCocone_ι_app, ModuleCat.forget₂_addCommGroup_full, AddCommGrpCat.FilteredColimits.forget₂AddGroup_preservesFilteredColimits, CochainComplex.HomComplex.leftHomologyData_π_hom_apply, PresheafOfModules.Sheafify.map_smul_eq, AddCommGrpCat.asHom_injective, CategoryTheory.Abelian.Ext.contravariant_sequence_exact₂', SheafOfModules.ιFree_mapFree_inv_assoc, FGModuleCat.instFiniteCarrierSigmaObjModuleCatOfFinite, CochainComplex.HomComplex.leftHomologyData_i_hom_apply, ModuleCat.smul_naturality, CategoryTheory.Abelian.Ext.preadditiveCoyoneda_homologySequenceδ_singleTriangle_apply, ModuleCat.HasColimit.colimitCocone_pt_isModule, CategoryTheory.Abelian.extFunctorObj_map, CategoryTheory.preadditiveYoneda_obj, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiprod_δ_assoc, AddCommGrpCat.ext_iff, AddCommGrpCat.uliftFunctor_additive, CategoryTheory.Adjunction.compPreadditiveYonedaIso_inv_app_app_apply, AddCommGrpCat.instMonoι, AddCommGrpCat.forget_commGrp_preserves_epi, CategoryTheory.preadditiveYonedaMap_app, AddCommGrpCat.coyonedaForget_inv_app_app, AddCommGrpCat.free_map_coe, AddCommGrpCat.instHasFiniteBiproducts, CategoryTheory.Abelian.Ext.covariant_sequence_exact₁', CategoryTheory.GrothendieckTopology.MayerVietorisSquare.sequence_exact, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_shortExact, AddCommGrpCat.coyonedaForget_hom_app_app_hom, CategoryTheory.Iso.addCommGroupIsoToAddEquiv_symm_apply, AddCommGrpCat.instFaithfulUliftFunctor, AddCommGrpCat.HasLimit.productLimitCone_isLimit_lift, CategoryTheory.Abelian.Ext.covariant_sequence_exact₃', ModuleCat.forget₂_map_homMk, instIsGrothendieckAbelianAddCommGrpCat, AddCommGrpCat.biprodIsoProd_inv_comp_snd_apply, AddCommGrpCat.toCommGrp_obj_coe, PresheafOfModules.toSheaf_map_sheafificationAdjunction_counit_app, CategoryTheory.Pretriangulated.instIsHomologicalOppositeAddCommGrpCatObjFunctorPreadditiveYoneda, AddCommGrpCat.binaryProductLimitCone_isLimit_lift, AddCommGrpCat.binaryProductLimitCone_cone_π_app_left, AddCommGrpCat.homAddEquiv_symm_apply_hom, CategoryTheory.additive_yonedaObj', AddCommGrpCat.hom_sub, SheafOfModules.IsQuasicoherent.of_coversTop, instAB4StarAddCommGrpCat, SheafOfModules.instAdditiveSheafAddCommGrpCatToSheaf, CategoryTheory.faithful_preadditiveCoyoneda, CategoryTheory.faithful_preadditiveYoneda, ModuleCat.forget₂AddCommGroup_preservesLimits, AddCommGrpCat.free_obj_coe, AddCommGrpCat.Colimits.quotUliftToQuot_ι, AddCommGrpCat.hom_id, PresheafOfModules.instReflectsIsomorphismsSheafOfModulesSheafAddCommGrpCatToSheaf_1, AddCommGrpCat.hom_nsmul, CategoryTheory.preservesLimits_preadditiveCoyoneda_obj, AddCommGrpCat.HasLimit.productLimitCone_cone_pt_coe, SheafOfModules.Presentation.quasicoherentData_presentation, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk₀_f_comp_biprodAddEquiv_symm_biprodIsoProd_hom, ModuleCat.forget₂_obj, AddCommGrpCat.Colimits.colimitCocone_pt, AddCommGrpCat.forget_commGrp_preserves_mono, CategoryTheory.whiskering_linearCoyoneda₂, SheafOfModules.presentationOfIsCokernelFree_relations, PresheafOfModules.sheafification_map, AddCommGrpCat.Colimits.Quot.desc_toCocone_desc, CategoryTheory.Pretriangulated.preadditiveYoneda_homologySequenceδ_apply, AddCommGrpCat.uliftFunctor_preservesLimitsOfSize, AddEquiv.toAddCommGrpIso_hom, AddCommGrpCat.hasColimit, SheafOfModules.instPreservesFiniteLimitsFunctorOppositeAddCommGrpCatCompSheafToSheafSheafToPresheaf, CategoryTheory.Abelian.instAdditiveAddCommGrpCatExtFunctorObj, PresheafOfModules.toSheaf_map_sheafificationHomEquiv_symm, CategoryTheory.whiskering_preadditiveYoneda, AddCommGrpCat.forget₂AddGroup_preservesLimits, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.instEpiSheafAddCommGrpCatGShortComplex, CategoryTheory.Abelian.extFunctor_obj, AddCommGrpCat.Colimits.quotToQuotUlift_ι, ModuleCat.smulNatTrans_apply_app, CategoryTheory.Abelian.extFunctor_map_app, AddCommGrpCat.zero_apply, CategoryTheory.Abelian.Ext.covariantSequence_exact, AddCommGrpCat.id_apply, AddCommGrpCat.int_hom_ext_iff, TopCat.Sheaf.IsFlasque.epi_of_shortExact, AddCommGrpCat.Colimits.Quot.desc_toCocone_desc_app, SheafOfModules.toSheaf_obj_obj, CategoryTheory.preservesLimits_preadditiveYoneda_obj, PresheafOfModules.Sheafify.smul_add, AddCommGrpCat.μ_forget_apply, CategoryTheory.additive_coyonedaObj', AddCommGrpCat.epi_iff_surjective, AddCommGrpCat.tensorObj_eq, AddCommGrpCat.forget₂_addGrp_map_ofHom, PresheafOfModules.instReflectsIsomorphismsSheafOfModulesSheafAddCommGrpCatToSheaf, TopCat.Sheaf.sections_exact_of_left_exact, CategoryTheory.full_preadditiveCoyoneda, FGModuleCat.instFiniteCarrierColimitModuleCatCompForget₂LinearMapIdObjIsFG, AddCommGrpCat.forget₂AddCommMon_preservesLimitsOfShape, CategoryTheory.Adjunction.compPreadditiveYonedaIso_hom_app_app_apply, AddCommGrpCat.coyonedaType_obj_map, AddCommGrpCat.coyonedaType_obj_obj_coe, AddCommGrpCat.mono_iff_injective, ModuleCat.HasColimit.instPreservesColimitAddCommGrpCatForget₂LinearMapIdCarrierAddMonoidHomCarrier, AddCommGrpCat.Colimits.toCocone_ι_app, AddCommGrpCat.Colimits.Quot.ι_desc, ModuleCat.FilteredColimits.forget₂AddCommGroup_preservesFilteredColimits, AddCommGrpCat.Colimits.Quot.map_ι, AddCommGrpCat.isZero_of_subsingleton, AddCommGrpCat.kernelIsoKer_inv_comp_ι, AddCommGrpCat.image.fac, AddCommGrpCat.HasLimit.productLimitCone_cone_π, ModuleCat.forget₂_obj_moduleCat_of, AddCommGrpCat.forget₂AddGroup_preservesLimit, AddCommGrpCat.injective_of_mono, AddCommGrpCat.epi_iff_range_eq_top, SheafOfModules.Presentation.map_relations_I, ModuleCat.instPreservesColimitsOfSizeAddCommGrpCatForget₂LinearMapIdCarrierAddMonoidHomCarrierOfHasColimitsOfSizeAddCommGrpMax, CategoryTheory.Abelian.Ext.covariant_sequence_exact₂', AddCommGrpCat.instFullAddGrpCatForget₂AddMonoidHomCarrierCarrier, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.δ_toBiprod_assoc, CategoryTheory.Abelian.Ext.mono_postcomp_mk₀_of_mono, instPreservesFiniteLimitsFunctorAddCommGrpCatColim, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.δ_toBiprod, ModuleCat.HasColimit.coconePointSMul_apply, SheafOfModules.ιFree_mapFree_inv, SheafOfModules.Presentation.mapRelations_mapGenerators, AddCommGrpCat.leftExactFunctorForgetEquivalence.instPreservesFiniteLimitsObjLeftExactFunctorTypeFunctorInverseAux, AddCommGrpCat.coe_id, AddCommGrpCat.forget₂AddGroup_preservesLimitsOfSize, ModuleCat.instReflectsIsomorphismsAddCommGrpCatForget₂LinearMapIdCarrierAddMonoidHomCarrier, SheafOfModules.relationsOfIsCokernelFree_I, CategoryTheory.Projective.projective_iff_preservesEpimorphisms_preadditiveCoyoneda_obj, AddCommGrpCat.enoughInjectives, AddCommGrpCat.Colimits.toCocone_pt_coe, AddCommGrpCat.uliftFunctor_preservesLimitsOfShape, PresheafOfModules.sheafifyMap_val, SheafOfModules.instFaithfulSheafAddCommGrpCatToSheaf, CategoryTheory.Abelian.instAdditiveOppositeFunctorAddCommGrpCatExtFunctor, PresheafOfModules.comp_toPresheaf_map_sheafifyHomEquiv'_symm_hom, AddCommGrpCat.ofHom_id, AddCommGrpCat.injective_as_module_iff, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiprod_biprodIsoProd_inv_apply, TopCat.Sheaf.IsFlasque.structured_arrows_elements_sheaf_chains_bounded, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_g, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.isPushoutAddCommGrpFreeSheaf, ModuleCat.mkOfSMul_smul, AddCommGrpCat.instReflectsIsomorphismsAddGrpCatForget₂AddMonoidHomCarrierCarrier, AddCommGrpCat.biprodIsoProd_inv_comp_desc, AddCommGrpCat.uliftFunctor_map, AddCommGrpCat.biprodIsoProd_inv_comp_snd, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓUnitOpensCarrierCarrierCommRingCatRingCatSheaf, CategoryTheory.full_preadditiveYoneda, CategoryTheory.Abelian.Ext.mono_precomp_mk₀_of_epi, SheafOfModules.Presentation.of_isIso_relations, AddCommGrpCat.hom_comp, AddCommGrpCat.uliftFunctor_obj, AddCommGrpCat.uliftFunctor_preservesLimit, ModuleCat.reflectsColimitsOfShape, ModuleCat.homMk_hom_apply, ModuleCat.forget₂AddCommGroup_reflectsLimitOfSize, AddCommGrpCat.biprodIsoProd_inv_comp_desc_apply, CochainComplex.HomComplex.leftHomologyData_H_coe, CochainComplex.HomComplex.leftHomologyData'_K_coe, AddCommGrpCat.ofHom_apply, AddCommGrpCat.hasColimitsOfShape, AddCommGrpCat.biprodIsoProd_inv_comp_fst_apply, instPreservesHomologyFunctorAddCommGrpCatColim, SheafOfModules.Presentation.of_isIso_generators, TopCat.Sheaf.IsFlasque.of_shortExact_of_isFlasque₁₂, CategoryTheory.Sheaf.cohomologyFunctor_obj, SheafOfModules.Presentation.mapRelations_mapGenerators_assoc, AddCommGrpCat.instIsLeftAdjointFree, SheafOfModules.map_ιFree_mapFree_hom, AddCommGrpCat.biproductIsoPi_inv_comp_π, SheafOfModules.toSheaf_map_hom, AddCommGrpCat.instIsSerreClassIsFinite, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toBiprod_fromBiprod_assoc, commGroupAddCommGroupEquivalence_unitIso, AddCommGrpCat.wellPowered_addCommGrp, AddCommGrpCat.HasLimit.lift_hom_apply, AddCommGrpCat.hasColimitsOfSize, ModuleCat.HasColimit.colimitCocone_pt_carrier, ModuleCat.forget₂_addCommGrp_additive, AddCommGrpCat.biprodIsoProd_inv_comp_fst, RingCat.forget₂AddCommGroup_preservesLimitsOfSize, CochainComplex.HomComplex_X, CochainComplex.HomComplex.leftHomologyData'_H_coe, AddCommGrpCat.forget₂_commMonCat_map_ofHom, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_f, AddCommGrpCat.forget₂AddCommMon_preservesLimitsOfSize, AddCommGrpCat.coyoneda_map_app, AddCommGrpCat.Colimits.Quot.desc_quotQuotUliftAddEquiv, AddCommGrpCat.forget_map, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.instMonoSheafAddCommGrpCatFShortComplex, SheafOfModules.relationsOfIsCokernelFree_s, ModuleCat.forget₂_reflectsLimits, AddCommGrpCat.kernelIsoKer_hom_comp_subtype, ModuleCat.forget₂PreservesColimitsOfShape, SheafOfModules.generatorsOfIsCokernelFree_π, CategoryTheory.Pretriangulated.instIsHomologicalAddCommGrpCatObjOppositeFunctorPreadditiveCoyoneda, AddCommGrpCat.instFullUliftFunctor, CochainComplex.HomComplex.leftHomologyData'_π, ModuleCat.forget₂AddCommGroup_reflectsLimit, instHasSeparatorAddCommGrpCat, SheafOfModules.Presentation.map_generators_I, ModuleCat.forget₂AddCommGroup_preservesLimit, PresheafOfModules.Sheafify.zero_smul, CategoryTheory.Abelian.Ext.contravariant_sequence_exact₃', instAB5AddCommGrpCat, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toBiprod_fromBiprod, CategoryTheory.Pretriangulated.preadditiveYoneda_shiftMap_apply, SheafOfModules.instPreservesFiniteLimitsSheafAddCommGrpCatToSheaf, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_X₂, SheafOfModules.map_ιFree_mapFree_hom_assoc, AlgebraicGeometry.instIsQuasicoherentOpensCarrierCarrierCommRingCatSpecTilde, CategoryTheory.whiskering_linearYoneda₂, PresheafOfModules.instReflectsFiniteLimitsSheafOfModulesSheafAddCommGrpCatToSheaf, AddCommGrpCat.hom_neg_apply, AlgebraicGeometry.Scheme.instIsGrothendieckAbelianSheafProEtTopologyAb, TopCat.Presheaf.restrict_sum, CommGrpCat.toAddCommGrp_obj_coe, ModuleCat.HasColimit.reflectsColimit, AddCommGrpCat.hom_add_apply, AddCommGrpCat.ofHom_injective, SheafOfModules.Presentation.quasicoherentData_I, PresheafOfModules.Sheafify.smul_zero, PresheafOfModules.Sheafify.map_smul, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiprod_δ, CategoryTheory.Pretriangulated.preadditiveYoneda_map_distinguished, PresheafOfModules.toSheafify_app_apply, AddCommGrpCat.instIsRightAdjointForgetAddMonoidHomCarrier, AddCommGrpCat.forget_isCorepresentable, AddCommGrpCat.binaryProductLimitCone_cone_π_app_right, CategoryTheory.Injective.injective_iff_preservesEpimorphisms_preadditiveYoneda_obj, SheafOfModules.generatorsOfIsCokernelFree_s, ModuleCat.forget₂AddCommGroupIsEquivalence, AddCommGrpCat.instPreservesColimitsOfSizeUliftFunctor, AddCommGrpCat.mono_iff_ker_eq_bot, CategoryTheory.preadditiveCoyoneda_obj, instHasExactLimitsOfShapeDiscreteAddCommGrpCat, AddEquiv.toAddCommGrpIso_inv, AddCommGrpCat.hom_neg, CommGrpCat.toAddCommGrp_map, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓFreeOpensCarrierCarrierCommRingCat, AddCommGrpCat.homAddEquiv_apply, PresheafOfModules.Sheafify.SMulCandidate.h, CategoryTheory.Abelian.Ext.contravariantSequence_exact, PresheafOfModules.toPresheaf_map_sheafificationHomEquiv, TopCat.Presheaf.sections_exact_of_exact, SheafOfModules.Presentation.map_π_eq, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toBiprod_apply, AddCommGrpCat.coyonedaType_map_app, commGroupAddCommGroupEquivalence_inverse, AddCommGrpCat.hasColimit_iff_small_quot, AddCommGrpCat.toCommGrp_map, CategoryTheory.Pretriangulated.preadditiveCoyoneda_homologySequenceδ_apply, AddCommGrpCat.instHasBinaryBiproducts, CochainComplex.HomComplex_d_hom_apply, PresheafOfModules.instPreservesFiniteLimitsSheafOfModulesSheafification, AddCommGrpCat.hasLimit_iff_small_sections, AddCommGrpCat.hom_zsmul, AddCommGrpCat.forget_preservesLimitsOfSize, PresheafOfModules.instPreservesFiniteLimitsSheafAddCommGrpCatCompSheafOfModulesSheafificationToSheaf, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_exact, SheafOfModules.Presentation.quasicoherentData_X, SheafOfModules.generatorsOfIsCokernelFree_I, CategoryTheory.Iso.addCommGroupIsoToAddEquiv_apply, CategoryTheory.whiskering_preadditiveCoyoneda, ModuleCat.forget₂_map, AddCommGrpCat.coyoneda_obj_map, AddCommGrpCat.forget_reflects_isos

---

← Back to Index