Documentation Verification Report

VanKampen

📁 Source: Mathlib/CategoryTheory/Limits/VanKampen.lean

Statistics

Metric	Count
Definitions `IsUniversalColimit`, `isColimit`, `IsVanKampenColimit`, `isColimit`	4
Theorems `isPullback_initial_to_of_isVanKampen`, `isVanKampen_iff`, `isVanKampen_mk`, `mono_inr_of_isVanKampen`, `isVanKampenColimit`, `isPullback_of_isColimit_left`, `isPullback_of_isColimit_right`, `isPullback_prod_of_isColimit`, `map_reflective`, `nonempty_isColimit_of_isPullback_left`, `nonempty_isColimit_of_isPullback_right`, `nonempty_isColimit_of_pullbackCone_left`, `nonempty_isColimit_of_pullbackCone_right`, `nonempty_isColimit_prod_of_isPullback`, `nonempty_isColimit_prod_of_pullbackCone`, `of_iso`, `of_mapCocone`, `precompose_isIso`, `whiskerEquivalence`, `whiskerEquivalence_iff`, `isUniversal`, `mapCocone_iff`, `map_reflective`, `of_iso`, `of_mapCocone`, `precompose_isIso`, `precompose_isIso_iff`, `whiskerEquivalence`, `whiskerEquivalence_iff`, `hasStrictInitial_of_isUniversal`, `isPullback_initial_to_of_cofan_isVanKampen`, `isPullback_of_cofan_isVanKampen`, `isUniversalColimit_extendCofan`, `isVanKampenColimit_extendCofan`, `isVanKampenColimit_of_evaluation`, `isVanKampenColimit_of_isEmpty`, `mono_of_cofan_isVanKampen`	37
Total	41

CategoryTheory

Definitions

