Extensive

📁 Source: Mathlib/CategoryTheory/Extensive.lean

Statistics

Metric	Count
Definitions FinitaryExtensive, FinitaryPreExtensive, HasPullbacksOfInclusions, PreservesPullbacksOfInclusions, Extensive, finitaryExtensiveTopCatAux	6
Theorems hasFiniteCoproducts, hasPullbacksOfInclusions, isPullback_initial_to, isPullback_initial_to_binaryCofan, isPullback_initial_to_sigma_ι, isVanKampen_finiteCoproducts, isVanKampen_finiteCoproducts_Fin, mono_inl_of_isColimit, mono_inr_of_isColimit, mono_ι, toFinitaryPreExtensive, vanKampen, van_kampen', hasFiniteCoproducts, hasPullbacksOfInclusions, hasPullbacks_of_inclusions, hasPullbacks_of_is_coproduct, isIso_sigmaDesc_fst, isIso_sigmaDesc_map, isPullback_sigmaDesc, isUniversal_finiteCoproducts, isUniversal_finiteCoproducts_Fin, universal', hasPullbackInl, hasPullbackInr, hasPullbackInr', instOfHasPullbacks, preservesPullbackInl', instOfPreservesLimitsOfShapeWalkingCospan, preservesPullbackInl, preservesPullbackInl', preservesPullbackInr, preservesPullbackInr', finitaryExtensive_TopCat, finitaryExtensive_functor, finitaryExtensive_iff_of_isTerminal, finitaryExtensive_of_preserves_and_reflects, finitaryExtensive_of_preserves_and_reflects_isomorphism, finitaryExtensive_of_reflective, hasStrictInitialObjects_of_finitaryPreExtensive, instCoproductsOfShapeDisjointOfFinitaryExtensiveOfFinite, instMonoCoprodOfFinitaryExtensive, instMonoι, instPreservesLimitWalkingCospanCospanOfIsIso, instPreservesLimitWalkingCospanCospanOfIsIso_1, finitaryExtensive	46
Total	52

CategoryTheory

Definitions

