Commit 2023-03-07 06:55 d9ec9907

View on Github →

feat: port CategoryTheory.Limits.Shapes.Pullbacks (#2522)

Estimated changes

Modified Mathlib.lean

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

added def CategoryTheory.Limits.Cocone.ofPushoutCocone

added def CategoryTheory.Limits.Cone.ofPullbackCone

added theorem CategoryTheory.Limits.PullbackCone.IsLimit.hom_ext

added def CategoryTheory.Limits.PullbackCone.IsLimit.lift'

added def CategoryTheory.Limits.PullbackCone.IsLimit.mk

added theorem CategoryTheory.Limits.PullbackCone.condition

added theorem CategoryTheory.Limits.PullbackCone.condition_one

added theorem CategoryTheory.Limits.PullbackCone.equalizer_ext

added def CategoryTheory.Limits.PullbackCone.ext

added def CategoryTheory.Limits.PullbackCone.flipIsLimit

added theorem CategoryTheory.Limits.PullbackCone.fst_colimit_cocone

added def CategoryTheory.Limits.PullbackCone.isLimitAux'

added def CategoryTheory.Limits.PullbackCone.isLimitAux

added def CategoryTheory.Limits.PullbackCone.isLimitMkIdId

added def CategoryTheory.Limits.PullbackCone.isLimitOfCompMono

added def CategoryTheory.Limits.PullbackCone.isLimitOfFactors

added def CategoryTheory.Limits.PullbackCone.isoMk

added def CategoryTheory.Limits.PullbackCone.mk

added theorem CategoryTheory.Limits.PullbackCone.mk_fst

added theorem CategoryTheory.Limits.PullbackCone.mk_snd

added theorem CategoryTheory.Limits.PullbackCone.mk_π_app_left

added theorem CategoryTheory.Limits.PullbackCone.mk_π_app_one

added theorem CategoryTheory.Limits.PullbackCone.mk_π_app_right

added theorem CategoryTheory.Limits.PullbackCone.mono_fst_of_is_pullback_of_mono

added theorem CategoryTheory.Limits.PullbackCone.mono_of_isLimitMkIdId

added theorem CategoryTheory.Limits.PullbackCone.mono_snd_of_is_pullback_of_mono

added def CategoryTheory.Limits.PullbackCone.ofCone

added theorem CategoryTheory.Limits.PullbackCone.snd_colimit_cocone

added theorem CategoryTheory.Limits.PullbackCone.π_app_left

added theorem CategoryTheory.Limits.PullbackCone.π_app_right

added def CategoryTheory.Limits.PushoutCocone.IsColimit.desc'

added theorem CategoryTheory.Limits.PushoutCocone.IsColimit.hom_ext

added def CategoryTheory.Limits.PushoutCocone.IsColimit.mk

added theorem CategoryTheory.Limits.PushoutCocone.coequalizer_ext

added theorem CategoryTheory.Limits.PushoutCocone.condition

added theorem CategoryTheory.Limits.PushoutCocone.condition_zero

added theorem CategoryTheory.Limits.PushoutCocone.epi_inl_of_is_pushout_of_epi

added theorem CategoryTheory.Limits.PushoutCocone.epi_inr_of_is_pushout_of_epi

added theorem CategoryTheory.Limits.PushoutCocone.epi_of_isColimitMkIdId

added def CategoryTheory.Limits.PushoutCocone.ext

added def CategoryTheory.Limits.PushoutCocone.flipIsColimit

added theorem CategoryTheory.Limits.PushoutCocone.inl_colimit_cocone

added theorem CategoryTheory.Limits.PushoutCocone.inr_colimit_cocone

added def CategoryTheory.Limits.PushoutCocone.isColimitAux'

added def CategoryTheory.Limits.PushoutCocone.isColimitAux

added def CategoryTheory.Limits.PushoutCocone.isColimitMkIdId

added def CategoryTheory.Limits.PushoutCocone.isColimitOfEpiComp

added def CategoryTheory.Limits.PushoutCocone.isColimitOfFactors

added def CategoryTheory.Limits.PushoutCocone.isoMk

added def CategoryTheory.Limits.PushoutCocone.mk

added theorem CategoryTheory.Limits.PushoutCocone.mk_inl

added theorem CategoryTheory.Limits.PushoutCocone.mk_inr

added theorem CategoryTheory.Limits.PushoutCocone.mk_ι_app_left

added theorem CategoryTheory.Limits.PushoutCocone.mk_ι_app_right

added theorem CategoryTheory.Limits.PushoutCocone.mk_ι_app_zero

added def CategoryTheory.Limits.PushoutCocone.ofCocone

added theorem CategoryTheory.Limits.PushoutCocone.ι_app_left

added theorem CategoryTheory.Limits.PushoutCocone.ι_app_right

added def CategoryTheory.Limits.WalkingCospan.ext

added def CategoryTheory.Limits.WalkingSpan.ext

added def CategoryTheory.Limits.baseChange

added def CategoryTheory.Limits.bigSquareIsPullback

added def CategoryTheory.Limits.bigSquareIsPushout

added def CategoryTheory.Limits.cospan

added def CategoryTheory.Limits.cospanCompIso

added theorem CategoryTheory.Limits.cospanCompIso_app_left

added theorem CategoryTheory.Limits.cospanCompIso_app_one

added theorem CategoryTheory.Limits.cospanCompIso_app_right

added theorem CategoryTheory.Limits.cospanCompIso_hom_app_left

added theorem CategoryTheory.Limits.cospanCompIso_hom_app_one

added theorem CategoryTheory.Limits.cospanCompIso_hom_app_right

added theorem CategoryTheory.Limits.cospanCompIso_inv_app_left

added theorem CategoryTheory.Limits.cospanCompIso_inv_app_one

added theorem CategoryTheory.Limits.cospanCompIso_inv_app_right

added def CategoryTheory.Limits.cospanExt

added theorem CategoryTheory.Limits.cospanExt_app_left

added theorem CategoryTheory.Limits.cospanExt_app_one

added theorem CategoryTheory.Limits.cospanExt_app_right

added theorem CategoryTheory.Limits.cospanExt_hom_app_left

added theorem CategoryTheory.Limits.cospanExt_hom_app_one

added theorem CategoryTheory.Limits.cospanExt_hom_app_right

added theorem CategoryTheory.Limits.cospanExt_inv_app_left

added theorem CategoryTheory.Limits.cospanExt_inv_app_one

added theorem CategoryTheory.Limits.cospanExt_inv_app_right

added theorem CategoryTheory.Limits.cospan_left

added theorem CategoryTheory.Limits.cospan_map_id

added theorem CategoryTheory.Limits.cospan_map_inl

added theorem CategoryTheory.Limits.cospan_map_inr

added theorem CategoryTheory.Limits.cospan_one

added theorem CategoryTheory.Limits.cospan_right

added def CategoryTheory.Limits.diagramIsoCospan

added def CategoryTheory.Limits.diagramIsoSpan

added theorem CategoryTheory.Limits.fst_eq_snd_of_mono_eq

added theorem CategoryTheory.Limits.hasPullback_assoc

added theorem CategoryTheory.Limits.hasPullback_assoc_symm

added theorem CategoryTheory.Limits.hasPullback_of_left_iso

added theorem CategoryTheory.Limits.hasPullback_of_right_iso

added theorem CategoryTheory.Limits.hasPullback_symmetry

added theorem CategoryTheory.Limits.hasPullbacks_of_hasLimit_cospan

added theorem CategoryTheory.Limits.hasPushout_assoc

added theorem CategoryTheory.Limits.hasPushout_assoc_symm

added theorem CategoryTheory.Limits.hasPushout_of_left_iso

added theorem CategoryTheory.Limits.hasPushout_of_right_iso

added theorem CategoryTheory.Limits.hasPushout_symmetry

added theorem CategoryTheory.Limits.hasPushouts_of_hasColimit_span

added theorem CategoryTheory.Limits.inl_comp_pushoutComparison

added theorem CategoryTheory.Limits.inl_comp_pushoutSymmetry_hom

added theorem CategoryTheory.Limits.inl_comp_pushoutSymmetry_inv

added theorem CategoryTheory.Limits.inl_eq_inr_of_epi_eq

added theorem CategoryTheory.Limits.inl_inl_pushoutAssoc_hom

added theorem CategoryTheory.Limits.inl_inl_pushoutLeftPushoutInrIso_hom

added theorem CategoryTheory.Limits.inl_inr_pushoutAssoc_inv

added theorem CategoryTheory.Limits.inl_pushoutAssoc_inv

added theorem CategoryTheory.Limits.inl_pushoutLeftPushoutInrIso_inv

added theorem CategoryTheory.Limits.inr_comp_pushoutComparison

added theorem CategoryTheory.Limits.inr_comp_pushoutSymmetry_hom

added theorem CategoryTheory.Limits.inr_comp_pushoutSymmetry_inv

added theorem CategoryTheory.Limits.inr_inl_pushoutAssoc_hom

added theorem CategoryTheory.Limits.inr_inl_pushoutLeftPushoutInrIso_hom

added theorem CategoryTheory.Limits.inr_inr_pushoutAssoc_inv

added theorem CategoryTheory.Limits.inr_pushoutAssoc_hom

added theorem CategoryTheory.Limits.inr_pushoutLeftPushoutInrIso_hom

added theorem CategoryTheory.Limits.inr_pushoutLeftPushoutInrIso_inv

added def CategoryTheory.Limits.leftSquareIsPullback

added theorem CategoryTheory.Limits.map_lift_pullbackComparison

added theorem CategoryTheory.Limits.pullback.condition

added def CategoryTheory.Limits.pullback.congrHom

added theorem CategoryTheory.Limits.pullback.congrHom_inv

added def CategoryTheory.Limits.pullback.desc'

added theorem CategoryTheory.Limits.pullback.hom_ext

added def CategoryTheory.Limits.pullback.lift'

added theorem CategoryTheory.Limits.pullback.lift_fst

added theorem CategoryTheory.Limits.pullback.lift_snd

added theorem CategoryTheory.Limits.pullback.mapDesc_comp

added def CategoryTheory.Limits.pullbackAssocIsPullback

added def CategoryTheory.Limits.pullbackAssocSymmIsPullback

added theorem CategoryTheory.Limits.pullbackAssoc_hom_fst

added theorem CategoryTheory.Limits.pullbackAssoc_hom_snd_fst

added theorem CategoryTheory.Limits.pullbackAssoc_hom_snd_snd

added theorem CategoryTheory.Limits.pullbackAssoc_inv_fst_fst

added theorem CategoryTheory.Limits.pullbackAssoc_inv_fst_snd

added theorem CategoryTheory.Limits.pullbackAssoc_inv_snd

added def CategoryTheory.Limits.pullbackComparison

added theorem CategoryTheory.Limits.pullbackComparison_comp_fst

added theorem CategoryTheory.Limits.pullbackComparison_comp_snd

added def CategoryTheory.Limits.pullbackConeOfLeftIso

added def CategoryTheory.Limits.pullbackConeOfLeftIsoIsLimit

added theorem CategoryTheory.Limits.pullbackConeOfLeftIso_fst

added theorem CategoryTheory.Limits.pullbackConeOfLeftIso_snd

added theorem CategoryTheory.Limits.pullbackConeOfLeftIso_x

added theorem CategoryTheory.Limits.pullbackConeOfLeftIso_π_app_left

added theorem CategoryTheory.Limits.pullbackConeOfLeftIso_π_app_none

added theorem CategoryTheory.Limits.pullbackConeOfLeftIso_π_app_right

added def CategoryTheory.Limits.pullbackConeOfRightIso

added def CategoryTheory.Limits.pullbackConeOfRightIsoIsLimit

added theorem CategoryTheory.Limits.pullbackConeOfRightIso_fst

added theorem CategoryTheory.Limits.pullbackConeOfRightIso_snd

added theorem CategoryTheory.Limits.pullbackConeOfRightIso_x

added theorem CategoryTheory.Limits.pullbackConeOfRightIso_π_app_left

added theorem CategoryTheory.Limits.pullbackConeOfRightIso_π_app_none

added theorem CategoryTheory.Limits.pullbackConeOfRightIso_π_app_right

added def CategoryTheory.Limits.pullbackIsPullback

added def CategoryTheory.Limits.pullbackPullbackLeftIsPullback

added def CategoryTheory.Limits.pullbackPullbackRightIsPullback

added theorem CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_fst

added theorem CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_snd

added theorem CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_fst

added theorem CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_fst

added theorem CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_snd

added def CategoryTheory.Limits.pullbackSymmetry

added theorem CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst

added theorem CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd

added theorem CategoryTheory.Limits.pullbackSymmetry_hom_of_mono_eq

added theorem CategoryTheory.Limits.pullbackSymmetry_inv_comp_fst

added theorem CategoryTheory.Limits.pullbackSymmetry_inv_comp_snd

added theorem CategoryTheory.Limits.pullback_symmetry_hom_of_epi_eq

added theorem CategoryTheory.Limits.pushout.condition

added def CategoryTheory.Limits.pushout.congrHom

added theorem CategoryTheory.Limits.pushout.congrHom_inv

added theorem CategoryTheory.Limits.pushout.hom_ext

added theorem CategoryTheory.Limits.pushout.inl_desc

added theorem CategoryTheory.Limits.pushout.inr_desc

added theorem CategoryTheory.Limits.pushout.mapLift_comp

added def CategoryTheory.Limits.pushoutAssocIsPushout

added def CategoryTheory.Limits.pushoutAssocSymmIsPushout

added def CategoryTheory.Limits.pushoutCoconeOfLeftIso

added def CategoryTheory.Limits.pushoutCoconeOfLeftIsoIsLimit

added theorem CategoryTheory.Limits.pushoutCoconeOfLeftIso_inl

added theorem CategoryTheory.Limits.pushoutCoconeOfLeftIso_inr

added theorem CategoryTheory.Limits.pushoutCoconeOfLeftIso_x

added theorem CategoryTheory.Limits.pushoutCoconeOfLeftIso_ι_app_left

added theorem CategoryTheory.Limits.pushoutCoconeOfLeftIso_ι_app_none

added theorem CategoryTheory.Limits.pushoutCoconeOfLeftIso_ι_app_right

added def CategoryTheory.Limits.pushoutCoconeOfRightIso

added def CategoryTheory.Limits.pushoutCoconeOfRightIsoIsLimit

added theorem CategoryTheory.Limits.pushoutCoconeOfRightIso_inl

added theorem CategoryTheory.Limits.pushoutCoconeOfRightIso_inr

added theorem CategoryTheory.Limits.pushoutCoconeOfRightIso_x

added theorem CategoryTheory.Limits.pushoutCoconeOfRightIso_ι_app_left

added theorem CategoryTheory.Limits.pushoutCoconeOfRightIso_ι_app_none

added theorem CategoryTheory.Limits.pushoutCoconeOfRightIso_ι_app_right

added def CategoryTheory.Limits.pushoutComparison

added theorem CategoryTheory.Limits.pushoutComparison_map_desc

added def CategoryTheory.Limits.pushoutIsPushout

added def CategoryTheory.Limits.pushoutPushoutLeftIsPushout

added def CategoryTheory.Limits.pushoutPushoutRightIsPushout

added def CategoryTheory.Limits.pushoutSymmetry

added def CategoryTheory.Limits.rightSquareIsPushout

added def CategoryTheory.Limits.span

added def CategoryTheory.Limits.spanCompIso

added theorem CategoryTheory.Limits.spanCompIso_app_left

added theorem CategoryTheory.Limits.spanCompIso_app_right

added theorem CategoryTheory.Limits.spanCompIso_app_zero

added theorem CategoryTheory.Limits.spanCompIso_hom_app_left

added theorem CategoryTheory.Limits.spanCompIso_hom_app_right

added theorem CategoryTheory.Limits.spanCompIso_hom_app_zero

added theorem CategoryTheory.Limits.spanCompIso_inv_app_left

added theorem CategoryTheory.Limits.spanCompIso_inv_app_right

added theorem CategoryTheory.Limits.spanCompIso_inv_app_zero

added def CategoryTheory.Limits.spanExt

added theorem CategoryTheory.Limits.spanExt_app_left

added theorem CategoryTheory.Limits.spanExt_app_one

added theorem CategoryTheory.Limits.spanExt_app_right

added theorem CategoryTheory.Limits.spanExt_hom_app_left

added theorem CategoryTheory.Limits.spanExt_hom_app_right

added theorem CategoryTheory.Limits.spanExt_hom_app_zero

added theorem CategoryTheory.Limits.spanExt_inv_app_left

added theorem CategoryTheory.Limits.spanExt_inv_app_right

added theorem CategoryTheory.Limits.spanExt_inv_app_zero

added theorem CategoryTheory.Limits.span_left

added theorem CategoryTheory.Limits.span_map_fst

added theorem CategoryTheory.Limits.span_map_id

added theorem CategoryTheory.Limits.span_map_snd

added theorem CategoryTheory.Limits.span_right

added theorem CategoryTheory.Limits.span_zero

added def CategoryTheory.Limits.walkingCospanOpEquiv

added def CategoryTheory.Limits.walkingSpanOpEquiv