Name	Category	Theorems
`IsUniversalColimit` 📖	MathDef	5 math math: `FinitaryPreExtensive.isUniversal_finiteCoproducts_Fin`, `IsVanKampenColimit.isUniversal`, `FinitaryPreExtensive.isUniversal_finiteCoproducts`, `IsUniversalColimit.whiskerEquivalence_iff`, `FinitaryPreExtensive.universal'`
`IsVanKampenColimit` 📖	MathDef	13 math math: `finitaryExtensive_iff_of_isTerminal`, `isVanKampenColimit_of_isEmpty`, `BinaryCofan.isVanKampen_iff`, `FinitaryExtensive.van_kampen'`, `IsInitial.isVanKampenColimit`, `FinitaryExtensive.isVanKampen_finiteCoproducts_Fin`, `FinitaryExtensive.vanKampen`, `FinitaryExtensive.isVanKampen_finiteCoproducts`, `BinaryCofan.isVanKampen_mk`, `IsVanKampenColimit.precompose_isIso_iff`, `IsVanKampenColimit.whiskerEquivalence_iff`, `IsVanKampenColimit.mapCocone_iff`, `IsPushout.isVanKampen_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasStrictInitial_of_isUniversal` 📖	mathematical	`IsUniversalColimit` `Discrete` `Limits.WalkingPair` `discreteCategory` `Limits.pair` `Limits.initial` `CategoryStruct.id` `Category.toCategoryStruct`	`Limits.HasStrictInitialObjects`	—	`Limits.hasStrictInitialObjects_of_initial_is_strict` `NatTrans.ext'` `Category.comp_id` `Category.id_comp` `NatTrans.Equifibered.of_discrete` `IsPullback.of_horiz_isIso` `IsIso.id` `Limits.IsInitial.hom_ext`
`isPullback_initial_to_of_cofan_isVanKampen` 📖	mathematical	`IsVanKampenColimit` `Discrete` `discreteCategory`	`IsPullback` `Limits.initial` `Functor.obj` `Functor` `Functor.category` `Functor.const` `Limits.Cocone.pt` `Limits.initial.to` `NatTrans.app` `Limits.Cocone.ι`	—	`Functor.hext` `Discrete.functor_map_id` `Unique.instSubsingleton` `Discrete.ext` `Lean.Meta.FastSubsingleton.helim` `isPullback_of_cofan_isVanKampen`
`isPullback_of_cofan_isVanKampen` 📖	mathematical	`IsVanKampenColimit` `Discrete` `discreteCategory` `Discrete.functor`	`IsPullback` `Limits.initial` `Limits.Cocone.pt` `Quiver.Hom` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `eqToHom` `CategoryStruct.comp` `Limits.initial.to`	—	`NatTrans.ext'` `Category.assoc` `Limits.initial.to_comp` `NatTrans.Equifibered.of_discrete` `instIsIsoEqToHom` `IsIso.eq_inv_comp` `Limits.IsInitial.hom_ext` `eqToHom_trans_assoc` `Category.id_comp`
`isUniversalColimit_extendCofan` 📖	mathematical	`IsUniversalColimit` `Discrete` `discreteCategory` `Discrete.functor` `Limits.WalkingPair` `Limits.pair` `Limits.Cocone.pt` `Limits.HasPullback` `Functor.obj` `Limits.WalkingPair.right` `Functor` `Functor.category` `Functor.const` `Limits.BinaryCofan.inr`	`extendCofan`	—	`Functor.hext` `Discrete.functor_map_id` `Category.assoc` `congr_app` `NatTrans.ext'` `Limits.limit.lift_π` `NatTrans.Equifibered.of_discrete` `IsPullback.of_right` `IsPullback.flip` `IsPullback.of_hasPullback` `Limits.pullback.condition` `Category.comp_id`
`isVanKampenColimit_extendCofan` 📖	mathematical	`IsVanKampenColimit` `Discrete` `discreteCategory` `Discrete.functor` `Limits.WalkingPair` `Limits.pair` `Limits.Cocone.pt` `Limits.HasPullback` `Functor.obj` `Limits.WalkingPair.right` `Functor` `Functor.category` `Functor.const` `Limits.BinaryCofan.inr`	`extendCofan`	—	`Limits.hasColimitOfHasColimitsOfShape` `Limits.hasColimitsOfShape_discrete` `Finite.of_fintype` `NatTrans.ext'` `congr_app` `Limits.Sigma.hom_ext` `Limits.colimit.ι_desc_assoc` `Category.assoc` `NatTrans.Equifibered.of_discrete` `Functor.hext` `Discrete.functor_map_id` `Limits.IsColimit.fac` `Limits.IsColimit.uniq` `Limits.colimit.ι_desc` `IsPullback.paste_horiz` `isUniversalColimit_extendCofan` `IsVanKampenColimit.isUniversal`
`isVanKampenColimit_of_evaluation` 📖	—	`IsVanKampenColimit` `Functor.comp` `Functor` `Functor.category` `Functor.obj` `evaluation` `Functor.mapCocone`	—	—	`NatTrans.ext'` `NatTrans.congr_app` `NatTrans.Equifibered.whiskerRight` `Limits.evaluation_preservesLimit` `Limits.hasLimitOfHasLimitsOfShape` `CommSq.w` `Limits.evaluation_preservesColimit` `Limits.hasColimitOfHasColimitsOfShape` `IsPullback.map`
`isVanKampenColimit_of_isEmpty` 📖	mathematical	—	`IsVanKampenColimit`	—	`instIsEmptyDiscrete` `PEmpty.instIsEmpty` `IsInitial.isVanKampenColimit` `IsVanKampenColimit.whiskerEquivalence_iff` `IsVanKampenColimit.of_iso` `IsVanKampenColimit.precompose_isIso` `Iso.isIso_hom` `Category.comp_id`
`mono_of_cofan_isVanKampen` 📖	mathematical	`IsVanKampenColimit` `Discrete` `discreteCategory`	`Mono` `Functor.obj` `Functor` `Functor.category` `Functor.const` `Limits.Cocone.pt` `NatTrans.app` `Limits.Cocone.ι`	—	`Functor.hext` `Discrete.functor_map_id` `Limits.PullbackCone.mono_of_isLimitMkIdId` `Category.id_comp` `eqToHom_trans` `IsPullback.paste_vert` `IsPullback.of_vert_isIso` `instIsIsoEqToHom` `IsIso.id` `Category.comp_id` `isPullback_of_cofan_isVanKampen`

