ConcreteSheafification

📁 Source: Mathlib/CategoryTheory/Sites/ConcreteSheafification.lean

Statistics

Metric	Count
Definitions meqOfSep, mk, isoSheafify, sheafification, sheafify, sheafifyLift, sheafifyMap, toSheafification, toSheafify, Meq, equiv, instCoeFunForallToTypeObjOppositeOpY, mk, pullback, refine, plusPlusAdjunction, plusPlusSheaf	17
Theorems eq_mk_iff_exists, exists_of_sep, exists_rep, inj_of_sep, isSheaf_of_sep, isSheaf_plus_plus, res_mk_eq_mk_pullback, sep, toPlus_apply, toPlus_eq_mk, toPlus_mk, isIso_toSheafify, isoSheafify_hom, isoSheafify_inv, sheafification_map, sheafification_obj, sheafifyLift_unique, sheafifyMap_comp, sheafifyMap_id, sheafifyMap_sheafifyLift, sheafifyMap_sheafifyLift_assoc, sheafify_hom_ext, sheafify_isSheaf, toSheafification_app, toSheafify_naturality, toSheafify_naturality_assoc, toSheafify_sheafifyLift, toSheafify_sheafifyLift_assoc, condition, congr_apply, equiv_apply, equiv_symm_eq_apply, ext, ext_iff, mk_apply, pullback_apply, pullback_refine, refine_apply, mono_iff_presheaf_mono, plusPlusAdjunction_counit_app_val, plusPlusAdjunction_unit_app, plusPlusSheaf_map_val, plusPlusSheaf_obj_val, plusPlusSheaf_preservesZeroMorphisms, presheaf_mono_of_mono, sheafToPresheaf_isRightAdjoint	46
Total	63

CategoryTheory

Definitions

