IsSheafFor

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

Statistics

Metric	Count
Definitions Compatible, familyOfElements, PullbackCompatible, toCompatible, FamilyOfElements, Compatible, IsAmalgamation, PullbackCompatible, SieveCompatible, compPresheafMap, functorPullback, functorPushforward, map, pullback, restrict, sieveExtend, singletonEquiv, IsSeparatedFor, IsSheafFor, amalgamate, extend, YonedaSheafCondition, compatibleEquivGenerateSieveCompatible, instInhabitedFamilyOfElementsBot, natTransEquivCompatibleFamily, shrinkFunctorHomEquiv	26
Theorems exists_familyOfElements, familyOfElements_compatible, familyOfElements_ofArrows_mk, pullbackCompatible_iff, toCompatible_coe, compPresheafMap, functorPullback, map, pullback, restrict, sieveExtend, to_sieveCompatible, compPresheafMap, map, compPresheafMap_comp, compPresheafMap_id, comp_of_compatible, compatible_singleton_iff, ext, ext_iff, isAmalgamation_iff_ofArrows, isAmalgamation_singleton_iff, map_apply, map_comp, map_id, restrict_map, singletonEquiv_apply, singletonEquiv_symm_apply, singletonEquiv_symm_apply_self, ext, isSheafFor, functorInclusion_comp_extend, functorInclusion_comp_extend_assoc, hom_ext, isAmalgamation, isSeparatedFor, unique_extend, valid_glue, compatibleEquivGenerateSieveCompatible_apply_coe, compatibleEquivGenerateSieveCompatible_symm_apply_coe, compatible_iff_sieveCompatible, extend_agrees, extend_restrict, extension_iff_amalgamation, isAmalgamation_restrict, isAmalgamation_sieveExtend, isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor, isSeparatedFor_iff_generate, isSeparatedFor_iso, isSeparatedFor_singleton, isSeparatedFor_top, isSheafFor_arrows_iff, isSheafFor_arrows_iff_pullbacks, isSheafFor_bind, isSheafFor_iff_bijective_shrinkFunctor_ι_comp, isSheafFor_iff_generate, isSheafFor_iff_of_iso, isSheafFor_iff_of_nat_equiv, isSheafFor_iff_yonedaSheafCondition, isSheafFor_iso, isSheafFor_ofArrows_iff_bijective_toCompabible, isSheafFor_of_nat_equiv, isSheafFor_over_map_op_comp_iff, isSheafFor_over_map_op_comp_ofArrows_iff, isSheafFor_pullback_iff, isSheafFor_singleton, isSheafFor_singleton_iso, isSheafFor_subsieve, isSheafFor_subsieve_aux, isSheafFor_top, isSheafFor_top_sieve, isSheafFor_trans, is_compatible_of_exists_amalgamation, pullbackCompatible_iff, restrict_extend, restrict_inj, shrinkFunctorHomEquiv_apply_coe, shrinkFunctorHomEquiv_symm_apply_app, shrinkFunctor_ι_comp_eq_iff_isAmalgamation	79
Total	105

CategoryTheory.Presieve

Definitions