CategoryTheory.BinaryCofan

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPullback_initial_to_of_isVanKampen` 📖	mathematical	`CategoryTheory.IsVanKampenColimit` `CategoryTheory.Discrete` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.discreteCategory` `CategoryTheory.Limits.pair`	`CategoryTheory.IsPullback` `CategoryTheory.Limits.initial` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.WalkingPair.left` `CategoryTheory.Limits.WalkingPair.right` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Limits.initial.to` `CategoryTheory.Limits.BinaryCofan.inl` `CategoryTheory.Limits.BinaryCofan.inr`	—	`CategoryTheory.IsPullback.flip` `CategoryTheory.NatTrans.ext'` `CategoryTheory.Limits.initial.to_comp` `CategoryTheory.Category.id_comp` `CategoryTheory.NatTrans.Equifibered.of_discrete` `CategoryTheory.Limits.BinaryCofan.isColimit_iff_isIso_inr` `CategoryTheory.IsIso.id`
`isVanKampen_iff` 📖	mathematical	—	`CategoryTheory.IsVanKampenColimit` `CategoryTheory.Discrete` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.discreteCategory` `CategoryTheory.Limits.pair` `CategoryTheory.Limits.IsColimit` `CategoryTheory.IsPullback` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.WalkingPair.left` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Limits.BinaryCofan.inl` `CategoryTheory.Limits.WalkingPair.right` `CategoryTheory.Limits.BinaryCofan.inr`	—	`CategoryTheory.NatTrans.ext'` `CategoryTheory.NatTrans.Equifibered.of_discrete` `CategoryTheory.Functor.hext` `CategoryTheory.Discrete.functor_map_id` `CategoryTheory.NatTrans.congr_app`
`isVanKampen_mk` 📖	mathematical	`CategoryTheory.IsPullback` `CategoryTheory.Functor.obj` `CategoryTheory.Discrete` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.discreteCategory` `CategoryTheory.Limits.pair` `CategoryTheory.Limits.WalkingPair.left` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Limits.BinaryCofan.inl` `CategoryTheory.Limits.WalkingPair.right` `CategoryTheory.Limits.BinaryCofan.inr`	`CategoryTheory.IsVanKampenColimit`	—	`isVanKampen_iff` `CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_inv_assoc` `CategoryTheory.Category.id_comp` `CategoryTheory.Iso.hom_inv_id_assoc` `CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom` `CategoryTheory.IsPullback.paste_vert` `CategoryTheory.IsPullback.of_vert_isIso` `CategoryTheory.IsIso.id` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp`
`mono_inr_of_isVanKampen` 📖	mathematical	`CategoryTheory.IsVanKampenColimit` `CategoryTheory.Discrete` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.discreteCategory` `CategoryTheory.Limits.pair`	`CategoryTheory.Mono` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.WalkingPair.right` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Limits.BinaryCofan.inr`	—	`CategoryTheory.Limits.PullbackCone.mono_of_isLimitMkIdId` `CategoryTheory.NatTrans.ext'` `CategoryTheory.Limits.initial.to_comp` `CategoryTheory.Category.id_comp` `CategoryTheory.NatTrans.Equifibered.of_discrete` `CategoryTheory.Limits.BinaryCofan.isColimit_iff_isIso_inr` `CategoryTheory.IsIso.id`