Name	Category	Theorems
Meq 📖	CompOp	2 math math: Meq.equiv_symm_eq_apply, Meq.equiv_apply
plusPlusAdjunction 📖	CompOp	5 math math: GrothendieckTopology.instIsIsoFunctorOppositeSheafSheafComposeNatTransPlusPlusAdjunction, GrothendieckTopology.sheafToPresheaf_map_sheafComposeNatTrans_eq_sheafifyCompIso_inv, plusPlusAdjunction_counit_app_val, plusPlusAdjunction_unit_app, GrothendieckTopology.instIsIsoSheafAppFunctorOppositeSheafComposeNatTransPlusPlusAdjunction
plusPlusSheaf 📖	CompOp	10 math math: plusPlusSheaf_obj_val, plusPlusSheaf_map_val, GrothendieckTopology.instIsIsoFunctorOppositeSheafSheafComposeNatTransPlusPlusAdjunction, GrothendieckTopology.sheafToPresheaf_map_sheafComposeNatTrans_eq_sheafifyCompIso_inv, preservesFiniteLimits_presheafToSheaf, plusPlusAdjunction_counit_app_val, plusPlusSheaf_preservesZeroMorphisms, plusPlusAdjunction_unit_app, preservesLimitsOfShape_presheafToSheaf, GrothendieckTopology.instIsIsoSheafAppFunctorOppositeSheafComposeNatTransPlusPlusAdjunction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
plusPlusAdjunction_counit_app_val 📖	mathematical	Limits.PreservesLimitsOfShape types Limits.WalkingMulticospan GrothendieckTopology.Cover.shape Limits.WalkingMulticospan.instSmallCategory forget Limits.HasMultiequalizer GrothendieckTopology.Cover.index Limits.HasColimitsOfShape Opposite GrothendieckTopology.Cover Category.opposite Preorder.smallCategory GrothendieckTopology.instPreorderCover Limits.PreservesColimitsOfShape	Sheaf.Hom.val Functor.obj Functor Functor.category Sheaf Sheaf.instCategorySheaf plusPlusSheaf sheafToPresheaf Functor.id NatTrans.app Functor.comp Adjunction.counit plusPlusAdjunction GrothendieckTopology.sheafifyLift Sheaf.val CategoryStruct.id Category.toCategoryStruct Sheaf.cond	—	—
plusPlusAdjunction_unit_app 📖	mathematical	Limits.PreservesLimitsOfShape types Limits.WalkingMulticospan GrothendieckTopology.Cover.shape Limits.WalkingMulticospan.instSmallCategory forget Limits.HasMultiequalizer GrothendieckTopology.Cover.index Limits.HasColimitsOfShape Opposite GrothendieckTopology.Cover Category.opposite Preorder.smallCategory GrothendieckTopology.instPreorderCover Limits.PreservesColimitsOfShape	NatTrans.app Functor Functor.category Functor.id Functor.comp Sheaf Sheaf.instCategorySheaf plusPlusSheaf sheafToPresheaf Adjunction.unit plusPlusAdjunction GrothendieckTopology.toSheafify	—	Category.comp_id
plusPlusSheaf_map_val 📖	mathematical	Limits.PreservesLimitsOfShape types Limits.WalkingMulticospan GrothendieckTopology.Cover.shape Limits.WalkingMulticospan.instSmallCategory forget Limits.HasMultiequalizer GrothendieckTopology.Cover.index Limits.HasColimitsOfShape Opposite GrothendieckTopology.Cover Category.opposite Preorder.smallCategory GrothendieckTopology.instPreorderCover Limits.PreservesColimitsOfShape	Sheaf.Hom.val GrothendieckTopology.sheafify GrothendieckTopology.sheafify_isSheaf Functor.map Functor Functor.category Sheaf Sheaf.instCategorySheaf plusPlusSheaf GrothendieckTopology.sheafifyMap	—	GrothendieckTopology.sheafify_isSheaf
plusPlusSheaf_obj_val 📖	mathematical	Limits.PreservesLimitsOfShape types Limits.WalkingMulticospan GrothendieckTopology.Cover.shape Limits.WalkingMulticospan.instSmallCategory forget Limits.HasMultiequalizer GrothendieckTopology.Cover.index Limits.HasColimitsOfShape Opposite GrothendieckTopology.Cover Category.opposite Preorder.smallCategory GrothendieckTopology.instPreorderCover Limits.PreservesColimitsOfShape	Sheaf.val Functor.obj Functor Functor.category Sheaf Sheaf.instCategorySheaf plusPlusSheaf GrothendieckTopology.sheafify	—	—
plusPlusSheaf_preservesZeroMorphisms 📖	mathematical	Limits.PreservesLimitsOfShape types Limits.WalkingMulticospan GrothendieckTopology.Cover.shape Limits.WalkingMulticospan.instSmallCategory forget Limits.HasMultiequalizer GrothendieckTopology.Cover.index Limits.HasColimitsOfShape Opposite GrothendieckTopology.Cover Category.opposite Preorder.smallCategory GrothendieckTopology.instPreorderCover Limits.PreservesColimitsOfShape	Functor.PreservesZeroMorphisms Functor Functor.category Sheaf Sheaf.instCategorySheaf Limits.instHasZeroMorphismsFunctor Preadditive.preadditiveHasZeroMorphisms instPreadditiveSheaf plusPlusSheaf	—	Sheaf.hom_ext NatTrans.ext' Limits.colimit.hom_ext Limits.hasColimitOfHasColimitsOfShape Limits.colimit.ι_map Limits.comp_zero GrothendieckTopology.plusMap_zero GrothendieckTopology.diagramNatTrans_zero Limits.zero_comp
presheaf_mono_of_mono 📖	mathematical	Limits.PreservesLimitsOfShape types Limits.WalkingMulticospan GrothendieckTopology.Cover.shape Limits.WalkingMulticospan.instSmallCategory forget Limits.HasMultiequalizer GrothendieckTopology.Cover.index Limits.HasColimitsOfShape Opposite GrothendieckTopology.Cover Category.opposite Preorder.smallCategory GrothendieckTopology.instPreorderCover Limits.PreservesColimitsOfShape	Mono Functor Functor.category Sheaf.val Sheaf.Hom.val	—	Functor.map_mono preservesMonomorphisms_of_preservesLimitsOfShape Functor.instPreservesLimitsOfShapeOfIsRightAdjoint sheafToPresheaf_isRightAdjoint
sheafToPresheaf_isRightAdjoint 📖	mathematical	Limits.PreservesLimitsOfShape types Limits.WalkingMulticospan GrothendieckTopology.Cover.shape Limits.WalkingMulticospan.instSmallCategory forget Limits.HasMultiequalizer GrothendieckTopology.Cover.index Limits.HasColimitsOfShape Opposite GrothendieckTopology.Cover Category.opposite Preorder.smallCategory GrothendieckTopology.instPreorderCover Limits.PreservesColimitsOfShape	Functor.IsRightAdjoint Functor Functor.category Sheaf Sheaf.instCategorySheaf sheafToPresheaf	—	Adjunction.isRightAdjoint

