Precoverage

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

Statistics

Metric	Count
Definitions PreservesPairwisePullbacks, Precoverage, HasIsos, HasPullbacks, IsStableUnderBaseChange, IsStableUnderComposition, IsStableUnderSup, PullbacksPreservedBy, comap, coverings, instBot, instCoeFunForallSetPresieve, instCompleteLattice, instInfSet, instMax, instMin, instPartialOrder, instSupSet, instTop	19
Theorems preservesLimit, preservesLimit_cospan_of_mem_presieve, mem_coverings_of_isIso, hasPullbacks_of_mem, mem_coverings_of_isPullback, comp_mem_coverings, sup_mem_coverings, preservesPairwisePullbacks_of_mem, comap_comp, comap_id, comap_inf, comp_mem_coverings, ext, ext_iff, hasPairwisePullbacks_of_mem, hasPullbacks_of_mem, instHasIsosComap, instHasIsosMin, instHasPullbacksComapOfCreatesLimitsOfShapeWalkingCospan, instHasPullbacksOfHasPullbacks, instIsStableUnderBaseChangeComapOfPreservesLimitsOfShapeWalkingCospan, instIsStableUnderBaseChangeMin, instIsStableUnderCompositionComap, instIsStableUnderCompositionMin, instIsStableUnderSupMin, instPullbacksPreservedByOfPreservesLimitsOfShapeWalkingCospan, mem_comap_iff, mem_coverings_of_isIso, mem_coverings_of_isPullback, preservesPairwisePullbacks_of_mem, pullbackArrows_mem, sup_mem_coverings, map_of_preservesPairwisePullbacks, instPreservesPairwisePullbacksOfPreservesLimitsOfShapeWalkingCospan	34
Total	53

CategoryTheory

Definitions

Name	Category	Theorems
Precoverage 📖	CompData	30 math math: Precoverage.instHasIsosMin, Precoverage.toGrothendieck_le_iff_le_toPrecoverage, AlgebraicGeometry.Scheme.proetalePrecoverage_le_precoverage_weaklyEtale, AlgebraicGeometry.Scheme.precoverage_mono, MorphismProperty.precoverage_monotone, Precoverage.instIsStableUnderSupMin, Precoverage.galoisConnection_toGrothendieck_toPrecoverage, AlgebraicGeometry.Scheme.etalePrecoverage_le_proetalePrecoverage, AlgebraicGeometry.Scheme.fppfPrecoverage_le_fpqcPrecoverage, AlgebraicGeometry.Scheme.zariskiPrecoverage_le_fppfPrecoverage, Precoverage.instIsStableUnderBaseChangeMin, AlgebraicGeometry.Scheme.zariskiPrecoverage_le_propQCPrecoverage, Precoverage.instIsStableUnderCompositionMin, Precoverage.Small.inf, AlgebraicGeometry.Scheme.proetalePrecoverage_le_fpqcPrecoverage, AlgebraicGeometry.Scheme.fppfPrecoverage_eq_inf, AlgebraicGeometry.Scheme.propQCPrecoverage_le_precoverage, AlgebraicGeometry.Scheme.zariskiPrecoverage_le_fpqcPrecoverage, AlgebraicGeometry.Scheme.precoverage_le_qcPrecoverage_of_isOpenMap, GrothendieckTopology.toPrecoverage_monotone, TopCat.precoverage_le_comap_uliftFunctor, Precoverage.toGrothendieck_monotone, Precoverage.toGrothendieck_bot, MorphismProperty.precoverage_inf, Precoverage.le_of_zeroHypercover, AlgebraicGeometry.Scheme.zariskiPrecoverage_le_qcPrecoverage, Precoverage.comap_inf, AlgebraicGeometry.Scheme.propQCPrecoverage_monotone, Precoverage.le_toPrecoverage_toGrothendieck, GrothendieckTopology.toPrecoverage_top

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instPreservesPairwisePullbacksOfPreservesLimitsOfShapeWalkingCospan 📖	mathematical	—	Functor.PreservesPairwisePullbacks	—	Limits.PreservesLimitsOfShape.preservesLimit

