Basic

📁 Source: Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean

Statistics

Metric	Count
Definitions AB4, AB4OfSize, AB4Star, AB4StarOfSize, AB5, AB5OfSize, AB5Star, AB5StarOfSize, CountableAB4, CountableAB4Star, HasExactColimitsOfShape, HasExactLimitsOfShape	12
Theorems of_AB5, ofShape, AB4OfSize_shrink, of_AB5Star, ofShape, AB4StarOfSize_shrink, ofShape, AB5OfSize_of_univLE, AB5OfSize_shrink, ofShape, AB5StarOfSize_of_univLE, AB5StarOfSize_shrink, hasExactColimitsOfShape, hasExactLimitsOfShape, ofShape, of_countableAB5, of_hasExactColimitsOfShape_nat, of_hasExactColimitsOfShape_nat_and_finite, ofShape, of_countableAB5Star, of_hasExactLimitsOfShape_nat, of_hasExactLimitsOfShape_nat_and_finite, domain_of_functor, of_codomain_equivalence, of_domain_equivalence, preservesFiniteLimits, domain_of_functor, of_codomain_equivalence, of_domain_equivalence, preservesFiniteColimits, hasExactColimitsOfShape_discrete_finite, hasExactColimitsOfShape_discrete_of_hasExactColimitsOfShape_finset_discrete, hasExactColimitsOfShape_of_final, hasExactColimitsOfShape_of_preservesMono, hasExactLimitsOfShape_discrete_finite, hasExactLimitsOfShape_discrete_of_hasExactLimitsOfShape_finset_discrete_op, hasExactLimitsOfShape_of_initial, hasExactLimitsOfShape_of_preservesEpi, instAB4OfSize, instAB4StarOfSize, instCountableAB4OfAB4OfSize, instCountableAB4StarOfAB4StarOfSize, preservesFiniteColimits_liftToFinset, preservesFiniteLimits_liftToFinset	44
Total	56

CategoryTheory

Definitions