Name	Category	Theorems
FamilyOfElements 📖	CompOp	14 math math: shrinkFunctorHomEquiv_apply_coe, CategoryTheory.Equalizer.firstObjEqFamily_inv, shrinkFunctorHomEquiv_symm_apply_app, CategoryTheory.Equalizer.firstObjEqFamily_hom, FamilyOfElements.singletonEquiv_symm_apply_self, FamilyOfElements.singletonEquiv_apply, CategoryTheory.Equalizer.Presieve.compatible_iff, FamilyOfElements.singletonEquiv_symm_apply, compatibleEquivGenerateSieveCompatible_apply_coe, shrinkFunctor_ι_comp_eq_iff_isAmalgamation, CategoryTheory.Equalizer.Sieve.compatible_iff, extension_iff_amalgamation, Arrows.Compatible.exists_familyOfElements, compatibleEquivGenerateSieveCompatible_symm_apply_coe
IsSeparatedFor 📖	MathDef	10 math math: isSeparatedFor_singleton, isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor, CategoryTheory.PreOneHypercover.IsStronglySeparatedFor.isSeparatedFor_sieve₁, isSeparatedFor_iso, CategoryTheory.PreOneHypercover.IsStronglySheafFor.isSeparatedFor_sieve₁, IsSheafFor.isSeparatedFor, isSeparatedFor_top, CategoryTheory.PreOneHypercover.IsStronglySeparatedFor.isSeparatedFor_presieve₀, CategoryTheory.Presheaf.subsingleton_iff_isSeparatedFor, isSeparatedFor_iff_generate
IsSheafFor 📖	MathDef	74 math math: isSheafFor_pullback_iff, CategoryTheory.regularTopology.isSheafFor_regular_of_projective, CategoryTheory.Equalizer.Sieve.equalizer_sheaf_condition, isSheaf_pretopology, IsSheafFor.singleton_of_isRepresentable_of_effectiveEpi, CategoryTheory.GrothendieckTopology.OneHypercover.isSheafFor_sieve_of_pullback, isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor, isSheafFor_comp_uliftFunctor_iff, CategoryTheory.PreOneHypercover.IsStronglySheafFor.isSheafFor_presieve₀, isSheafFor_iff_preservesProduct, isSheafFor_singleton, CategoryTheory.PreZeroHypercover.isSheafFor_iff_of_iso, AlgebraicGeometry.Scheme.Cover.isSheafFor_sigma_iff, CategoryTheory.Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange_of_small, isSheafFor_iff_yonedaSheafCondition, AlgebraicGeometry.isSheaf_propQCTopology_iff, CategoryTheory.Presheaf.isLimit_iff_isSheafFor_presieve, isSheafFor_top_sieve, isSheafFor_iff_bijective_shrinkFunctor_ι_comp, isSheafFor_of_factorsThru, CategoryTheory.Precoverage.isSheaf_toGrothendieck_iff, isSheafFor_iso, CategoryTheory.Equalizer.Presieve.isSheafFor_singleton_iff, CategoryTheory.Presheaf.IsSheaf.isSheafFor, IsSheafFor.comp_iff_of_preservesPairwisePullbacks, isSheafFor_arrows_iff, AlgebraicGeometry.isSheaf_type_propQCTopology_iff, isSheafFor_subsieve_aux, CategoryTheory.Equalizer.Presieve.sheaf_condition, CategoryTheory.Sieve.EffectiveEpimorphic.iff_forall_isSheafFor_yoneda, isSheafFor_of_nat_equiv, CategoryTheory.Pseudofunctor.isPrestackFor_iff_isSheafFor, CategoryTheory.Pseudofunctor.bijective_toDescentData_map_iff, isSheafFor_of_preservesProduct, CategoryTheory.Sheaf.isSheafFor_trans, isSheafFor_trans, isSheafFor_iff_generate, IsSheaf.isSheafFor_of_mem_precoverage, CategoryTheory.Equalizer.Presieve.Arrows.sheaf_condition, isSheafFor_over_map_op_comp_ofArrows_iff, isSheafFor_over_map_op_comp_iff, EffectiveEpimorphic.iff_forall_isSheafFor_yoneda, isSheafFor_singleton_iff_of_iso, CategoryTheory.PreOneHypercover.IsStronglySheafFor.isSheafFor_sieve_of_pullback, isSheaf_coverage, CategoryTheory.Pseudofunctor.IsPrestackFor.isSheafFor', CategoryTheory.isSheafFor_extensive_of_preservesFiniteProducts, isSheafFor_iff_of_nat_equiv, CategoryTheory.PreZeroHypercover.isLimit_toPreOneHypercover_type_iff, isSheafFor_sigmaDesc_iff, CategoryTheory.Precoverage.ZeroHypercover.Hom.isSheafFor_iff, CategoryTheory.Sieve.forallYonedaIsSheaf_iff_colimit, isSheafFor_arrows_iff_pullbacks, isSheafFor_bind, CategoryTheory.GrothendieckTopology.OneHypercover.isSheafFor_of_pullback, CategoryTheory.isSheaf_coherent, isSheafFor_subsieve, IsSeparatedFor.isSheafFor, CategoryTheory.presheafHom_isSheafFor, CategoryTheory.Sheaf.isSheafFor_bind, isSheafFor_iff_of_iso, CategoryTheory.Presheaf.isLimit_iff_isSheafFor, isSheafFor_singleton_iso, CategoryTheory.Pseudofunctor.isPrestackFor_iff_isSheafFor', CategoryTheory.PreOneHypercover.IsStronglySheafFor.isSheafFor_of_pullback, EffectiveEpimorphic.isSheafFor_of_isRepresentable, isSheafFor_top, CategoryTheory.Equalizer.Presieve.isSheafFor_singleton_iff_of_hasPullback, CategoryTheory.GrothendieckTopology.mem_iff_isSheafFor_closedSieves, CategoryTheory.PreZeroHypercover.isLimit_saturate_type_iff, IsSheaf.isSheafFor, isSheafFor_ofArrows_iff_bijective_toCompabible, isSheafFor_ofArrows_comp_iff, CategoryTheory.Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange
YonedaSheafCondition 📖	MathDef	1 math math: isSheafFor_iff_yonedaSheafCondition
compatibleEquivGenerateSieveCompatible 📖	CompOp	2 math math: compatibleEquivGenerateSieveCompatible_apply_coe, compatibleEquivGenerateSieveCompatible_symm_apply_coe
instInhabitedFamilyOfElementsBot 📖	CompOp	—
natTransEquivCompatibleFamily 📖	CompOp	—
shrinkFunctorHomEquiv 📖	CompOp	4 math math: shrinkFunctorHomEquiv_apply_coe, shrinkFunctorHomEquiv_symm_apply_app, shrinkFunctor_ι_comp_eq_iff_isAmalgamation, extension_iff_amalgamation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compatibleEquivGenerateSieveCompatible_apply_coe 📖	mathematical	—	FamilyOfElements CategoryTheory.Sieve.arrows CategoryTheory.Sieve.generate FamilyOfElements.Compatible DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike compatibleEquivGenerateSieveCompatible FamilyOfElements.sieveExtend	—	—
compatibleEquivGenerateSieveCompatible_symm_apply_coe 📖	mathematical	—	FamilyOfElements FamilyOfElements.Compatible DFunLike.coe Equiv CategoryTheory.Sieve.arrows CategoryTheory.Sieve.generate EquivLike.toFunLike Equiv.instEquivLike Equiv.symm compatibleEquivGenerateSieveCompatible FamilyOfElements.restrict CategoryTheory.Sieve.le_generate	—	—
compatible_iff_sieveCompatible 📖	mathematical	—	FamilyOfElements.Compatible CategoryTheory.Sieve.arrows FamilyOfElements.SieveCompatible	—	CategoryTheory.Sieve.downward_closed CategoryTheory.FunctorToTypes.map_id_apply CategoryTheory.Category.id_comp
extend_agrees 📖	mathematical	FamilyOfElements.Compatible	FamilyOfElements.sieveExtend CategoryTheory.Sieve.le_generate	—	CategoryTheory.Sieve.le_generate CategoryTheory.Category.id_comp CategoryTheory.FunctorToTypes.map_id_apply
extend_restrict 📖	mathematical	FamilyOfElements.Compatible CategoryTheory.Sieve.arrows CategoryTheory.Sieve.generate	FamilyOfElements.sieveExtend FamilyOfElements.restrict CategoryTheory.Sieve.arrows CategoryTheory.Sieve.generate CategoryTheory.Sieve.le_generate	—	CategoryTheory.Sieve.le_generate CategoryTheory.Sieve.downward_closed compatible_iff_sieveCompatible
extension_iff_amalgamation 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Subfunctor.toFunctor CategoryTheory.Functor.obj CategoryTheory.shrinkYoneda CategoryTheory.Sieve.shrinkFunctor CategoryTheory.Subfunctor.ι FamilyOfElements.IsAmalgamation CategoryTheory.Sieve.arrows FamilyOfElements FamilyOfElements.Compatible DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver EquivLike.toFunLike Equiv.instEquivLike shrinkFunctorHomEquiv Opposite.op CategoryTheory.shrinkYonedaEquiv	—	shrinkFunctor_ι_comp_eq_iff_isAmalgamation
isAmalgamation_restrict 📖	mathematical	CategoryTheory.Presieve Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CategoryTheory.instCompleteLatticePresieve FamilyOfElements.IsAmalgamation	FamilyOfElements.IsAmalgamation FamilyOfElements.restrict	—	—
isAmalgamation_sieveExtend 📖	mathematical	FamilyOfElements.IsAmalgamation	FamilyOfElements.IsAmalgamation CategoryTheory.Sieve.arrows CategoryTheory.Sieve.generate FamilyOfElements.sieveExtend	—	CategoryTheory.FunctorToTypes.map_comp_apply CategoryTheory.op_comp
isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor 📖	mathematical	—	IsSeparatedFor CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op FamilyOfElements.IsAmalgamation IsSheafFor	—	IsSeparatedFor.eq_1 existsUnique_of_exists_of_unique ExistsUnique.unique is_compatible_of_exists_amalgamation ExistsUnique.exists
isSeparatedFor_iff_generate 📖	mathematical	—	IsSeparatedFor CategoryTheory.Sieve.arrows CategoryTheory.Sieve.generate	—	CategoryTheory.Sieve.le_generate isAmalgamation_restrict isAmalgamation_sieveExtend
isSeparatedFor_iso 📖	mathematical	IsSeparatedFor	IsSeparatedFor	—	CategoryTheory.FunctorToTypes.inv_hom_id_app_apply FamilyOfElements.IsAmalgamation.map
isSeparatedFor_singleton 📖	mathematical	—	IsSeparatedFor singleton CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	IsSeparatedFor.eq_1 Equiv.forall_congr_left FamilyOfElements.singletonEquiv_symm_apply_self
isSeparatedFor_top 📖	mathematical	—	IsSeparatedFor Top.top CategoryTheory.Presieve OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.instCompleteLatticePresieve BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	CategoryTheory.FunctorToTypes.map_id_apply
isSheafFor_arrows_iff 📖	mathematical	—	IsSheafFor ofArrows ExistsUnique CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op	—	Arrows.Compatible.familyOfElements_compatible
isSheafFor_arrows_iff_pullbacks 📖	mathematical	—	IsSheafFor ofArrows ExistsUnique CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op	—	—
isSheafFor_bind 📖	mathematical	IsSheafFor CategoryTheory.Sieve.arrows IsSeparatedFor CategoryTheory.Sieve.pullback	IsSheafFor CategoryTheory.Sieve.arrows CategoryTheory.Sieve.bind	—	bind_comp CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' IsSheafFor.isAmalgamation compatible_iff_sieveCompatible IsSeparatedFor.ext CategoryTheory.Sieve.downward_closed IsSheafFor.isSeparatedFor CategoryTheory.FunctorToTypes.map_comp_apply CategoryTheory.op_comp IsSheafFor.valid_glue
isSheafFor_iff_bijective_shrinkFunctor_ι_comp 📖	mathematical	—	IsSheafFor CategoryTheory.Sieve.arrows Function.Bijective Quiver.Hom CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.shrinkYoneda CategoryTheory.Subfunctor.toFunctor CategoryTheory.Sieve.shrinkFunctor CategoryTheory.CategoryStruct.comp CategoryTheory.Subfunctor.ι	—	Equiv.forall_congr_left Equiv.apply_symm_apply
isSheafFor_iff_generate 📖	mathematical	—	IsSheafFor CategoryTheory.Sieve.arrows CategoryTheory.Sieve.generate	—	isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor isSeparatedFor_iff_generate CategoryTheory.Sieve.le_generate extend_restrict isAmalgamation_sieveExtend FamilyOfElements.Compatible.restrict restrict_extend isAmalgamation_restrict FamilyOfElements.Compatible.sieveExtend
isSheafFor_iff_of_iso 📖	mathematical	—	IsSheafFor	—	isSheafFor_iso
isSheafFor_iff_of_nat_equiv 📖	mathematical	DFunLike.coe Equiv CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	IsSheafFor	—	isSheafFor_of_nat_equiv Equiv.surjective Equiv.injective Equiv.apply_symm_apply Equiv.symm_apply_apply
isSheafFor_iff_yonedaSheafCondition 📖	mathematical	—	IsSheafFor CategoryTheory.Sieve.arrows YonedaSheafCondition	—	CategoryTheory.locallySmall_of_univLE UnivLE.self isSheafFor_iff_bijective_shrinkFunctor_ι_comp YonedaSheafCondition.eq_1 Function.bijective_iff_existsUnique Equiv.forall_congr_left Equiv.existsUnique_congr_left existsUnique_congr CategoryTheory.NatTrans.ext_iff Equiv.apply_symm_apply
isSheafFor_iso 📖	mathematical	IsSheafFor	IsSheafFor	—	isSheafFor_of_nat_equiv CategoryTheory.NatTrans.naturality
isSheafFor_ofArrows_iff_bijective_toCompabible 📖	mathematical	—	IsSheafFor ofArrows Function.Bijective CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op Arrows.Compatible Arrows.toCompatible	—	isSheafFor_arrows_iff ExistsUnique.unique
isSheafFor_of_nat_equiv 📖	mathematical	DFunLike.coe Equiv CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct IsSheafFor	IsSheafFor	—	Equiv.injective Equiv.apply_symm_apply EquivLike.toEmbeddingLike Equiv.symm_apply_apply IsSheafFor.isAmalgamation IsSheafFor.isSeparatedFor
isSheafFor_over_map_op_comp_iff 📖	mathematical	—	IsSheafFor CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.op CategoryTheory.Over.map CategoryTheory.Sieve.arrows CategoryTheory.Sieve.pullback CategoryTheory.Functor.obj CategoryTheory.Iso.inv CategoryTheory.Sieve.functorPushforward	—	CategoryTheory.Sieve.exists_eq_ofArrows isSheafFor_iff_generate isSheafFor_pullback_iff CategoryTheory.Iso.isIso_inv isSheafFor_over_map_op_comp_ofArrows_iff le_antisymm CategoryTheory.Category.assoc CategoryTheory.Over.w_assoc CategoryTheory.Over.w CategoryTheory.Functor.map_comp CategoryTheory.Over.OverMorphism.ext
isSheafFor_over_map_op_comp_ofArrows_iff 📖	mathematical	—	IsSheafFor CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.op CategoryTheory.Over.map ofArrows CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	CategoryTheory.Functor.congr_map CategoryTheory.Over.w CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Over.OverMorphism.ext CategoryTheory.Category.id_comp CategoryTheory.FunctorToTypes.map_comp_apply Function.Bijective.of_comp_iff' Equiv.bijective
isSheafFor_pullback_iff 📖	mathematical	—	IsSheafFor CategoryTheory.Sieve.arrows CategoryTheory.Sieve.pullback	—	CategoryTheory.Sieve.exists_eq_ofArrows CategoryTheory.Sieve.pullback_ofArrows_of_iso CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.strongMono_of_isIso CategoryTheory.Category.assoc CategoryTheory.IsIso.inv_hom_id CategoryTheory.Category.comp_id CategoryTheory.eq_whisker Function.Bijective.of_comp_iff' Equiv.bijective Function.Bijective.of_comp_iff CategoryTheory.Functor.map_isIso CategoryTheory.isIso_op CategoryTheory.op_inv CategoryTheory.Functor.map_inv CategoryTheory.FunctorToTypes.map_comp_apply
isSheafFor_singleton 📖	mathematical	—	IsSheafFor singleton ExistsUnique CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	IsSheafFor.eq_1 Equiv.forall_congr_left FamilyOfElements.singletonEquiv_symm_apply_self
isSheafFor_singleton_iso 📖	mathematical	—	IsSheafFor singleton CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	singleton_self CategoryTheory.FunctorToTypes.map_id_apply
isSheafFor_subsieve 📖	mathematical	CategoryTheory.Presieve Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CategoryTheory.instCompleteLatticePresieve CategoryTheory.Sieve.arrows IsSheafFor CategoryTheory.Sieve.pullback	IsSheafFor	—	isSheafFor_subsieve_aux CategoryTheory.Sieve.pullback_id IsSheafFor.isSeparatedFor
isSheafFor_subsieve_aux 📖	mathematical	CategoryTheory.Presieve Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CategoryTheory.instCompleteLatticePresieve CategoryTheory.Sieve.arrows IsSheafFor IsSeparatedFor CategoryTheory.Sieve.pullback	IsSheafFor	—	isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor IsSheafFor.isSeparatedFor isAmalgamation_restrict FamilyOfElements.Compatible.restrict IsSeparatedFor.ext CategoryTheory.FunctorToTypes.map_comp_apply CategoryTheory.op_comp IsSheafFor.valid_glue FamilyOfElements.restrict.eq_1 CategoryTheory.Category.id_comp CategoryTheory.FunctorToTypes.map_id_apply
isSheafFor_top 📖	mathematical	—	IsSheafFor Top.top CategoryTheory.Presieve OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.instCompleteLatticePresieve BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	CategoryTheory.Sieve.arrows_top CategoryTheory.Sieve.generate_of_singleton_isSplitEpi CategoryTheory.IsSplitEpi.of_iso CategoryTheory.IsIso.id isSheafFor_iff_generate isSheafFor_singleton_iso
isSheafFor_top_sieve 📖	mathematical	—	IsSheafFor Top.top CategoryTheory.Presieve OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.instCompleteLatticePresieve BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	isSheafFor_top
isSheafFor_trans 📖	mathematical	IsSheafFor CategoryTheory.Sieve.arrows IsSeparatedFor CategoryTheory.Sieve.pullback	IsSheafFor CategoryTheory.Sieve.arrows	—	isSheafFor_subsieve_aux isSheafFor_bind CategoryTheory.Sieve.pullback_comp IsSheafFor.isSeparatedFor CategoryTheory.Sieve.downward_closed CategoryTheory.Sieve.ext CategoryTheory.Sieve.pullback_apply CategoryTheory.Category.id_comp
is_compatible_of_exists_amalgamation 📖	mathematical	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op FamilyOfElements.IsAmalgamation	FamilyOfElements.Compatible	—	CategoryTheory.FunctorToTypes.map_comp_apply CategoryTheory.op_comp
pullbackCompatible_iff 📖	mathematical	—	FamilyOfElements.Compatible FamilyOfElements.PullbackCompatible	—	HasPairwisePullbacks.has_pullbacks CategoryTheory.Limits.pullback.condition CategoryTheory.Limits.pullback.lift_fst CategoryTheory.op_comp CategoryTheory.FunctorToTypes.map_comp_apply CategoryTheory.Limits.pullback.lift_snd
restrict_extend 📖	mathematical	FamilyOfElements.Compatible	FamilyOfElements.restrict CategoryTheory.Sieve.arrows CategoryTheory.Sieve.generate CategoryTheory.Sieve.le_generate FamilyOfElements.sieveExtend	—	CategoryTheory.Sieve.le_generate extend_agrees
restrict_inj 📖	—	FamilyOfElements.Compatible CategoryTheory.Sieve.arrows CategoryTheory.Sieve.generate FamilyOfElements.restrict CategoryTheory.Sieve.le_generate	—	—	CategoryTheory.Sieve.le_generate extend_restrict
shrinkFunctorHomEquiv_apply_coe 📖	mathematical	CategoryTheory.Sieve.arrows	FamilyOfElements CategoryTheory.Sieve.arrows FamilyOfElements.Compatible DFunLike.coe Equiv Quiver.Hom CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Subfunctor.toFunctor CategoryTheory.Functor.obj CategoryTheory.shrinkYoneda CategoryTheory.Sieve.shrinkFunctor EquivLike.toFunLike Equiv.instEquivLike shrinkFunctorHomEquiv CategoryTheory.NatTrans.app Opposite.op Set Set.instMembership CategoryTheory.Subfunctor.obj Opposite.unop Equiv.symm CategoryTheory.shrinkYonedaObjObjEquiv	—	—
shrinkFunctorHomEquiv_symm_apply_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Subfunctor.toFunctor CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.shrinkYoneda CategoryTheory.Sieve.shrinkFunctor DFunLike.coe Equiv FamilyOfElements CategoryTheory.Sieve.arrows FamilyOfElements.Compatible Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike Equiv.symm shrinkFunctorHomEquiv Opposite.unop CategoryTheory.shrinkYonedaObjObjEquiv Set Set.instMembership CategoryTheory.Subfunctor.obj	—	—
shrinkFunctor_ι_comp_eq_iff_isAmalgamation 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Subfunctor.toFunctor CategoryTheory.Functor.obj CategoryTheory.shrinkYoneda CategoryTheory.Sieve.shrinkFunctor CategoryTheory.Subfunctor.ι FamilyOfElements.IsAmalgamation CategoryTheory.Sieve.arrows FamilyOfElements FamilyOfElements.Compatible DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver EquivLike.toFunLike Equiv.instEquivLike shrinkFunctorHomEquiv Opposite.op CategoryTheory.shrinkYonedaEquiv	—	CategoryTheory.shrinkYonedaEquiv_naturality CategoryTheory.shrinkYonedaEquiv_comp CategoryTheory.shrinkYonedaEquiv_shrinkYoneda_map CategoryTheory.NatTrans.ext' CategoryTheory.types_ext Equiv.symm_apply_apply Mathlib.Tactic.DepRewrite.nddcongrArg

