Reflexive coequalizers

This file deals with reflexive pairs, which are pairs of morphisms with a common section.

A reflexive coequalizer is a coequalizer of such a pair. These kind of 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.

Main definitions

• IsReflexivePair is the predicate that f and g have a common section.
• WalkingReflexivePair is the diagram indexing pairs with a common section.
• A reflexiveCofork is a cocone on a diagram indexed by WalkingReflexivePair.
• WalkingReflexivePair.inclusionWalkingReflexivePair is the inclustion functor from WalkingParallelPair to WalkingReflexivePair. It acts on reflexive pairs as forgetting the common section.
• HasReflexiveCoequalizers is the predicate that a category has all colimits of reflexive pairs.
• reflexiveCoequalizerIsoCoequalizer: an isomorphism promoting the coequalizer of a reflexive pair to the colimit of a diagram out of the walking reflexive pair.

Main statements

• IsKernelPair.isReflexivePair: A kernel pair is a reflexive pair
• WalkingParallelPair.inclusionWalkingReflexivePair_final: The inclusion functor is final.
• hasReflexiveCoequalizers_iff: A category has coequalizers of reflexive pairs if and only iff it has all colimits of shape WalkingReflexivePair.

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.
• Bundle the reflexive pairs of kernel pairs and of adjunction as functors out of the walking reflexive pair.

