Documentation

Mathlib.CategoryTheory.Adhesive

Adhesive categories #

Main definitions #

Main Results #

References #

source
def CategoryTheory.IsPushout.IsVanKampen {C : Type u} [Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} :
IsPushout f g h i → 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
    source
    theorem CategoryTheory.IsPushout.IsVanKampen.flip {C : Type u} [Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} {H : IsPushout f g h i} (H' : H.IsVanKampen) :
    ⋯.IsVanKampen
    source
    theorem CategoryTheory.IsPushout.isVanKampen_iff {C : Type u} [Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} (H : IsPushout f g h i) :
    H.IsVanKampen ↔ IsVanKampenColimit (Limits.PushoutCocone.mk h i ⋯)
    source
    theorem CategoryTheory.is_coprod_iff_isPushout {C : Type u} [Category.{v, u} C] {X E Y YE : C} (c : Limits.BinaryCofan X E) (hc : Limits.IsColimit c) {f : X ⟶ Y} {iY : Y ⟶ YE} {fE : c.pt ⟶ YE} (H : CommSq f c.inl iY fE) :
    Nonempty (Limits.IsColimit (Limits.BinaryCofan.mk (CategoryStruct.comp c.inr fE) iY)) ↔ IsPushout f c.inl iY fE
    source
    theorem CategoryTheory.IsPushout.isVanKampen_inl {C : Type u} [Category.{v, u} C] {W E X Z : C} (c : Limits.BinaryCofan W E) [FinitaryExtensive C] [Limits.HasPullbacks C] (hc : Limits.IsColimit c) (f : W ⟶ X) (h : X ⟶ Z) (i : c.pt ⟶ Z) (H : IsPushout f c.inl h i) :
    H.IsVanKampen
    source
    theorem CategoryTheory.IsPushout.IsVanKampen.isPullback_of_mono_left {C : Type u} [Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} [Mono f] {H : IsPushout f g h i} (H' : H.IsVanKampen) :
    IsPullback f g h i
    source
    theorem CategoryTheory.IsPushout.IsVanKampen.isPullback_of_mono_right {C : Type u} [Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} [Mono g] {H : IsPushout f g h i} (H' : H.IsVanKampen) :
    IsPullback f g h i
    source
    theorem CategoryTheory.IsPushout.IsVanKampen.mono_of_mono_left {C : Type u} [Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} [Mono f] {H : IsPushout f g h i} (H' : H.IsVanKampen) :
    Mono i
    source
    theorem CategoryTheory.IsPushout.IsVanKampen.mono_of_mono_right {C : Type u} [Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} [Mono g] {H : IsPushout f g h i} (H' : H.IsVanKampen) :
    Mono h
    source
    class CategoryTheory.Adhesive (C : Type u) [Category.{v, u} C] :
    Prop

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

    Instances
      source
      theorem CategoryTheory.Adhesive.van_kampen' {C : Type u} [Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} [Adhesive C] [Mono g] (H : IsPushout f g h i) :
      H.IsVanKampen
      source
      theorem CategoryTheory.Adhesive.isPullback_of_isPushout_of_mono_left {C : Type u} [Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} [Adhesive C] (H : IsPushout f g h i) [Mono f] :
      IsPullback f g h i
      source
      theorem CategoryTheory.Adhesive.isPullback_of_isPushout_of_mono_right {C : Type u} [Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} [Adhesive C] (H : IsPushout f g h i) [Mono g] :
      IsPullback f g h i
      source
      theorem CategoryTheory.Adhesive.mono_of_isPushout_of_mono_left {C : Type u} [Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} [Adhesive C] (H : IsPushout f g h i) [Mono f] :
      Mono i
      source
      theorem CategoryTheory.Adhesive.mono_of_isPushout_of_mono_right {C : Type u} [Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} [Adhesive C] (H : IsPushout f g h i) [Mono g] :
      Mono h
      source
      instance CategoryTheory.Type.adhesive :
      Adhesive (Type u)
      source
      @[instance 100]
      instance CategoryTheory.Adhesive.toRegularMonoCategory {C : Type u} [Category.{v, u} C] [Adhesive C] :
      IsRegularMonoCategory C
      source
      instance CategoryTheory.adhesive_functor {C : Type u} [Category.{v, u} C] {D : Type u''} [Category.{v'', u''} D] [Adhesive C] [Limits.HasPullbacks C] [Limits.HasPushouts C] :
      Adhesive (Functor D C)
      source
      theorem CategoryTheory.adhesive_of_preserves_and_reflects {C : Type u} [Category.{v, u} C] {D : Type u''} [Category.{v'', u''} D] (F : Functor C D) [Adhesive D] [H₁ : ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst : Mono f], Limits.HasPullback f g] [H₂ : ∀ {X Y S : C} (f : S ⟶ X) (g : S ⟶ Y) [inst : Mono f], Limits.HasPushout f g] [Limits.PreservesLimitsOfShape Limits.WalkingCospan F] [Limits.ReflectsLimitsOfShape Limits.WalkingCospan F] [Limits.PreservesColimitsOfShape Limits.WalkingSpan F] [Limits.ReflectsColimitsOfShape Limits.WalkingSpan F] :
      Adhesive C
      source
      theorem CategoryTheory.adhesive_of_preserves_and_reflects_isomorphism {C : Type u} [Category.{v, u} C] {D : Type u''} [Category.{v'', u''} D] (F : Functor C D) [Adhesive D] [Limits.HasPullbacks C] [Limits.HasPushouts C] [Limits.PreservesLimitsOfShape Limits.WalkingCospan F] [Limits.PreservesColimitsOfShape Limits.WalkingSpan F] [F.ReflectsIsomorphisms] :
      Adhesive C
      source
      theorem CategoryTheory.adhesive_of_reflective {C : Type u} [Category.{v, u} C] {D : Type u''} [Category.{v'', u''} D] [Limits.HasPullbacks D] [Adhesive C] [Limits.HasPullbacks C] [Limits.HasPushouts C] [H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [inst : Mono f], Limits.HasPushout f g] {Gl : Functor C D} {Gr : Functor D C} (adj : Gl ⊣ Gr) [Gr.Full] [Gr.Faithful] [Limits.PreservesLimitsOfShape Limits.WalkingCospan Gl] :
      Adhesive D