Name	Category	Theorems
FinitaryExtensive 📖	CompData	12 math math: finitaryExtensive_iff_of_isTerminal, CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions, AlgebraicGeometry.instFinitaryExtensiveScheme, finitaryExtensive_of_reflective, SheafOfTypes.finitary_extensive, finitaryExtensive_of_preserves_and_reflects_isomorphism, instFinitaryExtensiveSheafOfHasPullbacksOfHasSheafify, finitaryExtensive_TopCat, finitaryExtensive_functor, types.finitaryExtensive, finitaryExtensive_of_preserves_and_reflects, CompHausLike.finitaryExtensive
FinitaryPreExtensive 📖	CompData	1 math math: FinitaryExtensive.toFinitaryPreExtensive
HasPullbacksOfInclusions 📖	CompData	4 math math: CompHausLike.instHasPullbacksOfInclusionsOfHasExplicitPullbacksOfInclusions, FinitaryPreExtensive.hasPullbacksOfInclusions, HasPullbacksOfInclusions.instOfHasPullbacks, FinitaryExtensive.hasPullbacksOfInclusions
PreservesPullbacksOfInclusions 📖	CompData	2 math math: CompHausLike.instPreservesPullbacksOfInclusionsTopCatCompHausLikeToTopOfHasExplicitPullbacksOfInclusions, PreservesPullbacksOfInclusions.instOfPreservesLimitsOfShapeWalkingCospan
finitaryExtensiveTopCatAux 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finitaryExtensive_TopCat 📖	mathematical	—	FinitaryExtensive TopCat TopCat.instCategory	—	finitaryExtensive_iff_of_isTerminal Limits.hasFiniteCoproducts_of_hasFiniteColimits Limits.hasFiniteColimits_of_hasColimits TopCat.topCat_hasColimits HasPullbacksOfInclusions.instOfHasPullbacks Limits.hasColimitsOfShape_discrete Finite.of_fintype Limits.hasLimitsOfShape_widePullbackShape Limits.hasFiniteWidePullbacks_of_hasFiniteLimits Limits.hasFiniteLimits_of_hasLimits TopCat.topCat_hasLimits CommSq.w Sum.inl_injective ConcreteCategory.congr_hom Limits.PullbackCone.condition Topology.IsInducing.continuous_iff Topology.IsEmbedding.isInducing Topology.IsEmbedding.inl ContinuousMap.continuous_toFun TopCat.ext Limits.IsTerminal.hom_ext Sum.inr_injective Topology.IsEmbedding.inr
finitaryExtensive_functor 📖	mathematical	—	FinitaryExtensive Functor Functor.category	—	Limits.functorCategoryHasColimitsOfShape Limits.hasColimitsOfShape_discrete FinitaryExtensive.hasFiniteCoproducts Finite.of_fintype HasPullbacksOfInclusions.instOfHasPullbacks Limits.functorCategoryHasLimitsOfShape isVanKampenColimit_of_evaluation FinitaryExtensive.vanKampen Limits.evaluation_preservesColimit Limits.hasColimitOfHasColimitsOfShape
finitaryExtensive_iff_of_isTerminal 📖	mathematical	—	FinitaryExtensive IsVanKampenColimit Discrete Limits.WalkingPair discreteCategory Limits.pair	—	Limits.hasColimitsOfShape_discrete Finite.of_fintype FinitaryExtensive.van_kampen' Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' IsPullback.paste_vert_iff
finitaryExtensive_of_preserves_and_reflects 📖	mathematical	—	FinitaryExtensive	—	Limits.hasColimitsOfShape_discrete Finite.of_fintype IsVanKampenColimit.of_iso Limits.hasColimitOfHasColimitsOfShape PreservesPullbacksOfInclusions.preservesPullbackInl' PreservesPullbacksOfInclusions.preservesPullbackInr' IsVanKampenColimit.of_mapCocone instPreservesLimitWalkingCospanCospanOfIsIso_1 Functor.map_isIso Discrete.instIsIso FinitaryExtensive.vanKampen Limits.PreservesColimitsOfShape.preservesColimit
finitaryExtensive_of_preserves_and_reflects_isomorphism 📖	mathematical	—	FinitaryExtensive	—	finitaryExtensive_of_preserves_and_reflects HasPullbacksOfInclusions.instOfHasPullbacks Limits.hasColimitsOfShape_discrete Finite.of_fintype PreservesPullbacksOfInclusions.instOfPreservesLimitsOfShapeWalkingCospan Limits.reflectsLimitsOfShape_of_reflectsIsomorphisms Limits.reflectsColimitsOfShape_of_reflectsIsomorphisms
finitaryExtensive_of_reflective 📖	mathematical	Limits.HasPullback Functor.obj Functor.id Functor.map NatTrans.app Functor.comp Adjunction.unit Limits.PreservesLimit Limits.WalkingCospan Limits.WidePullbackShape.category Limits.WalkingPair Limits.cospan	FinitaryExtensive	—	Limits.hasColimitsOfShape_discrete Finite.of_fintype FinitaryExtensive.hasFiniteCoproducts Adjunction.leftAdjoint_preservesColimits Adjunction.counit_isIso_of_R_fully_faithful IsVanKampenColimit.precompose_isIso_iff Iso.isIso_hom Limits.hasColimitOfHasColimitsOfShape Functor.hext Discrete.functor_map_id PreservesPullbacksOfInclusions.preservesPullbackInl' PreservesPullbacksOfInclusions.preservesPullbackInr' IsVanKampenColimit.of_iso IsVanKampenColimit.map_reflective FinitaryExtensive.vanKampen Limits.PreservesColimitsOfShape.preservesColimit Limits.PreservesFiniteColimits.preservesFiniteColimits Limits.PreservesColimits.preservesFiniteColimits
hasStrictInitialObjects_of_finitaryPreExtensive 📖	mathematical	—	Limits.HasStrictInitialObjects	—	hasStrictInitial_of_isUniversal Limits.hasColimitsOfShape_discrete FinitaryPreExtensive.hasFiniteCoproducts Finite.of_fintype FinitaryPreExtensive.universal' Limits.BinaryCofan.isColimit_iff_isIso_inr IsIso.id
instCoproductsOfShapeDisjointOfFinitaryExtensiveOfFinite 📖	mathematical	—	Limits.CoproductsOfShapeDisjoint	—	Limits.hasColimitsOfShape_discrete FinitaryExtensive.hasFiniteCoproducts Finite.of_fintype FinitaryExtensive.isPullback_initial_to IsPullback.of_isLimit FinitaryExtensive.mono_ι
instMonoCoprodOfFinitaryExtensive 📖	mathematical	—	Limits.MonoCoprod	—	BinaryCofan.mono_inr_of_isVanKampen Limits.hasColimitsOfShape_discrete FinitaryExtensive.hasFiniteCoproducts Finite.of_fintype FinitaryExtensive.vanKampen
instMonoι 📖	mathematical	—	Mono Limits.sigmaObj Limits.hasColimitOfHasColimitsOfShape Discrete discreteCategory Limits.hasColimitsOfShape_discrete FinitaryExtensive.hasFiniteCoproducts Discrete.functor Limits.Sigma.ι	—	FinitaryExtensive.mono_ι Limits.hasColimitOfHasColimitsOfShape Limits.hasColimitsOfShape_discrete FinitaryExtensive.hasFiniteCoproducts
instPreservesLimitWalkingCospanCospanOfIsIso 📖	mathematical	—	Limits.PreservesLimit Limits.WalkingCospan Limits.WidePullbackShape.category Limits.WalkingPair Limits.cospan	—	Limits.hasPullback_of_left_iso Limits.preservesLimit_of_preserves_limit_cone IsPullback.of_hasPullback Limits.pullback.condition IsPullback.of_vert_isIso Functor.map_isIso Limits.pullback_snd_iso_of_left_iso Functor.map_comp
instPreservesLimitWalkingCospanCospanOfIsIso_1 📖	mathematical	—	Limits.PreservesLimit Limits.WalkingCospan Limits.WidePullbackShape.category Limits.WalkingPair Limits.cospan	—	Limits.preservesPullback_symmetry instPreservesLimitWalkingCospanCospanOfIsIso

