Basic

📁 Source: Mathlib/CategoryTheory/Adhesive/Basic.lean

Statistics

Metric	Count
Definitions IsVanKampen	1
Theorems desc_mono_of_mono, hasPullback_of_mono_left, hasPushout_of_mono_left, isPullback_of_isPushout_of_mono_left, isPullback_of_isPushout_of_mono_right, isPushout_isPullback_isPullback_hom_ext, mono_of_isPushout_of_mono_left, mono_of_isPushout_of_mono_right, toRegularMonoCategory, van_kampen, van_kampen', exists_cube_filling, flip, isPullback_of_mono_left, isPullback_of_mono_right, mono_of_mono_left, mono_of_mono_right, isVanKampen_iff, isVanKampen_iff', isVanKampen_inl, isVanKampen_isPullback_isPullback_hom_ext, adhesive, adhesive_functor, adhesive_of_preserves_and_reflects, adhesive_of_preserves_and_reflects_isomorphism, adhesive_of_reflective, is_coprod_iff_isPushout	27
Total	28

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adhesive_functor 📖	mathematical	—	Adhesive Functor Functor.category	—	Limits.functorCategoryHasLimit Limits.hasLimitOfHasLimitsOfShape Limits.functorCategoryHasColimit Limits.hasColimitOfHasColimitsOfShape CommSq.w IsPushout.toCommSq IsPushout.isVanKampen_iff isVanKampenColimit_of_evaluation IsVanKampenColimit.precompose_isIso_iff Iso.isIso_inv IsVanKampenColimit.of_iso NatTrans.naturality IsPushout.map Limits.evaluation_preservesColimit Adhesive.van_kampen Functor.map_mono preservesMonomorphisms_of_preservesLimitsOfShape Limits.evaluation_preservesLimitsOfShape
adhesive_of_preserves_and_reflects 📖	mathematical	Limits.HasPullback Limits.HasPushout	Adhesive	—	CommSq.w IsPushout.toCommSq IsPushout.isVanKampen_iff IsVanKampenColimit.of_mapCocone Limits.PreservesLimitsOfShape.preservesLimit IsVanKampenColimit.precompose_isIso_iff Iso.isIso_inv IsVanKampenColimit.of_iso NatTrans.naturality IsPushout.map Limits.PreservesColimitsOfShape.preservesColimit Adhesive.van_kampen Functor.map_mono preservesMonomorphisms_of_preservesLimitsOfShape
adhesive_of_preserves_and_reflects_isomorphism 📖	mathematical	—	Adhesive	—	adhesive_of_preserves_and_reflects Limits.hasLimitOfHasLimitsOfShape Limits.hasColimitOfHasColimitsOfShape Limits.reflectsLimitsOfShape_of_reflectsIsomorphisms Limits.reflectsColimitsOfShape_of_reflectsIsomorphisms
adhesive_of_reflective 📖	mathematical	Limits.HasPushout	Adhesive	—	Adjunction.leftAdjoint_preservesColimits Adjunction.rightAdjoint_preservesLimits Limits.hasLimitOfHasLimitsOfShape Adhesive.hasPushout_of_mono_left Functor.map_mono preservesMonomorphisms_of_preservesLimitsOfShape Limits.PreservesFiniteLimits.preservesFiniteLimits Limits.PreservesLimits.preservesFiniteLimits IsPushout.of_hasPushout Adhesive.van_kampen CommSq.w IsPushout.toCommSq IsPushout.isVanKampen_iff Adjunction.counit_isIso_of_R_fully_faithful IsVanKampenColimit.precompose_isIso_iff Iso.isIso_hom IsVanKampenColimit.of_iso IsVanKampenColimit.map_reflective IsVanKampenColimit.precompose_isIso Limits.PreservesLimitsOfShape.preservesLimit Limits.PreservesColimitsOfShape.preservesColimit Limits.PreservesFiniteColimits.preservesFiniteColimits Limits.PreservesColimits.preservesFiniteColimits
is_coprod_iff_isPushout 📖	mathematical	CommSq Functor.obj Discrete Limits.WalkingPair discreteCategory Functor Functor.category Functor.const Limits.Cocone.pt Limits.pair Limits.WalkingPair.left Limits.BinaryCofan.inl	Limits.IsColimit Discrete Limits.WalkingPair discreteCategory Limits.pair Functor.obj Limits.WalkingPair.right CategoryStruct.comp Category.toCategoryStruct Functor Functor.category Functor.const Limits.Cocone.pt Limits.BinaryCofan.inr IsPushout Limits.WalkingPair.left Limits.BinaryCofan.inl	—	CommSq.w Limits.IsColimit.fac Limits.BinaryCofan.IsColimit.hom_ext CommSq.w_assoc Limits.PushoutCocone.condition Category.assoc Limits.PushoutCocone.IsColimit.hom_ext IsPushout.toCommSq

