Basic

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

Statistics

Metric	Count
Definitions IsVanKampen	1
Theorems hasPullback_of_mono_left, hasPushout_of_mono_left, isPullback_of_isPushout_of_mono_left, isPullback_of_isPushout_of_mono_right, mono_of_isPushout_of_mono_left, mono_of_isPushout_of_mono_right, toRegularMonoCategory, van_kampen, van_kampen', flip, isPullback_of_mono_left, isPullback_of_mono_right, mono_of_mono_left, mono_of_mono_right, isVanKampen_iff, isVanKampen_inl, adhesive, adhesive_functor, adhesive_of_preserves_and_reflects, adhesive_of_preserves_and_reflects_isomorphism, adhesive_of_reflective, is_coprod_iff_isPushout	22
Total	23

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 Limits.WalkingPair.right CategoryStruct.comp Category.toCategoryStruct Limits.BinaryCofan.inr IsPushout	—	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
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'
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	4 math math: CategoryTheory.Adhesive.van_kampen, CategoryTheory.Adhesive.van_kampen', 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_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.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

CategoryTheory.IsPushout.IsVanKampen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
flip 📖	mathematical	CategoryTheory.IsPushout 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