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} [CategoryTheory.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), CategoryTheory.CategoryStruct.comp s f = CategoryTheory.CategoryStruct.id B ∧ CategoryTheory.CategoryStruct.comp s g = CategoryTheory.CategoryStruct.id B

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

class CategoryTheory.IsCoreflexivePair {C : Type u} [CategoryTheory.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), CategoryTheory.CategoryStruct.comp f s = CategoryTheory.CategoryStruct.id A ∧ CategoryTheory.CategoryStruct.comp g s = CategoryTheory.CategoryStruct.id A

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

theorem CategoryTheory.IsReflexivePair.mk' {C : Type u} [CategoryTheory.Category.{v, u} C] {A B : C} {f 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) : CategoryTheory.IsReflexivePair f g

theorem CategoryTheory.IsCoreflexivePair.mk' {C : Type u} [CategoryTheory.Category.{v, u} C] {A B : C} {f 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) : CategoryTheory.IsCoreflexivePair f g

noncomputable def CategoryTheory.commonSection {C : Type u} [CategoryTheory.Category.{v, u} C] {A B : C} (f g : A ⟶ B) [CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {A B : C} (f g : A ⟶ B) [CategoryTheory.IsReflexivePair f g] : CategoryTheory.CategoryStruct.comp (CategoryTheory.commonSection f g) f = CategoryTheory.CategoryStruct.id B

@[simp]

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

@[simp]

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

@[simp]

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

noncomputable def CategoryTheory.commonRetraction {C : Type u} [CategoryTheory.Category.{v, u} C] {A B : C} (f g : A ⟶ B) [CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {A B : C} (f g : A ⟶ B) [CategoryTheory.IsCoreflexivePair f g] : CategoryTheory.CategoryStruct.comp f (CategoryTheory.commonRetraction f g) = CategoryTheory.CategoryStruct.id A

@[simp]

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

@[simp]

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

@[simp]

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

theorem CategoryTheory.IsKernelPair.isReflexivePair {C : Type u} [CategoryTheory.Category.{v, u} C] {A B R : C} {f g : R ⟶ A} {q : A ⟶ B} (h : CategoryTheory.IsKernelPair q f g) : CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {A B : C} {f g : A ⟶ B} [CategoryTheory.IsReflexivePair f g] : CategoryTheory.IsReflexivePair g f

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

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

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.

class CategoryTheory.Limits.HasReflexiveCoequalizers (C : Type u) [CategoryTheory.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) [CategoryTheory.IsReflexivePair f g] : CategoryTheory.Limits.HasCoequalizer f g

class CategoryTheory.Limits.HasCoreflexiveEqualizers (C : Type u) [CategoryTheory.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) [CategoryTheory.IsCoreflexivePair f g] : CategoryTheory.Limits.HasEqualizer f g

theorem CategoryTheory.Limits.hasCoequalizer_of_common_section (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasReflexiveCoequalizers C] {A B : C} {f 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) : CategoryTheory.Limits.HasCoequalizer f g

theorem CategoryTheory.Limits.hasEqualizer_of_common_retraction (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoreflexiveEqualizers C] {A B : C} {f 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) : CategoryTheory.Limits.HasEqualizer f g

@[instance 100]

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

If C has coequalizers, then it has reflexive coequalizers.

@[instance 100]

instance CategoryTheory.Limits.hasCoreflexiveEqualizers_of_hasEqualizers (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasEqualizers C] : CategoryTheory.Limits.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 : CategoryTheory.Limits.WalkingReflexivePair
• one : CategoryTheory.Limits.WalkingReflexivePair

instance CategoryTheory.Limits.instDecidableEqWalkingReflexivePair : DecidableEq CategoryTheory.Limits.WalkingReflexivePair

Equations

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

instance CategoryTheory.Limits.instInhabitedWalkingReflexivePair : Inhabited CategoryTheory.Limits.WalkingReflexivePair

Equations

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

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

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

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

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

Equations

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

def CategoryTheory.Limits.WalkingReflexivePair.Hom.comp {X Y Z : CategoryTheory.Limits.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 : CategoryTheory.SmallCategory CategoryTheory.Limits.WalkingReflexivePair

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Limits.WalkingParallelPair.inclusionWalkingReflexivePair : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.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✝ : CategoryTheory.Limits.WalkingParallelPair} (f : X✝ ⟶ Y✝) : CategoryTheory.Limits.WalkingParallelPair.inclusionWalkingReflexivePair.map f = match Y✝, X✝, f with | .(CategoryTheory.Limits.WalkingParallelPair.one), .(CategoryTheory.Limits.WalkingParallelPair.zero), CategoryTheory.Limits.WalkingParallelPairHom.left => CategoryTheory.Limits.WalkingReflexivePair.Hom.left | .(CategoryTheory.Limits.WalkingParallelPair.one), .(CategoryTheory.Limits.WalkingParallelPair.zero), CategoryTheory.Limits.WalkingParallelPairHom.right => CategoryTheory.Limits.WalkingReflexivePair.Hom.right | x, .(x), CategoryTheory.Limits.WalkingParallelPairHom.id .(x) => CategoryTheory.CategoryStruct.id (match x with | CategoryTheory.Limits.WalkingParallelPair.one => CategoryTheory.Limits.WalkingReflexivePair.zero | CategoryTheory.Limits.WalkingParallelPair.zero => CategoryTheory.Limits.WalkingReflexivePair.one)

@[simp]

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

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

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

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

The inclusion functor is a final functor

def CategoryTheory.Limits.reflexivePair {C : Type u} [CategoryTheory.Category.{v, u} C] {A B : C} (f g : A ⟶ B) (s : B ⟶ A) (sl : CategoryTheory.CategoryStruct.comp s f = CategoryTheory.CategoryStruct.id B := by aesop_cat) (sr : CategoryTheory.CategoryStruct.comp s g = CategoryTheory.CategoryStruct.id B := by aesop_cat) : CategoryTheory.Functor CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {A B : C} (f g : A ⟶ B) (s : B ⟶ A) {sl : CategoryTheory.CategoryStruct.comp s f = CategoryTheory.CategoryStruct.id B} {sr : CategoryTheory.CategoryStruct.comp s g = CategoryTheory.CategoryStruct.id B} : (CategoryTheory.Limits.reflexivePair f g s sl sr).obj CategoryTheory.Limits.WalkingReflexivePair.zero = B

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

noncomputable def CategoryTheory.Limits.ofIsReflexivePair {C : Type u} [CategoryTheory.Category.{v, u} C] {A B : C} (f g : A ⟶ B) [CategoryTheory.IsReflexivePair f g] : CategoryTheory.Functor CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {A B : C} (f g : A ⟶ B) [CategoryTheory.IsReflexivePair f g] : (CategoryTheory.Limits.ofIsReflexivePair f g).map CategoryTheory.Limits.WalkingReflexivePair.Hom.left = f

@[simp]

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

noncomputable def CategoryTheory.Limits.inclusionWalkingReflexivePairOfIsReflexivePairIso {C : Type u} [CategoryTheory.Category.{v, u} C] {A B : C} (f g : A ⟶ B) [CategoryTheory.IsReflexivePair f g] : CategoryTheory.Limits.WalkingParallelPair.inclusionWalkingReflexivePair.comp (CategoryTheory.Limits.ofIsReflexivePair f g) ≅ CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C} (e₀ : F.obj CategoryTheory.Limits.WalkingReflexivePair.zero ⟶ G.obj CategoryTheory.Limits.WalkingReflexivePair.zero) (e₁ : F.obj CategoryTheory.Limits.WalkingReflexivePair.one ⟶ G.obj CategoryTheory.Limits.WalkingReflexivePair.one) (h₁ : CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left) e₀ = CategoryTheory.CategoryStruct.comp e₁ (G.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left) := by aesop_cat) (h₂ : CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right) e₀ = CategoryTheory.CategoryStruct.comp e₁ (G.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right) := by aesop_cat) (h₃ : CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion) e₁ = CategoryTheory.CategoryStruct.comp e₀ (G.map CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C} (e₀ : F.obj CategoryTheory.Limits.WalkingReflexivePair.zero ⟶ G.obj CategoryTheory.Limits.WalkingReflexivePair.zero) (e₁ : F.obj CategoryTheory.Limits.WalkingReflexivePair.one ⟶ G.obj CategoryTheory.Limits.WalkingReflexivePair.one) (h₁ : CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left) e₀ = CategoryTheory.CategoryStruct.comp e₁ (G.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left) := by aesop_cat) (h₂ : CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right) e₀ = CategoryTheory.CategoryStruct.comp e₁ (G.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right) := by aesop_cat) (h₃ : CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion) e₁ = CategoryTheory.CategoryStruct.comp e₀ (G.map CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion) := by aesop_cat) : (CategoryTheory.Limits.reflexivePair.mkNatTrans e₀ e₁ h₁ h₂ h₃).app CategoryTheory.Limits.WalkingReflexivePair.zero = e₀

