mathlib documentation

category_theory.adhesive

Adhesive categories #

Main definitions #

Main Results #

TODO #

Show that the following are adhesive:

References #

@[nolint]
def category_theory.is_pushout.is_van_kampen {C : Type u} [category_theory.category C] {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (H : category_theory.is_pushout f g 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} [category_theory.category C] {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} {H : category_theory.is_pushout f g h i} (H' : H.is_van_kampen) :
@[class]

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} [category_theory.category C] {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} [category_theory.adhesive C] [category_theory.mono g] (H : category_theory.is_pushout f g h i) :