Opposites

📁 Source: Mathlib/CategoryTheory/Limits/Preserves/Opposites.lean

Statistics

Metric	Count
Definitions	0
Theorems preservesColimit_leftOp, preservesColimit_of_leftOp, preservesColimit_of_op, preservesColimit_of_rightOp, preservesColimit_of_unop, preservesColimit_op, preservesColimit_rightOp, preservesColimit_unop, preservesColimitsOfShape_leftOp, preservesColimitsOfShape_of_leftOp, preservesColimitsOfShape_of_op, preservesColimitsOfShape_of_rightOp, preservesColimitsOfShape_of_unop, preservesColimitsOfShape_op, preservesColimitsOfShape_rightOp, preservesColimitsOfShape_unop, preservesColimitsOfSize_leftOp, preservesColimitsOfSize_of_leftOp, preservesColimitsOfSize_of_op, preservesColimitsOfSize_of_rightOp, preservesColimitsOfSize_of_unop, preservesColimitsOfSize_op, preservesColimitsOfSize_rightOp, preservesColimitsOfSize_unop, preservesColimits_leftOp, preservesColimits_of_leftOp, preservesColimits_of_op, preservesColimits_of_rightOp, preservesColimits_of_unop, preservesColimits_op, preservesColimits_rightOp, preservesColimits_unop, preservesFiniteColimits_leftOp, preservesFiniteColimits_of_leftOp, preservesFiniteColimits_of_op, preservesFiniteColimits_of_rightOp, preservesFiniteColimits_of_unop, preservesFiniteColimits_op, preservesFiniteColimits_rightOp, preservesFiniteColimits_unop, preservesFiniteCoproducts_leftOp, preservesFiniteCoproducts_op, preservesFiniteCoproducts_rightOp, preservesFiniteCoproducts_unop, preservesFiniteLimits_leftOp, preservesFiniteLimits_of_leftOp, preservesFiniteLimits_of_op, preservesFiniteLimits_of_rightOp, preservesFiniteLimits_of_unop, preservesFiniteLimits_op, preservesFiniteLimits_rightOp, preservesFiniteLimits_unop, preservesFiniteProducts_leftOp, preservesFiniteProducts_op, preservesFiniteProducts_rightOp, preservesFiniteProducts_unop, preservesLimit_leftOp, preservesLimit_of_leftOp, preservesLimit_of_op, preservesLimit_of_rightOp, preservesLimit_of_unop, preservesLimit_op, preservesLimit_rightOp, preservesLimit_unop, preservesLimitsOfShape_leftOp, preservesLimitsOfShape_of_leftOp, preservesLimitsOfShape_of_op, preservesLimitsOfShape_of_rightOp, preservesLimitsOfShape_of_unop, preservesLimitsOfShape_op, preservesLimitsOfShape_rightOp, preservesLimitsOfShape_unop, preservesLimitsOfSize_leftOp, preservesLimitsOfSize_of_leftOp, preservesLimitsOfSize_of_op, preservesLimitsOfSize_of_rightOp, preservesLimitsOfSize_of_unop, preservesLimitsOfSize_op, preservesLimitsOfSize_rightOp, preservesLimitsOfSize_unop, preservesLimits_leftOp, preservesLimits_of_leftOp, preservesLimits_of_op, preservesLimits_of_rightOp, preservesLimits_of_unop, preservesLimits_op, preservesLimits_rightOp, preservesLimits_unop	88
Total	88