Name	Category	Theorems
AB4 📖	MathDef	3 math math: instAB4AddCommGrpCat, instAB4ModuleCat, Condensed.instAB4CondensedMod
AB4OfSize 📖	CompData	4 math math: IsGrothendieckAbelian.ab4OfSize, AB4OfSize_shrink, instAB4OfSize, AB4.of_AB5
AB4Star 📖	MathDef	3 math math: Condensed.instAB4StarCondensedMod, instAB4StarModuleCat, instAB4StarAddCommGrpCat
AB4StarOfSize 📖	CompData	3 math math: AB4StarOfSize_shrink, AB4Star.of_AB5Star, instAB4StarOfSize
AB5 📖	MathDef	5 math math: Condensed.instAB5CondensedMod, Limits.instAB5IndOfHasFiniteLimits, instAB5ModuleCat, instAB5AddCommGrpCat, Limits.instAB5Type
AB5OfSize 📖	CompData	5 math math: AB5OfSize_of_univLE, HomologicalComplex.ab5OfSize, Sheaf.ab5ofSize, AB5OfSize_shrink, IsGrothendieckAbelian.ab5OfSize
AB5Star 📖	MathDef	—
AB5StarOfSize 📖	CompData	2 math math: AB5StarOfSize_shrink, AB5StarOfSize_of_univLE
CountableAB4 📖	CompData	4 math math: CountableAB4.of_hasExactColimitsOfShape_nat_and_finite, instCountableAB4OfAB4OfSize, CountableAB4.of_hasExactColimitsOfShape_nat, CountableAB4.of_countableAB5
CountableAB4Star 📖	CompData	5 math math: instCountableAB4StarOfAB4StarOfSize, CountableAB4Star.of_hasExactLimitsOfShape_nat_and_finite, CountableAB4Star.of_hasExactLimitsOfShape_nat, LightCondensed.instCountableAB4StarLightCondMod, CountableAB4Star.of_countableAB5Star
HasExactColimitsOfShape 📖	CompData	18 math math: Condensed.hasExactColimitsOfShape, HasExactColimitsOfShape.domain_of_functor, hasExactColimitsOfShape_of_preservesMono, CountableAB4.ofShape, hasExactColimitsOfShape_of_final, instHasExactColimitsOfShapeFunctorOfHasFiniteLimits, Limits.instHasExactColimitsOfShapeIndOfHasFiniteLimits, hasExactColimitsOfShape_discrete_finite, Sheaf.instHasExactColimitsOfShapeOfHasFiniteLimitsOfPreservesColimitsOfShapeFunctorOppositeSheafToPresheaf, hasExactColimitsOfShape_discrete_of_hasExactColimitsOfShape_finset_discrete, HasExactColimitsOfShape.of_codomain_equivalence, AB5OfSize.ofShape, GrothendieckTopology.Point.instHasExactColimitsOfShapeOppositeElementsFiberOfLocallySmallOfAB5OfSizeOfHasFiniteLimits, Sheaf.hasExactColimitsOfShape, AB4OfSize.ofShape, HasExactColimitsOfShape.of_domain_equivalence, HomologicalComplex.hasExactColimitsOfShape, Adjunction.hasExactColimitsOfShape
HasExactLimitsOfShape 📖	CompData	15 math math: hasExactLimitsOfShape_of_initial, HasExactLimitsOfShape.domain_of_functor, Adjunction.hasExactLimitsOfShape, HasExactLimitsOfShape.of_domain_equivalence, AB4StarOfSize.ofShape, CountableAB4Star.ofShape, instHasExactLimitsOfShapeFunctorOfHasFiniteColimits, Condensed.hasExactLimitsOfShape, hasExactLimitsOfShape_discrete_of_hasExactLimitsOfShape_finset_discrete_op, hasExactLimitsOfShape_of_preservesEpi, hasExactLimitsOfShape_discrete_finite, Sheaf.instHasExactLimitsOfShapeOfHasFiniteColimitsOfPreservesFiniteColimitsFunctorOppositeSheafToPresheaf, AB5StarOfSize.ofShape, HasExactLimitsOfShape.of_codomain_equivalence, instHasExactLimitsOfShapeDiscreteAddCommGrpCat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
AB4OfSize_shrink 📖	mathematical	Limits.HasCoproducts	AB4OfSize Limits.hasCoproducts_shrink	—	Limits.hasCoproducts_shrink HasExactColimitsOfShape.of_domain_equivalence AB4OfSize.ofShape
AB4StarOfSize_shrink 📖	mathematical	Limits.HasProducts	AB4StarOfSize Limits.hasProducts_shrink	—	Limits.hasProducts_shrink HasExactLimitsOfShape.of_domain_equivalence AB4StarOfSize.ofShape
AB5OfSize_of_univLE 📖	mathematical	—	AB5OfSize Limits.hasFilteredColimitsOfSize_of_univLE	—	Limits.hasFilteredColimitsOfSize_of_univLE HasExactColimitsOfShape.of_domain_equivalence UnivLE.small locallySmall_of_univLE Limits.hasColimitsOfShape_of_has_filtered_colimits IsFiltered.of_equivalence AB5OfSize.ofShape
AB5OfSize_shrink 📖	mathematical	—	AB5OfSize Limits.hasFilteredColimitsOfSize_shrink	—	AB5OfSize_of_univLE univLE_of_max UnivLE.self
AB5StarOfSize_of_univLE 📖	mathematical	—	AB5StarOfSize Limits.hasCofilteredLimitsOfSize_of_univLE	—	Limits.hasCofilteredLimitsOfSize_of_univLE HasExactLimitsOfShape.of_domain_equivalence UnivLE.small locallySmall_of_univLE Limits.hasLimitsOfShape_of_has_cofiltered_limits IsCofiltered.of_equivalence AB5StarOfSize.ofShape
AB5StarOfSize_shrink 📖	mathematical	—	AB5StarOfSize Limits.hasCofilteredLimitsOfSize_shrink	—	AB5StarOfSize_of_univLE univLE_of_max UnivLE.self
hasExactColimitsOfShape_discrete_finite 📖	mathematical	—	HasExactColimitsOfShape Discrete discreteCategory Limits.hasColimitsOfShape_discrete Limits.hasFiniteCoproducts_of_hasFiniteBiproducts	—	Limits.hasColimitsOfShape_discrete Limits.hasFiniteCoproducts_of_hasFiniteBiproducts Limits.preservesFiniteLimits_of_natIso Limits.hasProductsOfShape_of_hasBiproductsOfShape Limits.hasBiproductsOfShape_finite Limits.hasCoproductsOfShape_of_hasBiproductsOfShape Limits.PreservesLimits.preservesFiniteLimits Adjunction.lim_preservesLimits
hasExactColimitsOfShape_discrete_of_hasExactColimitsOfShape_finset_discrete 📖	mathematical	—	HasExactColimitsOfShape Discrete discreteCategory	—	Limits.preservesFiniteLimits_of_natIso Limits.hasFiniteCoproducts_of_hasFiniteBiproducts Limits.comp_preservesFiniteLimits preservesFiniteLimits_liftToFinset HasExactColimitsOfShape.preservesFiniteLimits
hasExactColimitsOfShape_of_final 📖	mathematical	—	HasExactColimitsOfShape	—	Limits.preservesFiniteLimits_of_natIso Limits.comp_preservesFiniteLimits whiskeringLeft_preservesLimitsOfShape Limits.hasLimitsOfShape_of_hasFiniteLimits HasExactColimitsOfShape.preservesFiniteLimits
hasExactColimitsOfShape_of_preservesMono 📖	mathematical	—	HasExactColimitsOfShape	—	Functor.preservesFiniteLimits_of_preservesHomology Functor.additive_of_preservesBinaryBiproducts Abelian.hasBinaryBiproducts Functor.preservesZeroMorphisms_of_preserves_initial_object Limits.HasZeroObject.instFunctor Abelian.hasZeroObject Limits.PreservesColimitsOfShape.preservesColimit Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint Limits.instIsLeftAdjointFunctorColim Limits.preservesBinaryBiproducts_of_preservesBinaryCoproducts Functor.preservesHomology_of_preservesMonos_and_cokernels Functor.preservesZeroMorphisms_of_additive Limits.instHasFiniteProductsFunctor Abelian.has_finite_products Abelian.has_kernels
hasExactLimitsOfShape_discrete_finite 📖	mathematical	—	HasExactLimitsOfShape Discrete discreteCategory Limits.hasLimitsOfShape_discrete Limits.hasFiniteProducts_of_hasFiniteBiproducts	—	Limits.hasLimitsOfShape_discrete Limits.hasFiniteProducts_of_hasFiniteBiproducts Limits.preservesFiniteColimits_of_natIso Limits.hasCoproductsOfShape_of_hasBiproductsOfShape Limits.hasBiproductsOfShape_finite Limits.PreservesColimits.preservesFiniteColimits Adjunction.colim_preservesColimits
hasExactLimitsOfShape_discrete_of_hasExactLimitsOfShape_finset_discrete_op 📖	mathematical	—	HasExactLimitsOfShape Discrete discreteCategory	—	Limits.preservesFiniteColimits_of_natIso Limits.hasFiniteProducts_of_hasFiniteBiproducts Limits.comp_preservesFiniteColimits preservesFiniteColimits_liftToFinset HasExactLimitsOfShape.preservesFiniteColimits
hasExactLimitsOfShape_of_initial 📖	mathematical	—	HasExactLimitsOfShape	—	Limits.preservesFiniteColimits_of_natIso Limits.comp_preservesFiniteColimits whiskeringLeft_preservesColimitsOfShape Limits.hasColimitsOfShape_of_hasFiniteColimits HasExactLimitsOfShape.preservesFiniteColimits
hasExactLimitsOfShape_of_preservesEpi 📖	mathematical	—	HasExactLimitsOfShape	—	Functor.preservesFiniteColimits_of_preservesHomology Functor.additive_of_preservesBinaryBiproducts Abelian.hasBinaryBiproducts Functor.preservesZeroMorphisms_of_preserves_terminal_object Limits.HasZeroObject.instFunctor Abelian.hasZeroObject Limits.PreservesLimitsOfShape.preservesLimit Functor.instPreservesLimitsOfShapeOfIsRightAdjoint Limits.instIsRightAdjointFunctorLim Limits.preservesBinaryBiproducts_of_preservesBinaryProducts Functor.preservesHomology_of_preservesEpis_and_kernels Functor.preservesZeroMorphisms_of_additive Limits.instHasFiniteCoproductsFunctor Limits.hasFiniteCoproducts_of_hasFiniteColimits Abelian.hasFiniteColimits Abelian.has_cokernels
instAB4OfSize 📖	mathematical	Limits.HasCoproducts	AB4OfSize Limits.hasCoproducts_shrink	—	AB4OfSize_shrink
instAB4StarOfSize 📖	mathematical	Limits.HasProducts	AB4StarOfSize Limits.hasProducts_shrink	—	AB4StarOfSize_shrink
instCountableAB4OfAB4OfSize 📖	mathematical	Limits.HasCoproducts	CountableAB4 Limits.hasCountableCoproducts_of_hasCoproducts	—	Limits.hasCountableCoproducts_of_hasCoproducts Limits.instHasCoproductsOfShapeOfHasCountableCoproductsOfCountable AB4OfSize.ofShape
instCountableAB4StarOfAB4StarOfSize 📖	mathematical	Limits.HasProducts	CountableAB4Star Limits.hasCountableProducts_of_hasProducts	—	Limits.hasCountableProducts_of_hasProducts Limits.instHasProductsOfShapeOfHasCountableProductsOfCountable AB4StarOfSize.ofShape
preservesFiniteColimits_liftToFinset 📖	mathematical	—	Limits.PreservesFiniteColimits Functor Discrete discreteCategory Functor.category Opposite Finset Category.opposite Preorder.smallCategory PartialOrder.toPreorder Finset.partialOrder Limits.ProductsFromFiniteCofiltered.liftToFinset Limits.hasFiniteProducts_of_hasFiniteBiproducts	—	preservesFiniteColimits_of_evaluation Limits.hasFiniteProducts_of_hasFiniteBiproducts Limits.preservesFiniteColimits_of_natIso Limits.hasLimitsOfShape_discrete Finite.of_fintype Limits.comp_preservesFiniteColimits whiskeringLeft_preservesColimitsOfShape Limits.hasColimitsOfShape_of_hasFiniteColimits Limits.hasCoproductsOfShape_of_hasBiproductsOfShape Limits.hasBiproductsOfShape_finite Limits.PreservesColimits.preservesFiniteColimits Adjunction.colim_preservesColimits
preservesFiniteLimits_liftToFinset 📖	mathematical	—	Limits.PreservesFiniteLimits Functor Discrete discreteCategory Functor.category Finset Preorder.smallCategory PartialOrder.toPreorder Finset.partialOrder Limits.CoproductsFromFiniteFiltered.liftToFinset Limits.hasFiniteCoproducts_of_hasFiniteBiproducts	—	preservesFiniteLimits_of_evaluation Limits.hasFiniteCoproducts_of_hasFiniteBiproducts Limits.preservesFiniteLimits_of_natIso Limits.hasColimitsOfShape_discrete Finite.of_fintype Limits.comp_preservesFiniteLimits whiskeringLeft_preservesLimitsOfShape Limits.hasLimitsOfShape_of_hasFiniteLimits Limits.hasProductsOfShape_of_hasBiproductsOfShape Limits.hasBiproductsOfShape_finite Limits.hasCoproductsOfShape_of_hasBiproductsOfShape Limits.PreservesLimits.preservesFiniteLimits Adjunction.lim_preservesLimits