@[simp]

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

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

@[simp]

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

def CategoryTheory.Limits.reflexivePair.diagramIsoReflexivePair {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C) : F ≅ CategoryTheory.Limits.reflexivePair (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left) (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right) (F.map CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C) (x : CategoryTheory.Limits.WalkingReflexivePair) : (CategoryTheory.Limits.reflexivePair.diagramIsoReflexivePair F).inv.app x = match x with | CategoryTheory.Limits.WalkingReflexivePair.zero => CategoryTheory.CategoryStruct.id (F.obj CategoryTheory.Limits.WalkingReflexivePair.zero) | CategoryTheory.Limits.WalkingReflexivePair.one => CategoryTheory.CategoryStruct.id (F.obj CategoryTheory.Limits.WalkingReflexivePair.one)

@[simp]

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

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

@[simp]

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

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

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

Any functor out of the WalkingReflexivePair yields a reflexive pair

@[reducible, inline]

abbrev CategoryTheory.Limits.ReflexiveCofork {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C} (G : CategoryTheory.Limits.ReflexiveCofork F) : F.obj CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C} {X : C} (π : F.obj CategoryTheory.Limits.WalkingReflexivePair.zero ⟶ X) (h : CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left) π = CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right) π) : CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C} {X : C} (π : F.obj CategoryTheory.Limits.WalkingReflexivePair.zero ⟶ X) (h : CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left) π = CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right) π) : (CategoryTheory.Limits.ReflexiveCofork.mk π h).pt = X

