Structures · Category theory
CategoryTheory.Adhesive
A category is adhesive if it has pushouts and pullbacks along monomorphisms, and such pushouts are van Kampen.
- Defined in
- Mathlib.CategoryTheory.Adhesive.Basic
- Shape
- One type argument · adds hasPullback_of_mono_left, hasPushout_of_mono_left, van_kampen
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances3
- CategoryTheory.Functor
- CategoryTheory.Over
- CategoryTheory.Sheaf
How is a type an instance?
Loading the hierarchy index…
Assumed by19
- CategoryTheory.Adhesive.van_kampen
- CategoryTheory.Adhesive.van_kampen'
- CategoryTheory.adhesive_of_preserves_and_reflects
- CategoryTheory.adhesive_of_preserves_and_reflects_isomorphism
- CategoryTheory.Adhesive.desc_mono_of_mono
- CategoryTheory.Adhesive.isPullback_of_isPushout_of_mono_left
- CategoryTheory.Adhesive.mono_of_isPushout_of_mono_left
- CategoryTheory.Adhesive.hasPushout_of_mono_left
- CategoryTheory.Adhesive.isPushout_isPullback_isPullback_hom_ext
- CategoryTheory.Adhesive.mono_of_isPushout_of_mono_right
- CategoryTheory.Adhesive.isPullback_of_isPushout_of_mono_right
- CategoryTheory.adhesive_over
- CategoryTheory.instAdhesiveSheafOfHasPullbacksOfHasPushoutsOfHasSheafify
- CategoryTheory.Adhesive.hasPullback_of_mono_left
- CategoryTheory.Adhesive.toRegularMonoCategory
- CategoryTheory.Adhesive.instHasBinaryCoproductsSubobject
- CategoryTheory.adhesive_functor
- CategoryTheory.Adhesive.isColimitBinaryCofan
- CategoryTheory.adhesive_of_reflective
Ancestors0
No ancestors.