class CategoryTheory.IsReflexivePair {C : Type u} [Category.{v, u} 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.

• common_section' : ∃ (s : B ⟶ A), CategoryStruct.comp s f = CategoryStruct.id B ∧ CategoryStruct.comp s g = CategoryStruct.id B

theorem CategoryTheory.IsReflexivePair.common_section {C : Type u} [Category.{v, u} C] {A B : C} (f g : A ⟶ B) [IsReflexivePair f g] : ∃ (s : B ⟶ A), CategoryStruct.comp s f = CategoryStruct.id B ∧ CategoryStruct.comp s g = CategoryStruct.id B

class CategoryTheory.IsCoreflexivePair {C : Type u} [Category.{v, u} 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.

• common_retraction' : ∃ (s : B ⟶ A), CategoryStruct.comp f s = CategoryStruct.id A ∧ CategoryStruct.comp g s = CategoryStruct.id A

theorem CategoryTheory.IsCoreflexivePair.common_retraction {C : Type u} [Category.{v, u} C] {A B : C} (f g : A ⟶ B) [IsCoreflexivePair f g] : ∃ (s : B ⟶ A), CategoryStruct.comp f s = CategoryStruct.id A ∧ CategoryStruct.comp g s = CategoryStruct.id A

theorem CategoryTheory.IsReflexivePair.mk' {C : Type u} [Category.{v, u} C] {A B : C} {f g : A ⟶ B} (s : B ⟶ A) (sf : CategoryStruct.comp s f = CategoryStruct.id B) (sg : CategoryStruct.comp s g = CategoryStruct.id B) : IsReflexivePair f g

theorem CategoryTheory.IsCoreflexivePair.mk' {C : Type u} [Category.{v, u} C] {A B : C} {f g : A ⟶ B} (s : B ⟶ A) (fs : CategoryStruct.comp f s = CategoryStruct.id A) (gs : CategoryStruct.comp g s = CategoryStruct.id A) : IsCoreflexivePair f g

noncomputable def CategoryTheory.commonSection {C : Type u} [Category.{v, u} C] {A B : C} (f g : A ⟶ B) [IsReflexivePair f g] : B ⟶ A

Get the common section for a reflexive pair.

Equations

• CategoryTheory.commonSection f g = ⋯.choose

@[simp]

theorem CategoryTheory.section_comp_left {C : Type u} [Category.{v, u} C] {A B : C} (f g : A ⟶ B) [IsReflexivePair f g] : CategoryStruct.comp (commonSection f g) f = CategoryStruct.id B

@[simp]

theorem CategoryTheory.section_comp_left_assoc {C : Type u} [Category.{v, u} C] {A B : C} (f g : A ⟶ B) [IsReflexivePair f g] {Z : C} (h : B ⟶ Z) : CategoryStruct.comp (commonSection f g) (CategoryStruct.comp f h) = h

@[simp]

theorem CategoryTheory.section_comp_right {C : Type u} [Category.{v, u} C] {A B : C} (f g : A ⟶ B) [IsReflexivePair f g] : CategoryStruct.comp (commonSection f g) g = CategoryStruct.id B

@[simp]

theorem CategoryTheory.section_comp_right_assoc {C : Type u} [Category.{v, u} C] {A B : C} (f g : A ⟶ B) [IsReflexivePair f g] {Z : C} (h : B ⟶ Z) : CategoryStruct.comp (commonSection f g) (CategoryStruct.comp g h) = h

noncomputable def CategoryTheory.commonRetraction {C : Type u} [Category.{v, u} C] {A B : C} (f g : A ⟶ B) [IsCoreflexivePair f g] : B ⟶ A

Get the common retraction for a coreflexive pair.

Equations

• CategoryTheory.commonRetraction f g = ⋯.choose

@[simp]

theorem CategoryTheory.left_comp_retraction {C : Type u} [Category.{v, u} C] {A B : C} (f g : A ⟶ B) [IsCoreflexivePair f g] : CategoryStruct.comp f (commonRetraction f g) = CategoryStruct.id A

@[simp]

theorem CategoryTheory.left_comp_retraction_assoc {C : Type u} [Category.{v, u} C] {A B : C} (f g : A ⟶ B) [IsCoreflexivePair f g] {Z : C} (h : A ⟶ Z) : CategoryStruct.comp f (CategoryStruct.comp (commonRetraction f g) h) = h

@[simp]

theorem CategoryTheory.right_comp_retraction {C : Type u} [Category.{v, u} C] {A B : C} (f g : A ⟶ B) [IsCoreflexivePair f g] : CategoryStruct.comp g (commonRetraction f g) = CategoryStruct.id A

@[simp]

theorem CategoryTheory.right_comp_retraction_assoc {C : Type u} [Category.{v, u} C] {A B : C} (f g : A ⟶ B) [IsCoreflexivePair f g] {Z : C} (h : A ⟶ Z) : CategoryStruct.comp g (CategoryStruct.comp (commonRetraction f g) h) = h

theorem CategoryTheory.IsKernelPair.isReflexivePair {C : Type u} [Category.{v, u} C] {A B R : C} {f g : R ⟶ A} {q : A ⟶ B} (h : IsKernelPair q f g) : IsReflexivePair f g

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

theorem CategoryTheory.IsReflexivePair.swap {C : Type u} [Category.{v, u} C] {A B : C} {f g : A ⟶ B} [IsReflexivePair f g] : IsReflexivePair g f

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

theorem CategoryTheory.IsCoreflexivePair.swap {C : Type u} [Category.{v, u} C] {A B : C} {f g : A ⟶ B} [IsCoreflexivePair f g] : IsCoreflexivePair g f

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

instance CategoryTheory.instIsReflexivePairMapAppCounitObj {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) (B : D) : 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.

class CategoryTheory.Limits.HasReflexiveCoequalizers (C : Type u) [Category.{v, u} C] : Prop

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

• has_coeq ⦃A B : C⦄ (f g : A ⟶ B) [IsReflexivePair f g] : HasCoequalizer f g

class CategoryTheory.Limits.HasCoreflexiveEqualizers (C : Type u) [Category.{v, u} C] : Prop

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

• has_eq ⦃A B : C⦄ (f g : A ⟶ B) [IsCoreflexivePair f g] : HasEqualizer f g

theorem CategoryTheory.Limits.hasCoequalizer_of_common_section (C : Type u) [Category.{v, u} C] [HasReflexiveCoequalizers C] {A B : C} {f g : A ⟶ B} (r : B ⟶ A) (rf : CategoryStruct.comp r f = CategoryStruct.id B) (rg : CategoryStruct.comp r g = CategoryStruct.id B) : HasCoequalizer f g

theorem CategoryTheory.Limits.hasEqualizer_of_common_retraction (C : Type u) [Category.{v, u} C] [HasCoreflexiveEqualizers C] {A B : C} {f g : A ⟶ B} (r : B ⟶ A) (fr : CategoryStruct.comp f r = CategoryStruct.id A) (gr : CategoryStruct.comp g r = CategoryStruct.id A) : HasEqualizer f g

@[instance 100]

instance CategoryTheory.Limits.hasReflexiveCoequalizers_of_hasCoequalizers (C : Type u) [Category.{v, u} C] [HasCoequalizers C] : HasReflexiveCoequalizers C

If C has coequalizers, then it has reflexive coequalizers.

@[instance 100]

instance CategoryTheory.Limits.hasCoreflexiveEqualizers_of_hasEqualizers (C : Type u) [Category.{v, u} C] [HasEqualizers C] : HasCoreflexiveEqualizers C

If C has equalizers, then it has coreflexive equalizers.

inductive CategoryTheory.Limits.WalkingReflexivePair : Type

The type of objects for the diagram indexing reflexive (co)equalizers

• zero : WalkingReflexivePair
• one : WalkingReflexivePair

instance CategoryTheory.Limits.instDecidableEqWalkingReflexivePair : DecidableEq WalkingReflexivePair

Equations

• CategoryTheory.Limits.instDecidableEqWalkingReflexivePair x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance CategoryTheory.Limits.instInhabitedWalkingReflexivePair : Inhabited WalkingReflexivePair

Equations

• CategoryTheory.Limits.instInhabitedWalkingReflexivePair = { default := CategoryTheory.Limits.WalkingReflexivePair.zero }

inductive CategoryTheory.Limits.WalkingReflexivePair.Hom : WalkingReflexivePair → WalkingReflexivePair → Type

The type of morphisms for the diagram indexing reflexive (co)equalizers

• left : one.Hom zero
• right : one.Hom zero
• reflexion : zero.Hom one
• leftCompReflexion : one.Hom one
• rightCompReflexion : one.Hom one
• id (X : WalkingReflexivePair) : X.Hom X

instance CategoryTheory.Limits.WalkingReflexivePair.instDecidableEqHom {a✝ a✝¹ : WalkingReflexivePair} : DecidableEq (a✝.Hom a✝¹)

Equations

• CategoryTheory.Limits.WalkingReflexivePair.instDecidableEqHom = CategoryTheory.Limits.WalkingReflexivePair.decEqHom✝

def CategoryTheory.Limits.WalkingReflexivePair.Hom.comp {X Y Z : WalkingReflexivePair} : X.Hom Y → Y.Hom Z → X.Hom Z

Composition of morphisms in the diagram indexing reflexive (co)equalizers

Equations

• One or more equations did not get rendered due to their size.
• (CategoryTheory.Limits.WalkingReflexivePair.Hom.id x✝²).comp x✝ = x✝
• x✝.comp (CategoryTheory.Limits.WalkingReflexivePair.Hom.id x✝¹) = x✝
• CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion.comp CategoryTheory.Limits.WalkingReflexivePair.Hom.rightCompReflexion = CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion
• CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion.comp CategoryTheory.Limits.WalkingReflexivePair.Hom.leftCompReflexion = CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion
• CategoryTheory.Limits.WalkingReflexivePair.Hom.left.comp CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion = CategoryTheory.Limits.WalkingReflexivePair.Hom.leftCompReflexion
• CategoryTheory.Limits.WalkingReflexivePair.Hom.right.comp CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion = CategoryTheory.Limits.WalkingReflexivePair.Hom.rightCompReflexion
• CategoryTheory.Limits.WalkingReflexivePair.Hom.rightCompReflexion.comp CategoryTheory.Limits.WalkingReflexivePair.Hom.right = CategoryTheory.Limits.WalkingReflexivePair.Hom.right
• CategoryTheory.Limits.WalkingReflexivePair.Hom.rightCompReflexion.comp CategoryTheory.Limits.WalkingReflexivePair.Hom.left = CategoryTheory.Limits.WalkingReflexivePair.Hom.right
• CategoryTheory.Limits.WalkingReflexivePair.Hom.leftCompReflexion.comp CategoryTheory.Limits.WalkingReflexivePair.Hom.left = CategoryTheory.Limits.WalkingReflexivePair.Hom.left
• CategoryTheory.Limits.WalkingReflexivePair.Hom.leftCompReflexion.comp CategoryTheory.Limits.WalkingReflexivePair.Hom.right = CategoryTheory.Limits.WalkingReflexivePair.Hom.left

instance CategoryTheory.Limits.WalkingReflexivePair.category : SmallCategory WalkingReflexivePair

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.WalkingReflexivePair.Hom.id_eq (X : WalkingReflexivePair) : id X = CategoryStruct.id X

@[simp]

theorem CategoryTheory.Limits.WalkingReflexivePair.reflexion_comp_left : CategoryStruct.comp Hom.reflexion Hom.left = CategoryStruct.id zero

@[simp]

theorem CategoryTheory.Limits.WalkingReflexivePair.reflexion_comp_left_assoc {Z : WalkingReflexivePair} (h : zero ⟶ Z) : CategoryStruct.comp Hom.reflexion (CategoryStruct.comp Hom.left h) = h

@[simp]

theorem CategoryTheory.Limits.WalkingReflexivePair.reflexion_comp_right : CategoryStruct.comp Hom.reflexion Hom.right = CategoryStruct.id zero

@[simp]

theorem CategoryTheory.Limits.WalkingReflexivePair.reflexion_comp_right_assoc {Z : WalkingReflexivePair} (h : zero ⟶ Z) : CategoryStruct.comp Hom.reflexion (CategoryStruct.comp Hom.right h) = h

@[simp]

theorem CategoryTheory.Limits.WalkingReflexivePair.leftCompReflexion_eq : Hom.leftCompReflexion = CategoryStruct.comp Hom.left Hom.reflexion

@[simp]

theorem CategoryTheory.Limits.WalkingReflexivePair.rightCompReflexion_eq : Hom.rightCompReflexion = CategoryStruct.comp Hom.right Hom.reflexion

@[simp]

theorem CategoryTheory.Limits.WalkingReflexivePair.map_reflexion_comp_map_left {C : Type u} [Category.{v, u} C] (F : Functor WalkingReflexivePair C) : CategoryStruct.comp (F.map Hom.reflexion) (F.map Hom.left) = CategoryStruct.id (F.obj zero)

@[simp]

theorem CategoryTheory.Limits.WalkingReflexivePair.map_reflexion_comp_map_left_assoc {C : Type u} [Category.{v, u} C] (F : Functor WalkingReflexivePair C) {Z : C} (h : F.obj zero ⟶ Z) : CategoryStruct.comp (F.map Hom.reflexion) (CategoryStruct.comp (F.map Hom.left) h) = h

@[simp]

theorem CategoryTheory.Limits.WalkingReflexivePair.map_reflexion_comp_map_right {C : Type u} [Category.{v, u} C] (F : Functor WalkingReflexivePair C) : CategoryStruct.comp (F.map Hom.reflexion) (F.map Hom.right) = CategoryStruct.id (F.obj zero)

@[simp]

theorem CategoryTheory.Limits.WalkingReflexivePair.map_reflexion_comp_map_right_assoc {C : Type u} [Category.{v, u} C] (F : Functor WalkingReflexivePair C) {Z : C} (h : F.obj zero ⟶ Z) : CategoryStruct.comp (F.map Hom.reflexion) (CategoryStruct.comp (F.map Hom.right) h) = h

def CategoryTheory.Limits.WalkingParallelPair.inclusionWalkingReflexivePair : Functor WalkingParallelPair WalkingReflexivePair

The inclusion functor forgetting the common section

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.WalkingParallelPair.inclusionWalkingReflexivePair_map {X✝ Y✝ : WalkingParallelPair} (f : X✝ ⟶ Y✝) : inclusionWalkingReflexivePair.map f = match Y✝, X✝, f with | .(one), .(zero), WalkingParallelPairHom.left => WalkingReflexivePair.Hom.left | .(one), .(zero), WalkingParallelPairHom.right => WalkingReflexivePair.Hom.right | x, .(x), WalkingParallelPairHom.id .(x) => CategoryStruct.id (match x with | one => WalkingReflexivePair.zero | zero => WalkingReflexivePair.one)

@[simp]

theorem CategoryTheory.Limits.WalkingParallelPair.inclusionWalkingReflexivePair_obj (x : WalkingParallelPair) : inclusionWalkingReflexivePair.obj x = match x with | one => WalkingReflexivePair.zero | zero => WalkingReflexivePair.one

instance CategoryTheory.Limits.WalkingParallelPair.instNonemptyStructuredArrowWalkingReflexivePairInclusionWalkingReflexivePair (X : WalkingReflexivePair) : Nonempty (StructuredArrow X inclusionWalkingReflexivePair)

instance CategoryTheory.Limits.WalkingParallelPair.instIsConnectedStructuredArrowWalkingReflexivePairInclusionWalkingReflexivePair (X : WalkingReflexivePair) : IsConnected (StructuredArrow X inclusionWalkingReflexivePair)

instance CategoryTheory.Limits.WalkingParallelPair.inclusionWalkingReflexivePair_final : inclusionWalkingReflexivePair.Final

The inclusion functor is a final functor

def CategoryTheory.Limits.reflexivePair {C : Type u} [Category.{v, u} C] {A B : C} (f g : A ⟶ B) (s : B ⟶ A) (sl : CategoryStruct.comp s f = CategoryStruct.id B := by aesop_cat) (sr : CategoryStruct.comp s g = CategoryStruct.id B := by aesop_cat) : Functor WalkingReflexivePair C

Bundle the data of a parallel pair along with a common section as a functor out of the walking reflexive pair

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.reflexivePair_obj_zero {C : Type u} [Category.{v, u} C] {A B : C} (f g : A ⟶ B) (s : B ⟶ A) {sl : CategoryStruct.comp s f = CategoryStruct.id B} {sr : CategoryStruct.comp s g = CategoryStruct.id B} : (reflexivePair f g s sl sr).obj WalkingReflexivePair.zero = B

@[simp]

theorem CategoryTheory.Limits.reflexivePair_obj_one {C : Type u} [Category.{v, u} C] {A B : C} (f g : A ⟶ B) (s : B ⟶ A) {sl : CategoryStruct.comp s f = CategoryStruct.id B} {sr : CategoryStruct.comp s g = CategoryStruct.id B} : (reflexivePair f g s sl sr).obj WalkingReflexivePair.one = A

@[simp]

theorem CategoryTheory.Limits.reflexivePair_map_right {C : Type u} [Category.{v, u} C] {A B : C} (f g : A ⟶ B) (s : B ⟶ A) {sl : CategoryStruct.comp s f = CategoryStruct.id B} {sr : CategoryStruct.comp s g = CategoryStruct.id B} : (reflexivePair f g s sl sr).map WalkingReflexivePair.Hom.left = f

@[simp]

theorem CategoryTheory.Limits.reflexivePair_map_left {C : Type u} [Category.{v, u} C] {A B : C} (f g : A ⟶ B) (s : B ⟶ A) {sl : CategoryStruct.comp s f = CategoryStruct.id B} {sr : CategoryStruct.comp s g = CategoryStruct.id B} : (reflexivePair f g s sl sr).map WalkingReflexivePair.Hom.right = g

@[simp]

theorem CategoryTheory.Limits.reflexivePair_map_reflexion {C : Type u} [Category.{v, u} C] {A B : C} (f g : A ⟶ B) (s : B ⟶ A) {sl : CategoryStruct.comp s f = CategoryStruct.id B} {sr : CategoryStruct.comp s g = CategoryStruct.id B} : (reflexivePair f g s sl sr).map WalkingReflexivePair.Hom.reflexion = s

noncomputable def CategoryTheory.Limits.ofIsReflexivePair {C : Type u} [Category.{v, u} C] {A B : C} (f g : A ⟶ B) [IsReflexivePair f g] : Functor WalkingReflexivePair C

(Noncomputably) bundle the data of a reflexive pair as a functor out of the walking reflexive pair

Equations

• CategoryTheory.Limits.ofIsReflexivePair f g = CategoryTheory.Limits.reflexivePair f g (CategoryTheory.commonSection f g) ⋯ ⋯

@[simp]

theorem CategoryTheory.Limits.ofIsReflexivePair_map_left {C : Type u} [Category.{v, u} C] {A B : C} (f g : A ⟶ B) [IsReflexivePair f g] : (ofIsReflexivePair f g).map WalkingReflexivePair.Hom.left = f

@[simp]

theorem CategoryTheory.Limits.ofIsReflexivePair_map_right {C : Type u} [Category.{v, u} C] {A B : C} (f g : A ⟶ B) [IsReflexivePair f g] : (ofIsReflexivePair f g).map WalkingReflexivePair.Hom.right = g

noncomputable def CategoryTheory.Limits.inclusionWalkingReflexivePairOfIsReflexivePairIso {C : Type u} [Category.{v, u} C] {A B : C} (f g : A ⟶ B) [IsReflexivePair f g] : WalkingParallelPair.inclusionWalkingReflexivePair.comp (ofIsReflexivePair f g) ≅ parallelPair f g

The natural isomorphism between the diagram obtained by forgetting the reflexion of ofIsReflexivePair f g and the original parallel pair.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.reflexivePair.mkNatTrans {C : Type u} [Category.{v, u} C] {F G : Functor WalkingReflexivePair C} (e₀ : F.obj WalkingReflexivePair.zero ⟶ G.obj WalkingReflexivePair.zero) (e₁ : F.obj WalkingReflexivePair.one ⟶ G.obj WalkingReflexivePair.one) (h₁ : CategoryStruct.comp (F.map WalkingReflexivePair.Hom.left) e₀ = CategoryStruct.comp e₁ (G.map WalkingReflexivePair.Hom.left) := by aesop_cat) (h₂ : CategoryStruct.comp (F.map WalkingReflexivePair.Hom.right) e₀ = CategoryStruct.comp e₁ (G.map WalkingReflexivePair.Hom.right) := by aesop_cat) (h₃ : CategoryStruct.comp (F.map WalkingReflexivePair.Hom.reflexion) e₁ = CategoryStruct.comp e₀ (G.map WalkingReflexivePair.Hom.reflexion) := by aesop_cat) : F ⟶ G

A constructor for natural transformations between functors from WalkingReflexivePair.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.reflexivePair.mkNatTrans_app_zero {C : Type u} [Category.{v, u} C] {F G : Functor WalkingReflexivePair C} (e₀ : F.obj WalkingReflexivePair.zero ⟶ G.obj WalkingReflexivePair.zero) (e₁ : F.obj WalkingReflexivePair.one ⟶ G.obj WalkingReflexivePair.one) (h₁ : CategoryStruct.comp (F.map WalkingReflexivePair.Hom.left) e₀ = CategoryStruct.comp e₁ (G.map WalkingReflexivePair.Hom.left) := by aesop_cat) (h₂ : CategoryStruct.comp (F.map WalkingReflexivePair.Hom.right) e₀ = CategoryStruct.comp e₁ (G.map WalkingReflexivePair.Hom.right) := by aesop_cat) (h₃ : CategoryStruct.comp (F.map WalkingReflexivePair.Hom.reflexion) e₁ = CategoryStruct.comp e₀ (G.map WalkingReflexivePair.Hom.reflexion) := by aesop_cat) : (mkNatTrans e₀ e₁ h₁ h₂ h₃).app WalkingReflexivePair.zero = e₀

@[simp]

theorem CategoryTheory.Limits.reflexivePair.mkNatTrans_app_one {C : Type u} [Category.{v, u} C] {F G : Functor WalkingReflexivePair C} (e₀ : F.obj WalkingReflexivePair.zero ⟶ G.obj WalkingReflexivePair.zero) (e₁ : F.obj WalkingReflexivePair.one ⟶ G.obj WalkingReflexivePair.one) (h₁ : CategoryStruct.comp (F.map WalkingReflexivePair.Hom.left) e₀ = CategoryStruct.comp e₁ (G.map WalkingReflexivePair.Hom.left) := by aesop_cat) (h₂ : CategoryStruct.comp (F.map WalkingReflexivePair.Hom.right) e₀ = CategoryStruct.comp e₁ (G.map WalkingReflexivePair.Hom.right) := by aesop_cat) (h₃ : CategoryStruct.comp (F.map WalkingReflexivePair.Hom.reflexion) e₁ = CategoryStruct.comp e₀ (G.map WalkingReflexivePair.Hom.reflexion) := by aesop_cat) : (mkNatTrans e₀ e₁ h₁ h₂ h₃).app WalkingReflexivePair.one = e₁

def CategoryTheory.Limits.reflexivePair.mkNatIso {C : Type u} [Category.{v, u} C] {F G : Functor WalkingReflexivePair C} (e₀ : F.obj WalkingReflexivePair.zero ≅ G.obj WalkingReflexivePair.zero) (e₁ : F.obj WalkingReflexivePair.one ≅ G.obj WalkingReflexivePair.one) (h₁ : CategoryStruct.comp (F.map WalkingReflexivePair.Hom.left) e₀.hom = CategoryStruct.comp e₁.hom (G.map WalkingReflexivePair.Hom.left) := by aesop_cat) (h₂ : CategoryStruct.comp (F.map WalkingReflexivePair.Hom.right) e₀.hom = CategoryStruct.comp e₁.hom (G.map WalkingReflexivePair.Hom.right) := by aesop_cat) (h₃ : CategoryStruct.comp (F.map WalkingReflexivePair.Hom.reflexion) e₁.hom = CategoryStruct.comp e₀.hom (G.map WalkingReflexivePair.Hom.reflexion) := by aesop_cat) : F ≅ G

Constructor for natural isomorphisms between functors out of WalkingReflexivePair.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.reflexivePair.mkNatIso_inv_app {C : Type u} [Category.{v, u} C] {F G : Functor WalkingReflexivePair C} (e₀ : F.obj WalkingReflexivePair.zero ≅ G.obj WalkingReflexivePair.zero) (e₁ : F.obj WalkingReflexivePair.one ≅ G.obj WalkingReflexivePair.one) (h₁ : CategoryStruct.comp (F.map WalkingReflexivePair.Hom.left) e₀.hom = CategoryStruct.comp e₁.hom (G.map WalkingReflexivePair.Hom.left) := by aesop_cat) (h₂ : CategoryStruct.comp (F.map WalkingReflexivePair.Hom.right) e₀.hom = CategoryStruct.comp e₁.hom (G.map WalkingReflexivePair.Hom.right) := by aesop_cat) (h₃ : CategoryStruct.comp (F.map WalkingReflexivePair.Hom.reflexion) e₁.hom = CategoryStruct.comp e₀.hom (G.map WalkingReflexivePair.Hom.reflexion) := by aesop_cat) (x : WalkingReflexivePair) : (mkNatIso e₀ e₁ h₁ h₂ h₃).inv.app x = match x with | WalkingReflexivePair.zero => e₀.inv | WalkingReflexivePair.one => e₁.inv

@[simp]

theorem CategoryTheory.Limits.reflexivePair.mkNatIso_hom_app {C : Type u} [Category.{v, u} C] {F G : Functor WalkingReflexivePair C} (e₀ : F.obj WalkingReflexivePair.zero ≅ G.obj WalkingReflexivePair.zero) (e₁ : F.obj WalkingReflexivePair.one ≅ G.obj WalkingReflexivePair.one) (h₁ : CategoryStruct.comp (F.map WalkingReflexivePair.Hom.left) e₀.hom = CategoryStruct.comp e₁.hom (G.map WalkingReflexivePair.Hom.left) := by aesop_cat) (h₂ : CategoryStruct.comp (F.map WalkingReflexivePair.Hom.right) e₀.hom = CategoryStruct.comp e₁.hom (G.map WalkingReflexivePair.Hom.right) := by aesop_cat) (h₃ : CategoryStruct.comp (F.map WalkingReflexivePair.Hom.reflexion) e₁.hom = CategoryStruct.comp e₀.hom (G.map WalkingReflexivePair.Hom.reflexion) := by aesop_cat) (x : WalkingReflexivePair) : (mkNatIso e₀ e₁ h₁ h₂ h₃).hom.app x = match x with | WalkingReflexivePair.zero => e₀.hom | WalkingReflexivePair.one => e₁.hom

def CategoryTheory.Limits.reflexivePair.diagramIsoReflexivePair {C : Type u} [Category.{v, u} C] (F : Functor WalkingReflexivePair C) : F ≅ reflexivePair (F.map WalkingReflexivePair.Hom.left) (F.map WalkingReflexivePair.Hom.right) (F.map WalkingReflexivePair.Hom.reflexion) ⋯ ⋯

Every functor out of WalkingReflexivePair is isomorphic to the reflexivePair given by its components

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.reflexivePair.diagramIsoReflexivePair_inv_app {C : Type u} [Category.{v, u} C] (F : Functor WalkingReflexivePair C) (x : WalkingReflexivePair) : (diagramIsoReflexivePair F).inv.app x = match x with | WalkingReflexivePair.zero => CategoryStruct.id (F.obj WalkingReflexivePair.zero) | WalkingReflexivePair.one => CategoryStruct.id (F.obj WalkingReflexivePair.one)

@[simp]

theorem CategoryTheory.Limits.reflexivePair.diagramIsoReflexivePair_hom_app {C : Type u} [Category.{v, u} C] (F : Functor WalkingReflexivePair C) (x : WalkingReflexivePair) : (diagramIsoReflexivePair F).hom.app x = match x with | WalkingReflexivePair.zero => CategoryStruct.id (F.obj WalkingReflexivePair.zero) | WalkingReflexivePair.one => CategoryStruct.id (F.obj WalkingReflexivePair.one)

def CategoryTheory.Limits.reflexivePair.compRightIso {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] {A B : C} (f g : A ⟶ B) (s : B ⟶ A) (sl : CategoryStruct.comp s f = CategoryStruct.id B) (sr : CategoryStruct.comp s g = CategoryStruct.id B) (F : Functor C D) : (reflexivePair f g s sl sr).comp F ≅ reflexivePair (F.map f) (F.map g) (F.map s) ⋯ ⋯

A reflexivePair composed with a functor is isomorphic to the reflexivePair obtained by applying the functor at each map.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.reflexivePair.compRightIso_inv_app {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] {A B : C} (f g : A ⟶ B) (s : B ⟶ A) (sl : CategoryStruct.comp s f = CategoryStruct.id B) (sr : CategoryStruct.comp s g = CategoryStruct.id B) (F : Functor C D) (x : WalkingReflexivePair) : (compRightIso f g s sl sr F).inv.app x = match x with | WalkingReflexivePair.zero => CategoryStruct.id (F.obj B) | WalkingReflexivePair.one => CategoryStruct.id (F.obj A)

@[simp]

theorem CategoryTheory.Limits.reflexivePair.compRightIso_hom_app {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] {A B : C} (f g : A ⟶ B) (s : B ⟶ A) (sl : CategoryStruct.comp s f = CategoryStruct.id B) (sr : CategoryStruct.comp s g = CategoryStruct.id B) (F : Functor C D) (x : WalkingReflexivePair) : (compRightIso f g s sl sr F).hom.app x = match x with | WalkingReflexivePair.zero => CategoryStruct.id (F.obj B) | WalkingReflexivePair.one => CategoryStruct.id (F.obj A)

theorem CategoryTheory.Limits.reflexivePair.whiskerRightMkNatTrans {C : Type u} [Category.{v, u} C] {F G : Functor WalkingReflexivePair C} (e₀ : F.obj WalkingReflexivePair.zero ⟶ G.obj WalkingReflexivePair.zero) (e₁ : F.obj WalkingReflexivePair.one ⟶ G.obj WalkingReflexivePair.one) {h₁ : CategoryStruct.comp (F.map WalkingReflexivePair.Hom.left) e₀ = CategoryStruct.comp e₁ (G.map WalkingReflexivePair.Hom.left)} {h₂ : CategoryStruct.comp (F.map WalkingReflexivePair.Hom.right) e₀ = CategoryStruct.comp e₁ (G.map WalkingReflexivePair.Hom.right)} {h₃ : CategoryStruct.comp (F.map WalkingReflexivePair.Hom.reflexion) e₁ = CategoryStruct.comp e₀ (G.map WalkingReflexivePair.Hom.reflexion)} {D : Type u₂} [Category.{v₂, u₂} D] (H : Functor C D) : whiskerRight (mkNatTrans e₀ e₁ ⋯ ⋯ ⋯) H = mkNatTrans (H.map e₀) (H.map e₁) ⋯ ⋯ ⋯

instance CategoryTheory.Limits.reflexivePair.to_isReflexivePair {C : Type u} [Category.{v, u} C] {F : Functor WalkingReflexivePair C} : IsReflexivePair (F.map WalkingReflexivePair.Hom.left) (F.map WalkingReflexivePair.Hom.right)

Any functor out of the WalkingReflexivePair yields a reflexive pair

@[reducible, inline]

abbrev CategoryTheory.Limits.ReflexiveCofork {C : Type u} [Category.{v, u} C] (F : Functor WalkingReflexivePair C) : Type (max u v)

A ReflexiveCofork is a cocone over a WalkingReflexivePair-shaped diagram.

Equations

• CategoryTheory.Limits.ReflexiveCofork F = CategoryTheory.Limits.Cocone F

@[reducible, inline]

abbrev CategoryTheory.Limits.ReflexiveCofork.π {C : Type u} [Category.{v, u} C] {F : Functor WalkingReflexivePair C} (G : ReflexiveCofork F) : F.obj WalkingReflexivePair.zero ⟶ G.pt

The tail morphism of a reflexive cofork.

Equations

• G.π = G.ι.app CategoryTheory.Limits.WalkingReflexivePair.zero

def CategoryTheory.Limits.ReflexiveCofork.mk {C : Type u} [Category.{v, u} C] {F : Functor WalkingReflexivePair C} {X : C} (π : F.obj WalkingReflexivePair.zero ⟶ X) (h : CategoryStruct.comp (F.map WalkingReflexivePair.Hom.left) π = CategoryStruct.comp (F.map WalkingReflexivePair.Hom.right) π) : ReflexiveCofork F

Constructor for ReflexiveCofork

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.ReflexiveCofork.mk_pt {C : Type u} [Category.{v, u} C] {F : Functor WalkingReflexivePair C} {X : C} (π : F.obj WalkingReflexivePair.zero ⟶ X) (h : CategoryStruct.comp (F.map WalkingReflexivePair.Hom.left) π = CategoryStruct.comp (F.map WalkingReflexivePair.Hom.right) π) : (mk π h).pt = X

@[simp]

theorem CategoryTheory.Limits.ReflexiveCofork.mk_π {C : Type u} [Category.{v, u} C] {F : Functor WalkingReflexivePair C} {X : C} (π : F.obj WalkingReflexivePair.zero ⟶ X) (h : CategoryStruct.comp (F.map WalkingReflexivePair.Hom.left) π = CategoryStruct.comp (F.map WalkingReflexivePair.Hom.right) π) : (mk π h).π = π

theorem CategoryTheory.Limits.ReflexiveCofork.condition {C : Type u} [Category.{v, u} C] {F : Functor WalkingReflexivePair C} (G : ReflexiveCofork F) : CategoryStruct.comp (F.map WalkingReflexivePair.Hom.left) G.π = CategoryStruct.comp (F.map WalkingReflexivePair.Hom.right) G.π

@[simp]

theorem CategoryTheory.Limits.ReflexiveCofork.app_one_eq_π {C : Type u} [Category.{v, u} C] {F : Functor WalkingReflexivePair C} (G : ReflexiveCofork F) : G.ι.app WalkingReflexivePair.zero = G.π

@[reducible, inline]

abbrev CategoryTheory.Limits.ReflexiveCofork.toCofork {C : Type u} [Category.{v, u} C] {F : Functor WalkingReflexivePair C} (G : ReflexiveCofork F) : Cofork (F.map WalkingReflexivePair.Hom.left) (F.map WalkingReflexivePair.Hom.right)

The underlying Cofork of a ReflexiveCofork.

Equations

• G.toCofork = CategoryTheory.Limits.Cofork.ofπ G.π ⋯

def CategoryTheory.Limits.reflexiveCoforkEquivCofork {C : Type u} [Category.{v, u} C] (F : Functor WalkingReflexivePair C) : ReflexiveCofork F ≌ Cofork (F.map WalkingReflexivePair.Hom.left) (F.map WalkingReflexivePair.Hom.right)

Forgetting the reflexion yields an equivalence between cocones over a bundled reflexive pair and coforks on the underlying parallel pair.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.reflexiveCoforkEquivCofork_inverse_obj_pt {C : Type u} [Category.{v, u} C] (F : Functor WalkingReflexivePair C) (X : Cofork (F.map WalkingReflexivePair.Hom.left) (F.map WalkingReflexivePair.Hom.right)) : ((reflexiveCoforkEquivCofork F).inverse.obj X).pt = X.pt

@[simp]

theorem CategoryTheory.Limits.reflexiveCoforkEquivCofork_functor_obj_pt {C : Type u} [Category.{v, u} C] (F : Functor WalkingReflexivePair C) (X : Cocone F) : ((reflexiveCoforkEquivCofork F).functor.obj X).pt = X.pt

@[simp]

theorem CategoryTheory.Limits.reflexiveCoforkEquivCofork_functor_obj_π {C : Type u} [Category.{v, u} C] (F : Functor WalkingReflexivePair C) (G : ReflexiveCofork F) : ((reflexiveCoforkEquivCofork F).functor.obj G).π = G.π

@[simp]

theorem CategoryTheory.Limits.reflexiveCoforkEquivCofork_inverse_obj_π {C : Type u} [Category.{v, u} C] (F : Functor WalkingReflexivePair C) (G : Cofork (F.map WalkingReflexivePair.Hom.left) (F.map WalkingReflexivePair.Hom.right)) : ((reflexiveCoforkEquivCofork F).inverse.obj G).π = G.π

def CategoryTheory.Limits.reflexiveCoforkEquivCoforkObjIso {C : Type u} [Category.{v, u} C] (F : Functor WalkingReflexivePair C) (G : ReflexiveCofork F) : (reflexiveCoforkEquivCofork F).functor.obj G ≅ G.toCofork

The equivalence between reflexive coforks and coforks sends a reflexive cofork to its underlying cofork.

Equations

• CategoryTheory.Limits.reflexiveCoforkEquivCoforkObjIso F G = CategoryTheory.Limits.Cofork.ext (CategoryTheory.Iso.refl ((CategoryTheory.Limits.reflexiveCoforkEquivCofork F).functor.obj G).pt) ⋯

theorem CategoryTheory.Limits.hasReflexiveCoequalizer_iff_hasCoequalizer {C : Type u} [Category.{v, u} C] (F : Functor WalkingReflexivePair C) : HasColimit F ↔ HasCoequalizer (F.map WalkingReflexivePair.Hom.left) (F.map WalkingReflexivePair.Hom.right)

instance CategoryTheory.Limits.reflexivePair_hasColimit_of_hasCoequalizer {C : Type u} [Category.{v, u} C] (F : Functor WalkingReflexivePair C) [h : HasCoequalizer (F.map WalkingReflexivePair.Hom.left) (F.map WalkingReflexivePair.Hom.right)] : HasColimit F

def CategoryTheory.Limits.ReflexiveCofork.isColimitEquiv {C : Type u} [Category.{v, u} C] (F : Functor WalkingReflexivePair C) (G : ReflexiveCofork F) : IsColimit G.toCofork ≃ IsColimit G

A reflexive cofork is a colimit cocone if and only if the underlying cofork is.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.reflexiveCoequalizerIsoCoequalizer {C : Type u} [Category.{v, u} C] (F : Functor WalkingReflexivePair C) [HasCoequalizer (F.map WalkingReflexivePair.Hom.left) (F.map WalkingReflexivePair.Hom.right)] : colimit F ≅ coequalizer (F.map WalkingReflexivePair.Hom.left) (F.map WalkingReflexivePair.Hom.right)

The colimit of a functor out of the walking reflexive pair is the same as the colimit of the underlying parallel pair.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.ι_reflexiveCoequalizerIsoCoequalizer_hom {C : Type u} [Category.{v, u} C] (F : Functor WalkingReflexivePair C) [HasCoequalizer (F.map WalkingReflexivePair.Hom.left) (F.map WalkingReflexivePair.Hom.right)] : CategoryStruct.comp (colimit.ι F WalkingReflexivePair.zero) (reflexiveCoequalizerIsoCoequalizer F).hom = coequalizer.π (F.map WalkingReflexivePair.Hom.left) (F.map WalkingReflexivePair.Hom.right)

@[simp]

theorem CategoryTheory.Limits.ι_reflexiveCoequalizerIsoCoequalizer_hom_assoc {C : Type u} [Category.{v, u} C] (F : Functor WalkingReflexivePair C) [HasCoequalizer (F.map WalkingReflexivePair.Hom.left) (F.map WalkingReflexivePair.Hom.right)] {Z : C} (h : coequalizer (F.map WalkingReflexivePair.Hom.left) (F.map WalkingReflexivePair.Hom.right) ⟶ Z) : CategoryStruct.comp (colimit.ι F WalkingReflexivePair.zero) (CategoryStruct.comp (reflexiveCoequalizerIsoCoequalizer F).hom h) = CategoryStruct.comp (coequalizer.π (F.map WalkingReflexivePair.Hom.left) (F.map WalkingReflexivePair.Hom.right)) h

@[simp]

theorem CategoryTheory.Limits.π_reflexiveCoequalizerIsoCoequalizer_inv {C : Type u} [Category.{v, u} C] (F : Functor WalkingReflexivePair C) [HasCoequalizer (F.map WalkingReflexivePair.Hom.left) (F.map WalkingReflexivePair.Hom.right)] : CategoryStruct.comp (coequalizer.π (F.map WalkingReflexivePair.Hom.left) (F.map WalkingReflexivePair.Hom.right)) (reflexiveCoequalizerIsoCoequalizer F).inv = colimit.ι F WalkingReflexivePair.zero

@[simp]

theorem CategoryTheory.Limits.π_reflexiveCoequalizerIsoCoequalizer_inv_assoc {C : Type u} [Category.{v, u} C] (F : Functor WalkingReflexivePair C) [HasCoequalizer (F.map WalkingReflexivePair.Hom.left) (F.map WalkingReflexivePair.Hom.right)] {Z : C} (h : colimit F ⟶ Z) : CategoryStruct.comp (coequalizer.π (F.map WalkingReflexivePair.Hom.left) (F.map WalkingReflexivePair.Hom.right)) (CategoryStruct.comp (reflexiveCoequalizerIsoCoequalizer F).inv h) = CategoryStruct.comp (colimit.ι F WalkingReflexivePair.zero) h

instance CategoryTheory.Limits.ofIsReflexivePair_hasColimit_of_hasCoequalizer {C : Type u} [Category.{v, u} C] {A B : C} {f g : A ⟶ B} [IsReflexivePair f g] [h : HasCoequalizer f g] : HasColimit (ofIsReflexivePair f g)

def CategoryTheory.Limits.colimitOfIsReflexivePairIsoCoequalizer {C : Type u} [Category.{v, u} C] {A B : C} {f g : A ⟶ B} [IsReflexivePair f g] [h : HasCoequalizer f g] : colimit (ofIsReflexivePair f g) ≅ coequalizer f g

The coequalizer of a reflexive pair can be promoted to the colimit of a diagram out of the walking reflexive pair

Equations

• CategoryTheory.Limits.colimitOfIsReflexivePairIsoCoequalizer = CategoryTheory.Limits.reflexiveCoequalizerIsoCoequalizer (CategoryTheory.Limits.ofIsReflexivePair f g)

@[simp]

theorem CategoryTheory.Limits.ι_colimitOfIsReflexivePairIsoCoequalizer_hom {C : Type u} [Category.{v, u} C] {A B : C} {f g : A ⟶ B} [IsReflexivePair f g] [h : HasCoequalizer f g] : CategoryStruct.comp (colimit.ι (ofIsReflexivePair f g) WalkingReflexivePair.zero) colimitOfIsReflexivePairIsoCoequalizer.hom = coequalizer.π f g

@[simp]

theorem CategoryTheory.Limits.ι_colimitOfIsReflexivePairIsoCoequalizer_hom_assoc {C : Type u} [Category.{v, u} C] {A B : C} {f g : A ⟶ B} [IsReflexivePair f g] [h : HasCoequalizer f g] {Z : C} (h✝ : coequalizer f g ⟶ Z) : CategoryStruct.comp (colimit.ι (ofIsReflexivePair f g) WalkingReflexivePair.zero) (CategoryStruct.comp colimitOfIsReflexivePairIsoCoequalizer.hom h✝) = CategoryStruct.comp (coequalizer.π f g) h✝

@[simp]

theorem CategoryTheory.Limits.π_colimitOfIsReflexivePairIsoCoequalizer_inv {C : Type u} [Category.{v, u} C] {A B : C} {f g : A ⟶ B} [IsReflexivePair f g] [h : HasCoequalizer f g] : CategoryStruct.comp (coequalizer.π f g) colimitOfIsReflexivePairIsoCoequalizer.inv = colimit.ι (ofIsReflexivePair f g) WalkingReflexivePair.zero

@[simp]

theorem CategoryTheory.Limits.π_colimitOfIsReflexivePairIsoCoequalizer_inv_assoc {C : Type u} [Category.{v, u} C] {A B : C} {f g : A ⟶ B} [IsReflexivePair f g] [h : HasCoequalizer f g] {Z : C} (h✝ : colimit (ofIsReflexivePair f g) ⟶ Z) : CategoryStruct.comp (coequalizer.π f g) (CategoryStruct.comp colimitOfIsReflexivePairIsoCoequalizer.inv h✝) = CategoryStruct.comp (colimit.ι (ofIsReflexivePair f g) WalkingReflexivePair.zero) h✝

theorem CategoryTheory.Limits.hasReflexiveCoequalizers_iff {C : Type u} [Category.{v, u} C] : HasColimitsOfShape WalkingReflexivePair C ↔ HasReflexiveCoequalizers C

A category has coequalizers of reflexive pairs if and only if it has all colimits indexed by the walking reflexive pair.