@[simp]

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

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

@[simp]

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

@[reducible, inline]

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

The underlying Cofork of a ReflexiveCofork.

Equations

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

def CategoryTheory.Limits.reflexiveCoforkEquivCofork {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C) : CategoryTheory.Limits.ReflexiveCofork F ≌ CategoryTheory.Limits.Cofork (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left) (F.map CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C) (X : CategoryTheory.Limits.Cofork (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left) (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right)) : ((CategoryTheory.Limits.reflexiveCoforkEquivCofork F).inverse.obj X).pt = X.pt

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Limits.reflexiveCoforkEquivCoforkObjIso {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C) (G : CategoryTheory.Limits.ReflexiveCofork F) : (CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C) : CategoryTheory.Limits.HasColimit F ↔ CategoryTheory.Limits.HasCoequalizer (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left) (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right)

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

def CategoryTheory.Limits.ReflexiveCofork.isColimitEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C) (G : CategoryTheory.Limits.ReflexiveCofork F) : CategoryTheory.Limits.IsColimit G.toCofork ≃ CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C) [CategoryTheory.Limits.HasCoequalizer (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left) (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right)] : CategoryTheory.Limits.colimit F ≅ CategoryTheory.Limits.coequalizer (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left) (F.map CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C) [CategoryTheory.Limits.HasCoequalizer (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left) (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F CategoryTheory.Limits.WalkingReflexivePair.zero) (CategoryTheory.Limits.reflexiveCoequalizerIsoCoequalizer F).hom = CategoryTheory.Limits.coequalizer.π (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left) (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right)

@[simp]

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

@[simp]

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

@[simp]

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

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

def CategoryTheory.Limits.colimitOfIsReflexivePairIsoCoequalizer {C : Type u} [CategoryTheory.Category.{v, u} C] {A B : C} {f g : A ⟶ B} [CategoryTheory.IsReflexivePair f g] [h : CategoryTheory.Limits.HasCoequalizer f g] : CategoryTheory.Limits.colimit (CategoryTheory.Limits.ofIsReflexivePair f g) ≅ CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {A B : C} {f g : A ⟶ B} [CategoryTheory.IsReflexivePair f g] [h : CategoryTheory.Limits.HasCoequalizer f g] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.ofIsReflexivePair f g) CategoryTheory.Limits.WalkingReflexivePair.zero) CategoryTheory.Limits.colimitOfIsReflexivePairIsoCoequalizer.hom = CategoryTheory.Limits.coequalizer.π f g

@[simp]

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

@[simp]

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

@[simp]

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

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

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