CategoryTheory.IsInitial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isVanKampenColimit` 📖	mathematical	—	`CategoryTheory.IsVanKampenColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.empty` `CategoryTheory.Limits.asEmptyCocone`	—	`CategoryTheory.Functor.hext` `CategoryTheory.Limits.IsInitial.isIso_to`

CategoryTheory.IsUniversalColimit

Definitions

Name	Category	Theorems
`isColimit` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPullback_of_isColimit_left` 📖	mathematical	`CategoryTheory.IsUniversalColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor` `CategoryTheory.IsPullback`	`CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Limits.Cofan.IsColimit.desc` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	`CategoryTheory.CommSq.w` `CategoryTheory.IsPullback.toCommSq` `CategoryTheory.Category.assoc` `nonempty_isColimit_of_isPullback_left` `CategoryTheory.IsPullback.of_hasPullback` `CategoryTheory.Category.id_comp` `CategoryTheory.Limits.limit.lift_π` `CategoryTheory.IsPullback.of_iso` `CategoryTheory.Limits.Cofan.IsColimit.hom_ext` `CategoryTheory.Category.comp_id` `CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso_hom_desc` `CategoryTheory.Limits.IsColimit.fac` `CategoryTheory.Limits.pullback.lift_fst` `CategoryTheory.Limits.pullback.lift_snd`
`isPullback_of_isColimit_right` 📖	mathematical	`CategoryTheory.IsUniversalColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor` `CategoryTheory.IsPullback`	`CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Limits.Cofan.IsColimit.desc` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	`CategoryTheory.Category.assoc` `CategoryTheory.CommSq.w` `CategoryTheory.IsPullback.toCommSq` `nonempty_isColimit_of_isPullback_right` `CategoryTheory.IsPullback.of_hasPullback` `CategoryTheory.Category.id_comp` `CategoryTheory.Limits.limit.lift_π` `CategoryTheory.IsPullback.of_iso` `CategoryTheory.Limits.Cofan.IsColimit.hom_ext` `CategoryTheory.Category.comp_id` `CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso_hom_desc` `CategoryTheory.Limits.IsColimit.fac` `CategoryTheory.Limits.pullback.lift_fst` `CategoryTheory.Limits.pullback.lift_snd`
`isPullback_prod_of_isColimit` 📖	mathematical	`CategoryTheory.IsUniversalColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor` `CategoryTheory.Limits.HasPullback` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.IsPullback`	`CategoryTheory.Limits.Cofan.IsColimit.desc` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	`CategoryTheory.Category.assoc` `CategoryTheory.CommSq.w` `CategoryTheory.IsPullback.toCommSq` `nonempty_isColimit_prod_of_isPullback` `CategoryTheory.IsPullback.of_hasPullback` `CategoryTheory.Category.id_comp` `CategoryTheory.Limits.limit.lift_π` `CategoryTheory.IsPullback.of_iso` `CategoryTheory.Limits.Cofan.IsColimit.hom_ext` `CategoryTheory.Category.comp_id` `CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso_hom_desc` `CategoryTheory.Limits.IsColimit.fac` `CategoryTheory.Limits.pullback.lift_fst` `CategoryTheory.Limits.pullback.lift_snd`
`map_reflective` 📖	mathematical	`CategoryTheory.IsUniversalColimit` `CategoryTheory.Functor.comp` `CategoryTheory.Limits.HasPullback` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Functor.map` `CategoryTheory.NatTrans.app` `CategoryTheory.Adjunction.unit` `CategoryTheory.Limits.PreservesLimit` `CategoryTheory.Limits.WalkingCospan` `CategoryTheory.Limits.WidePullbackShape.category` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.cospan`	`CategoryTheory.Functor.mapCocone`	—	`CategoryTheory.Adjunction.rightAdjoint_preservesLimits` `CategoryTheory.Adjunction.leftAdjoint_preservesColimits` `CategoryTheory.Limits.pullback.condition` `CategoryTheory.IsPullback.of_hasPullback` `CategoryTheory.NatTrans.Equifibered.comp` `CategoryTheory.NatTrans.Equifibered.of_isIso` `CategoryTheory.IsIso.comp_isIso` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.Functor.isIso_whiskerLeft` `CategoryTheory.Adjunction.counit_isIso_of_R_fully_faithful` `CategoryTheory.Adjunction.instIsIsoAppCounitOfFullOfFaithful` `CategoryTheory.IsIso.eq_inv_of_inv_hom_id` `CategoryTheory.Adjunction.left_triangle_components` `CategoryTheory.cancel_mono` `CategoryTheory.mono_of_strongMono` `CategoryTheory.strongMono_of_isIso` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `CategoryTheory.Functor.map_comp` `CategoryTheory.Category.assoc` `CategoryTheory.Adjunction.counit_naturality` `CategoryTheory.Adjunction.counit_naturality_assoc` `CategoryTheory.NatTrans.congr_app` `CategoryTheory.Adjunction.unit_naturality` `CategoryTheory.Adjunction.right_triangle_components_assoc` `CategoryTheory.Limits.pullback.hom_ext` `CategoryTheory.Limits.pullback.lift.congr_simp` `CategoryTheory.Limits.pullback.lift_fst` `CategoryTheory.Limits.Cocone.w` `CategoryTheory.Limits.pullback.lift_snd` `CategoryTheory.NatTrans.naturality_assoc` `CategoryTheory.Functor.map_comp_assoc` `CategoryTheory.IsIso.inv_hom_id_assoc` `CategoryTheory.Iso.comp_inv_eq` `CategoryTheory.Limits.PreservesPullback.iso_hom_fst` `CategoryTheory.IsIso.comp_inv_eq` `CategoryTheory.Limits.PreservesPullback.iso_hom_snd` `CategoryTheory.Iso.inv_hom_id_assoc` `CategoryTheory.Limits.pullback.lift_fst_assoc` `CategoryTheory.IsIso.inv_hom_id` `CategoryTheory.Limits.Cocones.cocone_iso_of_hom_iso` `CategoryTheory.Limits.pullback_fst_iso_of_right_iso` `CategoryTheory.IsIso.inv_isIso` `CategoryTheory.IsIso.eq_comp_inv` `CategoryTheory.IsIso.id` `CategoryTheory.NatTrans.ext'` `CategoryTheory.NatTrans.Equifibered.whiskerRight` `CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit` `CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits` `CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits` `CategoryTheory.IsPullback.of_right` `CategoryTheory.IsPullback.paste_vert` `CategoryTheory.IsPullback.map` `CategoryTheory.IsPullback.of_vert_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Adjunction.right_triangle_components` `CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit` `CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape`
`nonempty_isColimit_of_isPullback_left` 📖	mathematical	`CategoryTheory.IsUniversalColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor` `CategoryTheory.IsPullback` `CategoryTheory.Limits.Cocone.pt`	`CategoryTheory.Limits.IsColimit`	—	`nonempty_isColimit_of_pullbackCone_left`
`nonempty_isColimit_of_isPullback_right` 📖	mathematical	`CategoryTheory.IsUniversalColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor` `CategoryTheory.IsPullback` `CategoryTheory.Limits.Cocone.pt`	`CategoryTheory.Limits.IsColimit`	—	`nonempty_isColimit_of_pullbackCone_right`
`nonempty_isColimit_of_pullbackCone_left` 📖	mathematical	`CategoryTheory.IsUniversalColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor`	`CategoryTheory.Limits.IsColimit` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Limits.WalkingCospan` `CategoryTheory.Limits.WidePullbackShape.category` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.cospan`	—	`CategoryTheory.Limits.PullbackCone.condition` `CategoryTheory.Category.assoc` `CategoryTheory.Limits.PullbackCone.IsLimit.hom_ext` `CategoryTheory.Limits.PullbackCone.IsLimit.lift_fst` `CategoryTheory.Limits.PullbackCone.IsLimit.lift_snd` `Equiv.nonempty_congr` `CategoryTheory.NatTrans.ext'` `CategoryTheory.NatTrans.Equifibered.of_discrete` `CategoryTheory.IsPullback.of_right` `CategoryTheory.IsPullback.of_isLimit`
`nonempty_isColimit_of_pullbackCone_right` 📖	mathematical	`CategoryTheory.IsUniversalColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor`	`CategoryTheory.Limits.IsColimit` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Limits.WalkingCospan` `CategoryTheory.Limits.WidePullbackShape.category` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.cospan`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Limits.PullbackCone.condition` `CategoryTheory.Limits.PullbackCone.IsLimit.hom_ext` `CategoryTheory.Limits.PullbackCone.IsLimit.lift_fst` `CategoryTheory.Limits.PullbackCone.IsLimit.lift_snd` `Equiv.nonempty_congr` `CategoryTheory.NatTrans.ext'` `CategoryTheory.NatTrans.Equifibered.of_discrete` `CategoryTheory.IsPullback.of_right` `CategoryTheory.IsPullback.flip` `CategoryTheory.IsPullback.of_isLimit`
`nonempty_isColimit_prod_of_isPullback` 📖	mathematical	`CategoryTheory.IsUniversalColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor` `CategoryTheory.Limits.HasPullback` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.IsPullback`	`CategoryTheory.Limits.IsColimit`	—	`nonempty_isColimit_prod_of_pullbackCone`
`nonempty_isColimit_prod_of_pullbackCone` 📖	mathematical	`CategoryTheory.IsUniversalColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor` `CategoryTheory.Limits.HasPullback` `CategoryTheory.Limits.Cocone.pt`	`CategoryTheory.Limits.IsColimit` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Limits.WalkingCospan` `CategoryTheory.Limits.WidePullbackShape.category` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.cospan`	—	`CategoryTheory.Limits.PullbackCone.condition` `CategoryTheory.Category.assoc` `CategoryTheory.Limits.pullback.condition` `CategoryTheory.Limits.PullbackCone.IsLimit.hom_ext` `CategoryTheory.Limits.PullbackCone.IsLimit.lift_fst` `CategoryTheory.Limits.limit.lift_π_assoc` `CategoryTheory.Limits.PullbackCone.IsLimit.lift_snd` `CategoryTheory.Limits.limit.lift_π` `Equiv.nonempty_congr` `nonempty_isColimit_of_pullbackCone_left` `CategoryTheory.Category.id_comp` `nonempty_isColimit_of_pullbackCone_right`
`of_iso` 📖	—	`CategoryTheory.IsUniversalColimit`	—	—	`CategoryTheory.NatTrans.ext'` `CategoryTheory.Limits.CoconeMorphism.w` `CategoryTheory.Functor.map_comp` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `CategoryTheory.Category.comp_id` `CategoryTheory.IsPullback.paste_vert` `CategoryTheory.IsPullback.of_vert_isIso` `CategoryTheory.IsIso.id` `CategoryTheory.Limits.instIsIsoHomInvCocone` `CategoryTheory.Category.id_comp`
`of_mapCocone` 📖	—	`CategoryTheory.IsUniversalColimit` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.mapCocone`	—	—	`CategoryTheory.NatTrans.ext'` `CategoryTheory.Functor.map_comp` `CategoryTheory.Functor.congr_map` `CategoryTheory.NatTrans.congr_app` `CategoryTheory.NatTrans.Equifibered.whiskerRight` `CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit` `CategoryTheory.IsPullback.map` `CategoryTheory.Limits.reflectsColimit_of_reflectsColimitsOfShape`
`precompose_isIso` 📖	mathematical	`CategoryTheory.IsUniversalColimit`	`CategoryTheory.Functor.obj` `CategoryTheory.Limits.Cocone` `CategoryTheory.Limits.Cocone.category` `CategoryTheory.Limits.Cocones.precompose`	—	`CategoryTheory.Category.assoc` `CategoryTheory.NatTrans.Equifibered.comp` `CategoryTheory.NatTrans.Equifibered.of_isIso` `CategoryTheory.Category.comp_id` `CategoryTheory.IsPullback.paste_vert` `CategoryTheory.IsPullback.of_vert_isIso` `CategoryTheory.NatIso.isIso_app_of_isIso` `CategoryTheory.IsIso.id`
`whiskerEquivalence` 📖	mathematical	`CategoryTheory.IsUniversalColimit`	`CategoryTheory.Functor.comp` `CategoryTheory.Equivalence.functor` `CategoryTheory.Limits.Cocone.whisker`	—	`Equiv.nonempty_congr` `CategoryTheory.NatTrans.ext'` `CategoryTheory.Category.assoc` `CategoryTheory.Equivalence.invFunIdAssoc_hom_app` `CategoryTheory.NatTrans.naturality` `CategoryTheory.Category.comp_id` `CategoryTheory.Functor.whiskerLeft_twice` `CategoryTheory.Category.id_comp` `CategoryTheory.NatTrans.Equifibered.comp` `CategoryTheory.NatTrans.Equifibered.whiskerLeft` `CategoryTheory.NatTrans.Equifibered.of_isIso` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.IsPullback.paste_vert` `CategoryTheory.IsPullback.of_vert_isIso` `CategoryTheory.NatIso.hom_app_isIso` `CategoryTheory.IsIso.id`
`whiskerEquivalence_iff` 📖	mathematical	—	`CategoryTheory.IsUniversalColimit` `CategoryTheory.Functor.comp` `CategoryTheory.Equivalence.functor` `CategoryTheory.Limits.Cocone.whisker`	—	`of_iso` `precompose_isIso` `CategoryTheory.Iso.isIso_inv` `whiskerEquivalence` `CategoryTheory.Functor.whiskerLeft_twice` `CategoryTheory.Equivalence.invFunIdAssoc_inv_app` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `CategoryTheory.NatTrans.naturality`

CategoryTheory.IsVanKampenColimit

Definitions

Name	Category	Theorems
`isColimit` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isUniversal` 📖	mathematical	`CategoryTheory.IsVanKampenColimit`	`CategoryTheory.IsUniversalColimit`	—	—
`mapCocone_iff` 📖	mathematical	—	`CategoryTheory.IsVanKampenColimit` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.mapCocone`	—	`of_mapCocone` `CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit` `CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits` `CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits` `CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint` `CategoryTheory.Functor.isRightAdjoint_of_isEquivalence` `CategoryTheory.Limits.ReflectsFiniteLimits.reflects` `CategoryTheory.Limits.instReflectsFiniteLimitsOfReflectsLimits` `CategoryTheory.Limits.fullyFaithful_reflectsLimits` `CategoryTheory.Functor.IsEquivalence.full` `CategoryTheory.Functor.IsEquivalence.faithful` `CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint` `CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence` `CategoryTheory.Limits.reflectsColimitsOfShape_of_reflectsColimits` `CategoryTheory.Limits.fullyFaithful_reflectsColimits` `CategoryTheory.Functor.isEquivalence_inv` `precompose_isIso_iff` `CategoryTheory.Iso.isIso_inv` `of_iso` `CategoryTheory.Functor.id_hcomp` `CategoryTheory.Functor.inv_fun_map` `CategoryTheory.Iso.hom_inv_id_app_assoc`
`map_reflective` 📖	mathematical	`CategoryTheory.IsVanKampenColimit` `CategoryTheory.Functor.comp` `CategoryTheory.Limits.HasPullback` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Functor.map` `CategoryTheory.NatTrans.app` `CategoryTheory.Adjunction.unit` `CategoryTheory.Limits.PreservesLimit` `CategoryTheory.Limits.WalkingCospan` `CategoryTheory.Limits.WidePullbackShape.category` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.cospan` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.ι`	`CategoryTheory.Functor.mapCocone`	—	`CategoryTheory.Adjunction.rightAdjoint_preservesLimits` `CategoryTheory.Adjunction.leftAdjoint_preservesColimits` `CategoryTheory.NatTrans.Equifibered.comp` `CategoryTheory.NatTrans.Equifibered.of_isIso` `CategoryTheory.IsIso.comp_isIso` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.Functor.isIso_whiskerLeft` `CategoryTheory.Adjunction.counit_isIso_of_R_fully_faithful` `CategoryTheory.cancel_mono` `CategoryTheory.mono_of_strongMono` `CategoryTheory.strongMono_of_isIso` `CategoryTheory.Adjunction.instIsIsoAppCounitOfFullOfFaithful` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `CategoryTheory.Functor.map_comp` `CategoryTheory.Category.assoc` `CategoryTheory.Adjunction.counit_naturality` `CategoryTheory.Adjunction.counit_naturality_assoc` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit` `CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape` `CategoryTheory.NatIso.isIso_app_of_isIso` `CategoryTheory.NatIso.isIso_inv_app` `CategoryTheory.IsIso.inv_hom_id_assoc` `CategoryTheory.Limits.IsColimit.hom_ext` `CategoryTheory.Limits.IsColimit.fac` `CategoryTheory.Functor.mapCocone_ι_app` `CategoryTheory.Limits.colimit.cocone_ι` `CategoryTheory.Limits.colimit.ι_desc` `CategoryTheory.NatTrans.congr_app` `CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso_hom_desc` `CategoryTheory.IsPullback.map` `CategoryTheory.NatTrans.ext'` `CategoryTheory.NatTrans.Equifibered.whiskerRight` `CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit` `CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits` `CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits` `CategoryTheory.IsPullback.paste_vert` `CategoryTheory.IsPullback.of_vert_isIso` `CategoryTheory.NatIso.inv_app_isIso` `CategoryTheory.IsIso.inv_comp_eq` `CategoryTheory.NatIso.inv_inv_app` `CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom` `CategoryTheory.IsUniversalColimit.map_reflective` `isUniversal`
`of_iso` 📖	—	`CategoryTheory.IsVanKampenColimit`	—	—	`CategoryTheory.NatTrans.ext'` `CategoryTheory.Limits.CoconeMorphism.w` `CategoryTheory.Functor.map_comp` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `CategoryTheory.Category.comp_id` `CategoryTheory.IsPullback.paste_vert_iff` `CategoryTheory.IsPullback.of_vert_isIso` `CategoryTheory.IsIso.id` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Iso.isIso_inv` `CategoryTheory.Category.id_comp` `CategoryTheory.NatTrans.congr_app`
`of_mapCocone` 📖	—	`CategoryTheory.Limits.PreservesLimit` `CategoryTheory.Limits.WalkingCospan` `CategoryTheory.Limits.WidePullbackShape.category` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.cospan` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.ι` `CategoryTheory.IsVanKampenColimit` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.mapCocone`	—	—	`CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit` `CategoryTheory.Limits.reflectsColimit_of_reflectsColimitsOfShape` `CategoryTheory.NatTrans.ext'` `CategoryTheory.Functor.map_comp` `CategoryTheory.Functor.congr_map` `CategoryTheory.NatTrans.congr_app` `CategoryTheory.NatTrans.Equifibered.whiskerRight` `CategoryTheory.IsPullback.map_iff` `CategoryTheory.Limits.reflectsLimit_of_reflectsLimitsOfShape`
`precompose_isIso` 📖	mathematical	`CategoryTheory.IsVanKampenColimit`	`CategoryTheory.Functor.obj` `CategoryTheory.Limits.Cocone` `CategoryTheory.Limits.Cocone.category` `CategoryTheory.Limits.Cocones.precompose`	—	`CategoryTheory.Category.assoc` `CategoryTheory.NatTrans.Equifibered.comp` `CategoryTheory.NatTrans.Equifibered.of_isIso` `CategoryTheory.IsPullback.of_vert_isIso` `CategoryTheory.NatIso.isIso_app_of_isIso` `CategoryTheory.IsIso.id` `CategoryTheory.Category.comp_id` `CategoryTheory.IsPullback.paste_vert_iff` `CategoryTheory.congr_app`
`precompose_isIso_iff` 📖	mathematical	—	`CategoryTheory.IsVanKampenColimit` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.Cocone` `CategoryTheory.Limits.Cocone.category` `CategoryTheory.Limits.Cocones.precompose`	—	`of_iso` `precompose_isIso` `CategoryTheory.IsIso.inv_isIso` `CategoryTheory.IsIso.inv_hom_id_assoc` `CategoryTheory.Category.comp_id`
`whiskerEquivalence` 📖	mathematical	`CategoryTheory.IsVanKampenColimit`	`CategoryTheory.Functor.comp` `CategoryTheory.Equivalence.functor` `CategoryTheory.Limits.Cocone.whisker`	—	`Equiv.nonempty_congr` `CategoryTheory.Equivalence.invFunIdAssoc_hom_app` `CategoryTheory.Category.comp_id` `CategoryTheory.IsPullback.paste_vert` `CategoryTheory.IsIso.id` `CategoryTheory.IsPullback.of_vert_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.NatIso.hom_app_isIso` `CategoryTheory.NatTrans.naturality` `CategoryTheory.NatTrans.naturality_assoc` `CategoryTheory.Equivalence.functor_unit_comp` `CategoryTheory.Functor.map_id` `CategoryTheory.Category.id_comp` `CategoryTheory.NatTrans.ext'` `CategoryTheory.Category.assoc` `CategoryTheory.congr_app` `CategoryTheory.NatTrans.Equifibered.comp` `CategoryTheory.NatTrans.Equifibered.whiskerLeft` `CategoryTheory.NatTrans.Equifibered.of_isIso` `CategoryTheory.Iso.isIso_hom`
`whiskerEquivalence_iff` 📖	mathematical	—	`CategoryTheory.IsVanKampenColimit` `CategoryTheory.Functor.comp` `CategoryTheory.Equivalence.functor` `CategoryTheory.Limits.Cocone.whisker`	—	`of_iso` `precompose_isIso` `CategoryTheory.Iso.isIso_inv` `whiskerEquivalence` `CategoryTheory.Functor.whiskerLeft_twice` `CategoryTheory.Equivalence.invFunIdAssoc_inv_app` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `CategoryTheory.NatTrans.naturality`

---

← Back to Index