CategoryTheory.FinitaryExtensive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasFiniteCoproducts 📖	mathematical	—	CategoryTheory.Limits.HasFiniteCoproducts	—	—
hasPullbacksOfInclusions 📖	mathematical	—	CategoryTheory.HasPullbacksOfInclusions CategoryTheory.Limits.hasColimitsOfShape_discrete hasFiniteCoproducts CategoryTheory.Limits.WalkingPair Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair	—	—
isPullback_initial_to 📖	mathematical	—	CategoryTheory.IsPullback CategoryTheory.Limits.initial CategoryTheory.Limits.hasColimitsOfShape_discrete hasFiniteCoproducts Finite.of_fintype Fintype.instPEmpty CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.initial.to CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι	—	CategoryTheory.isPullback_initial_to_of_cofan_isVanKampen CategoryTheory.Limits.hasColimitsOfShape_discrete hasFiniteCoproducts Finite.of_fintype isVanKampen_finiteCoproducts
isPullback_initial_to_binaryCofan 📖	mathematical	—	CategoryTheory.IsPullback CategoryTheory.Limits.initial CategoryTheory.Limits.hasColimitsOfShape_discrete hasFiniteCoproducts Finite.of_fintype Fintype.instPEmpty CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair CategoryTheory.Limits.WalkingPair.left CategoryTheory.Limits.WalkingPair.right CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.initial.to CategoryTheory.Limits.BinaryCofan.inl CategoryTheory.Limits.BinaryCofan.inr	—	CategoryTheory.BinaryCofan.isPullback_initial_to_of_isVanKampen CategoryTheory.Limits.hasColimitsOfShape_discrete hasFiniteCoproducts Finite.of_fintype vanKampen
isPullback_initial_to_sigma_ι 📖	mathematical	—	CategoryTheory.IsPullback CategoryTheory.Limits.initial CategoryTheory.Limits.hasColimitsOfShape_discrete hasFiniteCoproducts Finite.of_fintype Fintype.instPEmpty CategoryTheory.Limits.sigmaObj CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.functor CategoryTheory.Limits.initial.to CategoryTheory.Limits.Sigma.ι	—	isPullback_initial_to CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_discrete hasFiniteCoproducts
isVanKampen_finiteCoproducts 📖	mathematical	—	CategoryTheory.IsVanKampenColimit CategoryTheory.Discrete CategoryTheory.discreteCategory	—	Finite.exists_equiv_fin CategoryTheory.IsVanKampenColimit.whiskerEquivalence_iff isVanKampen_finiteCoproducts_Fin
isVanKampen_finiteCoproducts_Fin 📖	mathematical	—	CategoryTheory.IsVanKampenColimit CategoryTheory.Discrete CategoryTheory.discreteCategory	—	CategoryTheory.Functor.hext CategoryTheory.Discrete.functor_map_id CategoryTheory.isVanKampenColimit_of_isEmpty CategoryTheory.hasStrictInitialObjects_of_finitaryPreExtensive toFinitaryPreExtensive CategoryTheory.instIsEmptyDiscrete Fin.isEmpty' CategoryTheory.IsVanKampenColimit.of_iso CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_discrete hasFiniteCoproducts Finite.of_fintype CategoryTheory.isVanKampenColimit_extendCofan van_kampen' CategoryTheory.HasPullbacksOfInclusions.hasPullbackInr hasPullbacksOfInclusions
mono_inl_of_isColimit 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair CategoryTheory.Limits.WalkingPair.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.BinaryCofan.inl	—	mono_inr_of_isColimit
mono_inr_of_isColimit 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair CategoryTheory.Limits.WalkingPair.right CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.BinaryCofan.inr	—	CategoryTheory.BinaryCofan.mono_inr_of_isVanKampen CategoryTheory.Limits.hasColimitsOfShape_discrete hasFiniteCoproducts Finite.of_fintype vanKampen
mono_ι 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι	—	CategoryTheory.mono_of_cofan_isVanKampen CategoryTheory.Limits.hasColimitsOfShape_discrete hasFiniteCoproducts Finite.of_fintype isVanKampen_finiteCoproducts
toFinitaryPreExtensive 📖	mathematical	—	CategoryTheory.FinitaryPreExtensive	—	hasFiniteCoproducts hasPullbacksOfInclusions CategoryTheory.IsVanKampenColimit.isUniversal van_kampen'
vanKampen 📖	mathematical	—	CategoryTheory.IsVanKampenColimit CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory	—	CategoryTheory.Functor.hext CategoryTheory.Discrete.functor_map_id van_kampen'
van_kampen' 📖	mathematical	—	CategoryTheory.IsVanKampenColimit CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair	—	—