CategoryTheory.Presieve.Arrows

Definitions

Name	Category	Theorems
Compatible 📖	MathDef	11 math math: CategoryTheory.Pseudofunctor.DescentData.subtypeCompatibleHomEquiv_toCompatible_presheafHomObjHomEquiv, CategoryTheory.Equalizer.Presieve.Arrows.compatible_iff, CategoryTheory.PreZeroHypercover.sectionsSaturateEquiv_apply_coe, CategoryTheory.PreOneHypercover.IsStronglySeparatedFor.arrowsCompatible, CategoryTheory.Equalizer.Presieve.Arrows.compatible_iff_of_small, toCompatible_coe, pullbackCompatible_iff, CategoryTheory.PreZeroHypercover.sectionsSaturateEquiv_symm_apply_val, CategoryTheory.PreZeroHypercover.sectionsEquivOfHasPullbacks_symm_apply_val, CategoryTheory.Presieve.isSheafFor_ofArrows_iff_bijective_toCompabible, CategoryTheory.PreZeroHypercover.sectionsEquivOfHasPullbacks_apply_coe
PullbackCompatible 📖	MathDef	1 math math: pullbackCompatible_iff
toCompatible 📖	CompOp	3 math math: CategoryTheory.Pseudofunctor.DescentData.subtypeCompatibleHomEquiv_toCompatible_presheafHomObjHomEquiv, toCompatible_coe, CategoryTheory.Presieve.isSheafFor_ofArrows_iff_bijective_toCompabible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pullbackCompatible_iff 📖	mathematical	—	Compatible PullbackCompatible	—	CategoryTheory.Presieve.instHasPullbackOfHasPairwisePullbacksOfArrows CategoryTheory.Limits.pullback.condition CategoryTheory.Limits.pullback.lift_fst CategoryTheory.op_comp CategoryTheory.FunctorToTypes.map_comp_apply CategoryTheory.Limits.pullback.lift_snd
toCompatible_coe 📖	mathematical	—	Compatible toCompatible CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—

