Documentation

Mathlib.CategoryTheory.Adhesive

Adhesive categories #

Main definitions #

Main Results #

References #

def CategoryTheory.IsPushout.IsVanKampen {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} :

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} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} {H : CategoryTheory.IsPushout f g h i} (H' : H.IsVanKampen) :
    .IsVanKampen
    theorem CategoryTheory.IsPushout.isVanKampen_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (H : CategoryTheory.IsPushout f g h i) :
    theorem CategoryTheory.IsPushout.IsVanKampen.isPullback_of_mono_left {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} [CategoryTheory.Mono f] {H : CategoryTheory.IsPushout f g h i} (H' : H.IsVanKampen) :
    theorem CategoryTheory.IsPushout.IsVanKampen.isPullback_of_mono_right {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} [CategoryTheory.Mono g] {H : CategoryTheory.IsPushout f g h i} (H' : H.IsVanKampen) :
    theorem CategoryTheory.IsPushout.IsVanKampen.mono_of_mono_left {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} [CategoryTheory.Mono f] {H : CategoryTheory.IsPushout f g h i} (H' : H.IsVanKampen) :
    theorem CategoryTheory.IsPushout.IsVanKampen.mono_of_mono_right {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} [CategoryTheory.Mono g] {H : CategoryTheory.IsPushout f g h i} (H' : H.IsVanKampen) :

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

    Instances
      theorem CategoryTheory.Adhesive.van_kampen {C : Type u} :
      ∀ {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Adhesive C] {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} [inst_1 : CategoryTheory.Mono f] (H : CategoryTheory.IsPushout f g h i), H.IsVanKampen
      theorem CategoryTheory.Adhesive.van_kampen' {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} [CategoryTheory.Adhesive C] [CategoryTheory.Mono g] (H : CategoryTheory.IsPushout f g h i) :
      H.IsVanKampen
      @[instance 100]
      Equations
      • One or more equations did not get rendered due to their size.