# Documentation

## Main definitions #

• CategoryTheory.IsPushout.IsVanKampen: A convenience formulation for a pushout being a van Kampen colimit.
• CategoryTheory.Adhesive: A category is adhesive if it has pushouts and pullbacks along monomorphisms, and such pushouts are van Kampen.

## Main Results #

• CategoryTheory.Type.adhesive: The category of Type is adhesive.
• CategoryTheory.Adhesive.isPullback_of_isPushout_of_mono_left: In adhesive categories, pushouts along monomorphisms are pullbacks.
• CategoryTheory.Adhesive.mono_of_isPushout_of_mono_left: In adhesive categories, monomorphisms are stable under pushouts.
• CategoryTheory.Adhesive.toRegularMonoCategory: Monomorphisms in adhesive categories are regular (this implies that adhesive categories are balanced).
• CategoryTheory.adhesive_functor: The category C ⥤ D is adhesive if D has all pullbacks and all pushouts and is adhesive

## References #

def CategoryTheory.IsPushout.IsVanKampen {C : Type u} {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} :
Prop

A convenience formulation for a pushout being a van Kampen colimit. See IsPushout.isVanKampen_iff below.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.IsPushout.IsVanKampen.flip {C : Type u} {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} {H : } (H' : H.IsVanKampen) :
.IsVanKampen
theorem CategoryTheory.IsPushout.isVanKampen_iff {C : Type u} {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (H : ) :
H.IsVanKampen
theorem CategoryTheory.is_coprod_iff_isPushout {C : Type u} {X : C} {E : C} {Y : C} {YE : C} (c : ) (hc : ) {f : X Y} {iY : Y YE} {fE : c.pt YE} (H : CategoryTheory.CommSq f c.inl iY fE) :
theorem CategoryTheory.IsPushout.isVanKampen_inl {C : Type u} {W : C} {E : C} {X : C} {Z : C} (c : ) (hc : ) (f : W X) (h : X Z) (i : c.pt Z) (H : CategoryTheory.IsPushout f c.inl h i) :
H.IsVanKampen
theorem CategoryTheory.IsPushout.IsVanKampen.isPullback_of_mono_left {C : Type u} {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} {H : } (H' : H.IsVanKampen) :
theorem CategoryTheory.IsPushout.IsVanKampen.isPullback_of_mono_right {C : Type u} {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} {H : } (H' : H.IsVanKampen) :
theorem CategoryTheory.IsPushout.IsVanKampen.mono_of_mono_left {C : Type u} {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} {H : } (H' : H.IsVanKampen) :
theorem CategoryTheory.IsPushout.IsVanKampen.mono_of_mono_right {C : Type u} {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} {H : } (H' : H.IsVanKampen) :

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

• hasPullback_of_mono_left : ∀ {X Y S : C} (f : X S) (g : Y S) [inst : ],
• hasPushout_of_mono_left : ∀ {X Y S : C} (f : S X) (g : S Y) [inst : ],
• van_kampen : ∀ {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} [inst : ] (H : ), H.IsVanKampen
Instances
theorem CategoryTheory.Adhesive.hasPullback_of_mono_left {C : Type u} [self : ] {X : C} {Y : C} {S : C} (f : X S) (g : Y S) :
theorem CategoryTheory.Adhesive.hasPushout_of_mono_left {C : Type u} [self : ] {X : C} {Y : C} {S : C} (f : S X) (g : S Y) :
theorem CategoryTheory.Adhesive.van_kampen {C : Type u} [self : ] {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (H : ) :
H.IsVanKampen
theorem CategoryTheory.Adhesive.van_kampen' {C : Type u} {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (H : ) :
H.IsVanKampen
theorem CategoryTheory.Adhesive.isPullback_of_isPushout_of_mono_left {C : Type u} {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (H : ) :
theorem CategoryTheory.Adhesive.isPullback_of_isPushout_of_mono_right {C : Type u} {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (H : ) :
theorem CategoryTheory.Adhesive.mono_of_isPushout_of_mono_left {C : Type u} {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (H : ) :
theorem CategoryTheory.Adhesive.mono_of_isPushout_of_mono_right {C : Type u} {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (H : ) :
Equations
@[instance 100]
noncomputable instance CategoryTheory.Adhesive.toRegularMonoCategory {C : Type u} :
Equations
• One or more equations did not get rendered due to their size.
instance CategoryTheory.adhesive_functor {C : Type u} {D : Type u''} [] :
Equations
• =
theorem CategoryTheory.adhesive_of_preserves_and_reflects {C : Type u} {D : Type u''} [] (F : ) [H₁ : ∀ {X Y S : C} (f : X S) (g : Y S) [inst : ], ] [H₂ : ∀ {X Y S : C} (f : S X) (g : S Y) [inst : ], ] :
theorem CategoryTheory.adhesive_of_reflective {C : Type u} {D : Type u''} [] [H₂ : ∀ {X Y S : D} (f : S X) (g : S Y) [inst : ], ] {Gl : } {Gr : } (adj : Gl Gr) [Gr.Full] [Gr.Faithful] :