CategoryTheory.AB4

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_AB5 📖	mathematical	—	CategoryTheory.AB4OfSize CategoryTheory.Limits.hasCoproducts_of_finite_and_filtered CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteBiproducts	—	CategoryTheory.Limits.hasCoproducts_of_finite_and_filtered CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteBiproducts CategoryTheory.hasExactColimitsOfShape_discrete_of_hasExactColimitsOfShape_finset_discrete CategoryTheory.Limits.hasColimitsOfShape_of_has_filtered_colimits CategoryTheory.isFiltered_of_directed_le_nonempty Finset.isDirected_le CategoryTheory.AB5OfSize.ofShape

CategoryTheory.AB4OfSize

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofShape 📖	mathematical	CategoryTheory.Limits.HasCoproducts	CategoryTheory.HasExactColimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory	—	—

CategoryTheory.AB4Star

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_AB5Star 📖	mathematical	—	CategoryTheory.AB4StarOfSize CategoryTheory.Limits.hasProducts_of_finite_and_cofiltered CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteBiproducts	—	CategoryTheory.Limits.hasProducts_of_finite_and_cofiltered CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteBiproducts CategoryTheory.hasExactLimitsOfShape_discrete_of_hasExactLimitsOfShape_finset_discrete_op CategoryTheory.Limits.hasLimitsOfShape_of_has_cofiltered_limits CategoryTheory.isCofiltered_op_of_isFiltered CategoryTheory.isFiltered_of_directed_le_nonempty Finset.isDirected_le CategoryTheory.AB5StarOfSize.ofShape

