EquifiberedLimits

📁 Source: Mathlib/CategoryTheory/Limits/Shapes/Pullback/EquifiberedLimits.lean

Statistics

Metric	Count
Definitions	0
Theorems instIsClosedUnderColimitsOfShapeUnderFunctorCoequifiberedHomDiscretePUnitOfHasProductsOfShapeHom, instIsClosedUnderLimitsOfShapeOverFunctorEquifiberedHomDiscretePUnitOfHasCoproductsOfShapeHom	2
Total	2

CategoryTheory.NatTrans

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsClosedUnderColimitsOfShapeUnderFunctorCoequifiberedHomDiscretePUnitOfHasProductsOfShapeHom 📖	mathematical	CategoryTheory.Limits.HasProductsOfShape Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	CategoryTheory.ObjectProperty.IsClosedUnderColimitsOfShape CategoryTheory.Under CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.instCategoryUnder Coequifibered CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	CategoryTheory.Under.w CategoryTheory.MorphismProperty.cancel_right_of_respectsIso instRespectsIsoFunctorCoequifibered CategoryTheory.Comma.instIsIsoRight CategoryTheory.Iso.isIso_hom CategoryTheory.Limits.hasColimitsOfShape_of_equivalence CategoryTheory.Limits.hasCoproductsOfShape_opposite CategoryTheory.ObjectProperty.isClosedUnderColimitsOfShape_iff_op CategoryTheory.ObjectProperty.isClosedUnderLimitsOfShape_inverseImage_iff CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsOppositeOp CategoryTheory.Iso.isIso_inv instIsClosedUnderLimitsOfShapeOverFunctorEquifiberedHomDiscretePUnitOfHasCoproductsOfShapeHom
instIsClosedUnderLimitsOfShapeOverFunctorEquifiberedHomDiscretePUnitOfHasCoproductsOfShapeHom 📖	mathematical	CategoryTheory.Limits.HasCoproductsOfShape Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape CategoryTheory.Over CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.instCategoryOver Equifibered CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	naturality CategoryTheory.CommSq.w CategoryTheory.Limits.comp_preservesLimit CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Over.preservesLimitsOfShape_forget_of_isConnected CategoryTheory.preservesLimit_comp_of_createsLimit CategoryTheory.Limits.comp_preservesLimitsOfShape CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint CategoryTheory.evaluationIsRightAdjoint CategoryTheory.Category.assoc CategoryTheory.Over.w CategoryTheory.Limits.PullbackCone.condition CategoryTheory.IsPullback.hom_ext CategoryTheory.Category.id_comp CategoryTheory.IsPullback.lift_fst CategoryTheory.IsPullback.lift_fst_assoc CategoryTheory.IsPullback.lift_snd CategoryTheory.Limits.IsLimit.hom_ext CategoryTheory.Limits.IsLimit.fac_assoc CategoryTheory.IsConnected.is_nonempty Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Limits.IsLimit.fac CategoryTheory.isConnected_of_hasTerminal CategoryTheory.WithTerminal.instHasTerminal CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape.limitsOfShape_le CategoryTheory.Limits.IsTerminal.comp_from CategoryTheory.Category.comp_id CategoryTheory.Over.mkIdTerminal_from_left CategoryTheory.CreatesLimit.toReflectsLimit Equifibered.of_isIso CategoryTheory.IsIso.id

---

← Back to Index