Commit 2023-03-01 18:09 f826d24f

View on Github →

feat: port CategoryTheory.Limits.Shapes.WidePullbacks (#2453)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/Shapes/WidePullbacks.lean

added theorem CategoryTheory.Limits.WidePullback.eq_lift_of_comp_eq

added theorem CategoryTheory.Limits.WidePullback.hom_eq_lift

added theorem CategoryTheory.Limits.WidePullback.hom_ext

added theorem CategoryTheory.Limits.WidePullback.lift_base

added theorem CategoryTheory.Limits.WidePullback.lift_π

added theorem CategoryTheory.Limits.WidePullback.π_arrow

added inductive CategoryTheory.Limits.WidePullbackShape.Hom

added def CategoryTheory.Limits.WidePullbackShape.diagramIsoWideCospan

added def CategoryTheory.Limits.WidePullbackShape.equivalenceOfEquiv

added def CategoryTheory.Limits.WidePullbackShape.evalCasesBash

added theorem CategoryTheory.Limits.WidePullbackShape.hom_id

added def CategoryTheory.Limits.WidePullbackShape.mkCone

added def CategoryTheory.Limits.WidePullbackShape.uliftEquivalence

added def CategoryTheory.Limits.WidePullbackShape.wideCospan

added def CategoryTheory.Limits.WidePullbackShape

added theorem CategoryTheory.Limits.WidePushout.arrow_ι

added theorem CategoryTheory.Limits.WidePushout.eq_desc_of_comp_eq

added theorem CategoryTheory.Limits.WidePushout.head_desc

added theorem CategoryTheory.Limits.WidePushout.hom_eq_desc

added theorem CategoryTheory.Limits.WidePushout.hom_ext

added theorem CategoryTheory.Limits.WidePushout.ι_desc

added inductive CategoryTheory.Limits.WidePushoutShape.Hom

added def CategoryTheory.Limits.WidePushoutShape.diagramIsoWideSpan

added def CategoryTheory.Limits.WidePushoutShape.evalCasesBash'

added theorem CategoryTheory.Limits.WidePushoutShape.hom_id

added def CategoryTheory.Limits.WidePushoutShape.mkCocone

added def CategoryTheory.Limits.WidePushoutShape.wideSpan

added def CategoryTheory.Limits.WidePushoutShape

added theorem CategoryTheory.Limits.hasWidePullbacks_shrink

added def CategoryTheory.Limits.widePullbackShapeOp

added def CategoryTheory.Limits.widePullbackShapeOpEquiv

added def CategoryTheory.Limits.widePullbackShapeOpMap

added def CategoryTheory.Limits.widePullbackShapeOpUnop

added def CategoryTheory.Limits.widePullbackShapeUnop

added def CategoryTheory.Limits.widePullbackShapeUnopOp

added def CategoryTheory.Limits.widePushoutShapeOp

added def CategoryTheory.Limits.widePushoutShapeOpEquiv

added def CategoryTheory.Limits.widePushoutShapeOpMap

added def CategoryTheory.Limits.widePushoutShapeOpUnop

added def CategoryTheory.Limits.widePushoutShapeUnop

added def CategoryTheory.Limits.widePushoutShapeUnopOp