CategoryTheory.Presieve.Arrows.Compatible

Definitions

Name	Category	Theorems
familyOfElements 📖	CompOp	2 math math: familyOfElements_ofArrows_mk, familyOfElements_compatible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_familyOfElements 📖	mathematical	CategoryTheory.Presieve.Arrows.Compatible	CategoryTheory.Presieve.FamilyOfElements CategoryTheory.Presieve.ofArrows	—	CategoryTheory.Category.id_comp CategoryTheory.FunctorToTypes.map_id_apply CategoryTheory.Presieve.ofArrows_surj
familyOfElements_compatible 📖	mathematical	CategoryTheory.Presieve.Arrows.Compatible	CategoryTheory.Presieve.FamilyOfElements.Compatible CategoryTheory.Presieve.ofArrows familyOfElements	—	—
familyOfElements_ofArrows_mk 📖	mathematical	CategoryTheory.Presieve.Arrows.Compatible	familyOfElements	—	exists_familyOfElements

CategoryTheory.Presieve.FamilyOfElements

Definitions

Name	Category	Theorems
Compatible 📖	MathDef	26 math math: Compatible.map, CategoryTheory.Presieve.shrinkFunctorHomEquiv_apply_coe, isCompatible_map_smul, CategoryTheory.Presieve.is_compatible_of_exists_amalgamation, CategoryTheory.Presieve.shrinkFunctorHomEquiv_symm_apply_app, compatible_singleton_iff, CategoryTheory.Presieve.pullbackCompatible_iff, Compatible.functorPushforward, CategoryTheory.Equalizer.Presieve.compatible_iff, Compatible.pullback, CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily_compatible, CategoryTheory.Presieve.Arrows.Compatible.familyOfElements_compatible, CategoryTheory.Sieve.yonedaFamily_fromCocone_compatible, Compatible.restrict, Compatible.functorPullback, CategoryTheory.Presieve.compatibleEquivGenerateSieveCompatible_apply_coe, CategoryTheory.Presieve.shrinkFunctor_ι_comp_eq_iff_isAmalgamation, CategoryTheory.Subfunctor.Subpresheaf.family_of_elements_compatible, CategoryTheory.Equalizer.Sieve.compatible_iff, CategoryTheory.Presieve.compatible_iff_sieveCompatible, CategoryTheory.Presieve.extension_iff_amalgamation, Compatible.sieveExtend, CategoryTheory.Presheaf.FamilyOfElementsOnObjects.IsCompatible.familyOfElements_isCompatible, CategoryTheory.Subfunctor.family_of_elements_compatible, CategoryTheory.Presieve.compatibleEquivGenerateSieveCompatible_symm_apply_coe, Compatible.compPresheafMap
IsAmalgamation 📖	MathDef	12 math math: CategoryTheory.Presieve.IsSheafFor.isAmalgamation, CategoryTheory.Presieve.isAmalgamation_sieveExtend, CategoryTheory.Presieve.isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor, isAmalgamation_iff_ofArrows, IsAmalgamation.compPresheafMap, isAmalgamation_singleton_iff, CategoryTheory.Presieve.shrinkFunctor_ι_comp_eq_iff_isAmalgamation, isAmalgamation_map_localPreimage, CategoryTheory.Presieve.isAmalgamation_restrict, CategoryTheory.Presieve.extension_iff_amalgamation, IsAmalgamation.map, CategoryTheory.PresheafHom.isAmalgamation_iff
PullbackCompatible 📖	MathDef	1 math math: CategoryTheory.Presieve.pullbackCompatible_iff
SieveCompatible 📖	MathDef	2 math math: CategoryTheory.Presieve.compatible_iff_sieveCompatible, Compatible.to_sieveCompatible
compPresheafMap 📖	CompOp	—
functorPullback 📖	CompOp	1 math math: Compatible.functorPullback
functorPushforward 📖	CompOp	2 math math: Compatible.functorPushforward, CategoryTheory.CompatiblePreserving.apply_map
map 📖	CompOp	12 math math: Compatible.map, isCompatible_map_smul, map_apply, IsAmalgamation.compPresheafMap, compPresheafMap_comp, isAmalgamation_map_localPreimage, restrict_map, compPresheafMap_id, IsAmalgamation.map, map_comp, Compatible.compPresheafMap, map_id
pullback 📖	CompOp	1 math math: Compatible.pullback
restrict 📖	CompOp	6 math math: CategoryTheory.Presieve.extend_restrict, Compatible.restrict, CategoryTheory.Presieve.restrict_extend, restrict_map, CategoryTheory.Presieve.isAmalgamation_restrict, CategoryTheory.Presieve.compatibleEquivGenerateSieveCompatible_symm_apply_coe
sieveExtend 📖	CompOp	6 math math: CategoryTheory.Presieve.isAmalgamation_sieveExtend, CategoryTheory.Presieve.extend_restrict, CategoryTheory.Presieve.extend_agrees, CategoryTheory.Presieve.compatibleEquivGenerateSieveCompatible_apply_coe, CategoryTheory.Presieve.restrict_extend, Compatible.sieveExtend
singletonEquiv 📖	CompOp	3 math math: singletonEquiv_symm_apply_self, singletonEquiv_apply, singletonEquiv_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compPresheafMap_comp 📖	mathematical	—	map CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category	—	map_comp
compPresheafMap_id 📖	mathematical	—	map CategoryTheory.CategoryStruct.id CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category	—	map_id
comp_of_compatible 📖	mathematical	Compatible CategoryTheory.Sieve.arrows	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Sieve.downward_closed CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	—	CategoryTheory.Sieve.downward_closed CategoryTheory.FunctorToTypes.map_id_apply CategoryTheory.Category.id_comp
compatible_singleton_iff 📖	mathematical	—	Compatible CategoryTheory.Presieve.singleton CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
ext 📖	—	—	—	—	—
ext_iff 📖	—	—	—	—	ext
isAmalgamation_iff_ofArrows 📖	mathematical	—	IsAmalgamation CategoryTheory.Presieve.ofArrows CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
isAmalgamation_singleton_iff 📖	mathematical	—	IsAmalgamation CategoryTheory.Presieve.singleton CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
map_apply 📖	mathematical	—	map CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op	—	—
map_comp 📖	mathematical	—	map CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category	—	—
map_id 📖	mathematical	—	map CategoryTheory.CategoryStruct.id CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category	—	—
restrict_map 📖	mathematical	CategoryTheory.Presieve Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CategoryTheory.instCompleteLatticePresieve	map restrict	—	—
singletonEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.Presieve.FamilyOfElements CategoryTheory.Presieve.singleton CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op EquivLike.toFunLike Equiv.instEquivLike singletonEquiv	—	—
singletonEquiv_symm_apply 📖	mathematical	CategoryTheory.Presieve.singleton	DFunLike.coe Equiv CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op CategoryTheory.Presieve.FamilyOfElements CategoryTheory.Presieve.singleton EquivLike.toFunLike Equiv.instEquivLike Equiv.symm singletonEquiv CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom	—	—
singletonEquiv_symm_apply_self 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op CategoryTheory.Presieve.FamilyOfElements CategoryTheory.Presieve.singleton EquivLike.toFunLike Equiv.instEquivLike Equiv.symm singletonEquiv	—	CategoryTheory.FunctorToTypes.map_id_apply