CategoryTheory.Adhesive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
desc_mono_of_mono 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Limits.pushout CategoryTheory.Limits.pullback CategoryTheory.Limits.hasPullback_symmetry hasPullback_of_mono_left CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd hasPushout_of_mono_left CategoryTheory.Limits.pullback.fst_of_mono CategoryTheory.Limits.pushout.desc CategoryTheory.Limits.pullback.condition	—	CategoryTheory.Limits.hasPullback_symmetry hasPullback_of_mono_left hasPushout_of_mono_left CategoryTheory.Limits.pullback.fst_of_mono CategoryTheory.Limits.pullback.condition mono_of_isPushout_of_mono_right CategoryTheory.IsPushout.of_hasPushout CategoryTheory.Limits.pullback.snd_of_mono mono_of_isPushout_of_mono_left CategoryTheory.IsPullback.of_hasPullback CategoryTheory.IsPushout.IsVanKampen.exists_cube_filling van_kampen CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.IsPullback.isoPullback_hom_fst CategoryTheory.mono_comp CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom isPushout_isPullback_isPullback_hom_ext CategoryTheory.Limits.pullback.condition_assoc CategoryTheory.CommSq.w CategoryTheory.IsPullback.toCommSq CategoryTheory.Category.assoc CategoryTheory.eq_whisker CategoryTheory.Limits.pushout.inl_desc CategoryTheory.cancel_mono CategoryTheory.CommSq.w_assoc CategoryTheory.whisker_eq CategoryTheory.Limits.pushout.inr_desc CategoryTheory.Limits.pullback.lift_snd_assoc CategoryTheory.Limits.pushout.condition CategoryTheory.Limits.pullback.lift_fst_assoc
hasPullback_of_mono_left 📖	mathematical	—	CategoryTheory.Limits.HasPullback	—	—
hasPushout_of_mono_left 📖	mathematical	—	CategoryTheory.Limits.HasPushout	—	—
isPullback_of_isPushout_of_mono_left 📖	mathematical	CategoryTheory.IsPushout	CategoryTheory.IsPullback	—	CategoryTheory.IsPushout.IsVanKampen.isPullback_of_mono_left van_kampen
isPullback_of_isPushout_of_mono_right 📖	mathematical	CategoryTheory.IsPushout	CategoryTheory.IsPullback	—	CategoryTheory.IsPushout.IsVanKampen.isPullback_of_mono_right van_kampen'
isPushout_isPullback_isPullback_hom_ext 📖	—	CategoryTheory.IsPushout CategoryTheory.IsPullback CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—	CategoryTheory.IsPushout.isVanKampen_isPullback_isPullback_hom_ext van_kampen CategoryTheory.Limits.hasPullback_symmetry hasPullback_of_mono_left
mono_of_isPushout_of_mono_left 📖	mathematical	CategoryTheory.IsPushout	CategoryTheory.Mono	—	CategoryTheory.IsPushout.IsVanKampen.mono_of_mono_left van_kampen
mono_of_isPushout_of_mono_right 📖	mathematical	CategoryTheory.IsPushout	CategoryTheory.Mono	—	CategoryTheory.IsPushout.IsVanKampen.mono_of_mono_right van_kampen'
toRegularMonoCategory 📖	mathematical	—	CategoryTheory.IsRegularMonoCategory	—	hasPushout_of_mono_left CategoryTheory.Limits.pushout.condition isPullback_of_isPushout_of_mono_left CategoryTheory.IsPushout.of_hasPushout
van_kampen 📖	mathematical	CategoryTheory.IsPushout	CategoryTheory.IsPushout.IsVanKampen	—	—
van_kampen' 📖	mathematical	CategoryTheory.IsPushout	CategoryTheory.IsPushout.IsVanKampen	—	CategoryTheory.IsPushout.IsVanKampen.flip CategoryTheory.IsPushout.flip van_kampen