CategoryTheory.GrothendieckTopology

Definitions

Name	Category	Theorems
isoSheafify 📖	CompOp	2 math math: isoSheafify_hom, isoSheafify_inv
sheafification 📖	CompOp	9 math math: sheafificationWhiskerRightIso_hom_app, preservesLimitsOfShape_sheafification, toSheafification_app, sheafification_obj, preservesFiniteLimits_sheafification, sheafificationWhiskerLeftIso_hom_app, sheafification_map, sheafificationWhiskerLeftIso_inv_app, sheafificationWhiskerRightIso_inv_app
sheafify 📖	CompOp	29 math math: isoSheafify_hom, toSheafify_naturality_assoc, sheafifyMap_sheafifyLift_assoc, whiskerRight_toSheafify_sheafifyCompIso_hom_assoc, sheafificationWhiskerRightIso_hom_app, toSheafify_sheafifyLift_assoc, isIso_toSheafify, CategoryTheory.plusPlusSheaf_obj_val, sheafifyCompIso_inv_eq_sheafifyLift, sheafifyMap_id, sheafifyMap_sheafifyLift, CategoryTheory.Presheaf.isLocallySurjective_toSheafify, CategoryTheory.plusPlusSheaf_map_val, CategoryTheory.Presheaf.isLocallyInjective_toSheafify, toSheafify_comp_sheafifyCompIso_inv_assoc, sheafification_obj, sheafToPresheaf_map_sheafComposeNatTrans_eq_sheafifyCompIso_inv, CategoryTheory.toSheafify_plusPlusIsoSheafify_hom, sheafify_isSheaf, sheafifyMap_comp, toSheafify_comp_sheafifyCompIso_inv, sheafificationWhiskerLeftIso_hom_app, isoSheafify_inv, sheafificationWhiskerLeftIso_inv_app, whiskerRight_toSheafify_sheafifyCompIso_hom, toSheafify_naturality, CategoryTheory.toSheafify_plusPlusIsoSheafify_hom_assoc, sheafificationWhiskerRightIso_inv_app, toSheafify_sheafifyLift
sheafifyLift 📖	CompOp	8 math math: sheafifyMap_sheafifyLift_assoc, toSheafify_sheafifyLift_assoc, sheafifyCompIso_inv_eq_sheafifyLift, sheafifyMap_sheafifyLift, CategoryTheory.plusPlusAdjunction_counit_app_val, isoSheafify_inv, sheafifyLift_unique, toSheafify_sheafifyLift
sheafifyMap 📖	CompOp	8 math math: toSheafify_naturality_assoc, sheafifyMap_sheafifyLift_assoc, sheafifyMap_id, sheafifyMap_sheafifyLift, CategoryTheory.plusPlusSheaf_map_val, sheafifyMap_comp, sheafification_map, toSheafify_naturality
toSheafification 📖	CompOp	1 math math: toSheafification_app
toSheafify 📖	CompOp	17 math math: isoSheafify_hom, toSheafify_naturality_assoc, whiskerRight_toSheafify_sheafifyCompIso_hom_assoc, toSheafify_sheafifyLift_assoc, isIso_toSheafify, sheafifyCompIso_inv_eq_sheafifyLift, CategoryTheory.Presheaf.isLocallySurjective_toSheafify, toSheafification_app, CategoryTheory.Presheaf.isLocallyInjective_toSheafify, toSheafify_comp_sheafifyCompIso_inv_assoc, CategoryTheory.toSheafify_plusPlusIsoSheafify_hom, toSheafify_comp_sheafifyCompIso_inv, CategoryTheory.plusPlusAdjunction_unit_app, whiskerRight_toSheafify_sheafifyCompIso_hom, toSheafify_naturality, CategoryTheory.toSheafify_plusPlusIsoSheafify_hom_assoc, toSheafify_sheafifyLift

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIso_toSheafify 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover CategoryTheory.Presheaf.IsSheaf	CategoryTheory.IsIso CategoryTheory.Functor CategoryTheory.Functor.category sheafify toSheafify	—	CategoryTheory.IsIso.comp_isIso isIso_toPlus_of_isSheaf CategoryTheory.Functor.map_isIso
isoSheafify_hom 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover CategoryTheory.Presheaf.IsSheaf	CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category sheafify isoSheafify toSheafify	—	—
isoSheafify_inv 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover CategoryTheory.Presheaf.IsSheaf	CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category sheafify isoSheafify sheafifyLift CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	sheafifyLift_unique CategoryTheory.Category.id_comp
sheafification_map 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover	CategoryTheory.Functor.map CategoryTheory.Functor CategoryTheory.Functor.category sheafification sheafifyMap	—	—
sheafification_obj 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover	CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category sheafification sheafify	—	—
sheafifyLift_unique 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover CategoryTheory.Presheaf.IsSheaf CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category sheafify toSheafify	sheafifyLift	—	plusLift_unique CategoryTheory.Category.assoc plusMap_toPlus
sheafifyMap_comp 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover	sheafifyMap CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category sheafify	—	plusMap_comp
sheafifyMap_id 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover	sheafifyMap CategoryTheory.CategoryStruct.id CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category sheafify	—	plusMap_id
sheafifyMap_sheafifyLift 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover CategoryTheory.Presheaf.IsSheaf	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category sheafify sheafifyMap sheafifyLift	—	sheafifyLift_unique CategoryTheory.Category.assoc toSheafify_naturality toSheafify_sheafifyLift
sheafifyMap_sheafifyLift_assoc 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover CategoryTheory.Presheaf.IsSheaf	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category sheafify sheafifyMap sheafifyLift	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' sheafifyMap_sheafifyLift
sheafify_hom_ext 📖	—	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover CategoryTheory.Presheaf.IsSheaf CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category sheafify toSheafify	—	—	plus_hom_ext CategoryTheory.Category.assoc plusMap_toPlus
sheafify_isSheaf 📖	mathematical	CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.types CategoryTheory.Limits.WalkingMulticospan Cover.shape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.forget CategoryTheory.Limits.HasMultiequalizer Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover CategoryTheory.Limits.PreservesColimitsOfShape	CategoryTheory.Presheaf.IsSheaf sheafify	—	Plus.isSheaf_plus_plus
toSheafification_app 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover	CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id sheafification toSheafification toSheafify	—	—
toSheafify_naturality 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category sheafify toSheafify sheafifyMap	—	plusMap_toPlus toPlus_naturality toPlus_naturality_assoc CategoryTheory.Category.assoc
toSheafify_naturality_assoc 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category sheafify toSheafify sheafifyMap	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toSheafify_naturality
toSheafify_sheafifyLift 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover CategoryTheory.Presheaf.IsSheaf	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category sheafify toSheafify sheafifyLift	—	plusMap_toPlus toPlus_naturality CategoryTheory.Category.assoc toPlus_plusLift
toSheafify_sheafifyLift_assoc 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover CategoryTheory.Presheaf.IsSheaf	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category sheafify toSheafify sheafifyLift	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toSheafify_sheafifyLift

