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}
[Category.{v, u} C]
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
:
A convenient formulation for a pushout being a van Kampen colimit. For any commutative cube of
which a van Kampen pushout forms the bottom face and the back faces are pullbacks, the front faces
are pullbacks if and only if the top face is a pushout. See IsPushout.isVanKampen_iff below.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.IsPushout.IsVanKampen.exists_cube_filling
{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)
{X' Y' Z' : C}
{h' : X' ⟶ Z'}
{i' : Y' ⟶ Z'}
{αX : X' ⟶ X}
{αY : Y' ⟶ Y}
{αZ : Z' ⟶ Z}
[Limits.HasPullback αX f]
(hh : IsPullback h' αX αZ h)
(hi : IsPullback i' αY αZ i)
:
∃ (W' : C) (f' : W' ⟶ X') (g' : W' ⟶ Y') (αW : W' ⟶ W),
IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' h' i'
If a van Kampem pushout forms the bottom face of a commutative "half-cube" whose front faces are pullbacks, then there exist two back faces which are pullbacks and a top face which is a pushout.
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)
:
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)
:
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 ↔ ∀ ⦃X' Y' Z' : C⦄ (h' : X' ⟶ Z') (i' : Y' ⟶ Z') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (αZ : Z' ⟶ Z),
CommSq h' αX αZ h →
CommSq i' αY αZ i →
∀ [Limits.HasPullback αX f],
IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i ↔ ∃ (W' : C) (f' : W' ⟶ X') (g' : W' ⟶ Y') (αW : W' ⟶ W),
IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' h' i'
A pushout is van Kampen if and only if whenever it forms the bottom face of a commutative "half-cube", the front faces are pullbacks if and only if there exist back faces which are pullbacks and a top face which is a pushout.
theorem
CategoryTheory.IsPushout.isVanKampen_isPullback_isPullback_hom_ext
{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)
{X' Y' Z' : C}
{h' : X' ⟶ Z'}
{i' : Y' ⟶ Z'}
{αX : X' ⟶ X}
[Limits.HasPullback αX f]
{αY : Y' ⟶ Y}
{αZ : Z' ⟶ Z}
{W✝ : C}
{f₁ f₂ : Z' ⟶ W✝}
(hh : IsPullback h' αX αZ h)
(hi : IsPullback i' αY αZ i)
(h'_w : CategoryStruct.comp h' f₁ = CategoryStruct.comp h' f₂)
(i'_w : CategoryStruct.comp i' f₁ = CategoryStruct.comp i' f₂)
:
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
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)
:
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
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
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
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
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}
[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)
:
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
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
theorem
CategoryTheory.Adhesive.isPushout_isPullback_isPullback_hom_ext
{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 f]
(H : IsPushout f g h i)
{X' Y' Z' : C}
{h' : X' ⟶ Z'}
{i' : Y' ⟶ Z'}
{αX : X' ⟶ X}
{αY : Y' ⟶ Y}
{αZ : Z' ⟶ Z}
{W✝ : C}
{f₁ f₂ : Z' ⟶ W✝}
(hh : IsPullback h' αX αZ h)
(hi : IsPullback i' αY αZ i)
(h'_w : CategoryStruct.comp h' f₁ = CategoryStruct.comp h' f₂)
(i'_w : CategoryStruct.comp i' f₁ = CategoryStruct.comp i' f₂)
:
instance
CategoryTheory.Adhesive.desc_mono_of_mono
{C : Type u}
[Category.{v, u} C]
[Adhesive C]
{Z A B : C}
{a : A ⟶ Z}
{b : B ⟶ Z}
[Mono a]
[Mono b]
:
Mono (Limits.pushout.desc a b ⋯)
If a : A ⟶ Z and b : B ⟶ Z are monomorphisms in an adhesive category, then the map
pushout (pullback.fst a b) (pullback.snd a b) ⟶ Z induced by their pullback is a monomorphism.
See Theorem 5.1 in Lack and Sobociński.
@[instance 100]
instance
CategoryTheory.Adhesive.toRegularMonoCategory
{C : Type u}
[Category.{v, u} C]
[Adhesive C]
:
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]
:
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) [Mono f], Limits.HasPullback f g]
[H₂ : ∀ {X Y S : C} (f : S ⟶ X) (g : S ⟶ Y) [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
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
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) [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