CategoryTheory.IsPushout

Definitions

Name	Category	Theorems
IsVanKampen 📖	MathDef	6 math math: CategoryTheory.Adhesive.van_kampen, CategoryTheory.Adhesive.van_kampen', isVanKampen_iff', IsVanKampen.flip, isVanKampen_inl, isVanKampen_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isVanKampen_iff 📖	mathematical	CategoryTheory.IsPushout	IsVanKampen CategoryTheory.IsVanKampenColimit CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.span CategoryTheory.CommSq.w toCommSq	—	CategoryTheory.CommSq.w toCommSq CategoryTheory.Limits.Cocone.w Equiv.nonempty_congr CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id isColimit' CategoryTheory.NatTrans.congr_app CategoryTheory.NatTrans.naturality CategoryTheory.IsPullback.paste_horiz CategoryTheory.Functor.map_id CategoryTheory.IsPullback.toCommSq CategoryTheory.NatTrans.ext' CategoryTheory.Limits.PushoutCocone.condition_zero CategoryTheory.Category.assoc CategoryTheory.CommSq.w_assoc CategoryTheory.IsPullback.of_horiz_isIso CategoryTheory.IsIso.id
isVanKampen_iff' 📖	mathematical	CategoryTheory.IsPushout	IsVanKampen CategoryTheory.IsPullback Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.IsPushout	—	IsVanKampen.exists_cube_filling toCommSq CategoryTheory.IsPullback.hasPullback of_iso CategoryTheory.Category.comp_id CategoryTheory.IsPullback.isoIsPullback_hom_fst CategoryTheory.IsPullback.hom_ext CategoryTheory.Category.assoc CategoryTheory.CommSq.w CategoryTheory.IsPullback.isoIsPullback_hom_fst_assoc CategoryTheory.IsPullback.toCommSq CategoryTheory.IsPullback.isoIsPullback_hom_snd_assoc CategoryTheory.Category.id_comp
isVanKampen_inl 📖	mathematical	CategoryTheory.IsPushout CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.pair CategoryTheory.Limits.WalkingPair.left CategoryTheory.Limits.BinaryCofan.inl	IsVanKampen CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.pair CategoryTheory.Limits.WalkingPair.left CategoryTheory.Limits.BinaryCofan.inl	—	CategoryTheory.is_coprod_iff_isPushout toCommSq CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.BinaryCofan.isVanKampen_iff CategoryTheory.FinitaryExtensive.vanKampen CategoryTheory.CommSq.w CategoryTheory.IsPullback.toCommSq CategoryTheory.Limits.pullback.condition CategoryTheory.IsPullback.of_hasPullback CategoryTheory.Limits.pullback.condition_assoc CategoryTheory.Category.assoc CategoryTheory.Limits.pullback.lift_snd CategoryTheory.IsPullback.of_right CategoryTheory.Limits.pullback.lift_fst CategoryTheory.IsPullback.paste_horiz CategoryTheory.Category.id_comp CategoryTheory.IsPullback.paste_vert CategoryTheory.Limits.BinaryCofan.IsColimit.hom_ext CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom CategoryTheory.IsPullback.of_vert_isIso CategoryTheory.Iso.isIso_hom CategoryTheory.IsIso.id CategoryTheory.Category.comp_id
isVanKampen_isPullback_isPullback_hom_ext 📖	—	CategoryTheory.IsPushout IsVanKampen CategoryTheory.IsPullback CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—	IsVanKampen.exists_cube_filling hom_ext