CategoryTheory.Presieve.FamilyOfElements.Compatible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compPresheafMap 📖	mathematical	CategoryTheory.Presieve.FamilyOfElements.Compatible	CategoryTheory.Presieve.FamilyOfElements.Compatible CategoryTheory.Presieve.FamilyOfElements.map	—	map
functorPullback 📖	mathematical	CategoryTheory.Presieve.FamilyOfElements.Compatible CategoryTheory.Functor.obj	CategoryTheory.Presieve.FamilyOfElements.Compatible CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.op CategoryTheory.Presieve.functorPullback CategoryTheory.Presieve.FamilyOfElements.functorPullback	—	CategoryTheory.Functor.map_comp
map 📖	mathematical	CategoryTheory.Presieve.FamilyOfElements.Compatible	CategoryTheory.Presieve.FamilyOfElements.Compatible CategoryTheory.Presieve.FamilyOfElements.map	—	CategoryTheory.FunctorToTypes.naturality
pullback 📖	mathematical	CategoryTheory.Presieve.FamilyOfElements.Compatible CategoryTheory.Sieve.arrows	CategoryTheory.Presieve.FamilyOfElements.Compatible CategoryTheory.Sieve.arrows CategoryTheory.Sieve.pullback CategoryTheory.Presieve.FamilyOfElements.pullback	—	CategoryTheory.Sieve.downward_closed CategoryTheory.Category.assoc
restrict 📖	mathematical	CategoryTheory.Presieve Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CategoryTheory.instCompleteLatticePresieve CategoryTheory.Presieve.FamilyOfElements.Compatible	CategoryTheory.Presieve.FamilyOfElements.Compatible CategoryTheory.Presieve.FamilyOfElements.restrict	—	—
sieveExtend 📖	mathematical	CategoryTheory.Presieve.FamilyOfElements.Compatible	CategoryTheory.Presieve.FamilyOfElements.Compatible CategoryTheory.Sieve.arrows CategoryTheory.Sieve.generate CategoryTheory.Presieve.FamilyOfElements.sieveExtend	—	CategoryTheory.FunctorToTypes.map_comp_apply CategoryTheory.op_comp CategoryTheory.Category.assoc
to_sieveCompatible 📖	mathematical	CategoryTheory.Presieve.FamilyOfElements.Compatible CategoryTheory.Sieve.arrows	CategoryTheory.Presieve.FamilyOfElements.SieveCompatible	—	CategoryTheory.Presieve.compatible_iff_sieveCompatible