CategoryTheory.AB4StarOfSize

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofShape 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.HasExactLimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory	—	—

CategoryTheory.AB5OfSize

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofShape 📖	mathematical	—	CategoryTheory.HasExactColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_of_has_filtered_colimits	—	—

CategoryTheory.AB5StarOfSize

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofShape 📖	mathematical	—	CategoryTheory.HasExactLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_of_has_cofiltered_limits	—	—

CategoryTheory.Adjunction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasExactColimitsOfShape 📖	mathematical	—	CategoryTheory.HasExactColimitsOfShape	—	rightAdjoint_preservesLimits leftAdjoint_preservesColimits CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape counit_isIso_of_R_fully_faithful CategoryTheory.Limits.preservesLimit_of_natIso CategoryTheory.Limits.comp_preservesLimit CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.whiskeringRight_preservesLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.Limits.PreservesLimitsOfSize0.preservesFiniteLimits CategoryTheory.HasExactColimitsOfShape.preservesFiniteLimits
hasExactLimitsOfShape 📖	mathematical	—	CategoryTheory.HasExactLimitsOfShape	—	rightAdjoint_preservesLimits leftAdjoint_preservesColimits CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape unit_isIso_of_L_fully_faithful CategoryTheory.Limits.preservesColimit_of_natIso CategoryTheory.Limits.comp_preservesColimit CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.whiskeringRight_preservesColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_of_hasFiniteColimits CategoryTheory.Limits.PreservesFiniteColimits.preservesFiniteColimits CategoryTheory.Limits.PreservesColimitsOfSize0.preservesFiniteColimits CategoryTheory.HasExactLimitsOfShape.preservesFiniteColimits