CategoryTheory.Functor

Definitions

Name	Category	Theorems
PreservesPairwisePullbacks 📖	CompData	3 math math: CategoryTheory.Precoverage.PullbacksPreservedBy.preservesPairwisePullbacks_of_mem, CategoryTheory.Precoverage.preservesPairwisePullbacks_of_mem, CategoryTheory.instPreservesPairwisePullbacksOfPreservesLimitsOfShapeWalkingCospan

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preservesLimit_cospan_of_mem_presieve 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan	—	PreservesPairwisePullbacks.preservesLimit

CategoryTheory.Functor.PreservesPairwisePullbacks

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preservesLimit 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan	—	—

CategoryTheory.Precoverage

Definitions

Name	Category	Theorems
HasIsos 📖	CompData	9 math math: instHasIsosMin, CategoryTheory.MorphismProperty.instHasIsosPrecoverageOfContainsIdentitiesOfRespectsIso, CategoryTheory.GrothendieckTopology.instHasIsosToPrecoverage, AlgebraicGeometry.Scheme.instHasIsosPrecoverageOfContainsIdentitiesOfRespectsIso, HasIsos.of_preZeroHypercoverFamily, instHasIsosComap, instHasIsosFinite, AlgebraicGeometry.Scheme.instHasIsosQcPrecoverage, CategoryTheory.Types.instHasIsosJointlySurjectivePrecoverage
HasPullbacks 📖	CompData	3 math math: AlgebraicGeometry.Scheme.instHasPullbacksPrecoverageOfHasPullbacks, instHasPullbacksOfHasPullbacks, instHasPullbacksComapOfCreatesLimitsOfShapeWalkingCospan
IsStableUnderBaseChange 📖	CompData	10 math math: CategoryTheory.isStableUnderBaseChange_comap_jointlySurjectivePrecoverage, CategoryTheory.GrothendieckTopology.instIsStableUnderBaseChangeToPrecoverage, instIsStableUnderBaseChangeComapOfPreservesLimitsOfShapeWalkingCospan, CategoryTheory.MorphismProperty.instIsStableUnderBaseChangePrecoverageOfIsStableUnderBaseChange, instIsStableUnderBaseChangeMin, AlgebraicGeometry.Scheme.instIsStableUnderBaseChangeJointlySurjectivePrecoverage, CategoryTheory.instIsStableUnderBaseChangeJointlySurjectivePrecoverage, AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange, IsStableUnderBaseChange.of_preZeroHypercoverFamily_of_isClosedUnderIsomorphisms, AlgebraicGeometry.Scheme.instIsStableUnderBaseChangeQcPrecoverage
IsStableUnderComposition 📖	CompData	8 math math: AlgebraicGeometry.Scheme.instIsStableUnderCompositionQcPrecoverage, CategoryTheory.GrothendieckTopology.instIsStableUnderCompositionToPrecoverage, instIsStableUnderCompositionComap, instIsStableUnderCompositionMin, AlgebraicGeometry.Scheme.instIsStableUnderCompositionPrecoverageOfIsStableUnderComposition, CategoryTheory.Types.instIsStableUnderCompositionJointlySurjectivePrecoverage, IsStableUnderComposition.of_preZeroHypercoverFamily, CategoryTheory.MorphismProperty.instIsStableUnderCompositionPrecoverageOfIsStableUnderComposition
IsStableUnderSup 📖	CompData	4 math math: instIsStableUnderSupMin, IsStableUnderSup.of_preZeroHypercoverFamily, AlgebraicGeometry.Scheme.instIsStableUnderSupQcPrecoverage, CategoryTheory.Types.instIsStableUnderSupJointlySurjectivePrecoverage
PullbacksPreservedBy 📖	CompData	1 math math: instPullbacksPreservedByOfPreservesLimitsOfShapeWalkingCospan
comap 📖	CompOp	18 math math: CategoryTheory.MorphismProperty.toGrothendieck_comap_forget_eq_inducedTopology, CategoryTheory.isStableUnderBaseChange_comap_jointlySurjectivePrecoverage, CategoryTheory.Presieve.ofArrows_mem_comap_jointlySurjectivePrecoverage_iff, instIsStableUnderBaseChangeComapOfPreservesLimitsOfShapeWalkingCospan, CategoryTheory.MorphismProperty.comap_precoverage, instIsStableUnderCompositionComap, toGrothendieck_comap_eq_inducedTopology, instHasIsosComap, toGrothendieck_comap_le_inducedTopology, CategoryTheory.Presieve.mem_comap_jointlySurjectivePrecoverage_iff, TopCat.precoverage_le_comap_uliftFunctor, instSmallComap, CategoryTheory.over_toGrothendieck_eq_toGrothendieck_comap_forget, comap_inf, comap_id, instHasPullbacksComapOfCreatesLimitsOfShapeWalkingCospan, mem_comap_iff, comap_comp
coverings 📖	CompOp	65 math math: AlgebraicGeometry.Scheme.mem_propQCPrecoverage_iff_exists_quasiCompactCover, CategoryTheory.GrothendieckTopology.mem_toPretopology, CategoryTheory.PreZeroHypercover.presieve₀_mem_of_iso, ZeroHypercover.Small.exists_restrictIndex_mem, CategoryTheory.Coverage.ext_iff, RespectsIso.of_forall_exists_iso, CategoryTheory.Coverage.pullback, AlgebraicGeometry.Scheme.Hom.singleton_mem_fpqcPrecoverage, CategoryTheory.Types.mem_jointlySurjectivePrecoverage_iff, CategoryTheory.MorphismProperty.ofArrows_mem_precoverage, AlgebraicGeometry.Scheme.mem_jointlySurjectiveTopology_iff_jointlySurjectivePretopology, AlgebraicGeometry.Scheme.bot_mem_precoverage, CategoryTheory.Presieve.ofArrows_mem_comap_jointlySurjectivePrecoverage_iff, AlgebraicGeometry.Scheme.presieve₀_mem_precoverage_iff, preZeroHypercoverFamily_property, CategoryTheory.Pretopology.transitive, CategoryTheory.Pretopology.mem_toGrothendieck, CategoryTheory.PreZeroHypercover.presieve₀_mem_iff_of_iso, AlgebraicGeometry.Scheme.Hom.singleton_mem_qcPrecoverage, mem_coverings_of_isIso, mem_finite_iff, CategoryTheory.Pretopology.ext_iff, CategoryTheory.MorphismProperty.bot_mem_precoverage, IsStableUnderComposition.comp_mem_coverings, AlgebraicGeometry.Scheme.singleton_mem_precoverage_iff, AlgebraicGeometry.Scheme.Hom.singleton_mem_fppfPrecoverage, AlgebraicGeometry.Scheme.presieve₀_mem_qcPrecoverage_iff, HasIsos.mem_coverings_of_isIso, CategoryTheory.Types.singleton_mem_jointlySurjectivePrecoverage_iff, mem_toGrothendieck_iff_of_isStableUnderComposition, mem_iff_exists_zeroHypercover, ZeroHypercover.presieve₀_mem_of_iso, comp_mem_coverings, pullbackArrows_mem, AlgebraicGeometry.Scheme.Hom.singleton_mem_propQCPrecoverage, sup_mem_coverings, IsStableUnderBaseChange.mem_coverings_of_isPullback, ext_iff, mem_coverings_of_isPullback, IsStableUnderSup.sup_mem_coverings, ofArrows_mem_finite, CategoryTheory.Pretopology.has_isos, ZeroHypercover.Small.mem₀, CategoryTheory.PreZeroHypercoverFamily.mem_precoverage_iff, CategoryTheory.Pretopology.mem_inf, CategoryTheory.GrothendieckTopology.mem_toPrecoverage_iff, AlgebraicGeometry.Scheme.ofArrows_mem_precoverage_iff, CategoryTheory.Presieve.mem_comap_jointlySurjectivePrecoverage_iff, CategoryTheory.Pretopology.ofArrows_mem_finite, AlgebraicGeometry.Scheme.bot_mem_propQCPrecoverage, CategoryTheory.Pretopology.mem_sInf, RespectsIso.of_iso, ZeroHypercover.mem₀, CategoryTheory.Pretopology.mem_toCoverage, CategoryTheory.Coverage.sup_covering, AlgebraicGeometry.Scheme.bot_mem_qcPrecoverage, AlgebraicGeometry.Scheme.mem_pretopology_iff, AlgebraicGeometry.Scheme.Cover.mem_pretopology, CategoryTheory.PreZeroHypercover.presieve₀_mem_precoverage_iff, CategoryTheory.GrothendieckTopology.arrows_mem_toPrecoverage_iff, CategoryTheory.Pretopology.le_def, CategoryTheory.Pretopology.pullbacks, CategoryTheory.GrothendieckTopology.mem_toCoverage_iff, CategoryTheory.Types.ofArrows_mem_jointlySurjectivePrecoverage_iff, mem_comap_iff
instBot 📖	CompOp	1 math math: toGrothendieck_bot
instCoeFunForallSetPresieve 📖	CompOp	—
instCompleteLattice 📖	CompOp	—
instInfSet 📖	CompOp	—
instMax 📖	CompOp	—
instMin 📖	CompOp	8 math math: instHasIsosMin, instIsStableUnderSupMin, instIsStableUnderBaseChangeMin, instIsStableUnderCompositionMin, Small.inf, AlgebraicGeometry.Scheme.fppfPrecoverage_eq_inf, CategoryTheory.MorphismProperty.precoverage_inf, comap_inf
instPartialOrder 📖	CompOp	20 math math: toGrothendieck_le_iff_le_toPrecoverage, AlgebraicGeometry.Scheme.proetalePrecoverage_le_precoverage_weaklyEtale, AlgebraicGeometry.Scheme.precoverage_mono, CategoryTheory.MorphismProperty.precoverage_monotone, galoisConnection_toGrothendieck_toPrecoverage, AlgebraicGeometry.Scheme.etalePrecoverage_le_proetalePrecoverage, AlgebraicGeometry.Scheme.fppfPrecoverage_le_fpqcPrecoverage, AlgebraicGeometry.Scheme.zariskiPrecoverage_le_fppfPrecoverage, AlgebraicGeometry.Scheme.zariskiPrecoverage_le_propQCPrecoverage, AlgebraicGeometry.Scheme.proetalePrecoverage_le_fpqcPrecoverage, AlgebraicGeometry.Scheme.propQCPrecoverage_le_precoverage, AlgebraicGeometry.Scheme.zariskiPrecoverage_le_fpqcPrecoverage, AlgebraicGeometry.Scheme.precoverage_le_qcPrecoverage_of_isOpenMap, CategoryTheory.GrothendieckTopology.toPrecoverage_monotone, TopCat.precoverage_le_comap_uliftFunctor, toGrothendieck_monotone, le_of_zeroHypercover, AlgebraicGeometry.Scheme.zariskiPrecoverage_le_qcPrecoverage, AlgebraicGeometry.Scheme.propQCPrecoverage_monotone, le_toPrecoverage_toGrothendieck
instSupSet 📖	CompOp	—
instTop 📖	CompOp	1 math math: CategoryTheory.GrothendieckTopology.toPrecoverage_top

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap_comp 📖	mathematical	—	comap CategoryTheory.Functor.comp	—	ext Set.ext CategoryTheory.Presieve.exists_eq_ofArrows CategoryTheory.Presieve.map_ofArrows
comap_id 📖	mathematical	—	comap CategoryTheory.Functor.id	—	ext Set.ext CategoryTheory.Presieve.map_id
comap_inf 📖	mathematical	—	comap CategoryTheory.Precoverage instMin	—	—
comp_mem_coverings 📖	mathematical	CategoryTheory.Presieve Set Set.instMembership coverings CategoryTheory.Presieve.ofArrows	CategoryTheory.Presieve Set Set.instMembership coverings CategoryTheory.Presieve.ofArrows CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	le_antisymm CategoryTheory.Presieve.ofArrows.mk' CategoryTheory.Presieve.ofArrows.obj_idx CategoryTheory.Presieve.ofArrows.eq_eqToHom_comp_hom_idx IsStableUnderComposition.comp_mem_coverings CategoryTheory.Presieve.ofArrows.hom_idx CategoryTheory.eqToHom_trans_assoc CategoryTheory.Category.id_comp
ext 📖	—	coverings	—	—	—
ext_iff 📖	mathematical	—	coverings	—	ext
hasPairwisePullbacks_of_mem 📖	mathematical	CategoryTheory.Presieve Set Set.instMembership coverings	CategoryTheory.Presieve.HasPairwisePullbacks	—	CategoryTheory.Presieve.HasPullbacks.hasPullback hasPullbacks_of_mem
hasPullbacks_of_mem 📖	mathematical	CategoryTheory.Presieve Set Set.instMembership coverings	CategoryTheory.Presieve.HasPullbacks	—	HasPullbacks.hasPullbacks_of_mem
instHasIsosComap 📖	mathematical	—	HasIsos comap	—	CategoryTheory.Presieve.map_singleton mem_coverings_of_isIso CategoryTheory.Functor.map_isIso
instHasIsosMin 📖	mathematical	—	HasIsos CategoryTheory.Precoverage instMin	—	mem_coverings_of_isIso
instHasPullbacksComapOfCreatesLimitsOfShapeWalkingCospan 📖	mathematical	—	HasPullbacks comap	—	hasPullbacks_of_mem CategoryTheory.Presieve.hasPullback CategoryTheory.Presieve.map_map CategoryTheory.Limits.HasPullback.of_createsLimit
instHasPullbacksOfHasPullbacks 📖	mathematical	—	HasPullbacks	—	CategoryTheory.Presieve.instHasPullbacksOfHasPullbacks
instIsStableUnderBaseChangeComapOfPreservesLimitsOfShapeWalkingCospan 📖	mathematical	—	IsStableUnderBaseChange comap	—	CategoryTheory.Presieve.map_ofArrows mem_coverings_of_isPullback CategoryTheory.Functor.map_isPullback CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit
instIsStableUnderBaseChangeMin 📖	mathematical	—	IsStableUnderBaseChange CategoryTheory.Precoverage instMin	—	mem_coverings_of_isPullback
instIsStableUnderCompositionComap 📖	mathematical	—	IsStableUnderComposition comap	—	CategoryTheory.Presieve.map_ofArrows CategoryTheory.Functor.map_comp comp_mem_coverings
instIsStableUnderCompositionMin 📖	mathematical	—	IsStableUnderComposition CategoryTheory.Precoverage instMin	—	comp_mem_coverings
instIsStableUnderSupMin 📖	mathematical	—	IsStableUnderSup CategoryTheory.Precoverage instMin	—	sup_mem_coverings
instPullbacksPreservedByOfPreservesLimitsOfShapeWalkingCospan 📖	mathematical	—	PullbacksPreservedBy	—	CategoryTheory.instPreservesPairwisePullbacksOfPreservesLimitsOfShapeWalkingCospan
mem_comap_iff 📖	mathematical	—	CategoryTheory.Presieve Set Set.instMembership coverings comap CategoryTheory.Functor.obj CategoryTheory.Presieve.map	—	—
mem_coverings_of_isIso 📖	mathematical	—	CategoryTheory.Presieve Set Set.instMembership coverings CategoryTheory.Presieve.singleton	—	HasIsos.mem_coverings_of_isIso
mem_coverings_of_isPullback 📖	mathematical	CategoryTheory.Presieve Set Set.instMembership coverings CategoryTheory.Presieve.ofArrows CategoryTheory.IsPullback	CategoryTheory.Presieve Set Set.instMembership coverings CategoryTheory.Presieve.ofArrows	—	le_antisymm CategoryTheory.Presieve.ofArrows.mk' CategoryTheory.Presieve.ofArrows.obj_idx CategoryTheory.Presieve.ofArrows.hom_idx CategoryTheory.eqToHom_trans_assoc CategoryTheory.Category.id_comp IsStableUnderBaseChange.mem_coverings_of_isPullback
preservesPairwisePullbacks_of_mem 📖	mathematical	CategoryTheory.Presieve Set Set.instMembership coverings	CategoryTheory.Functor.PreservesPairwisePullbacks	—	PullbacksPreservedBy.preservesPairwisePullbacks_of_mem
pullbackArrows_mem 📖	mathematical	CategoryTheory.Presieve Set Set.instMembership coverings	CategoryTheory.Presieve Set Set.instMembership coverings CategoryTheory.Presieve.pullbackArrows	—	CategoryTheory.Presieve.exists_eq_ofArrows CategoryTheory.Presieve.hasPullback CategoryTheory.Presieve.instHasPullbacksOfArrowsOfHasPullback CategoryTheory.Presieve.ofArrows_pullback mem_coverings_of_isPullback CategoryTheory.IsPullback.flip CategoryTheory.IsPullback.of_hasPullback
sup_mem_coverings 📖	mathematical	CategoryTheory.Presieve Set Set.instMembership coverings	CategoryTheory.Presieve Set Set.instMembership coverings SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CategoryTheory.instCompleteLatticePresieve	—	IsStableUnderSup.sup_mem_coverings