CategoryTheory.FinitaryPreExtensive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasFiniteCoproducts 📖	mathematical	—	CategoryTheory.Limits.HasFiniteCoproducts	—	—
hasPullbacksOfInclusions 📖	mathematical	—	CategoryTheory.HasPullbacksOfInclusions CategoryTheory.Limits.hasColimitsOfShape_discrete hasFiniteCoproducts CategoryTheory.Limits.WalkingPair Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair	—	—
hasPullbacks_of_inclusions 📖	mathematical	—	CategoryTheory.Limits.HasPullback	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_discrete hasFiniteCoproducts hasPullbacks_of_is_coproduct
hasPullbacks_of_is_coproduct 📖	mathematical	—	CategoryTheory.Limits.HasPullback CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι	—	CategoryTheory.Functor.hext CategoryTheory.Discrete.functor_map_id CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_discrete hasFiniteCoproducts Subtype.finite Finite.of_fintype CategoryTheory.Limits.Sigma.hom_ext CategoryTheory.Limits.colimit.ι_desc_assoc CategoryTheory.Category.comp_id CategoryTheory.Category.assoc CategoryTheory.Limits.colimit.ι_desc CategoryTheory.Category.id_comp CategoryTheory.Limits.coprod.hom_ext CategoryTheory.Limits.coprod.desc_comp Subtype.prop CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_inv CategoryTheory.IsPullback.of_horiz_isIso CategoryTheory.IsIso.id CategoryTheory.Iso.isIso_inv CategoryTheory.Iso.hom_inv_id CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.HasPullbacksOfInclusions.preservesPullbackInl' hasPullbacksOfInclusions CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.IsPullback.paste_horiz CategoryTheory.IsPullback.of_hasPullback
isIso_sigmaDesc_fst 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Limits.sigmaObj CategoryTheory.Limits.pullback hasPullbacks_of_inclusions CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Limits.hasColimitsOfShape_discrete hasFiniteCoproducts CategoryTheory.Discrete.functor CategoryTheory.Limits.Sigma.desc CategoryTheory.Limits.pullback.fst	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_discrete hasFiniteCoproducts hasPullbacks_of_inclusions CategoryTheory.Limits.Cofan.nonempty_isColimit_iff_isIso_sigmaDesc isUniversal_finiteCoproducts CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_pullbackCone_left CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id CategoryTheory.IsPullback.id_horiz CategoryTheory.Limits.pullback.condition
isIso_sigmaDesc_map 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Limits.sigmaObj CategoryTheory.Limits.pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Limits.hasColimitsOfShape_discrete hasFiniteCoproducts Finite.instProd CategoryTheory.Discrete.functor CategoryTheory.Limits.Sigma.desc CategoryTheory.Limits.pullback.map CategoryTheory.Limits.Sigma.ι CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_discrete hasFiniteCoproducts CategoryTheory.Category.comp_id CategoryTheory.Limits.colimit.ι_desc Finite.instProd CategoryTheory.Limits.Cofan.nonempty_isColimit_iff_isIso_sigmaDesc CategoryTheory.IsUniversalColimit.nonempty_isColimit_prod_of_pullbackCone isUniversal_finiteCoproducts CategoryTheory.Category.id_comp CategoryTheory.Limits.limit.lift_π
isPullback_sigmaDesc 📖	mathematical	—	CategoryTheory.IsPullback CategoryTheory.Limits.sigmaObj CategoryTheory.Limits.pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Limits.hasColimitsOfShape_discrete hasFiniteCoproducts Finite.instProd CategoryTheory.Discrete.functor CategoryTheory.Limits.Sigma.desc CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.Sigma.ι CategoryTheory.Limits.pullback.snd	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_discrete hasFiniteCoproducts Finite.instProd CategoryTheory.Limits.Sigma.hom_ext CategoryTheory.Limits.colimit.ι_desc CategoryTheory.Category.id_comp CategoryTheory.IsUniversalColimit.isPullback_prod_of_isColimit isUniversal_finiteCoproducts CategoryTheory.IsPullback.of_hasPullback
isUniversal_finiteCoproducts 📖	mathematical	—	CategoryTheory.IsUniversalColimit CategoryTheory.Discrete CategoryTheory.discreteCategory	—	Finite.exists_equiv_fin CategoryTheory.IsUniversalColimit.whiskerEquivalence_iff isUniversal_finiteCoproducts_Fin
isUniversal_finiteCoproducts_Fin 📖	mathematical	—	CategoryTheory.IsUniversalColimit CategoryTheory.Discrete CategoryTheory.discreteCategory	—	CategoryTheory.Functor.hext CategoryTheory.Discrete.functor_map_id CategoryTheory.IsVanKampenColimit.isUniversal CategoryTheory.isVanKampenColimit_of_isEmpty CategoryTheory.hasStrictInitialObjects_of_finitaryPreExtensive CategoryTheory.instIsEmptyDiscrete Fin.isEmpty' CategoryTheory.IsUniversalColimit.of_iso CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_discrete hasFiniteCoproducts Finite.of_fintype CategoryTheory.isUniversalColimit_extendCofan universal' CategoryTheory.HasPullbacksOfInclusions.hasPullbackInr hasPullbacksOfInclusions
universal' 📖	mathematical	—	CategoryTheory.IsUniversalColimit CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair	—	—