CategoryTheory.CountableAB4

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofShape 📖	mathematical	—	CategoryTheory.HasExactColimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Limits.instHasCoproductsOfShapeOfHasCountableCoproductsOfCountable	—	—
of_countableAB5 📖	mathematical	—	CategoryTheory.CountableAB4	—	CategoryTheory.Functor.Final.hasColimitsOfShape_of_final Finset.countable CategoryTheory.discreteCountable CategoryTheory.isFiltered_of_directed_le_nonempty Finset.isDirected_le CategoryTheory.Limits.IsFiltered.sequentialFunctor_final CategoryTheory.hasExactColimitsOfShape_of_final CategoryTheory.hasExactColimitsOfShape_discrete_of_hasExactColimitsOfShape_finset_discrete CategoryTheory.Limits.instHasCoproductsOfShapeOfHasCountableCoproductsOfCountable
of_hasExactColimitsOfShape_nat 📖	mathematical	—	CategoryTheory.CountableAB4	—	CategoryTheory.Limits.instHasCoproductsOfShapeOfHasCountableCoproductsOfCountable instCountableNat of_hasExactColimitsOfShape_nat_and_finite Finite.to_countable CategoryTheory.hasExactColimitsOfShape_discrete_finite
of_hasExactColimitsOfShape_nat_and_finite 📖	mathematical	CategoryTheory.HasExactColimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Limits.instHasCoproductsOfShapeOfHasCountableCoproductsOfCountable Finite.to_countable	CategoryTheory.CountableAB4	—	CategoryTheory.Limits.instHasCoproductsOfShapeOfHasCountableCoproductsOfCountable Finite.to_countable instCountableNat CategoryTheory.hasExactColimitsOfShape_of_final CategoryTheory.Functor.final_of_isRightAdjoint CategoryTheory.Functor.isRightAdjoint_of_isEquivalence CategoryTheory.Equivalence.isEquivalence_inverse