CategoryTheory.GrothendieckTopology.Plus

Definitions

Name	Category	Theorems
meqOfSep 📖	CompOp	—
mk 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_mk_iff_exists 📖	mathematical	CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.types CategoryTheory.Limits.WalkingMulticospan CategoryTheory.GrothendieckTopology.Cover.shape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.forget CategoryTheory.Limits.HasColimitsOfShape Opposite CategoryTheory.GrothendieckTopology.Cover CategoryTheory.Category.opposite Preorder.smallCategory CategoryTheory.GrothendieckTopology.instPreorderCover CategoryTheory.Limits.HasMultiequalizer CategoryTheory.GrothendieckTopology.Cover.index CategoryTheory.Limits.PreservesColimitsOfShape	CategoryTheory.Meq.refine	—	CategoryTheory.Limits.Concrete.colimit_exists_of_rep_eq CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.isFiltered_op_of_isCofiltered CategoryTheory.isCofiltered_of_directed_ge_nonempty SemilatticeInf.instIsCodirectedOrder CategoryTheory.Meq.ext CategoryTheory.leOfHom CategoryTheory.GrothendieckTopology.Cover.Arrow.hf CategoryTheory.ConcreteCategory.comp_apply CategoryTheory.Limits.Multiequalizer.lift_ι CategoryTheory.Meq.equiv_symm_eq_apply CategoryTheory.Limits.Concrete.colimit_rep_eq_of_exists CategoryTheory.Limits.Concrete.multiequalizer_ext CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit
exists_of_sep 📖	mathematical	CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.types CategoryTheory.Limits.WalkingMulticospan CategoryTheory.GrothendieckTopology.Cover.shape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.forget CategoryTheory.Limits.HasColimitsOfShape Opposite CategoryTheory.GrothendieckTopology.Cover CategoryTheory.Category.opposite Preorder.smallCategory CategoryTheory.GrothendieckTopology.instPreorderCover CategoryTheory.Limits.HasMultiequalizer CategoryTheory.GrothendieckTopology.Cover.index CategoryTheory.Limits.PreservesColimitsOfShape	CategoryTheory.GrothendieckTopology.plusObj	—	inj_of_sep CategoryTheory.Meq.ext res_mk_eq_mk_pullback sep CategoryTheory.Sieve.le_pullback_bind CategoryTheory.GrothendieckTopology.Cover.Arrow.hf CategoryTheory.Sieve.downward_closed toPlus_apply CategoryTheory.GrothendieckTopology.Cover.Arrow.middle_spec CategoryTheory.Meq.condition exists_rep
exists_rep 📖	—	CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.types CategoryTheory.Limits.WalkingMulticospan CategoryTheory.GrothendieckTopology.Cover.shape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.forget CategoryTheory.Limits.HasColimitsOfShape Opposite CategoryTheory.GrothendieckTopology.Cover CategoryTheory.Category.opposite Preorder.smallCategory CategoryTheory.GrothendieckTopology.instPreorderCover CategoryTheory.Limits.HasMultiequalizer CategoryTheory.GrothendieckTopology.Cover.index CategoryTheory.Limits.PreservesColimitsOfShape	—	—	CategoryTheory.Limits.Concrete.colimit_exists_rep CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit Equiv.symm_apply_apply
inj_of_sep 📖	mathematical	CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.types CategoryTheory.Limits.WalkingMulticospan CategoryTheory.GrothendieckTopology.Cover.shape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.forget CategoryTheory.Limits.HasColimitsOfShape Opposite CategoryTheory.GrothendieckTopology.Cover CategoryTheory.Category.opposite Preorder.smallCategory CategoryTheory.GrothendieckTopology.instPreorderCover CategoryTheory.Limits.HasMultiequalizer CategoryTheory.GrothendieckTopology.Cover.index CategoryTheory.Limits.PreservesColimitsOfShape	CategoryTheory.Functor.obj Opposite.op CategoryTheory.GrothendieckTopology.plusObj DFunLike.coe CategoryTheory.ConcreteCategory.hom CategoryTheory.NatTrans.app CategoryTheory.GrothendieckTopology.toPlus	—	eq_mk_iff_exists
isSheaf_of_sep 📖	mathematical	CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.types CategoryTheory.Limits.WalkingMulticospan CategoryTheory.GrothendieckTopology.Cover.shape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.forget CategoryTheory.Limits.HasColimitsOfShape Opposite CategoryTheory.GrothendieckTopology.Cover CategoryTheory.Category.opposite Preorder.smallCategory CategoryTheory.GrothendieckTopology.instPreorderCover CategoryTheory.Limits.HasMultiequalizer CategoryTheory.GrothendieckTopology.Cover.index CategoryTheory.Limits.PreservesColimitsOfShape	CategoryTheory.Presheaf.IsSheaf CategoryTheory.GrothendieckTopology.plusObj	—	CategoryTheory.Presheaf.isSheaf_iff_multiequalizer CategoryTheory.isIso_of_reflects_iso CategoryTheory.isIso_iff_bijective sep CategoryTheory.Meq.equiv_apply CategoryTheory.ConcreteCategory.comp_apply CategoryTheory.Limits.Multiequalizer.lift_ι exists_of_sep Equiv.injective CategoryTheory.Meq.ext
isSheaf_plus_plus 📖	mathematical	CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.types CategoryTheory.Limits.WalkingMulticospan CategoryTheory.GrothendieckTopology.Cover.shape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.forget CategoryTheory.Limits.HasColimitsOfShape Opposite CategoryTheory.GrothendieckTopology.Cover CategoryTheory.Category.opposite Preorder.smallCategory CategoryTheory.GrothendieckTopology.instPreorderCover CategoryTheory.Limits.HasMultiequalizer CategoryTheory.GrothendieckTopology.Cover.index CategoryTheory.Limits.PreservesColimitsOfShape	CategoryTheory.Presheaf.IsSheaf CategoryTheory.GrothendieckTopology.plusObj	—	isSheaf_of_sep sep
res_mk_eq_mk_pullback 📖	mathematical	CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.types CategoryTheory.Limits.WalkingMulticospan CategoryTheory.GrothendieckTopology.Cover.shape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.forget CategoryTheory.Limits.HasColimitsOfShape Opposite CategoryTheory.GrothendieckTopology.Cover CategoryTheory.Category.opposite Preorder.smallCategory CategoryTheory.GrothendieckTopology.instPreorderCover CategoryTheory.Limits.HasMultiequalizer CategoryTheory.GrothendieckTopology.Cover.index	DFunLike.coe CategoryTheory.Functor.obj CategoryTheory.GrothendieckTopology.plusObj Opposite.op CategoryTheory.ConcreteCategory.hom CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.GrothendieckTopology.pullback CategoryTheory.Meq.pullback	—	CategoryTheory.comp_apply CategoryTheory.Limits.ι_colimMap_assoc CategoryTheory.Limits.colimit.ι_pre Equiv.injective Equiv.apply_symm_apply CategoryTheory.Meq.ext CategoryTheory.GrothendieckTopology.Cover.Arrow.hf CategoryTheory.ConcreteCategory.comp_apply CategoryTheory.Limits.Multiequalizer.lift_ι CategoryTheory.Meq.equiv_symm_eq_apply
sep 📖	—	CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.types CategoryTheory.Limits.WalkingMulticospan CategoryTheory.GrothendieckTopology.Cover.shape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.forget CategoryTheory.Limits.HasColimitsOfShape Opposite CategoryTheory.GrothendieckTopology.Cover CategoryTheory.Category.opposite Preorder.smallCategory CategoryTheory.GrothendieckTopology.instPreorderCover CategoryTheory.Limits.HasMultiequalizer CategoryTheory.GrothendieckTopology.Cover.index CategoryTheory.Limits.PreservesColimitsOfShape DFunLike.coe CategoryTheory.Functor.obj CategoryTheory.GrothendieckTopology.plusObj Opposite.op CategoryTheory.GrothendieckTopology.Cover.Arrow.Y CategoryTheory.ConcreteCategory.hom CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.GrothendieckTopology.Cover.Arrow.f	—	—	exists_rep eq_mk_iff_exists CategoryTheory.leOfHom CategoryTheory.Meq.ext CategoryTheory.Meq.congr_apply CategoryTheory.GrothendieckTopology.Cover.Arrow.middle_spec res_mk_eq_mk_pullback
toPlus_apply 📖	mathematical	CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.types CategoryTheory.Limits.WalkingMulticospan CategoryTheory.GrothendieckTopology.Cover.shape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.forget CategoryTheory.Limits.HasColimitsOfShape Opposite CategoryTheory.GrothendieckTopology.Cover CategoryTheory.Category.opposite Preorder.smallCategory CategoryTheory.GrothendieckTopology.instPreorderCover CategoryTheory.Limits.HasMultiequalizer CategoryTheory.GrothendieckTopology.Cover.index	DFunLike.coe CategoryTheory.Functor.obj Opposite.op CategoryTheory.GrothendieckTopology.Cover.Arrow.Y CategoryTheory.GrothendieckTopology.plusObj CategoryTheory.ConcreteCategory.hom CategoryTheory.NatTrans.app CategoryTheory.GrothendieckTopology.toPlus CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.GrothendieckTopology.Cover.Arrow.f	—	CategoryTheory.ConcreteCategory.comp_apply CategoryTheory.Limits.ι_colimMap_assoc CategoryTheory.Limits.colimit.ι_pre OrderTop.le_top CategoryTheory.Limits.colimit.w CategoryTheory.Limits.Concrete.multiequalizer_ext CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.Multiequalizer.lift_ι CategoryTheory.Meq.equiv_symm_eq_apply CategoryTheory.Functor.map_id CategoryTheory.id_apply CategoryTheory.Meq.condition
toPlus_eq_mk 📖	mathematical	CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.types CategoryTheory.Limits.WalkingMulticospan CategoryTheory.GrothendieckTopology.Cover.shape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.forget CategoryTheory.Limits.HasColimitsOfShape Opposite CategoryTheory.GrothendieckTopology.Cover CategoryTheory.Category.opposite Preorder.smallCategory CategoryTheory.GrothendieckTopology.instPreorderCover CategoryTheory.Limits.HasMultiequalizer CategoryTheory.GrothendieckTopology.Cover.index	DFunLike.coe CategoryTheory.Functor.obj Opposite.op CategoryTheory.GrothendieckTopology.plusObj CategoryTheory.ConcreteCategory.hom CategoryTheory.NatTrans.app CategoryTheory.GrothendieckTopology.toPlus Top.top OrderTop.toTop Preorder.toLE CategoryTheory.GrothendieckTopology.Cover.instOrderTop	—	—
toPlus_mk 📖	mathematical	CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.types CategoryTheory.Limits.WalkingMulticospan CategoryTheory.GrothendieckTopology.Cover.shape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.forget CategoryTheory.Limits.HasColimitsOfShape Opposite CategoryTheory.GrothendieckTopology.Cover CategoryTheory.Category.opposite Preorder.smallCategory CategoryTheory.GrothendieckTopology.instPreorderCover CategoryTheory.Limits.HasMultiequalizer CategoryTheory.GrothendieckTopology.Cover.index	DFunLike.coe CategoryTheory.Functor.obj Opposite.op CategoryTheory.GrothendieckTopology.plusObj CategoryTheory.ConcreteCategory.hom CategoryTheory.NatTrans.app CategoryTheory.GrothendieckTopology.toPlus	—	OrderTop.le_top CategoryTheory.Limits.colimit.w CategoryTheory.ConcreteCategory.comp_apply CategoryTheory.Limits.Concrete.multiequalizer_ext CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Category.assoc CategoryTheory.Limits.Multiequalizer.lift_ι CategoryTheory.Meq.equiv_symm_eq_apply