CategoryTheory.IsPushout.IsVanKampen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_cube_filling 📖	mathematical	CategoryTheory.IsPushout CategoryTheory.IsPushout.IsVanKampen CategoryTheory.IsPullback	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.IsPullback CategoryTheory.IsPushout	—	CategoryTheory.Category.assoc CategoryTheory.CommSq.w CategoryTheory.IsPullback.toCommSq CategoryTheory.Limits.pullback.condition_assoc CategoryTheory.IsPushout.toCommSq CategoryTheory.IsPullback.of_hasPullback CategoryTheory.IsPullback.of_right' CategoryTheory.IsPullback.paste_horiz CategoryTheory.IsPullback.lift_fst
flip 📖	mathematical	CategoryTheory.IsPushout CategoryTheory.IsPushout.IsVanKampen	CategoryTheory.IsPushout.IsVanKampen CategoryTheory.IsPushout.flip	—	CategoryTheory.CommSq.flip
isPullback_of_mono_left 📖	mathematical	CategoryTheory.IsPushout CategoryTheory.IsPushout.IsVanKampen	CategoryTheory.IsPullback	—	CategoryTheory.IsPullback.flip CategoryTheory.IsKernelPair.id_of_mono CategoryTheory.IsPullback.of_vert_isIso CategoryTheory.IsIso.id CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.CommSq.flip CategoryTheory.IsPushout.toCommSq CategoryTheory.IsPushout.of_horiz_isIso
isPullback_of_mono_right 📖	mathematical	CategoryTheory.IsPushout CategoryTheory.IsPushout.IsVanKampen	CategoryTheory.IsPullback	—	CategoryTheory.IsPullback.of_vert_isIso CategoryTheory.IsIso.id CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.IsKernelPair.id_of_mono CategoryTheory.IsPushout.toCommSq CategoryTheory.IsPushout.of_vert_isIso
mono_of_mono_left 📖	mathematical	CategoryTheory.IsPushout CategoryTheory.IsPushout.IsVanKampen	CategoryTheory.Mono	—	CategoryTheory.IsKernelPair.mono_of_isIso_fst CategoryTheory.IsKernelPair.id_of_mono CategoryTheory.IsPullback.of_vert_isIso CategoryTheory.IsIso.id CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.CommSq.flip CategoryTheory.IsPushout.toCommSq CategoryTheory.IsPushout.of_horiz_isIso
mono_of_mono_right 📖	mathematical	CategoryTheory.IsPushout CategoryTheory.IsPushout.IsVanKampen	CategoryTheory.Mono	—	CategoryTheory.IsKernelPair.mono_of_isIso_fst CategoryTheory.IsPullback.of_vert_isIso CategoryTheory.IsIso.id CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.IsKernelPair.id_of_mono CategoryTheory.IsPushout.toCommSq CategoryTheory.IsPushout.of_vert_isIso

CategoryTheory.Type

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adhesive 📖	mathematical	—	CategoryTheory.Adhesive CategoryTheory.types	—	CategoryTheory.Limits.Types.hasLimit UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Limits.Types.hasColimit CategoryTheory.IsPushout.IsVanKampen.flip CategoryTheory.IsPushout.flip CategoryTheory.IsPushout.isVanKampen_inl CategoryTheory.types.finitaryExtensive CategoryTheory.Limits.Types.instHasPullbacksType

---

← Back to Index