CategoryTheory.CountableAB4Star

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofShape 📖	mathematical	—	CategoryTheory.HasExactLimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Limits.instHasProductsOfShapeOfHasCountableProductsOfCountable	—	—
of_countableAB5Star 📖	mathematical	—	CategoryTheory.CountableAB4Star	—	CategoryTheory.Functor.Initial.hasLimitsOfShape_of_initial Finset.countable CategoryTheory.discreteCountable CategoryTheory.isFiltered_of_directed_le_nonempty Finset.isDirected_le CategoryTheory.Functor.initial_op_of_final CategoryTheory.Limits.IsFiltered.sequentialFunctor_final CategoryTheory.hasExactLimitsOfShape_of_initial CategoryTheory.hasExactLimitsOfShape_discrete_of_hasExactLimitsOfShape_finset_discrete_op CategoryTheory.Limits.instHasProductsOfShapeOfHasCountableProductsOfCountable
of_hasExactLimitsOfShape_nat 📖	mathematical	—	CategoryTheory.CountableAB4Star	—	CategoryTheory.Limits.instHasProductsOfShapeOfHasCountableProductsOfCountable instCountableNat of_hasExactLimitsOfShape_nat_and_finite Finite.to_countable CategoryTheory.hasExactLimitsOfShape_discrete_finite
of_hasExactLimitsOfShape_nat_and_finite 📖	mathematical	CategoryTheory.HasExactLimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Limits.instHasProductsOfShapeOfHasCountableProductsOfCountable Finite.to_countable	CategoryTheory.CountableAB4Star	—	CategoryTheory.Limits.instHasProductsOfShapeOfHasCountableProductsOfCountable Finite.to_countable instCountableNat CategoryTheory.hasExactLimitsOfShape_of_initial CategoryTheory.Functor.initial_of_isLeftAdjoint CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence CategoryTheory.Equivalence.isEquivalence_inverse

