Square

📁 Source: Mathlib/CategoryTheory/Limits/Preserves/Shapes/Square.lean

Statistics

Metric	Count
Definitions	0
Theorems iff_of_equiv, map, map_iff, of_equiv, of_map, map, map_iff, of_map, isPullback_iff_map_coyoneda_isPullback, isPushout_iff_op_map_yoneda_isPullback	10
Total	10

CategoryTheory.Square

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isPullback_iff_map_coyoneda_isPullback 📖	mathematical	—	IsPullback CategoryTheory.types map CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.coyoneda	—	IsPullback.map CategoryTheory.coyoneda_preservesLimit
isPushout_iff_op_map_yoneda_isPullback 📖	mathematical	—	IsPushout IsPullback CategoryTheory.types map Opposite CategoryTheory.Category.opposite op CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda	—	IsPullback.map IsPushout.op CategoryTheory.yoneda_preservesLimit CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp

CategoryTheory.Square.IsPullback

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iff_of_equiv 📖	mathematical	CategoryTheory.Square.X₁ CategoryTheory.types CategoryTheory.Square.X₂ DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Square.f₁₂ CategoryTheory.Square.X₃ CategoryTheory.Square.f₁₃ CategoryTheory.Square.X₄ CategoryTheory.Square.f₂₄ CategoryTheory.Square.f₃₄	CategoryTheory.Square.IsPullback	—	map_iff CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.Limits.Types.instPreservesLimitsOfSizeUliftFunctor CategoryTheory.Limits.reflectsLimit_of_reflectsLimitsOfShape CategoryTheory.Limits.reflectsLimitsOfShape_of_reflectsLimits CategoryTheory.Limits.fullyFaithful_reflectsLimits CategoryTheory.uliftFunctor_full CategoryTheory.uliftFunctor_faithful iff_of_iso CategoryTheory.types_ext ULift.down_injective
map 📖	mathematical	CategoryTheory.Square.IsPullback	CategoryTheory.Square.map	—	CategoryTheory.Square.fac
map_iff 📖	mathematical	—	CategoryTheory.Square.IsPullback CategoryTheory.Square.map	—	of_map map
of_equiv 📖	—	CategoryTheory.Square.X₁ CategoryTheory.types CategoryTheory.Square.X₂ DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Square.f₁₂ CategoryTheory.Square.X₃ CategoryTheory.Square.f₁₃ CategoryTheory.Square.X₄ CategoryTheory.Square.f₂₄ CategoryTheory.Square.f₃₄ CategoryTheory.Square.IsPullback	—	—	iff_of_equiv
of_map 📖	—	CategoryTheory.Square.IsPullback CategoryTheory.Square.map	—	—	CategoryTheory.IsPullback.of_map CategoryTheory.Square.fac

CategoryTheory.Square.IsPushout

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map 📖	mathematical	CategoryTheory.Square.IsPushout	CategoryTheory.Square.map	—	CategoryTheory.Square.fac
map_iff 📖	mathematical	—	CategoryTheory.Square.IsPushout CategoryTheory.Square.map	—	of_map map
of_map 📖	—	CategoryTheory.Square.IsPushout CategoryTheory.Square.map	—	—	CategoryTheory.IsPushout.of_map CategoryTheory.Square.fac

---

← Back to Index