CategoryTheory.Meq

Definitions

Name	Category	Theorems
equiv 📖	CompOp	2 math math: equiv_symm_eq_apply, equiv_apply
instCoeFunForallToTypeObjOppositeOpY 📖	CompOp	—
mk 📖	CompOp	—
pullback 📖	CompOp	3 math math: pullback_refine, CategoryTheory.GrothendieckTopology.Plus.res_mk_eq_mk_pullback, pullback_apply
refine 📖	CompOp	3 math math: pullback_refine, CategoryTheory.GrothendieckTopology.Plus.eq_mk_iff_exists, refine_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
condition 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.GrothendieckTopology.Cover.Arrow.Y CategoryTheory.GrothendieckTopology.Cover.Relation.fst CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.Z CategoryTheory.GrothendieckTopology.Cover.Relation.snd CategoryTheory.GrothendieckTopology.Cover.Relation.r CategoryTheory.ConcreteCategory.hom CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.g₁ CategoryTheory.Limits.MulticospanShape.fst CategoryTheory.GrothendieckTopology.Cover.shape CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.g₂ CategoryTheory.Limits.MulticospanShape.snd	—	—
congr_apply 📖	—	CategoryTheory.Sieve.arrows CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve	—	—	—
equiv_apply 📖	mathematical	CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.types CategoryTheory.Limits.WalkingMulticospan CategoryTheory.GrothendieckTopology.Cover.shape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.forget	DFunLike.coe Equiv CategoryTheory.ToType CategoryTheory.Limits.multiequalizer CategoryTheory.GrothendieckTopology.Cover.index CategoryTheory.Meq EquivLike.toFunLike Equiv.instEquivLike equiv CategoryTheory.Limits.MulticospanIndex.left CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.Multiequalizer.ι	—	—
equiv_symm_eq_apply 📖	mathematical	CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.types CategoryTheory.Limits.WalkingMulticospan CategoryTheory.GrothendieckTopology.Cover.shape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.forget	DFunLike.coe CategoryTheory.Limits.multiequalizer CategoryTheory.GrothendieckTopology.Cover.index CategoryTheory.Limits.MulticospanIndex.left CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.Multiequalizer.ι Equiv CategoryTheory.Meq CategoryTheory.ToType EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equiv	—	Equiv.apply_symm_apply
ext 📖	—	—	—	—	—
ext_iff 📖	—	—	—	—	ext
mk_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.GrothendieckTopology.Cover.Arrow.Y CategoryTheory.ConcreteCategory.hom CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.GrothendieckTopology.Cover.Arrow.f	—	—
pullback_apply 📖	mathematical	—	pullback CategoryTheory.GrothendieckTopology.Cover.Arrow.Y CategoryTheory.Functor.obj CategoryTheory.GrothendieckTopology.Cover Preorder.smallCategory CategoryTheory.GrothendieckTopology.instPreorderCover CategoryTheory.GrothendieckTopology.pullback CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.GrothendieckTopology.Cover.Arrow.f CategoryTheory.GrothendieckTopology.Cover.Arrow.hf	—	—
pullback_refine 📖	mathematical	—	refine CategoryTheory.Functor.obj CategoryTheory.GrothendieckTopology.Cover Preorder.smallCategory CategoryTheory.GrothendieckTopology.instPreorderCover CategoryTheory.GrothendieckTopology.pullback pullback CategoryTheory.Functor.map	—	—
refine_apply 📖	mathematical	—	refine CategoryTheory.GrothendieckTopology.Cover.Arrow.Y CategoryTheory.GrothendieckTopology.Cover.Arrow.f CategoryTheory.leOfHom CategoryTheory.GrothendieckTopology.Cover CategoryTheory.GrothendieckTopology.instPreorderCover CategoryTheory.GrothendieckTopology.Cover.Arrow.hf	—	—

CategoryTheory.Sheaf.Hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mono_iff_presheaf_mono 📖	mathematical	CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.types CategoryTheory.Limits.WalkingMulticospan CategoryTheory.GrothendieckTopology.Cover.shape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.forget CategoryTheory.Limits.HasMultiequalizer CategoryTheory.GrothendieckTopology.Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite CategoryTheory.GrothendieckTopology.Cover CategoryTheory.Category.opposite Preorder.smallCategory CategoryTheory.GrothendieckTopology.instPreorderCover CategoryTheory.Limits.PreservesColimitsOfShape	CategoryTheory.Mono CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Sheaf.val val	—	CategoryTheory.presheaf_mono_of_mono mono_of_presheaf_mono

---

← Back to Index