CategoryTheory.HasExactColimitsOfShape

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
domain_of_functor 📖	mathematical	—	CategoryTheory.HasExactColimitsOfShape	—	CategoryTheory.NatTrans.naturality CategoryTheory.Limits.comp_preservesLimit CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.whiskeringRight_preservesLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits preservesFiniteLimits CategoryTheory.Limits.reflectsLimit_of_reflectsLimitsOfShape CategoryTheory.Limits.ReflectsFiniteLimits.reflects
of_codomain_equivalence 📖	mathematical	—	CategoryTheory.HasExactColimitsOfShape CategoryTheory.Adjunction.hasColimitsOfShape_of_equivalence CategoryTheory.Equivalence.inverse CategoryTheory.Equivalence.isEquivalence_inverse	—	CategoryTheory.Adjunction.hasColimitsOfShape_of_equivalence CategoryTheory.Equivalence.isEquivalence_inverse CategoryTheory.Limits.preservesLimit_of_natIso CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence CategoryTheory.Limits.comp_preservesLimit CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint CategoryTheory.Functor.isRightAdjoint_of_isEquivalence CategoryTheory.preservesLimit_comp_of_createsLimit CategoryTheory.Limits.comp_preservesLimitsOfShape CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits preservesFiniteLimits CategoryTheory.Equivalence.isEquivalence_functor
of_domain_equivalence 📖	mathematical	—	CategoryTheory.HasExactColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_of_equivalence	—	CategoryTheory.Limits.hasColimitsOfShape_of_equivalence CategoryTheory.Limits.preservesFiniteLimits_of_natIso CategoryTheory.Functor.final_of_isRightAdjoint CategoryTheory.Functor.isRightAdjoint_of_isEquivalence CategoryTheory.Equivalence.isEquivalence_functor CategoryTheory.Limits.comp_preservesFiniteLimits CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint CategoryTheory.Functor.instIsEquivalenceObjWhiskeringLeft preservesFiniteLimits
preservesFiniteLimits 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.colim	—	—

CategoryTheory.HasExactLimitsOfShape

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
domain_of_functor 📖	mathematical	—	CategoryTheory.HasExactLimitsOfShape	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Category.assoc CategoryTheory.Iso.eq_inv_comp CategoryTheory.NatTrans.naturality CategoryTheory.Limits.comp_preservesColimit CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.whiskeringRight_preservesColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_of_hasFiniteColimits CategoryTheory.Limits.PreservesFiniteColimits.preservesFiniteColimits preservesFiniteColimits CategoryTheory.Limits.reflectsColimit_of_reflectsColimitsOfShape CategoryTheory.Limits.ReflectsFiniteColimits.reflects
of_codomain_equivalence 📖	mathematical	—	CategoryTheory.HasExactLimitsOfShape CategoryTheory.Adjunction.hasLimitsOfShape_of_equivalence CategoryTheory.Equivalence.inverse CategoryTheory.Equivalence.isEquivalence_inverse	—	CategoryTheory.Adjunction.hasLimitsOfShape_of_equivalence CategoryTheory.Equivalence.isEquivalence_inverse CategoryTheory.Limits.preservesColimit_of_natIso CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint CategoryTheory.Functor.isRightAdjoint_of_isEquivalence CategoryTheory.Limits.comp_preservesColimit CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence CategoryTheory.preservesColimit_comp_of_createsColimit CategoryTheory.Limits.comp_preservesColimitsOfShape CategoryTheory.Limits.PreservesFiniteColimits.preservesFiniteColimits preservesFiniteColimits CategoryTheory.Equivalence.isEquivalence_functor
of_domain_equivalence 📖	mathematical	—	CategoryTheory.HasExactLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_of_equivalence	—	CategoryTheory.Limits.hasLimitsOfShape_of_equivalence CategoryTheory.Limits.preservesFiniteColimits_of_natIso CategoryTheory.Functor.initial_of_isLeftAdjoint CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence CategoryTheory.Equivalence.isEquivalence_functor CategoryTheory.Limits.comp_preservesFiniteColimits CategoryTheory.Limits.PreservesColimits.preservesFiniteColimits CategoryTheory.Functor.instPreservesColimitsOfSizeOfIsLeftAdjoint CategoryTheory.Functor.instIsEquivalenceObjWhiskeringLeft preservesFiniteColimits
preservesFiniteColimits 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteColimits CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.lim	—	—

---

← Back to Index