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 ofTypeis 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 categoryC ⥤ Dis adhesive ifDhas 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 : C}
{X : C}
{Y : C}
{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 : 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)
:
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 : C}
{E : C}
{Y : C}
{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 : C}
{E : C}
{X : C}
{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 : 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)
:
CategoryTheory.IsPullback f g h i
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)
:
CategoryTheory.IsPullback f g h i
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.
- 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.hasPullback_of_mono_left
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[self : CategoryTheory.Adhesive C]
{X : C}
{Y : C}
{S : C}
(f : X ⟶ S)
(g : Y ⟶ S)
[CategoryTheory.Mono f]
:
theorem
CategoryTheory.Adhesive.hasPushout_of_mono_left
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[self : CategoryTheory.Adhesive C]
{X : C}
{Y : C}
{S : C}
(f : S ⟶ X)
(g : S ⟶ Y)
[CategoryTheory.Mono f]
:
theorem
CategoryTheory.Adhesive.van_kampen
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[self : CategoryTheory.Adhesive 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.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
theorem
CategoryTheory.Adhesive.isPullback_of_isPushout_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.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 : C}
{X : C}
{Y : C}
{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 : C}
{X : C}
{Y : C}
{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]
:
theorem
CategoryTheory.Adhesive.mono_of_isPushout_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.Adhesive C]
(H : CategoryTheory.IsPushout f g h i)
[CategoryTheory.Mono g]
:
Equations
@[instance 100]
noncomputable instance
CategoryTheory.Adhesive.toRegularMonoCategory
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Adhesive 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]
:
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]
:
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]
:
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]
: