Subcanonical

📁 Source: Mathlib/CategoryTheory/Sites/Hypercover/Subcanonical.lean

Statistics

Metric	Count
Definitions glueMorphisms, glueMorphisms	2
Theorems f_glueMorphisms, f_glueMorphisms_assoc, f_glueMorphisms, f_glueMorphisms_assoc, hom_ext, instIsLocalAtTargetIsomorphisms, isPullback_of_forall_isPullback	7
Total	9

CategoryTheory.GrothendieckTopology.OneHypercover

Definitions

Name	Category	Theorems
glueMorphisms 📖	CompOp	2 math math: f_glueMorphisms, f_glueMorphisms_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
f_glueMorphisms 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreOneHypercover.Y toPreOneHypercover CategoryTheory.PreZeroHypercover.X CategoryTheory.PreOneHypercover.toPreZeroHypercover CategoryTheory.PreOneHypercover.p₁ CategoryTheory.PreOneHypercover.p₂	CategoryTheory.PreZeroHypercover.f glueMorphisms	—	map_amalgamate CategoryTheory.GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable CategoryTheory.Functor.instIsRepresentableObjOppositeTypeYoneda
f_glueMorphisms_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreOneHypercover.Y toPreOneHypercover CategoryTheory.PreZeroHypercover.X CategoryTheory.PreOneHypercover.toPreZeroHypercover CategoryTheory.PreOneHypercover.p₁ CategoryTheory.PreOneHypercover.p₂	CategoryTheory.PreZeroHypercover.f glueMorphisms	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' f_glueMorphisms

CategoryTheory.Precoverage.ZeroHypercover

Definitions

Name	Category	Theorems
glueMorphisms 📖	CompOp	2 math math: f_glueMorphisms, f_glueMorphisms_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
f_glueMorphisms 📖	mathematical	CategoryTheory.PreZeroHypercover.HasPullbacks toPreZeroHypercover CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback CategoryTheory.PreZeroHypercover.X CategoryTheory.PreZeroHypercover.f CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd	glueMorphisms	—	CategoryTheory.GrothendieckTopology.OneHypercover.f_glueMorphisms
f_glueMorphisms_assoc 📖	mathematical	CategoryTheory.PreZeroHypercover.HasPullbacks toPreZeroHypercover CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback CategoryTheory.PreZeroHypercover.X CategoryTheory.PreZeroHypercover.f CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd	glueMorphisms	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' f_glueMorphisms
hom_ext 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.X toPreZeroHypercover CategoryTheory.PreZeroHypercover.f	—	—	CategoryTheory.Presieve.IsSheaf.isSheafFor_of_mem_precoverage CategoryTheory.GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable CategoryTheory.Functor.instIsRepresentableObjOppositeTypeYoneda mem₀ CategoryTheory.PreZeroHypercover.ext_of_isSeparatedFor CategoryTheory.Presieve.IsSheafFor.isSeparatedFor
instIsLocalAtTargetIsomorphisms 📖	mathematical	—	CategoryTheory.MorphismProperty.IsLocalAtTarget CategoryTheory.MorphismProperty.isomorphisms CategoryTheory.Precoverage.instHasPullbacksOfHasPullbacks	—	CategoryTheory.MorphismProperty.IsLocalAtTarget.mk_of_isStableUnderBaseChange CategoryTheory.Precoverage.instHasPullbacksOfHasPullbacks CategoryTheory.MorphismProperty.IsStableUnderBaseChange.isomorphisms instHasPullbackFOfHasPullbacksPresieve₀_1 instHasPullbacksPresieve₀OfHasPullbacks instHasPullbackFOfHasPullbacksPresieve₀ CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Limits.pullback.condition CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.cancel_epi CategoryTheory.epi_comp CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_hom CategoryTheory.Limits.pullback.map_isIso CategoryTheory.IsIso.id CategoryTheory.Category.assoc CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.IsIso.hom_inv_id_assoc CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_fst_assoc CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_snd_assoc hom_ext CategoryTheory.Limits.pullback.condition_assoc f_glueMorphisms f_glueMorphisms_assoc CategoryTheory.IsIso.inv_hom_id_assoc
isPullback_of_forall_isPullback 📖	—	CategoryTheory.IsPullback CategoryTheory.Limits.pullback CategoryTheory.PreZeroHypercover.X toPreZeroHypercover CategoryTheory.PreZeroHypercover.f instHasPullbackFOfHasPullbacksPresieve₀_1 instHasPullbacksPresieve₀OfHasPullbacks CategoryTheory.Precoverage.instHasPullbacksOfHasPullbacks CategoryTheory.Limits.pullback.snd CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback.fst	—	—	instHasPullbackFOfHasPullbacksPresieve₀_1 instHasPullbacksPresieve₀OfHasPullbacks CategoryTheory.Precoverage.instHasPullbacksOfHasPullbacks hom_ext CategoryTheory.Limits.pullback.condition_assoc CategoryTheory.Category.assoc CategoryTheory.CommSq.w CategoryTheory.IsPullback.toCommSq CategoryTheory.Limits.hasLimitOfHasLimitsOfShape instHasPullbackFOfHasPullbacksPresieve₀ CategoryTheory.MorphismProperty.IsLocalAtTarget.iff_of_zeroHypercover instIsLocalAtTargetIsomorphisms CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.IsPullback.paste_vert_iff CategoryTheory.IsPullback.of_hasPullback CategoryTheory.Limits.limit.lift_π CategoryTheory.IsPullback.flip CategoryTheory.Limits.pullback.hom_ext CategoryTheory.Limits.pullback.condition CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.Presieve.instHasPullbackOfHasPairwisePullbacksOfArrows CategoryTheory.Presieve.instHasPairwisePullbacksOfHasPullbacks CategoryTheory.Iso.eq_inv_comp CategoryTheory.IsPullback.isoPullback_hom_snd CategoryTheory.IsIso.comp_isIso CategoryTheory.Iso.isIso_inv CategoryTheory.Iso.isIso_hom CategoryTheory.IsPullback.of_iso_pullback

---

← Back to Index