CategoryTheory.HasPullbacksOfInclusions

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasPullbackInl 📖	mathematical	—	CategoryTheory.Limits.HasPullback CategoryTheory.Limits.coprod CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair CategoryTheory.Limits.coprod.inl	—	—
hasPullbackInr 📖	mathematical	—	CategoryTheory.Limits.HasPullback CategoryTheory.Limits.coprod CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair CategoryTheory.Limits.coprod.inr	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasPullback_symmetry hasPullbackInr'
hasPullbackInr' 📖	mathematical	—	CategoryTheory.Limits.HasPullback CategoryTheory.Limits.coprod CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair CategoryTheory.Limits.coprod.inr	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.IsPullback.of_horiz_isIso CategoryTheory.IsIso.id CategoryTheory.Iso.isIso_hom CategoryTheory.Category.id_comp CategoryTheory.Category.assoc CategoryTheory.Limits.coprod.desc_comp CategoryTheory.Limits.colimit.ι_desc CategoryTheory.Limits.coprod.desc_inl_inr CategoryTheory.Category.comp_id CategoryTheory.Limits.hasPullbackHorizPaste preservesPullbackInl' CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.IsPullback.paste_horiz CategoryTheory.IsPullback.of_hasPullback
instOfHasPullbacks 📖	mathematical	—	CategoryTheory.HasPullbacksOfInclusions	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasLimitOfHasLimitsOfShape
preservesPullbackInl' 📖	mathematical	—	CategoryTheory.Limits.HasPullback CategoryTheory.Limits.coprod CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair CategoryTheory.Limits.coprod.inl	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasPullback_symmetry hasPullbackInl