CategoryTheory.Limits

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preservesColimit_leftOp 📖	mathematical	—	PreservesColimit Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp	—	—
preservesColimit_of_leftOp 📖	mathematical	—	PreservesColimit Opposite CategoryTheory.Category.opposite	—	—
preservesColimit_of_op 📖	mathematical	—	PreservesColimit	—	—
preservesColimit_of_rightOp 📖	mathematical	—	PreservesColimit Opposite CategoryTheory.Category.opposite	—	—
preservesColimit_of_unop 📖	mathematical	—	PreservesColimit Opposite CategoryTheory.Category.opposite	—	—
preservesColimit_op 📖	mathematical	—	PreservesColimit Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	—	—
preservesColimit_rightOp 📖	mathematical	—	PreservesColimit Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp	—	—
preservesColimit_unop 📖	mathematical	—	PreservesColimit CategoryTheory.Functor.unop	—	—
preservesColimitsOfShape_leftOp 📖	mathematical	—	PreservesColimitsOfShape Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp	—	preservesColimit_leftOp PreservesLimitsOfShape.preservesLimit
preservesColimitsOfShape_of_leftOp 📖	mathematical	—	PreservesColimitsOfShape Opposite CategoryTheory.Category.opposite	—	preservesColimit_of_leftOp PreservesLimitsOfShape.preservesLimit
preservesColimitsOfShape_of_op 📖	mathematical	—	PreservesColimitsOfShape	—	preservesColimit_of_op PreservesLimitsOfShape.preservesLimit
preservesColimitsOfShape_of_rightOp 📖	mathematical	—	PreservesColimitsOfShape Opposite CategoryTheory.Category.opposite	—	preservesColimit_of_rightOp PreservesLimitsOfShape.preservesLimit
preservesColimitsOfShape_of_unop 📖	mathematical	—	PreservesColimitsOfShape Opposite CategoryTheory.Category.opposite	—	preservesColimit_of_unop PreservesLimitsOfShape.preservesLimit
preservesColimitsOfShape_op 📖	mathematical	—	PreservesColimitsOfShape Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	—	preservesColimit_op PreservesLimitsOfShape.preservesLimit
preservesColimitsOfShape_rightOp 📖	mathematical	—	PreservesColimitsOfShape Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp	—	preservesColimit_rightOp PreservesLimitsOfShape.preservesLimit
preservesColimitsOfShape_unop 📖	mathematical	—	PreservesColimitsOfShape CategoryTheory.Functor.unop	—	preservesColimit_unop PreservesLimitsOfShape.preservesLimit
preservesColimitsOfSize_leftOp 📖	mathematical	—	PreservesColimitsOfSize Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp	—	preservesColimitsOfShape_leftOp PreservesLimitsOfSize.preservesLimitsOfShape
preservesColimitsOfSize_of_leftOp 📖	mathematical	—	PreservesColimitsOfSize Opposite CategoryTheory.Category.opposite	—	preservesColimitsOfShape_of_leftOp PreservesLimitsOfSize.preservesLimitsOfShape
preservesColimitsOfSize_of_op 📖	mathematical	—	PreservesColimitsOfSize	—	preservesColimitsOfShape_of_op PreservesLimitsOfSize.preservesLimitsOfShape
preservesColimitsOfSize_of_rightOp 📖	mathematical	—	PreservesColimitsOfSize Opposite CategoryTheory.Category.opposite	—	preservesColimitsOfShape_of_rightOp PreservesLimitsOfSize.preservesLimitsOfShape
preservesColimitsOfSize_of_unop 📖	mathematical	—	PreservesColimitsOfSize Opposite CategoryTheory.Category.opposite	—	preservesColimitsOfShape_of_unop PreservesLimitsOfSize.preservesLimitsOfShape
preservesColimitsOfSize_op 📖	mathematical	—	PreservesColimitsOfSize Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	—	preservesColimitsOfShape_op PreservesLimitsOfSize.preservesLimitsOfShape
preservesColimitsOfSize_rightOp 📖	mathematical	—	PreservesColimitsOfSize Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp	—	preservesColimitsOfShape_rightOp PreservesLimitsOfSize.preservesLimitsOfShape
preservesColimitsOfSize_unop 📖	mathematical	—	PreservesColimitsOfSize CategoryTheory.Functor.unop	—	preservesColimitsOfShape_unop PreservesLimitsOfSize.preservesLimitsOfShape
preservesColimits_leftOp 📖	mathematical	—	PreservesColimits Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp	—	preservesColimitsOfShape_leftOp PreservesLimitsOfSize.preservesLimitsOfShape
preservesColimits_of_leftOp 📖	mathematical	—	PreservesColimits Opposite CategoryTheory.Category.opposite	—	preservesColimitsOfShape_of_leftOp PreservesLimitsOfSize.preservesLimitsOfShape
preservesColimits_of_op 📖	mathematical	—	PreservesColimits	—	preservesColimitsOfShape_of_op PreservesLimitsOfSize.preservesLimitsOfShape
preservesColimits_of_rightOp 📖	mathematical	—	PreservesColimits Opposite CategoryTheory.Category.opposite	—	preservesColimitsOfShape_of_rightOp PreservesLimitsOfSize.preservesLimitsOfShape
preservesColimits_of_unop 📖	mathematical	—	PreservesColimits Opposite CategoryTheory.Category.opposite	—	preservesColimitsOfShape_of_unop PreservesLimitsOfSize.preservesLimitsOfShape
preservesColimits_op 📖	mathematical	—	PreservesColimits Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	—	preservesColimitsOfShape_op PreservesLimitsOfSize.preservesLimitsOfShape
preservesColimits_rightOp 📖	mathematical	—	PreservesColimits Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp	—	preservesColimitsOfShape_rightOp PreservesLimitsOfSize.preservesLimitsOfShape
preservesColimits_unop 📖	mathematical	—	PreservesColimits CategoryTheory.Functor.unop	—	preservesColimitsOfShape_unop PreservesLimitsOfSize.preservesLimitsOfShape
preservesFiniteColimits_leftOp 📖	mathematical	—	PreservesFiniteColimits Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp	—	preservesColimitsOfShape_leftOp PreservesFiniteLimits.preservesFiniteLimits
preservesFiniteColimits_of_leftOp 📖	mathematical	—	PreservesFiniteColimits Opposite CategoryTheory.Category.opposite	—	preservesColimitsOfShape_of_leftOp PreservesFiniteLimits.preservesFiniteLimits
preservesFiniteColimits_of_op 📖	mathematical	—	PreservesFiniteColimits	—	preservesColimitsOfShape_of_op PreservesFiniteLimits.preservesFiniteLimits
preservesFiniteColimits_of_rightOp 📖	mathematical	—	PreservesFiniteColimits Opposite CategoryTheory.Category.opposite	—	preservesColimitsOfShape_of_rightOp PreservesFiniteLimits.preservesFiniteLimits
preservesFiniteColimits_of_unop 📖	mathematical	—	PreservesFiniteColimits Opposite CategoryTheory.Category.opposite	—	preservesColimitsOfShape_of_unop PreservesFiniteLimits.preservesFiniteLimits
preservesFiniteColimits_op 📖	mathematical	—	PreservesFiniteColimits Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	—	preservesColimitsOfShape_op PreservesFiniteLimits.preservesFiniteLimits
preservesFiniteColimits_rightOp 📖	mathematical	—	PreservesFiniteColimits Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp	—	preservesColimitsOfShape_rightOp PreservesFiniteLimits.preservesFiniteLimits
preservesFiniteColimits_unop 📖	mathematical	—	PreservesFiniteColimits CategoryTheory.Functor.unop	—	preservesColimitsOfShape_unop PreservesFiniteLimits.preservesFiniteLimits
preservesFiniteCoproducts_leftOp 📖	mathematical	—	PreservesFiniteCoproducts Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp	—	preservesColimitsOfShape_leftOp preservesLimitsOfShape_of_equiv instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts Finite.of_fintype
preservesFiniteCoproducts_op 📖	mathematical	—	PreservesFiniteCoproducts Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	—	preservesColimitsOfShape_op preservesLimitsOfShape_of_equiv instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts Finite.of_fintype
preservesFiniteCoproducts_rightOp 📖	mathematical	—	PreservesFiniteCoproducts Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp	—	preservesColimitsOfShape_rightOp preservesLimitsOfShape_of_equiv instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts Finite.of_fintype
preservesFiniteCoproducts_unop 📖	mathematical	—	PreservesFiniteCoproducts CategoryTheory.Functor.unop	—	preservesColimitsOfShape_unop preservesLimitsOfShape_of_equiv instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts Finite.of_fintype
preservesFiniteLimits_leftOp 📖	mathematical	—	PreservesFiniteLimits Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp	—	preservesLimitsOfShape_leftOp PreservesFiniteColimits.preservesFiniteColimits
preservesFiniteLimits_of_leftOp 📖	mathematical	—	PreservesFiniteLimits Opposite CategoryTheory.Category.opposite	—	preservesLimitsOfShape_of_leftOp PreservesFiniteColimits.preservesFiniteColimits
preservesFiniteLimits_of_op 📖	mathematical	—	PreservesFiniteLimits	—	preservesLimitsOfShape_of_op PreservesFiniteColimits.preservesFiniteColimits
preservesFiniteLimits_of_rightOp 📖	mathematical	—	PreservesFiniteLimits Opposite CategoryTheory.Category.opposite	—	preservesLimitsOfShape_of_rightOp PreservesFiniteColimits.preservesFiniteColimits
preservesFiniteLimits_of_unop 📖	mathematical	—	PreservesFiniteLimits Opposite CategoryTheory.Category.opposite	—	preservesLimitsOfShape_of_unop PreservesFiniteColimits.preservesFiniteColimits
preservesFiniteLimits_op 📖	mathematical	—	PreservesFiniteLimits Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	—	preservesLimitsOfShape_op PreservesFiniteColimits.preservesFiniteColimits
preservesFiniteLimits_rightOp 📖	mathematical	—	PreservesFiniteLimits Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp	—	preservesLimitsOfShape_rightOp PreservesFiniteColimits.preservesFiniteColimits
preservesFiniteLimits_unop 📖	mathematical	—	PreservesFiniteLimits CategoryTheory.Functor.unop	—	preservesLimitsOfShape_unop PreservesFiniteColimits.preservesFiniteColimits
preservesFiniteProducts_leftOp 📖	mathematical	—	PreservesFiniteProducts Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp	—	preservesLimitsOfShape_leftOp preservesColimitsOfShape_of_equiv instPreservesColimitsOfShapeDiscreteOfFiniteOfPreservesFiniteCoproducts Finite.of_fintype
preservesFiniteProducts_op 📖	mathematical	—	PreservesFiniteProducts Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	—	preservesLimitsOfShape_op preservesColimitsOfShape_of_equiv instPreservesColimitsOfShapeDiscreteOfFiniteOfPreservesFiniteCoproducts Finite.of_fintype
preservesFiniteProducts_rightOp 📖	mathematical	—	PreservesFiniteProducts Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp	—	preservesLimitsOfShape_rightOp preservesColimitsOfShape_of_equiv instPreservesColimitsOfShapeDiscreteOfFiniteOfPreservesFiniteCoproducts Finite.of_fintype
preservesFiniteProducts_unop 📖	mathematical	—	PreservesFiniteProducts CategoryTheory.Functor.unop	—	preservesLimitsOfShape_unop preservesColimitsOfShape_of_equiv instPreservesColimitsOfShapeDiscreteOfFiniteOfPreservesFiniteCoproducts Finite.of_fintype
preservesLimit_leftOp 📖	mathematical	—	PreservesLimit Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp	—	—
preservesLimit_of_leftOp 📖	mathematical	—	PreservesLimit Opposite CategoryTheory.Category.opposite	—	—
preservesLimit_of_op 📖	mathematical	—	PreservesLimit	—	—
preservesLimit_of_rightOp 📖	mathematical	—	PreservesLimit Opposite CategoryTheory.Category.opposite	—	—
preservesLimit_of_unop 📖	mathematical	—	PreservesLimit Opposite CategoryTheory.Category.opposite	—	—
preservesLimit_op 📖	mathematical	—	PreservesLimit Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	—	—
preservesLimit_rightOp 📖	mathematical	—	PreservesLimit Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp	—	—
preservesLimit_unop 📖	mathematical	—	PreservesLimit CategoryTheory.Functor.unop	—	—
preservesLimitsOfShape_leftOp 📖	mathematical	—	PreservesLimitsOfShape Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp	—	preservesLimit_leftOp PreservesColimitsOfShape.preservesColimit
preservesLimitsOfShape_of_leftOp 📖	mathematical	—	PreservesLimitsOfShape Opposite CategoryTheory.Category.opposite	—	preservesLimit_of_leftOp PreservesColimitsOfShape.preservesColimit
preservesLimitsOfShape_of_op 📖	mathematical	—	PreservesLimitsOfShape	—	preservesLimit_of_op PreservesColimitsOfShape.preservesColimit
preservesLimitsOfShape_of_rightOp 📖	mathematical	—	PreservesLimitsOfShape Opposite CategoryTheory.Category.opposite	—	preservesLimit_of_rightOp PreservesColimitsOfShape.preservesColimit
preservesLimitsOfShape_of_unop 📖	mathematical	—	PreservesLimitsOfShape Opposite CategoryTheory.Category.opposite	—	preservesLimit_of_unop PreservesColimitsOfShape.preservesColimit
preservesLimitsOfShape_op 📖	mathematical	—	PreservesLimitsOfShape Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	—	preservesLimit_op PreservesColimitsOfShape.preservesColimit
preservesLimitsOfShape_rightOp 📖	mathematical	—	PreservesLimitsOfShape Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp	—	preservesLimit_rightOp PreservesColimitsOfShape.preservesColimit
preservesLimitsOfShape_unop 📖	mathematical	—	PreservesLimitsOfShape CategoryTheory.Functor.unop	—	preservesLimit_unop PreservesColimitsOfShape.preservesColimit
preservesLimitsOfSize_leftOp 📖	mathematical	—	PreservesLimitsOfSize Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp	—	preservesLimitsOfShape_leftOp PreservesColimitsOfSize.preservesColimitsOfShape
preservesLimitsOfSize_of_leftOp 📖	mathematical	—	PreservesLimitsOfSize Opposite CategoryTheory.Category.opposite	—	preservesLimitsOfShape_of_leftOp PreservesColimitsOfSize.preservesColimitsOfShape
preservesLimitsOfSize_of_op 📖	mathematical	—	PreservesLimitsOfSize	—	preservesLimitsOfShape_of_op PreservesColimitsOfSize.preservesColimitsOfShape
preservesLimitsOfSize_of_rightOp 📖	mathematical	—	PreservesLimitsOfSize Opposite CategoryTheory.Category.opposite	—	preservesLimitsOfShape_of_rightOp PreservesColimitsOfSize.preservesColimitsOfShape
preservesLimitsOfSize_of_unop 📖	mathematical	—	PreservesLimitsOfSize Opposite CategoryTheory.Category.opposite	—	preservesLimitsOfShape_of_unop PreservesColimitsOfSize.preservesColimitsOfShape
preservesLimitsOfSize_op 📖	mathematical	—	PreservesLimitsOfSize Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	—	preservesLimitsOfShape_op PreservesColimitsOfSize.preservesColimitsOfShape
preservesLimitsOfSize_rightOp 📖	mathematical	—	PreservesLimitsOfSize Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp	—	preservesLimitsOfShape_rightOp PreservesColimitsOfSize.preservesColimitsOfShape
preservesLimitsOfSize_unop 📖	mathematical	—	PreservesLimitsOfSize CategoryTheory.Functor.unop	—	preservesLimitsOfShape_unop PreservesColimitsOfSize.preservesColimitsOfShape
preservesLimits_leftOp 📖	mathematical	—	PreservesLimits Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp	—	preservesLimitsOfShape_leftOp PreservesColimitsOfSize.preservesColimitsOfShape
preservesLimits_of_leftOp 📖	mathematical	—	PreservesLimits Opposite CategoryTheory.Category.opposite	—	preservesLimitsOfShape_of_leftOp PreservesColimitsOfSize.preservesColimitsOfShape
preservesLimits_of_op 📖	mathematical	—	PreservesLimits	—	preservesLimitsOfShape_of_op PreservesColimitsOfSize.preservesColimitsOfShape
preservesLimits_of_rightOp 📖	mathematical	—	PreservesLimits Opposite CategoryTheory.Category.opposite	—	preservesLimitsOfShape_of_rightOp PreservesColimitsOfSize.preservesColimitsOfShape
preservesLimits_of_unop 📖	mathematical	—	PreservesLimits Opposite CategoryTheory.Category.opposite	—	preservesLimitsOfShape_of_unop PreservesColimitsOfSize.preservesColimitsOfShape
preservesLimits_op 📖	mathematical	—	PreservesLimits Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	—	preservesLimitsOfShape_op PreservesColimitsOfSize.preservesColimitsOfShape
preservesLimits_rightOp 📖	mathematical	—	PreservesLimits Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp	—	preservesLimitsOfShape_rightOp PreservesColimitsOfSize.preservesColimitsOfShape
preservesLimits_unop 📖	mathematical	—	PreservesLimits CategoryTheory.Functor.unop	—	preservesLimitsOfShape_unop PreservesColimitsOfSize.preservesColimitsOfShape

---

← Back to Index