CategoryTheory.Precoverage.HasIsos

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_coverings_of_isIso 📖	mathematical	—	CategoryTheory.Presieve Set Set.instMembership CategoryTheory.Precoverage.coverings CategoryTheory.Presieve.singleton	—	—

CategoryTheory.Precoverage.HasPullbacks

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasPullbacks_of_mem 📖	mathematical	CategoryTheory.Presieve Set Set.instMembership CategoryTheory.Precoverage.coverings	CategoryTheory.Presieve.HasPullbacks	—	—

CategoryTheory.Precoverage.IsStableUnderBaseChange

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_coverings_of_isPullback 📖	mathematical	CategoryTheory.Presieve Set Set.instMembership CategoryTheory.Precoverage.coverings CategoryTheory.Presieve.ofArrows CategoryTheory.IsPullback	CategoryTheory.Presieve Set Set.instMembership CategoryTheory.Precoverage.coverings CategoryTheory.Presieve.ofArrows	—	—

CategoryTheory.Precoverage.IsStableUnderComposition

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_mem_coverings 📖	mathematical	CategoryTheory.Presieve Set Set.instMembership CategoryTheory.Precoverage.coverings CategoryTheory.Presieve.ofArrows	CategoryTheory.Presieve Set Set.instMembership CategoryTheory.Precoverage.coverings CategoryTheory.Presieve.ofArrows CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—

CategoryTheory.Precoverage.IsStableUnderSup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sup_mem_coverings 📖	mathematical	CategoryTheory.Presieve Set Set.instMembership CategoryTheory.Precoverage.coverings	CategoryTheory.Presieve Set Set.instMembership CategoryTheory.Precoverage.coverings SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CategoryTheory.instCompleteLatticePresieve	—	—

CategoryTheory.Precoverage.PullbacksPreservedBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preservesPairwisePullbacks_of_mem 📖	mathematical	CategoryTheory.Presieve Set Set.instMembership CategoryTheory.Precoverage.coverings	CategoryTheory.Functor.PreservesPairwisePullbacks	—	—

CategoryTheory.Presieve.HasPairwisePullbacks

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_of_preservesPairwisePullbacks 📖	mathematical	—	CategoryTheory.Presieve.HasPairwisePullbacks CategoryTheory.Functor.obj CategoryTheory.Presieve.map	—	has_pullbacks CategoryTheory.Functor.preservesLimit_cospan_of_mem_presieve CategoryTheory.Limits.hasPullback_of_preservesPullback

---

← Back to Index