Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-10 19:29 ad080011

View on Github →

feat(category_theory/limits): opposites of limit pullback cones (#14526) Among other similar statements, this PR associates a pullback_cone f g to a pushout_cocone f.op g.op, and it is a limit pullback cone if the original cocone is a colimit cocone.

Estimated changes

Modified src/category_theory/limits/opposites.lean

added def category_theory.limits.cospan_op

added def category_theory.limits.op_cospan

added def category_theory.limits.op_span

added def category_theory.limits.pullback_cone.is_limit_equiv_is_colimit_op

added def category_theory.limits.pullback_cone.is_limit_equiv_is_colimit_unop

added def category_theory.limits.pullback_cone.op

added theorem category_theory.limits.pullback_cone.op_inl

added theorem category_theory.limits.pullback_cone.op_inr

added def category_theory.limits.pullback_cone.op_unop

added def category_theory.limits.pullback_cone.unop

added theorem category_theory.limits.pullback_cone.unop_inl

added theorem category_theory.limits.pullback_cone.unop_inr

added def category_theory.limits.pullback_cone.unop_op

added def category_theory.limits.pushout_cocone.is_colimit_equiv_is_limit_op

added def category_theory.limits.pushout_cocone.is_colimit_equiv_is_limit_unop

added def category_theory.limits.pushout_cocone.op

added theorem category_theory.limits.pushout_cocone.op_fst

added theorem category_theory.limits.pushout_cocone.op_snd

added def category_theory.limits.pushout_cocone.op_unop

added def category_theory.limits.pushout_cocone.unop

added theorem category_theory.limits.pushout_cocone.unop_fst

added def category_theory.limits.pushout_cocone.unop_op

added theorem category_theory.limits.pushout_cocone.unop_snd

added def category_theory.limits.span_op

Modified src/category_theory/limits/shapes/pullbacks.lean