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 #
- If
Chas binary coproducts and reflexive coequalizers, then it has all coequalizers. - If
Tis a monad on cocomplete categoryC, thenAlgebra Tis cocomplete iff it has reflexive coequalizers. - If
Cis locally cartesian closed and has reflexive coequalizers, then it has images: in fact regular epi (and hence strong epi) images.
class
CategoryTheory.IsReflexivePair
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{B : C}
(f : A ⟶ B)
(g : A ⟶ B)
:
The pair f g : A ⟶ B is reflexive if there is a morphism B ⟶ A which is a section for both.
- common_section' : ∃ (s : B ⟶ A), CategoryTheory.CategoryStruct.comp s f = CategoryTheory.CategoryStruct.id B ∧ CategoryTheory.CategoryStruct.comp s g = CategoryTheory.CategoryStruct.id B
Instances
theorem
CategoryTheory.IsReflexivePair.common_section'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{B : C}
{f : A ⟶ B}
{g : A ⟶ B}
[self : CategoryTheory.IsReflexivePair f g]
:
theorem
CategoryTheory.IsReflexivePair.common_section
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{B : C}
(f : A ⟶ B)
(g : A ⟶ B)
[CategoryTheory.IsReflexivePair f g]
:
class
CategoryTheory.IsCoreflexivePair
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{B : C}
(f : A ⟶ B)
(g : A ⟶ B)
:
The pair f g : A ⟶ B is coreflexive if there is a morphism B ⟶ A which is a retraction for both.
- common_retraction' : ∃ (s : B ⟶ A), CategoryTheory.CategoryStruct.comp f s = CategoryTheory.CategoryStruct.id A ∧ CategoryTheory.CategoryStruct.comp g s = CategoryTheory.CategoryStruct.id A
Instances
theorem
CategoryTheory.IsCoreflexivePair.common_retraction'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{B : C}
{f : A ⟶ B}
{g : A ⟶ B}
[self : CategoryTheory.IsCoreflexivePair f g]
:
theorem
CategoryTheory.IsCoreflexivePair.common_retraction
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{B : C}
(f : A ⟶ B)
(g : A ⟶ B)
[CategoryTheory.IsCoreflexivePair f g]
:
theorem
CategoryTheory.IsReflexivePair.mk'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{B : C}
{f : A ⟶ B}
{g : A ⟶ B}
(s : B ⟶ A)
(sf : CategoryTheory.CategoryStruct.comp s f = CategoryTheory.CategoryStruct.id B)
(sg : CategoryTheory.CategoryStruct.comp s g = CategoryTheory.CategoryStruct.id B)
:
theorem
CategoryTheory.IsCoreflexivePair.mk'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{B : C}
{f : A ⟶ B}
{g : A ⟶ B}
(s : B ⟶ A)
(fs : CategoryTheory.CategoryStruct.comp f s = CategoryTheory.CategoryStruct.id A)
(gs : CategoryTheory.CategoryStruct.comp g s = CategoryTheory.CategoryStruct.id A)
:
noncomputable def
CategoryTheory.commonSection
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{B : C}
(f : A ⟶ B)
(g : A ⟶ B)
[CategoryTheory.IsReflexivePair f g]
:
B ⟶ A
Get the common section for a reflexive pair.
Equations
- CategoryTheory.commonSection f g = ⋯.choose
Instances For
@[simp]
theorem
CategoryTheory.section_comp_left_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{B : C}
(f : A ⟶ B)
(g : A ⟶ B)
[CategoryTheory.IsReflexivePair f g]
{Z : C}
(h : B ⟶ Z)
:
@[simp]
theorem
CategoryTheory.section_comp_left
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{B : C}
(f : A ⟶ B)
(g : A ⟶ B)
[CategoryTheory.IsReflexivePair f g]
:
@[simp]
theorem
CategoryTheory.section_comp_right_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{B : C}
(f : A ⟶ B)
(g : A ⟶ B)
[CategoryTheory.IsReflexivePair f g]
{Z : C}
(h : B ⟶ Z)
:
@[simp]
theorem
CategoryTheory.section_comp_right
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{B : C}
(f : A ⟶ B)
(g : A ⟶ B)
[CategoryTheory.IsReflexivePair f g]
:
noncomputable def
CategoryTheory.commonRetraction
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{B : C}
(f : A ⟶ B)
(g : A ⟶ B)
[CategoryTheory.IsCoreflexivePair f g]
:
B ⟶ A
Get the common retraction for a coreflexive pair.
Equations
- CategoryTheory.commonRetraction f g = ⋯.choose
Instances For
@[simp]
theorem
CategoryTheory.left_comp_retraction_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{B : C}
(f : A ⟶ B)
(g : A ⟶ B)
[CategoryTheory.IsCoreflexivePair f g]
{Z : C}
(h : A ⟶ Z)
:
@[simp]
theorem
CategoryTheory.left_comp_retraction
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{B : C}
(f : A ⟶ B)
(g : A ⟶ B)
[CategoryTheory.IsCoreflexivePair f g]
:
@[simp]
theorem
CategoryTheory.right_comp_retraction_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{B : C}
(f : A ⟶ B)
(g : A ⟶ B)
[CategoryTheory.IsCoreflexivePair f g]
{Z : C}
(h : A ⟶ Z)
:
@[simp]
theorem
CategoryTheory.right_comp_retraction
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{B : C}
(f : A ⟶ B)
(g : A ⟶ B)
[CategoryTheory.IsCoreflexivePair f g]
:
theorem
CategoryTheory.IsKernelPair.isReflexivePair
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{B : C}
{R : C}
{f : R ⟶ A}
{g : R ⟶ A}
{q : A ⟶ B}
(h : CategoryTheory.IsKernelPair q f g)
:
If f,g is a kernel pair for some morphism q, then it is reflexive.
theorem
CategoryTheory.IsReflexivePair.swap
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{B : C}
{f : A ⟶ B}
{g : A ⟶ B}
[CategoryTheory.IsReflexivePair f g]
:
If f,g is reflexive, then g,f is reflexive.
theorem
CategoryTheory.IsCoreflexivePair.swap
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{B : C}
{f : A ⟶ B}
{g : A ⟶ B}
[CategoryTheory.IsCoreflexivePair f g]
:
If f,g is coreflexive, then g,f is coreflexive.
instance
CategoryTheory.instIsReflexivePairMapAppCounitObj
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
(B : D)
:
CategoryTheory.IsReflexivePair (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.
Equations
- ⋯ = ⋯
class
CategoryTheory.Limits.HasReflexiveCoequalizers
(C : Type u)
[CategoryTheory.Category.{v, u} C]
:
C has reflexive coequalizers if it has coequalizers for every reflexive pair.
- has_coeq : ∀ ⦃A B : C⦄ (f g : A ⟶ B) [inst : CategoryTheory.IsReflexivePair f g], CategoryTheory.Limits.HasCoequalizer f g
Instances
theorem
CategoryTheory.Limits.HasReflexiveCoequalizers.has_coeq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[self : CategoryTheory.Limits.HasReflexiveCoequalizers C]
⦃A : C⦄
⦃B : C⦄
(f : A ⟶ B)
(g : A ⟶ B)
[CategoryTheory.IsReflexivePair f g]
:
class
CategoryTheory.Limits.HasCoreflexiveEqualizers
(C : Type u)
[CategoryTheory.Category.{v, u} C]
:
C has coreflexive equalizers if it has equalizers for every coreflexive pair.
- has_eq : ∀ ⦃A B : C⦄ (f g : A ⟶ B) [inst : CategoryTheory.IsCoreflexivePair f g], CategoryTheory.Limits.HasEqualizer f g
Instances
theorem
CategoryTheory.Limits.HasCoreflexiveEqualizers.has_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[self : CategoryTheory.Limits.HasCoreflexiveEqualizers C]
⦃A : C⦄
⦃B : C⦄
(f : A ⟶ B)
(g : A ⟶ B)
[CategoryTheory.IsCoreflexivePair f g]
:
theorem
CategoryTheory.Limits.hasCoequalizer_of_common_section
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasReflexiveCoequalizers C]
{A : C}
{B : C}
{f : A ⟶ B}
{g : A ⟶ B}
(r : B ⟶ A)
(rf : CategoryTheory.CategoryStruct.comp r f = CategoryTheory.CategoryStruct.id B)
(rg : CategoryTheory.CategoryStruct.comp r g = CategoryTheory.CategoryStruct.id B)
:
theorem
CategoryTheory.Limits.hasEqualizer_of_common_retraction
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasCoreflexiveEqualizers C]
{A : C}
{B : C}
{f : A ⟶ B}
{g : A ⟶ B}
(r : B ⟶ A)
(fr : CategoryTheory.CategoryStruct.comp f r = CategoryTheory.CategoryStruct.id A)
(gr : CategoryTheory.CategoryStruct.comp g r = CategoryTheory.CategoryStruct.id A)
:
@[instance 100]
instance
CategoryTheory.Limits.hasReflexiveCoequalizers_of_hasCoequalizers
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasCoequalizers C]
:
If C has coequalizers, then it has reflexive coequalizers.
Equations
- ⋯ = ⋯
@[instance 100]
instance
CategoryTheory.Limits.hasCoreflexiveEqualizers_of_hasEqualizers
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasEqualizers C]
:
If C has equalizers, then it has coreflexive equalizers.
Equations
- ⋯ = ⋯