CategoryTheory.Presieve.FamilyOfElements.IsAmalgamation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compPresheafMap 📖	mathematical	CategoryTheory.Presieve.FamilyOfElements.IsAmalgamation	CategoryTheory.Presieve.FamilyOfElements.IsAmalgamation CategoryTheory.Presieve.FamilyOfElements.map CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op	—	map
map 📖	mathematical	CategoryTheory.Presieve.FamilyOfElements.IsAmalgamation	CategoryTheory.Presieve.FamilyOfElements.IsAmalgamation CategoryTheory.Presieve.FamilyOfElements.map CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op	—	CategoryTheory.NatTrans.naturality CategoryTheory.types_comp_apply

CategoryTheory.Presieve.IsSeparatedFor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	CategoryTheory.Presieve.IsSeparatedFor CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—	—
isSheafFor 📖	mathematical	CategoryTheory.Presieve.IsSeparatedFor CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op CategoryTheory.Presieve.FamilyOfElements.IsAmalgamation	CategoryTheory.Presieve.IsSheafFor	—	CategoryTheory.Presieve.isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor

CategoryTheory.Presieve.IsSheafFor

Definitions

Name	Category	Theorems
amalgamate 📖	CompOp	3 math math: isAmalgamation, CategoryTheory.Functor.IsCoverDense.sheaf_eq_amalgamation, valid_glue
extend 📖	CompOp	3 math math: unique_extend, functorInclusion_comp_extend, functorInclusion_comp_extend_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
functorInclusion_comp_extend 📖	mathematical	CategoryTheory.Presieve.IsSheafFor CategoryTheory.Sieve.arrows	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Sieve.functor CategoryTheory.Functor.obj CategoryTheory.yoneda CategoryTheory.Sieve.functorInclusion extend	—	ExistsUnique.exists CategoryTheory.Presieve.isSheafFor_iff_yonedaSheafCondition
functorInclusion_comp_extend_assoc 📖	mathematical	CategoryTheory.Presieve.IsSheafFor CategoryTheory.Sieve.arrows	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Sieve.functor CategoryTheory.Functor.obj CategoryTheory.yoneda CategoryTheory.Sieve.functorInclusion extend	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' functorInclusion_comp_extend
hom_ext 📖	—	CategoryTheory.Presieve.IsSheafFor CategoryTheory.Sieve.arrows CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Sieve.functor CategoryTheory.Functor.obj CategoryTheory.yoneda CategoryTheory.Sieve.functorInclusion	—	—	unique_extend
isAmalgamation 📖	mathematical	CategoryTheory.Presieve.IsSheafFor CategoryTheory.Presieve.FamilyOfElements.Compatible	CategoryTheory.Presieve.FamilyOfElements.IsAmalgamation amalgamate	—	ExistsUnique.exists
isSeparatedFor 📖	mathematical	CategoryTheory.Presieve.IsSheafFor	CategoryTheory.Presieve.IsSeparatedFor	—	CategoryTheory.Presieve.isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor
unique_extend 📖	mathematical	CategoryTheory.Presieve.IsSheafFor CategoryTheory.Sieve.arrows CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Sieve.functor CategoryTheory.Functor.obj CategoryTheory.yoneda CategoryTheory.Sieve.functorInclusion	extend	—	ExistsUnique.unique CategoryTheory.Presieve.isSheafFor_iff_yonedaSheafCondition functorInclusion_comp_extend
valid_glue 📖	mathematical	CategoryTheory.Presieve.IsSheafFor CategoryTheory.Presieve.FamilyOfElements.Compatible	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct amalgamate	—	isAmalgamation

---

← Back to Index