# mathlib3documentation

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

## Main definitions #

• category_theory.is_pushout.is_van_kampen: A convenience formulation for a pushout being a van Kampen colimit.
• category_theory.adhesive: A category is adhesive if it has pushouts and pullbacks along monomorphisms, and such pushouts are van Kampen.

## Main Results #

• category_theory.type.adhesive: The category of Type is adhesive.
• category_theory.adhesive.is_pullback_of_is_pushout_of_mono_left: In adhesive categories, pushouts along monomorphisms are pullbacks.
• category_theory.adhesive.mono_of_is_pushout_of_mono_left: In adhesive categories, monomorphisms are stable under pushouts.
• category_theory.adhesive.to_regular_mono_category: Monomorphisms in adhesive categories are regular (this implies that adhesive categories are balanced).

## TODO #

Show that the following are adhesive:

• functor categories into adhesive categories
• the categories of sheaves over a site

## References #

@[nolint]
def category_theory.is_pushout.is_van_kampen {C : Type u} {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (H : i) :
Prop

A convenience formulation for a pushout being a van Kampen colimit. See is_pushout.is_van_kampen_iff below.

Equations
theorem category_theory.is_pushout.is_van_kampen.flip {C : Type u} {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} {H : i} (H' : H.is_van_kampen) :
theorem category_theory.is_pushout.is_van_kampen_iff {C : Type u} {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (H : i) :
theorem category_theory.is_coprod_iff_is_pushout {C : Type u} {X E Y YE : C} {f : X Y} {iY : Y YE} {fE : c.X YE} (H : iY fE) :
fE
theorem category_theory.is_pushout.is_van_kampen_inl {C : Type u} {W E X Z : C} (f : W X) (h : X Z) (i : c.X Z) (H : i) :
theorem category_theory.is_pushout.is_van_kampen.is_pullback_of_mono_left {C : Type u} {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} {H : i} (H' : H.is_van_kampen) :
i
theorem category_theory.is_pushout.is_van_kampen.is_pullback_of_mono_right {C : Type u} {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} {H : i} (H' : H.is_van_kampen) :
i
theorem category_theory.is_pushout.is_van_kampen.mono_of_mono_left {C : Type u} {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} {H : i} (H' : H.is_van_kampen) :
theorem category_theory.is_pushout.is_van_kampen.mono_of_mono_right {C : Type u} {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} {H : i} (H' : H.is_van_kampen) :
@[class]
structure category_theory.adhesive (C : Type u)  :
Prop
• has_pullback_of_mono_left : {X Y S : C} (f : X S) (g : Y S) [_inst_3_1 : ,
• has_pushout_of_mono_left : {X Y S : C} (f : S X) (g : S Y) [_inst_3_1 : ,
• van_kampen : {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} [_inst_3_1 : (H : i), H.is_van_kampen

A category is adhesive if it has pushouts and pullbacks along monomorphisms, and such pushouts are van Kampen.

Instances of this typeclass
theorem category_theory.adhesive.van_kampen' {C : Type u} {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (H : i) :
theorem category_theory.adhesive.is_pullback_of_is_pushout_of_mono_left {C : Type u} {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (H : i)  :
i
theorem category_theory.adhesive.is_pullback_of_is_pushout_of_mono_right {C : Type u} {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (H : i)  :
i
theorem category_theory.adhesive.mono_of_is_pushout_of_mono_left {C : Type u} {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (H : i)  :
theorem category_theory.adhesive.mono_of_is_pushout_of_mono_right {C : Type u} {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (H : i)  :
@[protected, instance]
@[protected, instance]
Equations