Adhesive categories #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Main definitions #
category_theory.is_pushout.is_van_kampen: A convenience formulation for a pushout being a van Kampen colimit.category_theory.adhesive: A category is adhesive if it has pushouts and pullbacks along monomorphisms, and such pushouts are van Kampen.
Main Results #
category_theory.type.adhesive: The category ofTypeis adhesive.category_theory.adhesive.is_pullback_of_is_pushout_of_mono_left: In adhesive categories, pushouts along monomorphisms are pullbacks.category_theory.adhesive.mono_of_is_pushout_of_mono_left: In adhesive categories, monomorphisms are stable under pushouts.category_theory.adhesive.to_regular_mono_category: Monomorphisms in adhesive categories are regular (this implies that adhesive categories are balanced).
TODO #
Show that the following are adhesive:
- functor categories into adhesive categories
- the categories of sheaves over a site
References #
@[nolint]
def
category_theory.is_pushout.is_van_kampen
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
(H : category_theory.is_pushout f g h i) :
Prop
A convenience formulation for a pushout being a van Kampen colimit.
See is_pushout.is_van_kampen_iff below.
Equations
- H.is_van_kampen = ∀ ⦃W' X' Y' Z' : C⦄ (f' : W' ⟶ X') (g' : W' ⟶ Y') (h' : X' ⟶ Z') (i' : Y' ⟶ Z') (αW : W' ⟶ W) (αX : X' ⟶ X) (αY : Y' ⟶ Y) (αZ : Z' ⟶ Z), category_theory.is_pullback f' αW αX f → category_theory.is_pullback g' αW αY g → category_theory.comm_sq h' αX αZ h → category_theory.comm_sq i' αY αZ i → category_theory.comm_sq f' g' h' i' → (category_theory.is_pushout f' g' h' i' ↔ category_theory.is_pullback h' αX αZ h ∧ category_theory.is_pullback i' αY αZ i)
theorem
category_theory.is_pushout.is_van_kampen.flip
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
{H : category_theory.is_pushout f g h i}
(H' : H.is_van_kampen) :
theorem
category_theory.is_pushout.is_van_kampen_iff
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
(H : category_theory.is_pushout f g h i) :
theorem
category_theory.is_coprod_iff_is_pushout
{C : Type u}
[category_theory.category C]
{X E Y YE : C}
(c : category_theory.limits.binary_cofan X E)
(hc : category_theory.limits.is_colimit c)
{f : X ⟶ Y}
{iY : Y ⟶ YE}
{fE : c.X ⟶ YE}
(H : category_theory.comm_sq f c.inl iY fE) :
nonempty (category_theory.limits.is_colimit (category_theory.limits.binary_cofan.mk (c.inr ≫ fE) iY)) ↔ category_theory.is_pushout f c.inl iY fE
theorem
category_theory.is_pushout.is_van_kampen_inl
{C : Type u}
[category_theory.category C]
{W E X Z : C}
(c : category_theory.limits.binary_cofan W E)
[category_theory.finitary_extensive C]
[category_theory.limits.has_pullbacks C]
(hc : category_theory.limits.is_colimit c)
(f : W ⟶ X)
(h : X ⟶ Z)
(i : c.X ⟶ Z)
(H : category_theory.is_pushout f c.inl h i) :
theorem
category_theory.is_pushout.is_van_kampen.is_pullback_of_mono_left
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
[category_theory.mono f]
{H : category_theory.is_pushout f g h i}
(H' : H.is_van_kampen) :
category_theory.is_pullback f g h i
theorem
category_theory.is_pushout.is_van_kampen.is_pullback_of_mono_right
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
[category_theory.mono g]
{H : category_theory.is_pushout f g h i}
(H' : H.is_van_kampen) :
category_theory.is_pullback f g h i
theorem
category_theory.is_pushout.is_van_kampen.mono_of_mono_left
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
[category_theory.mono f]
{H : category_theory.is_pushout f g h i}
(H' : H.is_van_kampen) :
theorem
category_theory.is_pushout.is_van_kampen.mono_of_mono_right
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
[category_theory.mono g]
{H : category_theory.is_pushout f g h i}
(H' : H.is_van_kampen) :
@[class]
- has_pullback_of_mono_left : ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [_inst_3_1 : category_theory.mono f], category_theory.limits.has_pullback f g
- has_pushout_of_mono_left : ∀ {X Y S : C} (f : S ⟶ X) (g : S ⟶ Y) [_inst_3_1 : category_theory.mono f], category_theory.limits.has_pushout f g
- van_kampen : ∀ {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} [_inst_3_1 : category_theory.mono f] (H : category_theory.is_pushout f g h i), H.is_van_kampen
A category is adhesive if it has pushouts and pullbacks along monomorphisms, and such pushouts are van Kampen.
Instances of this typeclass
theorem
category_theory.adhesive.van_kampen'
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
[category_theory.adhesive C]
[category_theory.mono g]
(H : category_theory.is_pushout f g h i) :
theorem
category_theory.adhesive.is_pullback_of_is_pushout_of_mono_left
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
[category_theory.adhesive C]
(H : category_theory.is_pushout f g h i)
[category_theory.mono f] :
category_theory.is_pullback f g h i
theorem
category_theory.adhesive.is_pullback_of_is_pushout_of_mono_right
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
[category_theory.adhesive C]
(H : category_theory.is_pushout f g h i)
[category_theory.mono g] :
category_theory.is_pullback f g h i
theorem
category_theory.adhesive.mono_of_is_pushout_of_mono_left
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
[category_theory.adhesive C]
(H : category_theory.is_pushout f g h i)
[category_theory.mono f] :
theorem
category_theory.adhesive.mono_of_is_pushout_of_mono_right
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
[category_theory.adhesive C]
(H : category_theory.is_pushout f g h i)
[category_theory.mono g] :
@[protected, instance]
noncomputable
def
category_theory.adhesive.to_regular_mono_category
{C : Type u}
[category_theory.category C]
[category_theory.adhesive C] :
Equations
- category_theory.adhesive.to_regular_mono_category = {regular_mono_of_mono := λ (X Y : C) (f : X ⟶ Y) (hf : category_theory.mono f), {Z := category_theory.limits.pushout f f _, left := category_theory.limits.pushout.inl _, right := category_theory.limits.pushout.inr _, w := _, is_limit := _.is_limit_fork}}