mathlib documentation

category_theory.limits.shapes.reflexive

Reflexive coequalizers #

We define reflexive pairs as a pair of morphisms which have a common section. We say a category has reflexive coequalizers if it has coequalizers of all reflexive pairs. Reflexive coequalizers often enjoy nicer properties than general coequalizers, and feature heavily in some versions of the monadicity theorem.

We also give some examples of reflexive pairs: for an adjunction F ⊣ G with counit ε, the pair (FGε_B, ε_FGB) is reflexive. If a pair f,g is a kernel pair for some morphism, then it is reflexive.

TODO #

@[class]
structure category_theory.is_reflexive_pair {C : Type u} [category_theory.category C] {A B : C} (f g : A B) :
Prop

The pair f g : A ⟶ B is reflexive if there is a morphism B ⟶ A which is a section for both.

Instances
@[class]
structure category_theory.is_coreflexive_pair {C : Type u} [category_theory.category C] {A B : C} (f g : A B) :
Prop

The pair f g : A ⟶ B is coreflexive if there is a morphism B ⟶ A which is a retraction for both.

theorem category_theory.is_reflexive_pair.mk' {C : Type u} [category_theory.category C] {A B : C} {f g : A B} (s : B A) (sf : s f = 𝟙 B) (sg : s g = 𝟙 B) :
theorem category_theory.is_coreflexive_pair.mk' {C : Type u} [category_theory.category C] {A B : C} {f g : A B} (s : B A) (fs : f s = 𝟙 A) (gs : g s = 𝟙 A) :
def category_theory.common_section {C : Type u} [category_theory.category C] {A B : C} (f g : A B) [category_theory.is_reflexive_pair f g] :
B A

Get the common section for a reflexive pair.

Equations
@[simp]
theorem category_theory.section_comp_left_assoc {C : Type u} [category_theory.category C] {A B : C} (f g : A B) [category_theory.is_reflexive_pair f g] {X' : C} (f' : B X') :
@[simp]
theorem category_theory.section_comp_right_assoc {C : Type u} [category_theory.category C] {A B : C} (f g : A B) [category_theory.is_reflexive_pair f g] {X' : C} (f' : B X') :

Get the common retraction for a coreflexive pair.

Equations
@[simp]
theorem category_theory.left_comp_retraction_assoc {C : Type u} [category_theory.category C] {A B : C} (f g : A B) [category_theory.is_coreflexive_pair f g] {X' : C} (f' : A X') :
@[simp]
theorem category_theory.right_comp_retraction_assoc {C : Type u} [category_theory.category C] {A B : C} (f g : A B) [category_theory.is_coreflexive_pair f g] {X' : C} (f' : A X') :

If f,g is a kernel pair for some morphism q, then it is reflexive.

If f,g is reflexive, then g,f is reflexive.

If f,g is coreflexive, then g,f is coreflexive.

@[instance]
def category_theory.app.is_reflexive_pair {C : Type u} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G : D C} (adj : F G) (B : D) :

For an adjunction F ⊣ G with counit ε, the pair (FGε_B, ε_FGB) is reflexive.

@[class]

C has reflexive coequalizers if it has coequalizers for every reflexive pair.

Instances
@[class]

C has coreflexive equalizers if it has equalizers for every coreflexive pair.

Instances