Sheaf

📁 Source: Mathlib/CategoryTheory/Topos/Sheaf.lean

Statistics

Metric	Count
Definitions classifier, truth, χ, classifier, truth, Ω, χ	7
Theorems isClosed_χ_app_apply_of_isSheaf_of_isSeparated, classifier_truth, classifier_Ω, classifier_Ω₀, classifier_χ, classifier_χ₀, comp_χ_eq, isPullback_χ_truth, truth_app, χ_app, χ_unique, classifier_truth, classifier_Ω, classifier_Ω₀, classifier_χ, classifier_χ₀, instHasSubobjectClassifierTypeOfEssentiallySmall, isPullback_χ_truth, truth_hom, Ω_obj, χ_hom, χ_unique, instHasSubobjectClassifierFunctorOppositeTypeOfEssentiallySmall	23
Total	30

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasSubobjectClassifierFunctorOppositeTypeOfEssentiallySmall 📖	mathematical	—	HasSubobjectClassifier Functor Opposite Category.opposite types Functor.category	—	—

CategoryTheory.GrothendieckTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isClosed_χ_app_apply_of_isSheaf_of_isSeparated 📖	mathematical	CategoryTheory.Presieve.IsSheaf CategoryTheory.Presieve.IsSeparated	IsClosed Opposite.unop CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.sieves CategoryTheory.Presheaf.χ	—	CategoryTheory.mono_iff_injective CategoryTheory.instMonoAppOfFunctor CategoryTheory.Limits.Types.instHasPullbacksType CategoryTheory.FunctorToTypes.naturality CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Presieve.IsSeparatedFor.ext CategoryTheory.Presieve.IsSheafFor.valid_glue CategoryTheory.op_comp CategoryTheory.FunctorToTypes.map_comp_apply

CategoryTheory.Presheaf

Definitions

Name	Category	Theorems
classifier 📖	CompOp	5 math math: classifier_Ω, classifier_χ, classifier_truth, classifier_Ω₀, classifier_χ₀
truth 📖	CompOp	5 math math: comp_χ_eq, truth_app, CategoryTheory.Sheaf.truth_hom, classifier_truth, isPullback_χ_truth
χ 📖	CompOp	7 math math: comp_χ_eq, χ_app, classifier_χ, χ_unique, CategoryTheory.Sheaf.χ_hom, isPullback_χ_truth, CategoryTheory.GrothendieckTopology.isClosed_χ_app_apply_of_isSheaf_of_isSeparated

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
classifier_truth 📖	mathematical	—	CategoryTheory.Subobject.Classifier.truth CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category classifier truth	—	—
classifier_Ω 📖	mathematical	—	CategoryTheory.Subobject.Classifier.Ω CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category classifier CategoryTheory.Functor.sieves	—	—
classifier_Ω₀ 📖	mathematical	—	CategoryTheory.Subobject.Classifier.Ω₀ CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category classifier CategoryTheory.Functor.obj CategoryTheory.Functor.const	—	—
classifier_χ 📖	mathematical	—	CategoryTheory.Subobject.Classifier.χ CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category classifier χ	—	—
classifier_χ₀ 📖	mathematical	—	CategoryTheory.Subobject.Classifier.χ₀ CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category classifier CategoryTheory.Limits.IsTerminal.from CategoryTheory.Functor.obj CategoryTheory.Functor.const CategoryTheory.Functor.isTerminalConst CategoryTheory.Limits.Types.isTerminalPUnit	—	—
comp_χ_eq 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.sieves χ CategoryTheory.Functor.obj CategoryTheory.Functor.const CategoryTheory.Limits.IsTerminal.from CategoryTheory.Functor.isTerminalConst CategoryTheory.Limits.Types.isTerminalPUnit truth	—	CategoryTheory.NatTrans.ext' CategoryTheory.types_ext CategoryTheory.Sieve.ext CategoryTheory.FunctorToTypes.naturality
isPullback_χ_truth 📖	mathematical	—	CategoryTheory.IsPullback CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.Functor.const CategoryTheory.Functor.sieves CategoryTheory.Limits.IsTerminal.from CategoryTheory.Functor.isTerminalConst CategoryTheory.Limits.Types.isTerminalPUnit χ truth	—	CategoryTheory.IsPullback.of_forall_isPullback_app CategoryTheory.Limits.Types.isPullback_iff comp_χ_eq CategoryTheory.mono_iff_injective CategoryTheory.instMonoAppOfFunctor CategoryTheory.Limits.Types.instHasPullbacksType CategoryTheory.FunctorToTypes.map_id_apply
truth_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Functor.sieves truth Top.top CategoryTheory.Sieve Opposite.unop OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.Sieve.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	—
χ_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.sieves χ Opposite.unop CategoryTheory.Functor.obj Opposite.op CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
χ_unique 📖	mathematical	CategoryTheory.IsPullback CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.Functor.const CategoryTheory.Functor.sieves CategoryTheory.Limits.IsTerminal.from CategoryTheory.Functor.isTerminalConst CategoryTheory.Limits.Types.isTerminalPUnit truth	χ	—	CategoryTheory.NatTrans.ext' CategoryTheory.types_ext CategoryTheory.Limits.Types.instHasPullbacksType CategoryTheory.Sieve.ext CategoryTheory.Sieve.mem_iff_pullback_eq_top Quiver.Hom.unop_op CategoryTheory.Functor.sieves_map CategoryTheory.FunctorToTypes.naturality CategoryTheory.FunctorToTypes.comp CategoryTheory.NatTrans.comp_app

