Documentation

Mathlib.CategoryTheory.Adhesive

Adhesive categories #

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 #

https://ncatlab.org/nlab/show/adhesive+category
[Stephen Lack and Paweł Sobociński, Adhesive Categories][adhesive2004]

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

CategoryTheory.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

theorem CategoryTheory.IsPushout.IsVanKampen.flip {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y 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 X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} (H : CategoryTheory.IsPushout f g h i) :

H.IsVanKampen ↔ CategoryTheory.IsVanKampenColimit (CategoryTheory.Limits.PushoutCocone.mk h i ⋯)

theorem CategoryTheory.is_coprod_iff_isPushout {C : Type u} [CategoryTheory.Category.{v, u} C] {X E Y YE : C} (c : CategoryTheory.Limits.BinaryCofan X E) (hc : CategoryTheory.Limits.IsColimit c) {f : X ⟶ Y} {iY : Y ⟶ YE} {fE : c.pt ⟶ YE} (H : CategoryTheory.CommSq f c.inl iY fE) :

Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk (CategoryTheory.CategoryStruct.comp c.inr fE) iY)) ↔ CategoryTheory.IsPushout f c.inl iY fE

theorem CategoryTheory.IsPushout.isVanKampen_inl {C : Type u} [CategoryTheory.Category.{v, u} C] {W E X Z : C} (c : CategoryTheory.Limits.BinaryCofan W E) [CategoryTheory.FinitaryExtensive C] [CategoryTheory.Limits.HasPullbacks C] (hc : CategoryTheory.Limits.IsColimit c) (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} [CategoryTheory.Category.{v, u} C] {W X Y 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) :

CategoryTheory.IsPullback f g h i

theorem CategoryTheory.IsPushout.IsVanKampen.isPullback_of_mono_right {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y 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) :

CategoryTheory.IsPullback f g h i

theorem CategoryTheory.IsPushout.IsVanKampen.mono_of_mono_left {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y 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) :

CategoryTheory.Mono i

theorem CategoryTheory.IsPushout.IsVanKampen.mono_of_mono_right {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y 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) :

CategoryTheory.Mono h

class CategoryTheory.Adhesive (C : Type u) [CategoryTheory.Category.{v, u} C] :

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 : CategoryTheory.Mono f], CategoryTheory.Limits.HasPullback f g
hasPushout_of_mono_left : ∀ {X Y S : C} (f : S ⟶ X) (g : S ⟶ Y) [inst : CategoryTheory.Mono f], CategoryTheory.Limits.HasPushout f g
van_kampen : ∀ {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} [inst : CategoryTheory.Mono f] (H : CategoryTheory.IsPushout f g h i), H.IsVanKampen

Instances

theorem CategoryTheory.Adhesive.van_kampen' {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y 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

theorem CategoryTheory.Adhesive.isPullback_of_isPushout_of_mono_left {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} [CategoryTheory.Adhesive C] (H : CategoryTheory.IsPushout f g h i) [CategoryTheory.Mono f] :

CategoryTheory.IsPullback f g h i

theorem CategoryTheory.Adhesive.isPullback_of_isPushout_of_mono_right {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} [CategoryTheory.Adhesive C] (H : CategoryTheory.IsPushout f g h i) [CategoryTheory.Mono g] :

CategoryTheory.IsPullback f g h i

theorem CategoryTheory.Adhesive.mono_of_isPushout_of_mono_left {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} [CategoryTheory.Adhesive C] (H : CategoryTheory.IsPushout f g h i) [CategoryTheory.Mono f] :

CategoryTheory.Mono i

theorem CategoryTheory.Adhesive.mono_of_isPushout_of_mono_right {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} [CategoryTheory.Adhesive C] (H : CategoryTheory.IsPushout f g h i) [CategoryTheory.Mono g] :

CategoryTheory.Mono h

instance CategoryTheory.Type.adhesive :

CategoryTheory.Adhesive (Type u)

Equations

CategoryTheory.Type.adhesive = ⋯

@[instance 100]

noncomputable instance CategoryTheory.Adhesive.toRegularMonoCategory {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Adhesive C] :

CategoryTheory.RegularMonoCategory C

Equations

One or more equations did not get rendered due to their size.

instance CategoryTheory.adhesive_functor {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u''} [CategoryTheory.Category.{v'', u''} D] [CategoryTheory.Adhesive C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasPushouts C] :

CategoryTheory.Adhesive (CategoryTheory.Functor D C)

Equations

⋯ = ⋯

theorem CategoryTheory.adhesive_of_preserves_and_reflects {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u''} [CategoryTheory.Category.{v'', u''} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Adhesive D] [H₁ : ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst : CategoryTheory.Mono f], CategoryTheory.Limits.HasPullback f g] [H₂ : ∀ {X Y S : C} (f : S ⟶ X) (g : S ⟶ Y) [inst : CategoryTheory.Mono f], CategoryTheory.Limits.HasPushout f g] [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F] [CategoryTheory.Limits.ReflectsLimitsOfShape CategoryTheory.Limits.WalkingCospan F] [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingSpan F] [CategoryTheory.Limits.ReflectsColimitsOfShape CategoryTheory.Limits.WalkingSpan F] :

CategoryTheory.Adhesive C

theorem CategoryTheory.adhesive_of_preserves_and_reflects_isomorphism {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u''} [CategoryTheory.Category.{v'', u''} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Adhesive D] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F] [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingSpan F] [F.ReflectsIsomorphisms] :

CategoryTheory.Adhesive C

theorem CategoryTheory.adhesive_of_reflective {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u''} [CategoryTheory.Category.{v'', u''} D] [CategoryTheory.Limits.HasPullbacks D] [CategoryTheory.Adhesive C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasPushouts C] [H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [inst : CategoryTheory.Mono f], CategoryTheory.Limits.HasPushout f g] {Gl : CategoryTheory.Functor C D} {Gr : CategoryTheory.Functor D C} (adj : Gl ⊣ Gr) [Gr.Full] [Gr.Faithful] [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan Gl] :

CategoryTheory.Adhesive D