CategoryTheory.PreservesPullbacksOfInclusions

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instOfPreservesLimitsOfShapeWalkingCospan 📖	mathematical	—	CategoryTheory.PreservesPullbacksOfInclusions	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit
preservesPullbackInl 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.coprod CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Limits.pair CategoryTheory.Limits.coprod.inl	—	—
preservesPullbackInl' 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.coprod CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Limits.pair CategoryTheory.Limits.coprod.inl	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.preservesPullback_symmetry preservesPullbackInl
preservesPullbackInr 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.coprod CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Limits.pair CategoryTheory.Limits.coprod.inr	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.preservesPullback_symmetry preservesPullbackInr'
preservesPullbackInr' 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.coprod CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Limits.pair CategoryTheory.Limits.coprod.inr	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.preservesLimit_of_iso_diagram CategoryTheory.Category.id_comp CategoryTheory.Category.assoc CategoryTheory.Limits.coprod.desc_comp CategoryTheory.Limits.colimit.ι_desc CategoryTheory.Limits.coprod.desc_inl_inr CategoryTheory.Category.comp_id preservesPullbackInl'

CategoryTheory.Presieve

Definitions

Name	Category	Theorems
Extensive 📖	CompData	1 math math: CategoryTheory.instExtensiveOfArrowsι

CategoryTheory.types

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finitaryExtensive 📖	mathematical	—	CategoryTheory.FinitaryExtensive CategoryTheory.types	—	CategoryTheory.finitaryExtensive_iff_of_isTerminal CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self CategoryTheory.HasPullbacksOfInclusions.instOfHasPullbacks CategoryTheory.Limits.hasColimitsOfShape_discrete Finite.of_fintype CategoryTheory.Limits.Types.instHasPullbacksType CategoryTheory.CommSq.w CategoryTheory.Limits.PullbackCone.condition CategoryTheory.Limits.IsTerminal.hom_ext CategoryTheory.types_ext

---

← Back to Index