CategoryTheory.Sheaf

Definitions

Name	Category	Theorems
classifier 📖	CompOp	5 math math: classifier_χ, classifier_truth, classifier_Ω₀, classifier_Ω, classifier_χ₀
truth 📖	CompOp	3 math math: isPullback_χ_truth, classifier_truth, truth_hom
Ω 📖	CompOp	5 math math: isPullback_χ_truth, χ_hom, classifier_Ω, truth_hom, Ω_obj
χ 📖	CompOp	4 math math: isPullback_χ_truth, classifier_χ, χ_hom, χ_unique

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
classifier_truth 📖	mathematical	—	CategoryTheory.Subobject.Classifier.truth CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf classifier truth	—	—
classifier_Ω 📖	mathematical	—	CategoryTheory.Subobject.Classifier.Ω CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf classifier Ω	—	—
classifier_Ω₀ 📖	mathematical	—	CategoryTheory.Subobject.Classifier.Ω₀ CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf classifier terminal CategoryTheory.Limits.Types.isTerminalPUnit	—	—
classifier_χ 📖	mathematical	—	CategoryTheory.Subobject.Classifier.χ CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf classifier χ	—	—
classifier_χ₀ 📖	mathematical	—	CategoryTheory.Subobject.Classifier.χ₀ CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf classifier CategoryTheory.Limits.IsTerminal.from terminal CategoryTheory.Limits.Types.isTerminalPUnit isTerminalTerminal	—	—
instHasSubobjectClassifierTypeOfEssentiallySmall 📖	mathematical	—	CategoryTheory.HasSubobjectClassifier CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf	—	CategoryTheory.Functor.locallyCoverDense_of_isCoverDense CategoryTheory.Functor.IsLocallyFull.of_full CategoryTheory.Equivalence.full_inverse CategoryTheory.Equivalence.instIsCoverDenseOfIsEquivalence CategoryTheory.Equivalence.isEquivalence_inverse CategoryTheory.Functor.IsLocallyFaithful.of_faithful CategoryTheory.Equivalence.faithful_inverse CategoryTheory.Functor.instIsDenseSubsiteInducedTopologyOfIsCoverDense
isPullback_χ_truth 📖	mathematical	—	CategoryTheory.IsPullback CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf terminal CategoryTheory.Limits.Types.isTerminalPUnit Ω CategoryTheory.Limits.IsTerminal.from isTerminalTerminal χ truth	—	CategoryTheory.IsPullback.of_map CategoryTheory.CreatesLimit.toReflectsLimit CategoryTheory.Limits.Types.instHasPullbacksType CategoryTheory.ObjectProperty.hom_ext CategoryTheory.cancel_mono CategoryTheory.Subfunctor.instMonoFunctorTypeι CategoryTheory.Category.assoc CategoryTheory.Presheaf.comp_χ_eq CategoryTheory.IsPullback.of_right CategoryTheory.Category.comp_id CategoryTheory.Presheaf.isPullback_χ_truth CategoryTheory.presheaf_mono_of_mono CategoryTheory.Functor.corepresentable_preservesLimitsOfShape CategoryTheory.Types.instIsCorepresentableForgetTypeHom CategoryTheory.Limits.Types.hasLimit UnivLE.small UnivLE.self CategoryTheory.Limits.Types.hasColimitsOfShape Opposite.small CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence CategoryTheory.Types.instIsEquivalenceForgetTypeHom CategoryTheory.reflectsIsomorphisms_of_reflectsMonomorphisms_of_reflectsEpimorphisms CategoryTheory.balanced_of_strongMonoCategory CategoryTheory.strongMonoCategory_of_regularMonoCategory CategoryTheory.Adhesive.toRegularMonoCategory CategoryTheory.Type.adhesive CategoryTheory.reflectsMonomorphisms_of_reflectsLimitsOfShape CategoryTheory.Limits.ReflectsFiniteLimits.reflects CategoryTheory.Limits.reflectsFiniteLimits_of_reflectsIsomorphisms CategoryTheory.reflectsIsomorphisms_of_full_and_faithful CategoryTheory.Types.instFullForgetTypeHom CategoryTheory.instFaithfulForget CategoryTheory.Limits.hasFiniteLimits_of_hasLimits CategoryTheory.Limits.Types.hasLimitsOfSize CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits CategoryTheory.Types.instPreservesLimitsOfSizeForgetTypeHom CategoryTheory.reflectsEpimorphisms_of_reflectsColimitsOfShape CategoryTheory.Limits.ReflectsFiniteColimits.reflects CategoryTheory.Limits.reflectsFiniteColimitsOfReflectsIsomorphisms CategoryTheory.Limits.hasFiniteColimits_of_hasColimits CategoryTheory.Limits.Types.hasColimitsOfSize CategoryTheory.Limits.PreservesColimits.preservesFiniteColimits CategoryTheory.Types.instPreservesColimitsOfSizeForgetTypeHom CategoryTheory.IsPullback.of_horiz_isIso_mono CategoryTheory.IsIso.id CategoryTheory.Category.id_comp
truth_hom 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.ObjectProperty.FullSubcategory.obj terminal CategoryTheory.Limits.Types.isTerminalPUnit Ω truth CategoryTheory.Subfunctor.lift CategoryTheory.Functor.sieves CategoryTheory.Functor.obj CategoryTheory.Functor.const CategoryTheory.Presheaf.truth CategoryTheory.Functor.closedSieves	—	—
Ω_obj 📖	mathematical	—	CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf Ω CategoryTheory.Subfunctor.toFunctor CategoryTheory.Functor.sieves CategoryTheory.Functor.closedSieves	—	—
χ_hom 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.ObjectProperty.FullSubcategory.obj Ω χ CategoryTheory.Subfunctor.lift CategoryTheory.Functor.sieves CategoryTheory.Presheaf.χ CategoryTheory.Functor.closedSieves	—	—
χ_unique 📖	mathematical	CategoryTheory.IsPullback CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf terminal CategoryTheory.Limits.Types.isTerminalPUnit Ω CategoryTheory.Limits.IsTerminal.from isTerminalTerminal truth	χ	—	CategoryTheory.ObjectProperty.hom_ext CategoryTheory.cancel_mono CategoryTheory.Subfunctor.instMonoFunctorTypeι χ_hom CategoryTheory.Subfunctor.lift_ι CategoryTheory.Presheaf.χ_unique CategoryTheory.IsPullback.of_horiz_isIso_mono CategoryTheory.IsIso.id CategoryTheory.Category.id_comp CategoryTheory.IsPullback.map CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit CategoryTheory.Limits.Types.instHasPullbacksType CategoryTheory.Limits.functorCategoryHasLimit CategoryTheory.Limits.Types.hasLimit UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Category.comp_id CategoryTheory.IsPullback.paste_horiz

---

← Back to Index