mathlib3 documentation

category_theory.limits.shapes.reflexive

Reflexive coequalizers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

If C has binary coproducts and reflexive coequalizers, then it has all coequalizers.
If T is a monad on cocomplete category C, then algebra T is cocomplete iff it has reflexive coequalizers.
If C is locally cartesian closed and has reflexive coequalizers, then it has images: in fact regular epi (and hence strong epi) images.

@[class]

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

Prop

common_section : ∃ (s : B ⟶ A), s ≫ f = 𝟙 B ∧ s ≫ g = 𝟙 B

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

Instances of this typeclass

@[class]

structure category_theory.is_coreflexive_pair {C : Type u} [category_theory.category C] {A B : C} (f g : A ⟶ B) :

Prop

common_retraction : ∃ (s : B ⟶ A), f ≫ s = 𝟙 A ∧ g ≫ s = 𝟙 A

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) :

category_theory.is_reflexive_pair f g

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) :

category_theory.is_coreflexive_pair f g

noncomputable 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

category_theory.common_section f g = _.some

@[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') :

category_theory.common_section f g ≫ f ≫ f' = f'

@[simp]

theorem category_theory.section_comp_left {C : Type u} [category_theory.category C] {A B : C} (f g : A ⟶ B) [category_theory.is_reflexive_pair f g] :

category_theory.common_section f g ≫ f = 𝟙 B

@[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') :

category_theory.common_section f g ≫ g ≫ f' = f'

@[simp]

theorem category_theory.section_comp_right {C : Type u} [category_theory.category C] {A B : C} (f g : A ⟶ B) [category_theory.is_reflexive_pair f g] :

category_theory.common_section f g ≫ g = 𝟙 B

noncomputable def category_theory.common_retraction {C : Type u} [category_theory.category C] {A B : C} (f g : A ⟶ B) [category_theory.is_coreflexive_pair f g] :

B ⟶ A

Get the common retraction for a coreflexive pair.

Equations

category_theory.common_retraction f g = _.some

@[simp]

theorem category_theory.left_comp_retraction {C : Type u} [category_theory.category C] {A B : C} (f g : A ⟶ B) [category_theory.is_coreflexive_pair f g] :

f ≫ category_theory.common_retraction f g = 𝟙 A

@[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') :

f ≫ category_theory.common_retraction f g ≫ f' = f'

@[simp]

theorem category_theory.right_comp_retraction {C : Type u} [category_theory.category C] {A B : C} (f g : A ⟶ B) [category_theory.is_coreflexive_pair f g] :

g ≫ category_theory.common_retraction f g = 𝟙 A

@[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') :

g ≫ category_theory.common_retraction f g ≫ f' = f'

theorem category_theory.is_kernel_pair.is_reflexive_pair {C : Type u} [category_theory.category C] {A B R : C} {f g : R ⟶ A} {q : A ⟶ B} (h : category_theory.is_kernel_pair q f g) :

category_theory.is_reflexive_pair f g

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

theorem category_theory.is_reflexive_pair.swap {C : Type u} [category_theory.category C] {A B : C} {f g : A ⟶ B} [category_theory.is_reflexive_pair f g] :

category_theory.is_reflexive_pair g f

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

theorem category_theory.is_coreflexive_pair.swap {C : Type u} [category_theory.category C] {A B : C} {f g : A ⟶ B} [category_theory.is_coreflexive_pair f g] :

category_theory.is_coreflexive_pair g f

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

@[protected, 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) :

category_theory.is_reflexive_pair (F.map (G.map (adj.counit.app B))) (adj.counit.app (F.obj (G.obj B)))

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

@[class]

structure category_theory.limits.has_reflexive_coequalizers (C : Type u) [category_theory.category C] :

Prop

has_coeq : ∀ ⦃A B : C⦄ (f g : A ⟶ B) [_inst_3 : category_theory.is_reflexive_pair f g], category_theory.limits.has_coequalizer f g

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

Instances of this typeclass

category_theory.limits.has_reflexive_coequalizers_of_has_coequalizers

@[class]

structure category_theory.limits.has_coreflexive_equalizers (C : Type u) [category_theory.category C] :

Prop

has_eq : ∀ ⦃A B : C⦄ (f g : A ⟶ B) [_inst_3 : category_theory.is_coreflexive_pair f g], category_theory.limits.has_equalizer f g

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

Instances of this typeclass

category_theory.limits.has_coreflexive_equalizers_of_has_equalizers

theorem category_theory.limits.has_coequalizer_of_common_section (C : Type u) [category_theory.category C] [category_theory.limits.has_reflexive_coequalizers C] {A B : C} {f g : A ⟶ B} (r : B ⟶ A) (rf : r ≫ f = 𝟙 B) (rg : r ≫ g = 𝟙 B) :

category_theory.limits.has_coequalizer f g

theorem category_theory.limits.has_equalizer_of_common_retraction (C : Type u) [category_theory.category C] [category_theory.limits.has_coreflexive_equalizers C] {A B : C} {f g : A ⟶ B} (r : B ⟶ A) (fr : f ≫ r = 𝟙 A) (gr : g ≫ r = 𝟙 A) :

category_theory.limits.has_equalizer f g

@[protected, instance]

def category_theory.limits.has_reflexive_coequalizers_of_has_coequalizers (C : Type u) [category_theory.category C] [category_theory.limits.has_coequalizers C] :

category_theory.limits.has_reflexive_coequalizers C

If C has coequalizers, then it has reflexive coequalizers.

@[protected, instance]

def category_theory.limits.has_coreflexive_equalizers_of_has_equalizers (C : Type u) [category_theory.category C] [category_theory.limits.has_equalizers C] :

category_theory.limits.has_coreflexive_equalizers C

If C has equalizers, then it has coreflexive equalizers.