Mathlib.CategoryTheory.Limits.Shapes.Equalizers

CategoryTheory.Limits.WalkingParallelPair inductive

: Type

Full source

/-- The type of objects for the diagram indexing a (co)equalizer. -/
inductive WalkingParallelPair : Type
  | zero
  | one
  deriving DecidableEq, Inhabited

Indexing category for (co)equalizer diagrams

Informal description

The inductive type `WalkingParallelPair` represents the indexing category used for (co)equalizer diagrams in category theory. It consists of two objects and two parallel morphisms between them, forming the basic diagram over which (co)equalizers are defined.

CategoryTheory.Limits.instDecidableEqWalkingParallelPair instance

: DecidableEq✝ CategoryTheory.Limits.WalkingParallelPair

Full source

DecidableEq, Inhabited

Decidable Equality for the Indexing Category of (Co)equalizers

Informal description

The indexing category `WalkingParallelPair` for (co)equalizer diagrams has decidable equality.

CategoryTheory.Limits.instInhabitedWalkingParallelPair instance

: Inhabited✝ (@CategoryTheory.Limits.WalkingParallelPair)

Full source

Inhabited

Inhabited Indexing Category for (Co)equalizers

Informal description

The indexing category `WalkingParallelPair` for (co)equalizer diagrams is inhabited.

CategoryTheory.Limits.WalkingParallelPairHom inductive

: WalkingParallelPair → WalkingParallelPair → Type

Full source

/-- The type family of morphisms for the diagram indexing a (co)equalizer. -/
inductive WalkingParallelPairHom : WalkingParallelPair → WalkingParallelPair → Type
  | left : WalkingParallelPairHom zero one
  | right : WalkingParallelPairHom zero one
  | id (X : WalkingParallelPair) : WalkingParallelPairHom X X
  deriving DecidableEq

Morphisms in the indexing category for (co)equalizers

Informal description

The type family `WalkingParallelPairHom` represents the morphisms in the indexing category for (co)equalizer diagrams. It consists of the identity morphisms for each object and two parallel morphisms between the two objects, forming the basic structure over which (co)equalizers are defined.

CategoryTheory.Limits.instDecidableEqWalkingParallelPairHom instance

{a✝} {a✝¹} : DecidableEq✝ (@CategoryTheory.Limits.WalkingParallelPairHom✝ a✝ a✝¹)

Full source

DecidableEq

Decidable Equality of Morphisms in the Walking Parallel Pair Category

Informal description

For any two morphisms in the indexing category for (co)equalizer diagrams, there is a decidable equality relation between them.

CategoryTheory.Limits.instInhabitedWalkingParallelPairHomZeroOne instance

: Inhabited (WalkingParallelPairHom zero one)

Full source

/-- Satisfying the inhabited linter -/
instance : Inhabited (WalkingParallelPairHom zero one) where default := WalkingParallelPairHom.left

Inhabited Morphisms from Zero to One in Walking Parallel Pair Category

Informal description

The type of morphisms from the object `zero` to the object `one` in the walking parallel pair category is inhabited.

CategoryTheory.Limits.WalkingParallelPairHom.comp definition

 :
  -- Porting note: changed X Y Z to implicit to match comp fields in precategory∀ {X Y Z : WalkingParallelPair}
    (_ : WalkingParallelPairHom X Y) (_ : WalkingParallelPairHom Y Z), WalkingParallelPairHom X Z

Full source

/-- Composition of morphisms in the indexing diagram for (co)equalizers. -/
def WalkingParallelPairHom.comp :
    -- Porting note: changed X Y Z to implicit to match comp fields in precategory
    ∀ {X Y Z : WalkingParallelPair} (_ : WalkingParallelPairHom X Y)
      (_ : WalkingParallelPairHom Y Z), WalkingParallelPairHom X Z
  | _, _, _, id _, h => h
  | _, _, _, left, id one => left
  | _, _, _, right, id one => right

Composition of morphisms in the walking parallel pair category

Informal description

The composition of morphisms in the indexing category for (co)equalizers. Given morphisms $f : X \to Y$ and $g : Y \to Z$ in the walking parallel pair category, their composition $f \circ g : X \to Z$ is defined as follows: - If $f$ is the identity morphism, then $f \circ g = g$. - If $g$ is the identity morphism on the object `one`, then: - If $f$ is the left morphism, $f \circ g$ is the left morphism. - If $f$ is the right morphism, $f \circ g$ is the right morphism.

CategoryTheory.Limits.WalkingParallelPairHom.id_comp theorem

{X Y : WalkingParallelPair} (g : WalkingParallelPairHom X Y) : comp (id X) g = g

Full source

theorem WalkingParallelPairHom.id_comp
    {X Y : WalkingParallelPair} (g : WalkingParallelPairHom X Y) : comp (id X) g = g :=
  rfl

Left Identity Law for Morphisms in Walking Parallel Pair Category

Informal description

For any morphism $g : X \to Y$ in the walking parallel pair category, the composition of the identity morphism $\mathrm{id}_X$ with $g$ equals $g$, i.e., $\mathrm{id}_X \circ g = g$.

CategoryTheory.Limits.WalkingParallelPairHom.comp_id theorem

{X Y : WalkingParallelPair} (f : WalkingParallelPairHom X Y) : comp f (id Y) = f

Full source

theorem WalkingParallelPairHom.comp_id
    {X Y : WalkingParallelPair} (f : WalkingParallelPairHom X Y) : comp f (id Y) = f := by
  cases f <;> rfl

Right Identity Law for Morphisms in Walking Parallel Pair Category

Informal description

For any morphism $f : X \to Y$ in the walking parallel pair category, the composition of $f$ with the identity morphism $\mathrm{id}_Y$ equals $f$, i.e., $f \circ \mathrm{id}_Y = f$.

CategoryTheory.Limits.WalkingParallelPairHom.assoc theorem

 {X Y Z W : WalkingParallelPair} (f : WalkingParallelPairHom X Y) (g : WalkingParallelPairHom Y Z)
  (h : WalkingParallelPairHom Z W) : comp (comp f g) h = comp f (comp g h)

Full source

theorem WalkingParallelPairHom.assoc {X Y Z W : WalkingParallelPair}
    (f : WalkingParallelPairHom X Y) (g : WalkingParallelPairHom Y Z)
    (h : WalkingParallelPairHom Z W) : comp (comp f g) h = comp f (comp g h) := by
  cases f <;> cases g <;> cases h <;> rfl

Associativity of Composition in Walking Parallel Pair Category

Informal description

For any morphisms $f \colon X \to Y$, $g \colon Y \to Z$, and $h \colon Z \to W$ in the walking parallel pair category, the composition operation satisfies the associativity law: $$(f \circ g) \circ h = f \circ (g \circ h).$$

CategoryTheory.Limits.walkingParallelPairHomCategory instance

: SmallCategory WalkingParallelPair

Full source

instance walkingParallelPairHomCategory : SmallCategory WalkingParallelPair where
  Hom := WalkingParallelPairHom
  id := id
  comp := comp
  comp_id := comp_id
  id_comp := id_comp
  assoc := assoc

The Small Category Structure on Walking Parallel Pair

Informal description

The walking parallel pair category is a small category consisting of two objects and two parallel morphisms between them, which serves as the indexing category for (co)equalizer diagrams in category theory.

CategoryTheory.Limits.walkingParallelPairHom_id theorem

(X : WalkingParallelPair) : WalkingParallelPairHom.id X = 𝟙 X

Full source

@[simp]
theorem walkingParallelPairHom_id (X : WalkingParallelPair) : WalkingParallelPairHom.id X = 𝟙 X :=
  rfl

Identity Morphism in Walking Parallel Pair Category

Informal description

For any object $X$ in the walking parallel pair category, the identity morphism defined by `WalkingParallelPairHom.id` is equal to the categorical identity morphism $\mathrm{id}_X$.

CategoryTheory.Limits.walkingParallelPairOp definition

: WalkingParallelPair ⥤ WalkingParallelPairᵒᵖ

Full source

/-- The functor `WalkingParallelPair ⥤ WalkingParallelPairᵒᵖ` sending left to left and right to
right.
-/
def walkingParallelPairOp : WalkingParallelPairWalkingParallelPair ⥤ WalkingParallelPairᵒᵖ where
  obj x := op <| by cases x; exacts [one, zero]
  map f := by
    cases f <;> apply Quiver.Hom.op
    exacts [left, right, WalkingParallelPairHom.id _]
  map_comp := by rintro _ _ _ (_|_|_) g <;> cases g <;> rfl

Opposite functor of the walking parallel pair category

Informal description

The functor from the walking parallel pair category to its opposite category, which maps the objects by swapping them and preserves the morphisms (sending left to left and right to right).

CategoryTheory.Limits.walkingParallelPairOp_zero theorem

: walkingParallelPairOp.obj zero = op one

Full source

@[simp]
theorem walkingParallelPairOp_zero : walkingParallelPairOp.obj zero = op one := rfl

Functor Maps Zero to Opposite of One in Walking Parallel Pair Category

Informal description

The functor `walkingParallelPairOp` maps the object `zero` in the walking parallel pair category to the opposite of the object `one`, i.e., $\text{walkingParallelPairOp}(\text{zero}) = \text{op}(\text{one})$.

CategoryTheory.Limits.walkingParallelPairOp_one theorem

: walkingParallelPairOp.obj one = op zero

Full source

@[simp]
theorem walkingParallelPairOp_one : walkingParallelPairOp.obj one = op zero := rfl

Functorial Mapping of `one` to Opposite `zero` in Walking Parallel Pair Category

Informal description

The functor `walkingParallelPairOp` maps the object `one` in the walking parallel pair category to the opposite object `zero` in the opposite category, i.e., $\text{walkingParallelPairOp}(\text{one}) = \text{op}(\text{zero})$.

CategoryTheory.Limits.walkingParallelPairOp_left theorem

: walkingParallelPairOp.map left = @Quiver.Hom.op _ _ zero one left

Full source

@[simp]
theorem walkingParallelPairOp_left :
    walkingParallelPairOp.map left = @Quiver.Hom.op _ _ zero one left := rfl

Mapping of Left Morphism under Opposite Functor for Walking Parallel Pair

Informal description

The functor `walkingParallelPairOp` maps the morphism `left` in the walking parallel pair category to the opposite morphism `left` in the opposite category, where the source and target objects are swapped.

CategoryTheory.Limits.walkingParallelPairOp_right theorem

: walkingParallelPairOp.map right = @Quiver.Hom.op _ _ zero one right

Full source

@[simp]
theorem walkingParallelPairOp_right :
    walkingParallelPairOp.map right = @Quiver.Hom.op _ _ zero one right := rfl

Mapping of Right Morphism under Opposite Functor for Walking Parallel Pair

Informal description

The functor `walkingParallelPairOp` maps the morphism `right` in the walking parallel pair category to the opposite morphism `right` in the opposite category, viewed as a morphism from `zero` to `one` in the opposite category.

CategoryTheory.Limits.walkingParallelPairOpEquiv definition

: WalkingParallelPair ≌ WalkingParallelPairᵒᵖ

Full source

/--
The equivalence `WalkingParallelPair ⥤ WalkingParallelPairᵒᵖ` sending left to left and right to
right.
-/
@[simps functor inverse]
def walkingParallelPairOpEquiv : WalkingParallelPairWalkingParallelPair ≌ WalkingParallelPairᵒᵖ where
  functor := walkingParallelPairOp
  inverse := walkingParallelPairOp.leftOp
  unitIso :=
    NatIso.ofComponents (fun j => eqToIso (by cases j <;> rfl))
      (by rintro _ _ (_ | _ | _) <;> simp)
  counitIso :=
    NatIso.ofComponents (fun j => eqToIso (by
            induction' j with X
            cases X <;> rfl))
      (fun {i} {j} f => by
      induction' i with i
      induction' j with j
      let g := f.unop
      have : f = g.op := rfl
      rw [this]
      cases i <;> cases j <;> cases g <;> rfl)
  functor_unitIso_comp := fun j => by cases j <;> rfl

Equivalence between walking parallel pair category and its opposite

Informal description

The equivalence of categories between the walking parallel pair category and its opposite category, where the functor maps objects by swapping them and preserves the morphisms (sending left to left and right to right), and the inverse functor similarly reverses the objects while preserving the morphisms.

CategoryTheory.Limits.walkingParallelPairOpEquiv_unitIso_zero theorem

: walkingParallelPairOpEquiv.unitIso.app zero = Iso.refl zero

Full source

@[simp]
theorem walkingParallelPairOpEquiv_unitIso_zero :
    walkingParallelPairOpEquiv.unitIso.app zero = Iso.refl zero := rfl

Unit Isomorphism at Zero in Walking Parallel Pair Equivalence

Informal description

The unit isomorphism of the equivalence between the walking parallel pair category and its opposite category, when applied to the object `zero`, is equal to the identity isomorphism on `zero`.

CategoryTheory.Limits.walkingParallelPairOpEquiv_unitIso_one theorem

: walkingParallelPairOpEquiv.unitIso.app one = Iso.refl one

Full source

@[simp]
theorem walkingParallelPairOpEquiv_unitIso_one :
    walkingParallelPairOpEquiv.unitIso.app one = Iso.refl one := rfl

Unit Isomorphism at One in Walking Parallel Pair Equivalence

Informal description

The unit isomorphism of the equivalence between the walking parallel pair category and its opposite category, when applied to the object `one`, is equal to the identity isomorphism on `one`.

CategoryTheory.Limits.walkingParallelPairOpEquiv_counitIso_zero theorem

: walkingParallelPairOpEquiv.counitIso.app (op zero) = Iso.refl (op zero)

Full source

@[simp]
theorem walkingParallelPairOpEquiv_counitIso_zero :
    walkingParallelPairOpEquiv.counitIso.app (op zero) = Iso.refl (op zero) := rfl

Counit Isomorphism at Zero in Walking Parallel Pair Equivalence

Informal description

The counit isomorphism of the equivalence between the walking parallel pair category and its opposite, when applied to the object `zero`, is equal to the identity isomorphism on `op zero`.

CategoryTheory.Limits.walkingParallelPairOpEquiv_counitIso_one theorem

: walkingParallelPairOpEquiv.counitIso.app (op one) = Iso.refl (op one)

Full source

@[simp]
theorem walkingParallelPairOpEquiv_counitIso_one :
    walkingParallelPairOpEquiv.counitIso.app (op one) = Iso.refl (op one) :=
  rfl

Counit isomorphism at one in walking parallel pair equivalence

Informal description

The counit isomorphism of the equivalence between the walking parallel pair category and its opposite category, when applied to the object $\text{op}(\text{one})$, is equal to the identity isomorphism on $\text{op}(\text{one})$.

CategoryTheory.Limits.parallelPair definition

(f g : X ⟶ Y) : WalkingParallelPair ⥤ C

Full source

/-- `parallelPair f g` is the diagram in `C` consisting of the two morphisms `f` and `g` with
    common domain and codomain. -/
def parallelPair (f g : X ⟶ Y) : WalkingParallelPairWalkingParallelPair ⥤ C where
  obj x :=
    match x with
    | zero => X
    | one => Y
  map h :=
    match h with
    | WalkingParallelPairHom.id _ => 𝟙 _
    | left => f
    | right => g
  -- `sorry` can cope with this, but it's too slow:
  map_comp := by
    rintro _ _ _ ⟨⟩ g <;> cases g <;> {dsimp; simp}

Parallel pair functor

Informal description

Given two parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$, the functor $\text{parallelPair}(f, g)$ maps the objects of the walking parallel pair category to $X$ and $Y$, and the non-identity morphisms to $f$ and $g$ respectively. This functor encodes the diagram consisting of $X$ and $Y$ with two parallel arrows between them given by $f$ and $g$.

CategoryTheory.Limits.parallelPair_obj_zero theorem

(f g : X ⟶ Y) : (parallelPair f g).obj zero = X

Full source

@[simp]
theorem parallelPair_obj_zero (f g : X ⟶ Y) : (parallelPair f g).obj zero = X := rfl

Parallel Pair Functor Maps Zero to Domain

Informal description

For any two parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$, the functor $\text{parallelPair}(f, g)$ maps the object $\text{zero}$ of the walking parallel pair category to the object $X$ in $\mathcal{C}$.

CategoryTheory.Limits.parallelPair_obj_one theorem

(f g : X ⟶ Y) : (parallelPair f g).obj one = Y

Full source

@[simp]
theorem parallelPair_obj_one (f g : X ⟶ Y) : (parallelPair f g).obj one = Y := rfl

Parallel Pair Functor Maps One to Codomain

Informal description

For any two parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$, the object assigned to `one` by the parallel pair functor $\text{parallelPair}(f, g)$ is $Y$. That is, $\text{parallelPair}(f, g)(\text{one}) = Y$.

CategoryTheory.Limits.parallelPair_map_left theorem

(f g : X ⟶ Y) : (parallelPair f g).map left = f

Full source

@[simp]
theorem parallelPair_map_left (f g : X ⟶ Y) : (parallelPair f g).map left = f := rfl

Left morphism mapping in parallel pair functor

Informal description

For any two parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$, the functor $\text{parallelPair}(f, g)$ maps the left morphism of the walking parallel pair category to $f$.

CategoryTheory.Limits.parallelPair_map_right theorem

(f g : X ⟶ Y) : (parallelPair f g).map right = g

Full source

@[simp]
theorem parallelPair_map_right (f g : X ⟶ Y) : (parallelPair f g).map right = g := rfl

Right morphism in parallel pair equals $g$

Informal description

For any two parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$, the image of the right morphism under the parallel pair functor $\text{parallelPair}(f, g)$ is equal to $g$.

CategoryTheory.Limits.parallelPair_functor_obj theorem

{F : WalkingParallelPair ⥤ C} (j : WalkingParallelPair) : (parallelPair (F.map left) (F.map right)).obj j = F.obj j

Full source

@[simp]
theorem parallelPair_functor_obj {F : WalkingParallelPairWalkingParallelPair ⥤ C} (j : WalkingParallelPair) :
    (parallelPair (F.map left) (F.map right)).obj j = F.obj j := by cases j <;> rfl

Parallel Pair Functor Preserves Objects

Informal description

For any functor $F$ from the walking parallel pair category to a category $\mathcal{C}$, and for any object $j$ in the walking parallel pair category, the object obtained by applying the parallel pair functor (constructed from $F$'s actions on the left and right morphisms) to $j$ is equal to $F$ applied to $j$. In other words, $(\text{parallelPair}(F(\text{left}), F(\text{right})))(j) = F(j)$.

CategoryTheory.Limits.diagramIsoParallelPair definition

(F : WalkingParallelPair ⥤ C) : F ≅ parallelPair (F.map left) (F.map right)

Full source

/-- Every functor indexing a (co)equalizer is naturally isomorphic (actually, equal) to a
    `parallelPair` -/
@[simps!]
def diagramIsoParallelPair (F : WalkingParallelPairWalkingParallelPair ⥤ C) :
    F ≅ parallelPair (F.map left) (F.map right) :=
  NatIso.ofComponents (fun j => eqToIso <| by cases j <;> rfl) (by rintro _ _ (_|_|_) <;> simp)

Natural isomorphism between a functor and its parallel pair representation

Informal description

For any functor $F$ from the walking parallel pair category to a category $\mathcal{C}$, there is a natural isomorphism between $F$ and the parallel pair functor formed by the images of the left and right morphisms under $F$. This isomorphism is constructed componentwise, with each component being an isomorphism induced by equality of objects.

CategoryTheory.Limits.parallelPairHom definition

 {X' Y' : C} (f g : X ⟶ Y) (f' g' : X' ⟶ Y') (p : X ⟶ X') (q : Y ⟶ Y') (wf : f ≫ q = p ≫ f') (wg : g ≫ q = p ≫ g') :
  parallelPair f g ⟶ parallelPair f' g'

Full source

/-- Construct a morphism between parallel pairs. -/
def parallelPairHom {X' Y' : C} (f g : X ⟶ Y) (f' g' : X' ⟶ Y') (p : X ⟶ X') (q : Y ⟶ Y')
    (wf : f ≫ q = p ≫ f') (wg : g ≫ q = p ≫ g') : parallelPairparallelPair f g ⟶ parallelPair f' g' where
  app j :=
    match j with
    | zero => p
    | one => q
  naturality := by
    rintro _ _ ⟨⟩ <;> {dsimp; simp [wf,wg]}

Natural transformation between parallel pairs

Informal description

Given two parallel pairs of morphisms $(f, g : X \to Y)$ and $(f', g' : X' \to Y')$ in a category $\mathcal{C}$, and morphisms $p : X \to X'$ and $q : Y \to Y'$ such that the diagrams commute (i.e., $f \circ q = p \circ f'$ and $g \circ q = p \circ g'$), the function `parallelPairHom` constructs a natural transformation from the parallel pair functor of $(f, g)$ to the parallel pair functor of $(f', g')$. Specifically, the natural transformation maps: - The object `zero` to $p$ - The object `one` to $q$

CategoryTheory.Limits.parallelPairHom_app_zero theorem

 {X' Y' : C} (f g : X ⟶ Y) (f' g' : X' ⟶ Y') (p : X ⟶ X') (q : Y ⟶ Y') (wf : f ≫ q = p ≫ f') (wg : g ≫ q = p ≫ g') :
  (parallelPairHom f g f' g' p q wf wg).app zero = p

Full source

@[simp]
theorem parallelPairHom_app_zero {X' Y' : C} (f g : X ⟶ Y) (f' g' : X' ⟶ Y') (p : X ⟶ X')
    (q : Y ⟶ Y') (wf : f ≫ q = p ≫ f') (wg : g ≫ q = p ≫ g') :
    (parallelPairHom f g f' g' p q wf wg).app zero = p :=
  rfl

Zero Component of Parallel Pair Natural Transformation Equals $p$

Informal description

Given two parallel pairs of morphisms $(f, g : X \to Y)$ and $(f', g' : X' \to Y')$ in a category $\mathcal{C}$, and morphisms $p : X \to X'$ and $q : Y \to Y'$ such that the diagrams commute (i.e., $f \circ q = p \circ f'$ and $g \circ q = p \circ g'$), the zero component of the natural transformation $\text{parallelPairHom}(f, g, f', g', p, q, wf, wg)$ is equal to $p$.

CategoryTheory.Limits.parallelPairHom_app_one theorem

 {X' Y' : C} (f g : X ⟶ Y) (f' g' : X' ⟶ Y') (p : X ⟶ X') (q : Y ⟶ Y') (wf : f ≫ q = p ≫ f') (wg : g ≫ q = p ≫ g') :
  (parallelPairHom f g f' g' p q wf wg).app one = q

Full source

@[simp]
theorem parallelPairHom_app_one {X' Y' : C} (f g : X ⟶ Y) (f' g' : X' ⟶ Y') (p : X ⟶ X')
    (q : Y ⟶ Y') (wf : f ≫ q = p ≫ f') (wg : g ≫ q = p ≫ g') :
    (parallelPairHom f g f' g' p q wf wg).app one = q :=
  rfl

Component at One of Natural Transformation Between Parallel Pairs Equals $q$

Informal description

Given two parallel pairs of morphisms $(f, g : X \to Y)$ and $(f', g' : X' \to Y')$ in a category $\mathcal{C}$, and morphisms $p : X \to X'$ and $q : Y \to Y'$ such that the diagrams commute (i.e., $f \circ q = p \circ f'$ and $g \circ q = p \circ g'$), the component of the natural transformation $\text{parallelPairHom}(f, g, f', g', p, q, wf, wg)$ at the object $\text{one}$ is equal to $q$.

CategoryTheory.Limits.parallelPair.ext definition

 {F G : WalkingParallelPair ⥤ C} (zero : F.obj zero ≅ G.obj zero) (one : F.obj one ≅ G.obj one)
  (left : F.map left ≫ one.hom = zero.hom ≫ G.map left) (right : F.map right ≫ one.hom = zero.hom ≫ G.map right) : F ≅ G

Full source

/-- Construct a natural isomorphism between functors out of the walking parallel pair from
its components. -/
@[simps!]
def parallelPair.ext {F G : WalkingParallelPairWalkingParallelPair ⥤ C} (zero : F.obj zero ≅ G.obj zero)
    (one : F.obj one ≅ G.obj one) (left : F.map left ≫ one.hom = zero.hom ≫ G.map left)
    (right : F.map right ≫ one.hom = zero.hom ≫ G.map right) : F ≅ G :=
  NatIso.ofComponents
    (by
      rintro ⟨j⟩
      exacts [zero, one])
    (by rintro _ _ ⟨_⟩ <;> simp [left, right])

Natural isomorphism between parallel pair functors

Informal description

Given two functors $F, G$ from the walking parallel pair category to a category $\mathcal{C}$, and isomorphisms $\text{zero} : F(\text{zero}) \cong G(\text{zero})$ and $\text{one} : F(\text{one}) \cong G(\text{one})$ between their images on the two objects, along with commuting squares for the left and right morphisms, there exists a natural isomorphism $F \cong G$.

CategoryTheory.Limits.parallelPair.eqOfHomEq definition

{f g f' g' : X ⟶ Y} (hf : f = f') (hg : g = g') : parallelPair f g ≅ parallelPair f' g'

Full source

/-- Construct a natural isomorphism between `parallelPair f g` and `parallelPair f' g'` given
equalities `f = f'` and `g = g'`. -/
@[simps!]
def parallelPair.eqOfHomEq {f g f' g' : X ⟶ Y} (hf : f = f') (hg : g = g') :
    parallelPairparallelPair f g ≅ parallelPair f' g' :=
  parallelPair.ext (Iso.refl _) (Iso.refl _) (by simp [hf]) (by simp [hg])

Natural isomorphism of parallel pairs under equality of morphisms

Informal description

Given two pairs of parallel morphisms $(f, g)$ and $(f', g')$ from $X$ to $Y$ in a category $\mathcal{C}$, if $f = f'$ and $g = g'$, then the parallel pair functors $\text{parallelPair}(f, g)$ and $\text{parallelPair}(f', g')$ are naturally isomorphic.

CategoryTheory.Limits.Fork abbrev

(f g : X ⟶ Y)

Full source

/-- A fork on `f` and `g` is just a `Cone (parallelPair f g)`. -/
abbrev Fork (f g : X ⟶ Y) :=
  Cone (parallelPair f g)

Fork as a Cone over a Parallel Pair

Informal description

A *fork* on two parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$ is a cone over the diagram formed by the parallel pair $(f, g)$.

CategoryTheory.Limits.Cofork abbrev

(f g : X ⟶ Y)

Full source

/-- A cofork on `f` and `g` is just a `Cocone (parallelPair f g)`. -/
abbrev Cofork (f g : X ⟶ Y) :=
  Cocone (parallelPair f g)

Cofork Construction for Parallel Morphisms

Informal description

Given two parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$, a cofork on $f$ and $g$ is a cocone over the diagram formed by the parallel pair $(f, g)$.

CategoryTheory.Limits.Fork.ι definition

(t : Fork f g)

Full source

/-- A fork `t` on the parallel pair `f g : X ⟶ Y` consists of two morphisms
    `t.π.app zero : t.pt ⟶ X`
    and `t.π.app one : t.pt ⟶ Y`. Of these, only the first one is interesting, and we give it the
    shorter name `Fork.ι t`. -/
def Fork.ι (t : Fork f g) :=
  t.π.app zero

Inclusion morphism of a fork

Informal description

Given a fork $t$ on two parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$, the morphism $\iota_t : t.\text{pt} \to X$ is the component of the natural transformation $t.\pi$ at the first object of the walking parallel pair category. This morphism represents the "interesting part" of the fork, as the other component is determined by composition with $f$ or $g$.

CategoryTheory.Limits.Fork.app_zero_eq_ι theorem

(t : Fork f g) : t.π.app zero = t.ι

Full source

@[simp]
theorem Fork.app_zero_eq_ι (t : Fork f g) : t.π.app zero = t.ι :=
  rfl

Fork Component at Zero Equals Inclusion Morphism

Informal description

For any fork $t$ on parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$, the component of the natural transformation $t.\pi$ at the zero object of the walking parallel pair category equals the inclusion morphism $\iota_t$ of the fork, i.e., $t.\pi(\text{zero}) = t.\iota$.

CategoryTheory.Limits.Cofork.π definition

(t : Cofork f g)

Full source

/-- A cofork `t` on the parallelPair `f g : X ⟶ Y` consists of two morphisms
    `t.ι.app zero : X ⟶ t.pt` and `t.ι.app one : Y ⟶ t.pt`. Of these, only the second one is
    interesting, and we give it the shorter name `Cofork.π t`. -/
def Cofork.π (t : Cofork f g) :=
  t.ι.app one

Cofork projection morphism

Informal description

Given a cofork $t$ on the parallel pair of morphisms $f, g : X \to Y$ in a category $\mathcal{C}$, the morphism $\pi_t : Y \to t.pt$ is the component of the cocone $t$ at the target object $Y$ (where $t.pt$ is the vertex of the cocone). This is the only non-trivial morphism in the cofork structure.

CategoryTheory.Limits.Cofork.app_one_eq_π theorem

(t : Cofork f g) : t.ι.app one = t.π

Full source

@[simp]
theorem Cofork.app_one_eq_π (t : Cofork f g) : t.ι.app one = t.π :=
  rfl

Cofork Component at One Equals Projection Morphism

Informal description

For any cofork $t$ of parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$, the cocone's component at the terminal object of the walking parallel pair category equals the cofork's projection morphism, i.e., $t.\iota(\text{one}) = t.\pi$.

CategoryTheory.Limits.Fork.app_one_eq_ι_comp_left theorem

(s : Fork f g) : s.π.app one = s.ι ≫ f

Full source

@[simp]
theorem Fork.app_one_eq_ι_comp_left (s : Fork f g) : s.π.app one = s.ι ≫ f := by
  rw [← s.app_zero_eq_ι, ← s.w left, parallelPair_map_left]

Fork Component at One Equals Inclusion Composed with Left Morphism

Informal description

For any fork $s$ of parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$, the component of the cone $s.\pi$ at the terminal object of the walking parallel pair category equals the composition of the inclusion morphism $s.\iota$ with $f$, i.e., $s.\pi(\text{one}) = s.\iota \circ f$.

CategoryTheory.Limits.Fork.app_one_eq_ι_comp_right theorem

(s : Fork f g) : s.π.app one = s.ι ≫ g

Full source

@[reassoc]
theorem Fork.app_one_eq_ι_comp_right (s : Fork f g) : s.π.app one = s.ι ≫ g := by
  rw [← s.app_zero_eq_ι, ← s.w right, parallelPair_map_right]

Fork Component at One Equals Inclusion Composed with Right Morphism

Informal description

For any fork $s$ of parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$, the component of the natural transformation $s.\pi$ at the terminal object of the walking parallel pair category equals the composition of the inclusion morphism $s.\iota$ with $g$, i.e., $s.\pi(\text{one}) = s.\iota \circ g$.

CategoryTheory.Limits.Cofork.app_zero_eq_comp_π_left theorem

(s : Cofork f g) : s.ι.app zero = f ≫ s.π

Full source

@[simp]
theorem Cofork.app_zero_eq_comp_π_left (s : Cofork f g) : s.ι.app zero = f ≫ s.π := by
  rw [← s.app_one_eq_π, ← s.w left, parallelPair_map_left]

Cofork Component at Zero Equals Composition of Left Morphism with Projection

Informal description

For any cofork $s$ of parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$, the cocone's component at the initial object of the walking parallel pair category satisfies $s.\iota(\text{zero}) = f \circ s.\pi$.

CategoryTheory.Limits.Cofork.app_zero_eq_comp_π_right theorem

(s : Cofork f g) : s.ι.app zero = g ≫ s.π

Full source

@[reassoc]
theorem Cofork.app_zero_eq_comp_π_right (s : Cofork f g) : s.ι.app zero = g ≫ s.π := by
  rw [← s.app_one_eq_π, ← s.w right, parallelPair_map_right]

Cofork Component at Zero Equals Composition with Projection via Right Morphism

Informal description

For any cofork $s$ of parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$, the cocone's component at the initial object of the walking parallel pair category equals the composition of $g$ with the cofork's projection morphism, i.e., $s.\iota(\text{zero}) = g \circ s.\pi$.

CategoryTheory.Limits.Fork.ofι definition

{P : C} (ι : P ⟶ X) (w : ι ≫ f = ι ≫ g) : Fork f g

Full source

/-- A fork on `f g : X ⟶ Y` is determined by the morphism `ι : P ⟶ X` satisfying `ι ≫ f = ι ≫ g`.
-/
@[simps]
def Fork.ofι {P : C} (ι : P ⟶ X) (w : ι ≫ f = ι ≫ g) : Fork f g where
  pt := P
  π :=
    { app := fun X => by
        cases X
        · exact ι
        · exact ι ≫ f
      naturality := fun {X} {Y} f =>
        by cases X <;> cases Y <;> cases f <;> dsimp <;> simp; assumption }

Construction of a fork from a morphism satisfying the parallel condition

Informal description

Given an object $P$ in a category $\mathcal{C}$ and a morphism $\iota : P \to X$ such that $\iota \circ f = \iota \circ g$, the function `Fork.ofι` constructs a fork over the parallel pair $(f, g : X \to Y)$. The constructed fork has $P$ as its vertex and $\iota$ as the morphism from $P$ to $X$, with the condition that the compositions $\iota \circ f$ and $\iota \circ g$ are equal.

CategoryTheory.Limits.Cofork.ofπ definition

{P : C} (π : Y ⟶ P) (w : f ≫ π = g ≫ π) : Cofork f g

Full source

/-- A cofork on `f g : X ⟶ Y` is determined by the morphism `π : Y ⟶ P` satisfying
    `f ≫ π = g ≫ π`. -/
@[simps]
def Cofork.ofπ {P : C} (π : Y ⟶ P) (w : f ≫ π = g ≫ π) : Cofork f g where
  pt := P
  ι :=
    { app := fun X => WalkingParallelPair.casesOn X (f ≫ π) π
      naturality := fun i j f => by cases f <;> dsimp <;> simp [w] }

Cofork construction from a morphism satisfying the coequalizer condition

Informal description

Given an object $P$ in a category $\mathcal{C}$ and a morphism $\pi: Y \to P$ such that $f \circ \pi = g \circ \pi$, the construction `Cofork.ofπ` produces a cofork on the parallel pair of morphisms $f, g: X \to Y$. The cofork consists of the object $P$ and the morphism $\pi$ satisfying the given condition.

CategoryTheory.Limits.Fork.ι_ofι theorem

{P : C} (ι : P ⟶ X) (w : ι ≫ f = ι ≫ g) : (Fork.ofι ι w).ι = ι

Full source

@[simp]
theorem Fork.ι_ofι {P : C} (ι : P ⟶ X) (w : ι ≫ f = ι ≫ g) : (Fork.ofι ι w).ι = ι :=
  rfl

Inclusion Morphism of Constructed Fork Equals Original Morphism

Informal description

Given an object $P$ in a category $\mathcal{C}$ and a morphism $\iota: P \to X$ such that $\iota \circ f = \iota \circ g$, the inclusion morphism $\iota$ of the fork constructed via `Fork.ofι` is equal to $\iota$ itself. In other words, $(Fork.ofι\, \iota\, w).\iota = \iota$.

CategoryTheory.Limits.Cofork.π_ofπ theorem

{P : C} (π : Y ⟶ P) (w : f ≫ π = g ≫ π) : (Cofork.ofπ π w).π = π

Full source

@[simp]
theorem Cofork.π_ofπ {P : C} (π : Y ⟶ P) (w : f ≫ π = g ≫ π) : (Cofork.ofπ π w).π = π :=
  rfl

Cofork Projection of Constructed Cofork Equals Input Morphism

Informal description

For any object $P$ in a category $\mathcal{C}$ and morphism $\pi: Y \to P$ satisfying $f \circ \pi = g \circ \pi$, the projection morphism of the cofork constructed via `Cofork.ofπ` equals $\pi$, i.e., $(Cofork.ofπ\, \pi\, w).π = π$.

CategoryTheory.Limits.Fork.condition theorem

(t : Fork f g) : t.ι ≫ f = t.ι ≫ g

Full source

@[reassoc (attr := simp)]
theorem Fork.condition (t : Fork f g) : t.ι ≫ f = t.ι ≫ g := by
  rw [← t.app_one_eq_ι_comp_left, ← t.app_one_eq_ι_comp_right]

Fork Condition: $\iota \circ f = \iota \circ g$

Informal description

For any fork $t$ of parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$, the composition of the inclusion morphism $t.\iota$ with $f$ equals its composition with $g$, i.e., $t.\iota \circ f = t.\iota \circ g$.

CategoryTheory.Limits.Cofork.condition theorem

(t : Cofork f g) : f ≫ t.π = g ≫ t.π

Full source

@[reassoc (attr := simp)]
theorem Cofork.condition (t : Cofork f g) : f ≫ t.π = g ≫ t.π := by
  rw [← t.app_zero_eq_comp_π_left, ← t.app_zero_eq_comp_π_right]

Cofork Condition: $f \circ \pi = g \circ \pi$

Informal description

For any cofork $t$ of parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$, the composition of $f$ with the cofork's projection morphism $t.\pi : Y \to t.pt$ equals the composition of $g$ with $t.\pi$, i.e., $f \circ t.\pi = g \circ t.\pi$.

CategoryTheory.Limits.Fork.equalizer_ext theorem

 (s : Fork f g) {W : C} {k l : W ⟶ s.pt} (h : k ≫ s.ι = l ≫ s.ι) :
  ∀ j : WalkingParallelPair, k ≫ s.π.app j = l ≫ s.π.app j

Full source

/-- To check whether two maps are equalized by both maps of a fork, it suffices to check it for the
    first map -/
theorem Fork.equalizer_ext (s : Fork f g) {W : C} {k l : W ⟶ s.pt} (h : k ≫ s.ι = l ≫ s.ι) :
    ∀ j : WalkingParallelPair, k ≫ s.π.app j = l ≫ s.π.app j
  | zero => h
  | one => by
    have : k ≫ ι s ≫ f = l ≫ ι s ≫ f := by
      simp only [← Category.assoc]; exact congrArg (· ≫ f) h
    rw [s.app_one_eq_ι_comp_left, this]

Uniqueness of Morphisms into Equalizer Fork via Inclusion Condition

Informal description

Let $s$ be a fork of two parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$. For any object $W$ and any pair of morphisms $k, l : W \to s.\mathrm{pt}$ such that $k \circ s.\iota = l \circ s.\iota$, the compositions $k \circ s.\pi_j$ and $l \circ s.\pi_j$ are equal for all objects $j$ in the walking parallel pair category.

CategoryTheory.Limits.Cofork.coequalizer_ext theorem

 (s : Cofork f g) {W : C} {k l : s.pt ⟶ W} (h : Cofork.π s ≫ k = Cofork.π s ≫ l) :
  ∀ j : WalkingParallelPair, s.ι.app j ≫ k = s.ι.app j ≫ l

Full source

/-- To check whether two maps are coequalized by both maps of a cofork, it suffices to check it for
    the second map -/
theorem Cofork.coequalizer_ext (s : Cofork f g) {W : C} {k l : s.pt ⟶ W}
    (h : Cofork.πCofork.π s ≫ k = Cofork.πCofork.π s ≫ l) : ∀ j : WalkingParallelPair, s.ι.app j ≫ k = s.ι.app j ≫ l
  | zero => by simp only [s.app_zero_eq_comp_π_left, Category.assoc, h]
  | one => h

Morphism Equality Extension Property for Cofork Projections

Informal description

Let $s$ be a cofork of parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$. For any object $W$ and any pair of morphisms $k, l : s.\mathrm{pt} \to W$, if $s.\pi \circ k = s.\pi \circ l$, then for every object $j$ in the walking parallel pair category, we have $s.\iota_j \circ k = s.\iota_j \circ l$.

CategoryTheory.Limits.Fork.IsLimit.hom_ext theorem

{s : Fork f g} (hs : IsLimit s) {W : C} {k l : W ⟶ s.pt} (h : k ≫ Fork.ι s = l ≫ Fork.ι s) : k = l

Full source

theorem Fork.IsLimit.hom_ext {s : Fork f g} (hs : IsLimit s) {W : C} {k l : W ⟶ s.pt}
    (h : k ≫ Fork.ι s = l ≫ Fork.ι s) : k = l :=
  hs.hom_ext <| Fork.equalizer_ext _ h

Uniqueness of Morphisms into Equalizer Limit via Inclusion Condition

Informal description

Let $s$ be a fork of two parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$, and suppose $s$ is a limit cone. For any object $W$ and any pair of morphisms $k, l : W \to s.\mathrm{pt}$ such that $k \circ s.\iota = l \circ s.\iota$, we have $k = l$.

CategoryTheory.Limits.Cofork.IsColimit.hom_ext theorem

{s : Cofork f g} (hs : IsColimit s) {W : C} {k l : s.pt ⟶ W} (h : Cofork.π s ≫ k = Cofork.π s ≫ l) : k = l

Full source

theorem Cofork.IsColimit.hom_ext {s : Cofork f g} (hs : IsColimit s) {W : C} {k l : s.pt ⟶ W}
    (h : Cofork.πCofork.π s ≫ k = Cofork.πCofork.π s ≫ l) : k = l :=
  hs.hom_ext <| Cofork.coequalizer_ext _ h

Uniqueness of Morphisms from Colimit Cofork

Informal description

Let $s$ be a cofork of parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$, and suppose $s$ is a colimit cofork. For any object $W$ and any pair of morphisms $k, l : s.\mathrm{pt} \to W$, if the compositions $s.\pi \circ k$ and $s.\pi \circ l$ are equal, then $k = l$.

CategoryTheory.Limits.Fork.IsLimit.lift_ι theorem

{s t : Fork f g} (hs : IsLimit s) : hs.lift t ≫ s.ι = t.ι

Full source

@[reassoc (attr := simp)]
theorem Fork.IsLimit.lift_ι {s t : Fork f g} (hs : IsLimit s) : hs.lift t ≫ s.ι = t.ι :=
  hs.fac _ _

Commutativity of Limit Lift with Fork Inclusion

Informal description

Let $s$ and $t$ be forks over parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$. If $s$ is a limit cone, then the lifting morphism $\text{lift}(s, t) : t.\text{pt} \to s.\text{pt}$ composed with the inclusion morphism $\iota_s : s.\text{pt} \to X$ equals the inclusion morphism $\iota_t : t.\text{pt} \to X$.

CategoryTheory.Limits.Cofork.IsColimit.π_desc theorem

{s t : Cofork f g} (hs : IsColimit s) : s.π ≫ hs.desc t = t.π

Full source

@[reassoc (attr := simp)]
theorem Cofork.IsColimit.π_desc {s t : Cofork f g} (hs : IsColimit s) : s.π ≫ hs.desc t = t.π :=
  hs.fac _ _

Colimit Cofork Projection Property: $\pi_s \circ hs.desc\, t = \pi_t$

Informal description

Given two coforks $s$ and $t$ on parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$, if $s$ is a colimit cofork, then the composition of the cofork projection $\pi_s : Y \to s.pt$ with the colimit-induced morphism $hs.desc\, t : s.pt \to t.pt$ equals the cofork projection $\pi_t : Y \to t.pt$, i.e., $\pi_s \circ hs.desc\, t = \pi_t$.

CategoryTheory.Limits.Fork.IsLimit.lift definition

{s : Fork f g} (hs : IsLimit s) {W : C} (k : W ⟶ X) (h : k ≫ f = k ≫ g) : W ⟶ s.pt

Full source

/-- If `s` is a limit fork over `f` and `g`, then a morphism `k : W ⟶ X` satisfying
    `k ≫ f = k ≫ g` induces a morphism `l : W ⟶ s.pt` such that `l ≫ fork.ι s = k`. -/
def Fork.IsLimit.lift {s : Fork f g} (hs : IsLimit s) {W : C} (k : W ⟶ X) (h : k ≫ f = k ≫ g) :
    W ⟶ s.pt :=
  hs.lift (Fork.ofι _ h)

Universal property of a limit fork

Informal description

Given a limit fork $s$ over parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$, and a morphism $k : W \to X$ such that $k \circ f = k \circ g$, there exists a unique morphism $l : W \to s.\text{pt}$ (where $s.\text{pt}$ is the vertex of the fork) satisfying $l \circ s.\iota = k$, where $s.\iota$ is the morphism from the vertex of the fork to $X$.

CategoryTheory.Limits.Fork.IsLimit.lift_ι' theorem

 {s : Fork f g} (hs : IsLimit s) {W : C} (k : W ⟶ X) (h : k ≫ f = k ≫ g) : Fork.IsLimit.lift hs k h ≫ Fork.ι s = k

Full source

@[reassoc (attr := simp)]
lemma Fork.IsLimit.lift_ι' {s : Fork f g} (hs : IsLimit s) {W : C} (k : W ⟶ X) (h : k ≫ f = k ≫ g) :
    Fork.IsLimit.liftFork.IsLimit.lift hs k h ≫ Fork.ι s = k :=
    hs.fac _ _

Commutativity of Limit Fork Lift with Inclusion: $l \circ \iota_s = k$

Informal description

Given a limit fork $s$ over parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$, and a morphism $k : W \to X$ such that $k \circ f = k \circ g$, the composition of the induced morphism $l : W \to s.\text{pt}$ (where $l$ is obtained from the universal property of the limit) with the fork inclusion $\iota_s : s.\text{pt} \to X$ equals $k$, i.e., $l \circ \iota_s = k$.

CategoryTheory.Limits.Fork.IsLimit.lift' definition

 {s : Fork f g} (hs : IsLimit s) {W : C} (k : W ⟶ X) (h : k ≫ f = k ≫ g) : { l : W ⟶ s.pt // l ≫ Fork.ι s = k }

Full source

/-- If `s` is a limit fork over `f` and `g`, then a morphism `k : W ⟶ X` satisfying
    `k ≫ f = k ≫ g` induces a morphism `l : W ⟶ s.pt` such that `l ≫ fork.ι s = k`. -/
def Fork.IsLimit.lift' {s : Fork f g} (hs : IsLimit s) {W : C} (k : W ⟶ X) (h : k ≫ f = k ≫ g) :
    { l : W ⟶ s.pt // l ≫ Fork.ι s = k } :=
  ⟨Fork.IsLimit.lift hs k h, by simp⟩

Universal property of limit fork (dependent pair version)

Informal description

Given a limit fork $s$ over parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$, and a morphism $k : W \to X$ such that $k \circ f = k \circ g$, there exists a unique morphism $l : W \to s.\mathrm{pt}$ (where $s.\mathrm{pt}$ is the vertex of the fork) satisfying $l \circ s.\iota = k$, where $s.\iota$ is the morphism from the vertex of the fork to $X$. This is presented as a dependent pair consisting of the morphism $l$ and a proof that it satisfies the required commutative condition.

CategoryTheory.Limits.Cofork.IsColimit.desc definition

{s : Cofork f g} (hs : IsColimit s) {W : C} (k : Y ⟶ W) (h : f ≫ k = g ≫ k) : s.pt ⟶ W

Full source

/-- If `s` is a colimit cofork over `f` and `g`, then a morphism `k : Y ⟶ W` satisfying
    `f ≫ k = g ≫ k` induces a morphism `l : s.pt ⟶ W` such that `cofork.π s ≫ l = k`. -/
def Cofork.IsColimit.desc {s : Cofork f g} (hs : IsColimit s) {W : C} (k : Y ⟶ W)
    (h : f ≫ k = g ≫ k) : s.pt ⟶ W :=
  hs.desc (Cofork.ofπ _ h)

Universal property of colimit cofork

Informal description

Given a cofork $ s $ over parallel morphisms $ f, g : X \to Y $ in a category $ \mathcal{C} $, if $ s $ is a colimit cofork, then for any morphism $ k : Y \to W $ satisfying $ f \circ k = g \circ k $, there exists a unique morphism $ l : s.\text{pt} \to W $ such that the cofork projection $ \text{cofork}.\pi \, s $ composed with $ l $ equals $ k $. This morphism $ l $ is the universal morphism induced by the colimit property of $ s $.

CategoryTheory.Limits.Cofork.IsColimit.π_desc' theorem

 {s : Cofork f g} (hs : IsColimit s) {W : C} (k : Y ⟶ W) (h : f ≫ k = g ≫ k) :
  Cofork.π s ≫ Cofork.IsColimit.desc hs k h = k

Full source

@[reassoc (attr := simp)]
lemma Cofork.IsColimit.π_desc' {s : Cofork f g} (hs : IsColimit s) {W : C} (k : Y ⟶ W)
    (h : f ≫ k = g ≫ k) : Cofork.πCofork.π s ≫ Cofork.IsColimit.desc hs k h = k :=
  hs.fac _ _

Commutativity of colimit cofork universal property

Informal description

Given a cofork $s$ over parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$, if $s$ is a colimit cofork, then for any morphism $k : Y \to W$ satisfying $f \circ k = g \circ k$, the composition of the cofork projection $\pi_s : Y \to s.\text{pt}$ with the induced morphism $\text{desc}_s(k) : s.\text{pt} \to W$ equals $k$, i.e., $\pi_s \circ \text{desc}_s(k) = k$.

CategoryTheory.Limits.Cofork.IsColimit.desc' definition

 {s : Cofork f g} (hs : IsColimit s) {W : C} (k : Y ⟶ W) (h : f ≫ k = g ≫ k) : { l : s.pt ⟶ W // Cofork.π s ≫ l = k }

Full source

/-- If `s` is a colimit cofork over `f` and `g`, then a morphism `k : Y ⟶ W` satisfying
    `f ≫ k = g ≫ k` induces a morphism `l : s.pt ⟶ W` such that `cofork.π s ≫ l = k`. -/
def Cofork.IsColimit.desc' {s : Cofork f g} (hs : IsColimit s) {W : C} (k : Y ⟶ W)
    (h : f ≫ k = g ≫ k) : { l : s.pt ⟶ W // Cofork.π s ≫ l = k } :=
  ⟨Cofork.IsColimit.desc hs k h, by simp⟩

Universal property of colimit cofork (subtype version)

Informal description

Given a cofork $ s $ over parallel morphisms $ f, g : X \to Y $ in a category $ \mathcal{C} $, if $ s $ is a colimit cofork, then for any morphism $ k : Y \to W $ satisfying $ f \circ k = g \circ k $, there exists a unique morphism $ l : s.\text{pt} \to W $ such that the cofork projection $ \pi_s $ composed with $ l $ equals $ k $. This morphism $ l $ is the universal morphism induced by the colimit property of $ s $, and it satisfies the equation $ \pi_s \circ l = k $.

CategoryTheory.Limits.Fork.IsLimit.existsUnique theorem

 {s : Fork f g} (hs : IsLimit s) {W : C} (k : W ⟶ X) (h : k ≫ f = k ≫ g) : ∃! l : W ⟶ s.pt, l ≫ Fork.ι s = k

Full source

theorem Fork.IsLimit.existsUnique {s : Fork f g} (hs : IsLimit s) {W : C} (k : W ⟶ X)
    (h : k ≫ f = k ≫ g) : ∃! l : W ⟶ s.pt, l ≫ Fork.ι s = k :=
  ⟨hs.lift <| Fork.ofι _ h, hs.fac _ _, fun _ hm =>
    Fork.IsLimit.hom_ext hs <| hm.symm ▸ (hs.fac (Fork.ofι _ h) WalkingParallelPair.zero).symm⟩

Universal Property of Equalizer Limit Cone

Informal description

Let $s$ be a fork over two parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$, and suppose $s$ is a limit cone. For any object $W$ and any morphism $k : W \to X$ such that $k \circ f = k \circ g$, there exists a unique morphism $l : W \to s.\mathrm{pt}$ satisfying $l \circ s.\iota = k$.

CategoryTheory.Limits.Cofork.IsColimit.existsUnique theorem

 {s : Cofork f g} (hs : IsColimit s) {W : C} (k : Y ⟶ W) (h : f ≫ k = g ≫ k) : ∃! d : s.pt ⟶ W, Cofork.π s ≫ d = k

Full source

theorem Cofork.IsColimit.existsUnique {s : Cofork f g} (hs : IsColimit s) {W : C} (k : Y ⟶ W)
    (h : f ≫ k = g ≫ k) : ∃! d : s.pt ⟶ W, Cofork.π s ≫ d = k :=
  ⟨hs.desc <| Cofork.ofπ _ h, hs.fac _ _, fun _ hm =>
    Cofork.IsColimit.hom_ext hs <| hm.symm ▸ (hs.fac (Cofork.ofπ _ h) WalkingParallelPair.one).symm⟩

Universal property of colimit cofork (unique existence version)

Informal description

Let $\mathcal{C}$ be a category, and let $f, g : X \to Y$ be parallel morphisms in $\mathcal{C}$. Given a cofork $s$ of $f$ and $g$ that is a colimit cofork, then for any object $W$ and morphism $k : Y \to W$ satisfying $f \circ k = g \circ k$, there exists a unique morphism $d : s.\mathrm{pt} \to W$ such that $\pi_s \circ d = k$, where $\pi_s : Y \to s.\mathrm{pt}$ is the cofork projection.

CategoryTheory.Limits.Fork.IsLimit.mk definition

 (t : Fork f g) (lift : ∀ s : Fork f g, s.pt ⟶ t.pt) (fac : ∀ s : Fork f g, lift s ≫ Fork.ι t = Fork.ι s)
  (uniq : ∀ (s : Fork f g) (m : s.pt ⟶ t.pt) (_ : m ≫ t.ι = s.ι), m = lift s) : IsLimit t

Full source

/-- This is a slightly more convenient method to verify that a fork is a limit cone. It
    only asks for a proof of facts that carry any mathematical content -/
@[simps]
def Fork.IsLimit.mk (t : Fork f g) (lift : ∀ s : Fork f g, s.pt ⟶ t.pt)
    (fac : ∀ s : Fork f g, lift s ≫ Fork.ι t = Fork.ι s)
    (uniq : ∀ (s : Fork f g) (m : s.pt ⟶ t.pt) (_ : m ≫ t.ι = s.ι), m = lift s) : IsLimit t :=
  { lift
    fac := fun s j =>
      WalkingParallelPair.casesOn j (fac s) <| by
        erw [← s.w left, ← t.w left, ← Category.assoc, fac]; rfl
    uniq := fun s m j => by aesop}

Construction of a limit cone for a fork

Informal description

Given a fork $t$ on two parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$, a function $\text{lift}$ that for any fork $s$ provides a morphism from the vertex of $s$ to the vertex of $t$, and proofs that: 1. $\text{lift}(s) \circ \iota_t = \iota_s$ for any fork $s$ (preservation of the fork condition), 2. any morphism $m$ from the vertex of $s$ to the vertex of $t$ satisfying $m \circ \iota_t = \iota_s$ must equal $\text{lift}(s)$ (uniqueness), then $t$ is a limit cone over the parallel pair $(f, g)$. This means $t$ is an equalizer of $f$ and $g$.

CategoryTheory.Limits.Fork.IsLimit.mk' definition

 {X Y : C} {f g : X ⟶ Y} (t : Fork f g)
  (create : ∀ s : Fork f g, { l // l ≫ t.ι = s.ι ∧ ∀ {m}, m ≫ t.ι = s.ι → m = l }) : IsLimit t

Full source

/-- This is another convenient method to verify that a fork is a limit cone. It
    only asks for a proof of facts that carry any mathematical content, and allows access to the
    same `s` for all parts. -/
def Fork.IsLimit.mk' {X Y : C} {f g : X ⟶ Y} (t : Fork f g)
    (create : ∀ s : Fork f g, { l // l ≫ t.ι = s.ι ∧ ∀ {m}, m ≫ t.ι = s.ι → m = l }) : IsLimit t :=
  Fork.IsLimit.mk t (fun s => (create s).1) (fun s => (create s).2.1) fun s _ w => (create s).2.2 w

Verification of a fork as a limit cone via universal property

Informal description

Given a fork $t$ on two parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$, to verify that $t$ is a limit cone, it suffices to provide a function $\text{create}$ that for any other fork $s$ produces a morphism $l : s.\text{pt} \to t.\text{pt}$ such that: 1. $l \circ \iota_t = \iota_s$, and 2. any morphism $m : s.\text{pt} \to t.\text{pt}$ satisfying $m \circ \iota_t = \iota_s$ must equal $l$. Here $\iota_t$ and $\iota_s$ denote the inclusion morphisms of the forks $t$ and $s$ respectively.

CategoryTheory.Limits.Cofork.IsColimit.mk definition

 (t : Cofork f g) (desc : ∀ s : Cofork f g, t.pt ⟶ s.pt) (fac : ∀ s : Cofork f g, Cofork.π t ≫ desc s = Cofork.π s)
  (uniq : ∀ (s : Cofork f g) (m : t.pt ⟶ s.pt) (_ : t.π ≫ m = s.π), m = desc s) : IsColimit t

Full source

/-- This is a slightly more convenient method to verify that a cofork is a colimit cocone. It
    only asks for a proof of facts that carry any mathematical content -/
def Cofork.IsColimit.mk (t : Cofork f g) (desc : ∀ s : Cofork f g, t.pt ⟶ s.pt)
    (fac : ∀ s : Cofork f g, Cofork.πCofork.π t ≫ desc s = Cofork.π s)
    (uniq : ∀ (s : Cofork f g) (m : t.pt ⟶ s.pt) (_ : t.π ≫ m = s.π), m = desc s) : IsColimit t :=
  { desc
    fac := fun s j =>
      WalkingParallelPair.casesOn j (by erw [← s.w left, ← t.w left, Category.assoc, fac]; rfl)
        (fac s)
    uniq := by aesop }

Verification of Cofork as Colimit Cocone

Informal description

Given a cofork $ t $ on parallel morphisms $ f, g : X \to Y $ in a category $ \mathcal{C} $, to verify that $ t $ is a colimit cocone, it suffices to provide: 1. A function `desc` that for any other cofork $ s $ produces a morphism $ t.pt \to s.pt $, 2. A proof `fac` that for any cofork $ s $, the composition $ \pi_t \circ \text{desc}(s) $ equals $ \pi_s $, and 3. A proof `uniq` that any morphism $ m : t.pt \to s.pt $ satisfying $ \pi_t \circ m = \pi_s $ must equal $ \text{desc}(s) $. Here $ \pi_t $ and $ \pi_s $ denote the cocone morphisms from $ Y $ to the respective vertices of the coforks $ t $ and $ s $.

CategoryTheory.Limits.Cofork.IsColimit.mk' definition

 {X Y : C} {f g : X ⟶ Y} (t : Cofork f g)
  (create : ∀ s : Cofork f g, { l : t.pt ⟶ s.pt // t.π ≫ l = s.π ∧ ∀ {m}, t.π ≫ m = s.π → m = l }) : IsColimit t

Full source

/-- This is another convenient method to verify that a fork is a limit cone. It
    only asks for a proof of facts that carry any mathematical content, and allows access to the
    same `s` for all parts. -/
def Cofork.IsColimit.mk' {X Y : C} {f g : X ⟶ Y} (t : Cofork f g)
    (create : ∀ s : Cofork f g, { l : t.pt ⟶ s.pt // t.π ≫ l = s.π
                                    ∧ ∀ {m}, t.π ≫ m = s.π → m = l }) : IsColimit t :=
  Cofork.IsColimit.mk t (fun s => (create s).1) (fun s => (create s).2.1) fun s _ w =>
    (create s).2.2 w

Verification of Cofork as Colimit Cocone via Universal Property

Informal description

Given a cofork $ t $ on parallel morphisms $ f, g : X \to Y $ in a category $ \mathcal{C} $, to verify that $ t $ is a colimit cocone, it suffices to provide a function `create` that for any other cofork $ s $ produces a morphism $ l : t.pt \to s.pt $ such that: 1. The composition $ \pi_t \circ l $ equals $ \pi_s $, and 2. Any morphism $ m : t.pt \to s.pt $ satisfying $ \pi_t \circ m = \pi_s $ must equal $ l $. Here $ \pi_t $ and $ \pi_s $ denote the cocone morphisms from $ Y $ to the respective vertices of the coforks $ t $ and $ s $.

CategoryTheory.Limits.Fork.IsLimit.ofExistsUnique definition

{t : Fork f g} (hs : ∀ s : Fork f g, ∃! l : s.pt ⟶ t.pt, l ≫ Fork.ι t = Fork.ι s) : IsLimit t

Full source

/-- Noncomputably make a limit cone from the existence of unique factorizations. -/
noncomputable def Fork.IsLimit.ofExistsUnique {t : Fork f g}
    (hs : ∀ s : Fork f g, ∃! l : s.pt ⟶ t.pt, l ≫ Fork.ι t = Fork.ι s) : IsLimit t := by
  choose d hd hd' using hs
  exact Fork.IsLimit.mk _ d hd fun s m hm => hd' _ _ hm

Existence and uniqueness of morphisms implies limit cone for a fork

Informal description

Given a fork $ t $ on two parallel morphisms $ f, g : X \to Y $ in a category $ \mathcal{C} $, if for every fork $ s $ there exists a unique morphism $ l : s.pt \to t.pt $ such that $ l \circ \iota_t = \iota_s $, then $ t $ is a limit cone over the parallel pair $(f, g)$. Here $ \iota_t $ and $ \iota_s $ denote the inclusion morphisms of the forks $ t $ and $ s $ respectively.

CategoryTheory.Limits.Cofork.IsColimit.ofExistsUnique definition

{t : Cofork f g} (hs : ∀ s : Cofork f g, ∃! d : t.pt ⟶ s.pt, Cofork.π t ≫ d = Cofork.π s) : IsColimit t

Full source

/-- Noncomputably make a colimit cocone from the existence of unique factorizations. -/
noncomputable def Cofork.IsColimit.ofExistsUnique {t : Cofork f g}
    (hs : ∀ s : Cofork f g, ∃! d : t.pt ⟶ s.pt, Cofork.π t ≫ d = Cofork.π s) : IsColimit t := by
  choose d hd hd' using hs
  exact Cofork.IsColimit.mk _ d hd fun s m hm => hd' _ _ hm

Uniqueness of morphisms implies cofork is colimit

Informal description

Given a cofork $ t $ on parallel morphisms $ f, g : X \to Y $ in a category $ \mathcal{C} $, if for every other cofork $ s $ there exists a unique morphism $ d : t.pt \to s.pt $ such that the composition $ \pi_t \circ d = \pi_s $ (where $ \pi_t $ and $ \pi_s $ are the cocone morphisms from $ Y $ to the respective vertices of $ t $ and $ s $), then $ t $ is a colimit cocone for the parallel pair $ (f, g) $.

CategoryTheory.Limits.Fork.IsLimit.homIso definition

 {X Y : C} {f g : X ⟶ Y} {t : Fork f g} (ht : IsLimit t) (Z : C) : (Z ⟶ t.pt) ≃ { h : Z ⟶ X // h ≫ f = h ≫ g }

Full source

/--
Given a limit cone for the pair `f g : X ⟶ Y`, for any `Z`, morphisms from `Z` to its point are in
bijection with morphisms `h : Z ⟶ X` such that `h ≫ f = h ≫ g`.
Further, this bijection is natural in `Z`: see `Fork.IsLimit.homIso_natural`.
This is a special case of `IsLimit.homIso'`, often useful to construct adjunctions.
-/
@[simps]
def Fork.IsLimit.homIso {X Y : C} {f g : X ⟶ Y} {t : Fork f g} (ht : IsLimit t) (Z : C) :
    (Z ⟶ t.pt) ≃ { h : Z ⟶ X // h ≫ f = h ≫ g } where
  toFun k := ⟨k ≫ t.ι, by simp only [Category.assoc, t.condition]⟩
  invFun h := (Fork.IsLimit.lift' ht _ h.prop).1
  left_inv _ := Fork.IsLimit.hom_ext ht (Fork.IsLimit.lift' _ _ _).prop
  right_inv _ := Subtype.ext (Fork.IsLimit.lift' ht _ _).prop

Bijection between morphisms to a limit fork and equalizing morphisms

Informal description

Given a limit fork $ t $ over parallel morphisms $ f, g : X \to Y $ in a category $ \mathcal{C} $, for any object $ Z $ in $ \mathcal{C} $, there is a natural bijection between morphisms $ k : Z \to t.\mathrm{pt} $ (where $ t.\mathrm{pt} $ is the vertex of the fork) and morphisms $ h : Z \to X $ such that $ h \circ f = h \circ g $. More precisely: - The forward direction maps $ k $ to $ k \circ \iota_t $, where $ \iota_t : t.\mathrm{pt} \to X $ is the fork morphism. - The backward direction maps such an $ h $ to the unique morphism $ k $ satisfying $ k \circ \iota_t = h $, guaranteed by the universal property of the limit fork. This bijection is natural in $ Z $, meaning it respects precomposition with morphisms between objects.

CategoryTheory.Limits.Fork.IsLimit.homIso_natural theorem

 {X Y : C} {f g : X ⟶ Y} {t : Fork f g} (ht : IsLimit t) {Z Z' : C} (q : Z' ⟶ Z) (k : Z ⟶ t.pt) :
  (Fork.IsLimit.homIso ht _ (q ≫ k) : Z' ⟶ X) = q ≫ (Fork.IsLimit.homIso ht _ k : Z ⟶ X)

Full source

/-- The bijection of `Fork.IsLimit.homIso` is natural in `Z`. -/
theorem Fork.IsLimit.homIso_natural {X Y : C} {f g : X ⟶ Y} {t : Fork f g} (ht : IsLimit t)
    {Z Z' : C} (q : Z' ⟶ Z) (k : Z ⟶ t.pt) :
    (Fork.IsLimit.homIso ht _ (q ≫ k) : Z' ⟶ X) = q ≫ (Fork.IsLimit.homIso ht _ k : Z ⟶ X) :=
  Category.assoc _ _ _

Naturality of the Equalizer Hom-Bijection with Respect to Precomposition

Informal description

Let $\mathcal{C}$ be a category, $X, Y$ objects in $\mathcal{C}$, and $f, g : X \to Y$ parallel morphisms. Given a fork $t$ over $(f, g)$ that is a limit cone, and objects $Z, Z'$ in $\mathcal{C}$, for any morphism $q : Z' \to Z$ and any morphism $k : Z \to t.\mathrm{pt}$ (where $t.\mathrm{pt}$ is the vertex of the fork), the following diagram commutes: The image of $q \circ k$ under the bijection $\mathrm{homIso}$ (which maps to morphisms $Z' \to X$ equalizing $f$ and $g$) equals $q$ composed with the image of $k$ under $\mathrm{homIso}$. In symbols: $$ \mathrm{homIso}_{ht}(Z') (q \circ k) = q \circ \mathrm{homIso}_{ht}(Z) (k) $$ This expresses the naturality of the bijection $\mathrm{homIso}$ with respect to precomposition.

CategoryTheory.Limits.Cofork.IsColimit.homIso definition

 {X Y : C} {f g : X ⟶ Y} {t : Cofork f g} (ht : IsColimit t) (Z : C) : (t.pt ⟶ Z) ≃ { h : Y ⟶ Z // f ≫ h = g ≫ h }

Full source

/-- Given a colimit cocone for the pair `f g : X ⟶ Y`, for any `Z`, morphisms from the cocone point
to `Z` are in bijection with morphisms `h : Y ⟶ Z` such that `f ≫ h = g ≫ h`.
Further, this bijection is natural in `Z`: see `Cofork.IsColimit.homIso_natural`.
This is a special case of `IsColimit.homIso'`, often useful to construct adjunctions.
-/
@[simps]
def Cofork.IsColimit.homIso {X Y : C} {f g : X ⟶ Y} {t : Cofork f g} (ht : IsColimit t) (Z : C) :
    (t.pt ⟶ Z) ≃ { h : Y ⟶ Z // f ≫ h = g ≫ h } where
  toFun k := ⟨t.π ≫ k, by simp only [← Category.assoc, t.condition]⟩
  invFun h := (Cofork.IsColimit.desc' ht _ h.prop).1
  left_inv _ := Cofork.IsColimit.hom_ext ht (Cofork.IsColimit.desc' _ _ _).prop
  right_inv _ := Subtype.ext (Cofork.IsColimit.desc' ht _ _).prop

Bijection between morphisms from coequalizer and parallel-equalizing morphisms

Informal description

Given a cofork $ t $ over parallel morphisms $ f, g : X \to Y $ in a category $ \mathcal{C} $, if $ t $ is a colimit cofork, then for any object $ Z $ in $ \mathcal{C} $, there is a natural bijection between morphisms from the cofork vertex $ t.\text{pt} $ to $ Z $ and morphisms $ h : Y \to Z $ such that $ f \circ h = g \circ h $. More precisely, the bijection is given by: - The forward direction maps $ k : t.\text{pt} \to Z $ to $ \pi_t \circ k $, where $ \pi_t $ is the cofork projection $ Y \to t.\text{pt} $. - The backward direction maps $ h : Y \to Z $ (satisfying $ f \circ h = g \circ h $) to the unique morphism $ t.\text{pt} \to Z $ induced by the universal property of the colimit cofork $ t $.

CategoryTheory.Limits.Cofork.IsColimit.homIso_natural theorem

 {X Y : C} {f g : X ⟶ Y} {t : Cofork f g} {Z Z' : C} (q : Z ⟶ Z') (ht : IsColimit t) (k : t.pt ⟶ Z) :
  (Cofork.IsColimit.homIso ht _ (k ≫ q) : Y ⟶ Z') = (Cofork.IsColimit.homIso ht _ k : Y ⟶ Z) ≫ q

Full source

/-- The bijection of `Cofork.IsColimit.homIso` is natural in `Z`. -/
theorem Cofork.IsColimit.homIso_natural {X Y : C} {f g : X ⟶ Y} {t : Cofork f g} {Z Z' : C}
    (q : Z ⟶ Z') (ht : IsColimit t) (k : t.pt ⟶ Z) :
    (Cofork.IsColimit.homIso ht _ (k ≫ q) : Y ⟶ Z') =
      (Cofork.IsColimit.homIso ht _ k : Y ⟶ Z) ≫ q :=
  (Category.assoc _ _ _).symm

Naturality of the Bijection between Cofork Morphisms and Parallel-Equalizing Morphisms

Informal description

Let $\mathcal{C}$ be a category, $X, Y$ objects in $\mathcal{C}$, and $f, g : X \to Y$ parallel morphisms. Given a cofork $t$ of $f$ and $g$ that is a colimit, for any objects $Z, Z'$ in $\mathcal{C}$ and morphism $q : Z \to Z'$, the following diagram commutes: For any morphism $k : t.\text{pt} \to Z$, we have: \[ \text{homIso}_{ht}(Z') (k \circ q) = \text{homIso}_{ht}(Z)(k) \circ q \] where $\text{homIso}_{ht}(Z)$ denotes the bijection between morphisms from the cofork vertex $t.\text{pt}$ to $Z$ and morphisms $h : Y \to Z$ satisfying $f \circ h = g \circ h$.

CategoryTheory.Limits.Cone.ofFork definition

{F : WalkingParallelPair ⥤ C} (t : Fork (F.map left) (F.map right)) : Cone F

Full source

/-- This is a helper construction that can be useful when verifying that a category has all
    equalizers. Given `F : WalkingParallelPair ⥤ C`, which is really the same as
    `parallelPair (F.map left) (F.map right)`, and a fork on `F.map left` and `F.map right`,
    we get a cone on `F`.

    If you're thinking about using this, have a look at `hasEqualizers_of_hasLimit_parallelPair`,
    which you may find to be an easier way of achieving your goal. -/
def Cone.ofFork {F : WalkingParallelPairWalkingParallelPair ⥤ C} (t : Fork (F.map left) (F.map right)) : Cone F where
  pt := t.pt
  π :=
    { app := fun X => t.π.app X ≫ eqToHom (by simp)
      naturality := by rintro _ _ (_|_|_) <;> {dsimp; simp [t.condition]}}

Cone construction from a fork on parallel morphisms

Informal description

Given a functor $F$ from the walking parallel pair category to a category $\mathcal{C}$ (which is equivalent to specifying two parallel morphisms $f, g : X \to Y$ in $\mathcal{C}$) and a fork $t$ on $F(\text{left})$ and $F(\text{right})$, this construction produces a cone over $F$ with the same cone point as $t$ and appropriately modified cone morphisms.

CategoryTheory.Limits.Cocone.ofCofork definition

{F : WalkingParallelPair ⥤ C} (t : Cofork (F.map left) (F.map right)) : Cocone F

Full source

/-- This is a helper construction that can be useful when verifying that a category has all
    coequalizers. Given `F : WalkingParallelPair ⥤ C`, which is really the same as
    `parallelPair (F.map left) (F.map right)`, and a cofork on `F.map left` and `F.map right`,
    we get a cocone on `F`.

    If you're thinking about using this, have a look at
    `hasCoequalizers_of_hasColimit_parallelPair`, which you may find to be an easier way of
    achieving your goal. -/
def Cocone.ofCofork {F : WalkingParallelPairWalkingParallelPair ⥤ C} (t : Cofork (F.map left) (F.map right)) :
    Cocone F where
  pt := t.pt
  ι :=
    { app := fun X => eqToHomeqToHom (by simp) ≫ t.ι.app X
      naturality := by rintro _ _ (_|_|_) <;> {dsimp; simp [t.condition]}}

Cocone construction from a cofork on parallel morphisms

Informal description

Given a functor $F$ from the walking parallel pair category to a category $\mathcal{C}$ (which is equivalent to specifying two parallel morphisms $f, g : X \to Y$ in $\mathcal{C}$) and a cofork $t$ on $F(\text{left})$ and $F(\text{right})$, this construction produces a cocone over $F$ with the same cocone point as $t$ and appropriately modified cocone morphisms.

CategoryTheory.Limits.Cone.ofFork_π theorem

 {F : WalkingParallelPair ⥤ C} (t : Fork (F.map left) (F.map right)) (j) :
  (Cone.ofFork t).π.app j = t.π.app j ≫ eqToHom (by simp)

Full source

@[simp]
theorem Cone.ofFork_π {F : WalkingParallelPairWalkingParallelPair ⥤ C} (t : Fork (F.map left) (F.map right)) (j) :
    (Cone.ofFork t).π.app j = t.π.app j ≫ eqToHom (by simp) := rfl

Projection Morphism of Cone Constructed from Fork

Informal description

For any functor $F$ from the walking parallel pair category to a category $\mathcal{C}$ and any fork $t$ on the parallel morphisms $F(\text{left})$ and $F(\text{right})$, the projection morphism of the cone constructed from $t$ at any object $j$ is equal to the composition of the fork's projection morphism at $j$ with the identity morphism induced by the equality of objects (which holds by definition).

CategoryTheory.Limits.Cocone.ofCofork_ι theorem

 {F : WalkingParallelPair ⥤ C} (t : Cofork (F.map left) (F.map right)) (j) :
  (Cocone.ofCofork t).ι.app j = eqToHom (by simp) ≫ t.ι.app j

Full source

@[simp]
theorem Cocone.ofCofork_ι {F : WalkingParallelPairWalkingParallelPair ⥤ C} (t : Cofork (F.map left) (F.map right))
    (j) : (Cocone.ofCofork t).ι.app j = eqToHomeqToHom (by simp) ≫ t.ι.app j := rfl

Cocone Morphism Construction from Cofork

Informal description

For any functor $F$ from the walking parallel pair category to a category $\mathcal{C}$ and any cofork $t$ on the parallel pair $(F(\text{left}), F(\text{right}))$, the cocone morphism $\iota_j$ of the cocone constructed from $t$ at object $j$ is equal to the composition of an identity morphism (constructed via `eqToHom` with a trivial proof) with the cofork morphism $\iota_j$ of $t$.

CategoryTheory.Limits.Fork.ofCone definition

{F : WalkingParallelPair ⥤ C} (t : Cone F) : Fork (F.map left) (F.map right)

Full source

/-- Given `F : WalkingParallelPair ⥤ C`, which is really the same as
    `parallelPair (F.map left) (F.map right)` and a cone on `F`, we get a fork on
    `F.map left` and `F.map right`. -/
def Fork.ofCone {F : WalkingParallelPairWalkingParallelPair ⥤ C} (t : Cone F) : Fork (F.map left) (F.map right) where
  pt := t.pt
  π := { app := fun X => t.π.app X ≫ eqToHom (by simp)
         naturality := by rintro _ _ (_|_|_) <;> {dsimp; simp}}

Fork construction from a cone over a parallel pair

Informal description

Given a functor $F : \text{WalkingParallelPair} \to \mathcal{C}$ (which is equivalent to a parallel pair of morphisms $F(\text{left})$ and $F(\text{right})$) and a cone $t$ over $F$, this constructs a fork on the parallel pair $(F(\text{left}), F(\text{right}))$. The fork has the same vertex as the original cone, and its projection maps are obtained by composing the cone's projections with appropriate identity morphisms.

CategoryTheory.Limits.Cofork.ofCocone definition

{F : WalkingParallelPair ⥤ C} (t : Cocone F) : Cofork (F.map left) (F.map right)

Full source

/-- Given `F : WalkingParallelPair ⥤ C`, which is really the same as
    `parallelPair (F.map left) (F.map right)` and a cocone on `F`, we get a cofork on
    `F.map left` and `F.map right`. -/
def Cofork.ofCocone {F : WalkingParallelPairWalkingParallelPair ⥤ C} (t : Cocone F) :
    Cofork (F.map left) (F.map right) where
  pt := t.pt
  ι := { app := fun X => eqToHomeqToHom (by simp) ≫ t.ι.app X
         naturality := by rintro _ _ (_|_|_) <;> {dsimp; simp}}

Cofork from cocone over parallel pair diagram

Informal description

Given a functor $F$ from the walking parallel pair category to a category $\mathcal{C}$ and a cocone $t$ over $F$, the construction `Cofork.ofCocone` produces a cofork on the parallel pair $(F(\text{left}), F(\text{right}))$. The vertex of the cofork is the vertex of the cocone $t$, and the cofork morphisms are obtained by composing the cocone morphisms with appropriate identity morphisms.

CategoryTheory.Limits.Fork.ofCone_π theorem

{F : WalkingParallelPair ⥤ C} (t : Cone F) (j) : (Fork.ofCone t).π.app j = t.π.app j ≫ eqToHom (by simp)

Full source

@[simp]
theorem Fork.ofCone_π {F : WalkingParallelPairWalkingParallelPair ⥤ C} (t : Cone F) (j) :
    (Fork.ofCone t).π.app j = t.π.app j ≫ eqToHom (by simp) := rfl

Projection Morphism Equality in Fork Construction from Cone

Informal description

Given a functor $F$ from the walking parallel pair category to a category $\mathcal{C}$ and a cone $t$ over $F$, the projection morphism $(Fork.ofCone t).\pi_j$ at object $j$ is equal to the composition of the cone's projection $t.\pi_j$ with the identity morphism (via `eqToHom`).

CategoryTheory.Limits.Cofork.ofCocone_ι theorem

{F : WalkingParallelPair ⥤ C} (t : Cocone F) (j) : (Cofork.ofCocone t).ι.app j = eqToHom (by simp) ≫ t.ι.app j

Full source

@[simp]
theorem Cofork.ofCocone_ι {F : WalkingParallelPairWalkingParallelPair ⥤ C} (t : Cocone F) (j) :
    (Cofork.ofCocone t).ι.app j = eqToHomeqToHom (by simp) ≫ t.ι.app j := rfl

Cofork Morphism from Cocone Construction

Informal description

Given a functor $F$ from the walking parallel pair category to a category $\mathcal{C}$ and a cocone $t$ over $F$, for any object $j$ in the walking parallel pair category, the morphism $(Cofork.ofCocone\, t).\iota_j$ is equal to the composition of an equality isomorphism (simplified by the `simp` tactic) with the cocone morphism $t.\iota_j$.

CategoryTheory.Limits.Fork.ι_postcompose theorem

 {f' g' : X ⟶ Y} {α : parallelPair f g ⟶ parallelPair f' g'} {c : Fork f g} :
  Fork.ι ((Cones.postcompose α).obj c) = c.ι ≫ α.app _

Full source

@[simp]
theorem Fork.ι_postcompose {f' g' : X ⟶ Y} {α : parallelPairparallelPair f g ⟶ parallelPair f' g'}
    {c : Fork f g} : Fork.ι ((Cones.postcompose α).obj c) = c.ι ≫ α.app _ :=
  rfl

Naturality of Fork Inclusion under Postcomposition

Informal description

Given parallel morphisms $f, g : X \to Y$ and $f', g' : X \to Y$ in a category $\mathcal{C}$, a natural transformation $\alpha$ between the parallel pair functors $(f, g)$ and $(f', g')$, and a fork $c$ over $(f, g)$, the inclusion morphism of the postcomposed fork $(Cones.postcompose \alpha).obj c$ is equal to the composition of $c.\iota$ with $\alpha$ applied to the first object of the walking parallel pair category, i.e., $\iota_{(Cones.postcompose \alpha).obj c} = \iota_c \circ \alpha_{\text{pt}}$.

CategoryTheory.Limits.Cofork.π_precompose theorem

 {f' g' : X ⟶ Y} {α : parallelPair f g ⟶ parallelPair f' g'} {c : Cofork f' g'} :
  Cofork.π ((Cocones.precompose α).obj c) = α.app _ ≫ c.π

Full source

@[simp]
theorem Cofork.π_precompose {f' g' : X ⟶ Y} {α : parallelPairparallelPair f g ⟶ parallelPair f' g'}
    {c : Cofork f' g'} : Cofork.π ((Cocones.precompose α).obj c) = α.app _ ≫ c.π :=
  rfl

Precomposition of Cofork Projection via Natural Transformation

Informal description

Given parallel morphisms $f, g : X \to Y$ and $f', g' : X \to Y$ in a category $\mathcal{C}$, a natural transformation $\alpha$ between the parallel pair functors $(f, g)$ and $(f', g')$, and a cofork $c$ on $(f', g')$, the projection morphism of the precomposed cofork $(Cocones.precompose \alpha).obj c$ is equal to the composition of $\alpha$ applied to the target object followed by the projection morphism of $c$.

CategoryTheory.Limits.Fork.mkHom definition

{s t : Fork f g} (k : s.pt ⟶ t.pt) (w : k ≫ t.ι = s.ι) : s ⟶ t

Full source

/-- Helper function for constructing morphisms between equalizer forks.
-/
@[simps]
def Fork.mkHom {s t : Fork f g} (k : s.pt ⟶ t.pt) (w : k ≫ t.ι = s.ι) : s ⟶ t where
  hom := k
  w := by
    rintro ⟨_ | _⟩
    · exact w
    · simp only [Fork.app_one_eq_ι_comp_left,← Category.assoc]
      congr

Morphism between forks induced by a commuting morphism

Informal description

Given two forks $s$ and $t$ on parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$, and a morphism $k : s.\text{pt} \to t.\text{pt}$ such that $k \circ t.\iota = s.\iota$, this constructs a morphism of forks from $s$ to $t$. Here, $s.\iota$ and $t.\iota$ are the inclusion morphisms of the respective forks, and the condition ensures that the morphism $k$ commutes with these inclusions.

CategoryTheory.Limits.ForkOfι.ext definition

 {P : C} {ι ι' : P ⟶ X} (w : ι ≫ f = ι ≫ g) (w' : ι' ≫ f = ι' ≫ g) (h : ι = ι') : Fork.ofι ι w ≅ Fork.ofι ι' w'

Full source

/-- Two forks of the form `ofι` are isomorphic whenever their `ι`'s are equal. -/
def ForkOfι.ext {P : C} {ι ι' : P ⟶ X} (w : ι ≫ f = ι ≫ g) (w' : ι' ≫ f = ι' ≫ g) (h : ι = ι') :
    Fork.ofιFork.ofι ι w ≅ Fork.ofι ι' w' :=
  Fork.ext (Iso.refl _) (by simp [h])

Isomorphism of forks from equal morphisms

Informal description

Given an object $P$ in a category $\mathcal{C}$ and two morphisms $\iota, \iota' : P \to X$ such that both $\iota \circ f = \iota \circ g$ and $\iota' \circ f = \iota' \circ g$ hold, if $\iota = \iota'$, then the forks constructed via `Fork.ofι` from $\iota$ and $\iota'$ are isomorphic.

CategoryTheory.Limits.Fork.isoForkOfι definition

(c : Fork f g) : c ≅ Fork.ofι c.ι c.condition

Full source

/-- Every fork is isomorphic to one of the form `Fork.of_ι _ _`. -/
def Fork.isoForkOfι (c : Fork f g) : c ≅ Fork.ofι c.ι c.condition :=
  Fork.ext (by simp only [Fork.ofι_pt, Functor.const_obj_obj]; rfl) (by simp)

Isomorphism between a fork and its canonical construction via `Fork.ofι`

Informal description

For any fork $c$ over parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$, the fork $c$ is isomorphic to the fork constructed via `Fork.ofι` using its own inclusion morphism $c.\iota$ and the condition $c.\iota \circ f = c.\iota \circ g$.

CategoryTheory.Limits.Cofork.mkHom definition

{s t : Cofork f g} (k : s.pt ⟶ t.pt) (w : s.π ≫ k = t.π) : s ⟶ t

Full source

/-- Helper function for constructing morphisms between coequalizer coforks.
-/
@[simps]
def Cofork.mkHom {s t : Cofork f g} (k : s.pt ⟶ t.pt) (w : s.π ≫ k = t.π) : s ⟶ t where
  hom := k
  w := by
    rintro ⟨_ | _⟩
    · simp [Cofork.app_zero_eq_comp_π_left, w]
    · exact w

Morphism between coforks induced by a vertex morphism

Informal description

Given two coforks $s$ and $t$ on parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$, and a morphism $k : s.pt \to t.pt$ between their vertices such that the composition $s.\pi \circ k$ equals $t.\pi$, this constructs a morphism from $s$ to $t$ in the category of coforks.

CategoryTheory.Limits.Fork.hom_comp_ι theorem

{s t : Fork f g} (f : s ⟶ t) : f.hom ≫ t.ι = s.ι

Full source

@[reassoc (attr := simp)]
theorem Fork.hom_comp_ι {s t : Fork f g} (f : s ⟶ t) : f.hom ≫ t.ι = s.ι := by
  cases s; cases t; cases f; aesop

Compatibility of Fork Morphism with Inclusion: $\varphi_{\text{hom}} \circ \iota_t = \iota_s$

Informal description

Given two forks $s$ and $t$ over parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$, and a morphism $\varphi : s \to t$ between these forks, the composition $\varphi_{\text{hom}} \circ \iota_t$ equals $\iota_s$, where $\iota_s$ and $\iota_t$ are the inclusion morphisms of the forks $s$ and $t$ respectively. In other words, the following diagram commutes: \[ \varphi_{\text{hom}} \circ \iota_t = \iota_s. \]

CategoryTheory.Limits.Fork.π_comp_hom theorem

{s t : Cofork f g} (f : s ⟶ t) : s.π ≫ f.hom = t.π

Full source

@[reassoc (attr := simp)]
theorem Fork.π_comp_hom {s t : Cofork f g} (f : s ⟶ t) : s.π ≫ f.hom = t.π := by
  cases s; cases t; cases f; aesop

Compatibility of Cofork Projection with Morphism

Informal description

Given two coforks $s$ and $t$ on parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$, and a morphism $\varphi : s \to t$ between them, the composition of the cofork projection $\pi_s : Y \to s.pt$ with $\varphi$ equals the cofork projection $\pi_t : Y \to t.pt$, i.e., $\pi_s \circ \varphi = \pi_t$.

CategoryTheory.Limits.Cofork.isoCoforkOfπ definition

(c : Cofork f g) : c ≅ Cofork.ofπ c.π c.condition

Full source

/-- Every cofork is isomorphic to one of the form `Cofork.ofπ _ _`. -/
def Cofork.isoCoforkOfπ (c : Cofork f g) : c ≅ Cofork.ofπ c.π c.condition :=
  Cofork.ext (by simp only [Cofork.ofπ_pt, Functor.const_obj_obj]; rfl) (by dsimp; simp)

Isomorphism between a cofork and its canonical construction via `Cofork.ofπ`

Informal description

For any cofork $c$ of parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$, there is an isomorphism between $c$ and the cofork constructed via `Cofork.ofπ` using $c$'s projection morphism $\pi_c$ and its condition $f \circ \pi_c = g \circ \pi_c$.

CategoryTheory.Limits.HasEqualizer abbrev

Full source

/-- `HasEqualizer f g` represents a particular choice of limiting cone
for the parallel pair of morphisms `f` and `g`.
-/
abbrev HasEqualizer :=
  HasLimit (parallelPair f g)

Existence of Equalizer for Parallel Morphisms

Informal description

A category $\mathcal{C}$ has an equalizer for a pair of parallel morphisms $f, g : X \to Y$ if there exists a limiting cone over the diagram formed by $f$ and $g$. This means there exists an object $E$ and a morphism $\iota : E \to X$ such that $\iota$ equalizes $f$ and $g$ (i.e., $f \circ \iota = g \circ \iota$), and for any other object $Z$ with a morphism $h : Z \to X$ that equalizes $f$ and $g$, there exists a unique morphism $u : Z \to E$ making the appropriate diagram commute.

CategoryTheory.Limits.equalizer abbrev

: C

Full source

/-- If an equalizer of `f` and `g` exists, we can access an arbitrary choice of such by
    saying `equalizer f g`. -/
noncomputable abbrev equalizer : C :=
  limit (parallelPair f g)

Equalizer Object for Parallel Morphisms $f$ and $g$

Informal description

Given two parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$, the equalizer $\mathrm{equalizer}(f, g)$ is an object of $\mathcal{C}$ equipped with a morphism $\iota : \mathrm{equalizer}(f, g) \to X$ such that $f \circ \iota = g \circ \iota$, and which is universal with this property.

CategoryTheory.Limits.equalizer.ι abbrev

: equalizer f g ⟶ X

Full source

/-- If an equalizer of `f` and `g` exists, we can access the inclusion
    `equalizer f g ⟶ X` by saying `equalizer.ι f g`. -/
noncomputable abbrev equalizer.ι : equalizerequalizer f g ⟶ X :=
  limit.π (parallelPair f g) zero

Inclusion Morphism of the Equalizer

Informal description

Given two parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$, the morphism $\iota : \mathrm{equalizer}(f, g) \to X$ is the canonical inclusion from the equalizer object to $X$, satisfying $f \circ \iota = g \circ \iota$.

CategoryTheory.Limits.equalizer.fork abbrev

: Fork f g

Full source

/-- An equalizer cone for a parallel pair `f` and `g` -/
noncomputable abbrev equalizer.fork : Fork f g :=
  limit.cone (parallelPair f g)

Equalizer Fork for Parallel Morphisms $f$ and $g$

Informal description

The fork associated with the equalizer of two parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$ is a cone over the diagram formed by $f$ and $g$, where the morphism $\iota : E \to X$ (from the vertex $E$ of the cone to $X$) satisfies $f \circ \iota = g \circ \iota$.

CategoryTheory.Limits.equalizer.fork_ι theorem

: (equalizer.fork f g).ι = equalizer.ι f g

Full source

@[simp]
theorem equalizer.fork_ι : (equalizer.fork f g).ι = equalizer.ι f g :=
  rfl

Equality of Fork Inclusion and Equalizer Inclusion Morphisms

Informal description

For any two parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$, the inclusion morphism $\iota$ of the equalizer fork is equal to the canonical inclusion morphism from the equalizer object to $X$, i.e., $\iota_{\text{fork}} = \iota_{\text{equalizer}}$.

CategoryTheory.Limits.equalizer.fork_π_app_zero theorem

: (equalizer.fork f g).π.app zero = equalizer.ι f g

Full source

@[simp]
theorem equalizer.fork_π_app_zero : (equalizer.fork f g).π.app zero = equalizer.ι f g :=
  rfl

Equalizer Fork Projection at Zero Equals Inclusion Morphism

Informal description

For a parallel pair of morphisms $f, g : X \to Y$ in a category $\mathcal{C}$, the projection morphism $\pi$ of the equalizer fork evaluated at the `zero` object of the walking parallel pair category equals the inclusion morphism $\iota$ of the equalizer. That is, $(\mathrm{equalizer.fork}\, f\, g).\pi\, \mathrm{zero} = \mathrm{equalizer.\iota}\, f\, g$.

CategoryTheory.Limits.equalizer.condition theorem

: equalizer.ι f g ≫ f = equalizer.ι f g ≫ g

Full source

@[reassoc]
theorem equalizer.condition : equalizer.ιequalizer.ι f g ≫ f = equalizer.ιequalizer.ι f g ≫ g :=
  Fork.condition <| limit.cone <| parallelPair f g

Equalizer Condition: $f \circ \iota = g \circ \iota$

Informal description

For any two parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$, the inclusion morphism $\iota : \mathrm{equalizer}(f, g) \to X$ satisfies $f \circ \iota = g \circ \iota$.

CategoryTheory.Limits.equalizerIsEqualizer definition

: IsLimit (Fork.ofι (equalizer.ι f g) (equalizer.condition f g))

Full source

/-- The equalizer built from `equalizer.ι f g` is limiting. -/
noncomputable def equalizerIsEqualizer : IsLimit (Fork.ofι (equalizer.ι f g)
    (equalizer.condition f g)) :=
  IsLimit.ofIsoLimit (limit.isLimit _) (Fork.ext (Iso.refl _) (by simp))

Equalizer as a limiting cone

Informal description

The equalizer constructed from the inclusion morphism $\iota : \mathrm{equalizer}(f, g) \to X$ and the condition $f \circ \iota = g \circ \iota$ is a limiting cone, i.e., it satisfies the universal property of the equalizer for the parallel pair of morphisms $f, g : X \to Y$ in the category $\mathcal{C}$.

CategoryTheory.Limits.equalizer.lift abbrev

{W : C} (k : W ⟶ X) (h : k ≫ f = k ≫ g) : W ⟶ equalizer f g

Full source

/-- A morphism `k : W ⟶ X` satisfying `k ≫ f = k ≫ g` factors through the equalizer of `f` and `g`
    via `equalizer.lift : W ⟶ equalizer f g`. -/
noncomputable abbrev equalizer.lift {W : C} (k : W ⟶ X) (h : k ≫ f = k ≫ g) : W ⟶ equalizer f g :=
  limit.lift (parallelPair f g) (Fork.ofι k h)

Universal Property of Equalizer: Factorization of Morphisms

Informal description

Given an object $W$ in a category $\mathcal{C}$ and a morphism $k : W \to X$ such that $k \circ f = k \circ g$, there exists a unique morphism $\mathrm{equalizer.lift}(k, h) : W \to \mathrm{equalizer}(f, g)$ that factors $k$ through the equalizer of $f$ and $g$. Here, $h$ is the proof that $k$ equalizes $f$ and $g$.

CategoryTheory.Limits.equalizer.lift_ι theorem

{W : C} (k : W ⟶ X) (h : k ≫ f = k ≫ g) : equalizer.lift k h ≫ equalizer.ι f g = k

Full source

@[reassoc]
theorem equalizer.lift_ι {W : C} (k : W ⟶ X) (h : k ≫ f = k ≫ g) :
    equalizer.liftequalizer.lift k h ≫ equalizer.ι f g = k :=
  limit.lift_π _ _

Composition of Equalizer Lift with Inclusion Equals Original Morphism

Informal description

Given an object $W$ in a category $\mathcal{C}$ and a morphism $k : W \to X$ such that $k \circ f = k \circ g$, the composition of the equalizer lift $\mathrm{equalizer.lift}(k, h)$ with the equalizer inclusion $\iota$ equals $k$, i.e., $\mathrm{equalizer.lift}(k, h) \circ \iota = k$.

CategoryTheory.Limits.equalizer.lift' definition

{W : C} (k : W ⟶ X) (h : k ≫ f = k ≫ g) : { l : W ⟶ equalizer f g // l ≫ equalizer.ι f g = k }

Full source

/-- A morphism `k : W ⟶ X` satisfying `k ≫ f = k ≫ g` induces a morphism `l : W ⟶ equalizer f g`
    satisfying `l ≫ equalizer.ι f g = k`. -/
noncomputable def equalizer.lift' {W : C} (k : W ⟶ X) (h : k ≫ f = k ≫ g) :
    { l : W ⟶ equalizer f g // l ≫ equalizer.ι f g = k } :=
  ⟨equalizer.lift k h, equalizer.lift_ι _ _⟩

Factorization through equalizer with proof

Informal description

Given an object $W$ in a category $\mathcal{C}$ and a morphism $k : W \to X$ such that $k \circ f = k \circ g$, there exists a unique morphism $l : W \to \mathrm{equalizer}(f, g)$ such that $l \circ \iota = k$, where $\iota : \mathrm{equalizer}(f, g) \to X$ is the equalizer inclusion. This is packaged as a dependent pair where the first component is the morphism $l$ and the second component is the proof that $l \circ \iota = k$.

CategoryTheory.Limits.equalizer.hom_ext theorem

{W : C} {k l : W ⟶ equalizer f g} (h : k ≫ equalizer.ι f g = l ≫ equalizer.ι f g) : k = l

Full source

/-- Two maps into an equalizer are equal if they are equal when composed with the equalizer map. -/
@[ext]
theorem equalizer.hom_ext {W : C} {k l : W ⟶ equalizer f g}
    (h : k ≫ equalizer.ι f g = l ≫ equalizer.ι f g) : k = l :=
  Fork.IsLimit.hom_ext (limit.isLimit _) h

Uniqueness of Morphisms into Equalizer via Inclusion Condition

Informal description

Let $\mathcal{C}$ be a category with an equalizer for two parallel morphisms $f, g : X \to Y$. For any object $W$ in $\mathcal{C}$ and any pair of morphisms $k, l : W \to \mathrm{equalizer}(f, g)$, if $k \circ \iota = l \circ \iota$ where $\iota : \mathrm{equalizer}(f, g) \to X$ is the equalizer inclusion, then $k = l$.

CategoryTheory.Limits.equalizer.existsUnique theorem

{W : C} (k : W ⟶ X) (h : k ≫ f = k ≫ g) : ∃! l : W ⟶ equalizer f g, l ≫ equalizer.ι f g = k

Full source

theorem equalizer.existsUnique {W : C} (k : W ⟶ X) (h : k ≫ f = k ≫ g) :
    ∃! l : W ⟶ equalizer f g, l ≫ equalizer.ι f g = k :=
  Fork.IsLimit.existsUnique (limit.isLimit _) _ h

Universal Property of Equalizers

Informal description

Given two parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$ with an equalizer, for any object $W$ and morphism $k : W \to X$ such that $k \circ f = k \circ g$, there exists a unique morphism $l : W \to \mathrm{equalizer}(f, g)$ satisfying $l \circ \iota = k$, where $\iota : \mathrm{equalizer}(f, g) \to X$ is the equalizer inclusion.

CategoryTheory.Limits.equalizer.ι_mono instance

: Mono (equalizer.ι f g)

Full source

/-- An equalizer morphism is a monomorphism -/
instance equalizer.ι_mono : Mono (equalizer.ι f g) where
  right_cancellation _ _ w := equalizer.hom_ext w

Equalizer Inclusion is Monic

Informal description

The inclusion morphism $\iota : \mathrm{equalizer}(f, g) \to X$ of the equalizer of two parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$ is a monomorphism.

CategoryTheory.Limits.mono_of_isLimit_fork theorem

{c : Fork f g} (i : IsLimit c) : Mono (Fork.ι c)

Full source

/-- The equalizer morphism in any limit cone is a monomorphism. -/
theorem mono_of_isLimit_fork {c : Fork f g} (i : IsLimit c) : Mono (Fork.ι c) :=
  { right_cancellation := fun _ _ w => Fork.IsLimit.hom_ext i w }

Inclusion morphism of a limit fork is monic

Informal description

Let $\mathcal{C}$ be a category, and let $f, g : X \to Y$ be two parallel morphisms in $\mathcal{C}$. Given a fork $c$ over $(f, g)$ that is a limit cone, the inclusion morphism $\iota_c : c.\mathrm{pt} \to X$ is a monomorphism.

CategoryTheory.Limits.idFork definition

(h : f = g) : Fork f g

Full source

/-- The identity determines a cone on the equalizer diagram of `f` and `g` if `f = g`. -/
def idFork (h : f = g) : Fork f g :=
  Fork.ofι (𝟙 X) <| h ▸ rfl

Identity fork for equal parallel morphisms

Informal description

Given two parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$ such that $f = g$, the identity morphism $\text{id}_X$ forms a cone (called a *fork*) over the parallel pair diagram. This fork has $X$ as its vertex and satisfies the condition that $\text{id}_X \circ f = \text{id}_X \circ g$ (which holds trivially since $f = g$).

CategoryTheory.Limits.isLimitIdFork definition

(h : f = g) : IsLimit (idFork h)

Full source

/-- The identity on `X` is an equalizer of `(f, g)`, if `f = g`. -/
def isLimitIdFork (h : f = g) : IsLimit (idFork h) :=
  Fork.IsLimit.mk _ (fun s => Fork.ι s) (fun _ => Category.comp_id _) fun s m h => by
    convert h
    exact (Category.comp_id _).symm

Identity fork is a limit cone for equal parallel morphisms

Informal description

Given two parallel morphisms $ f, g : X \to Y $ in a category $\mathcal{C}$ such that $ f = g $, the identity fork (formed by the identity morphism $\text{id}_X$) is a limit cone over the parallel pair diagram $(f, g)$. This means that $\text{id}_X$ is an equalizer of $f$ and $g$ when they are equal.

CategoryTheory.Limits.isIso_limit_cone_parallelPair_of_eq theorem

(h₀ : f = g) {c : Fork f g} (h : IsLimit c) : IsIso c.ι

Full source

/-- Every equalizer of `(f, g)`, where `f = g`, is an isomorphism. -/
theorem isIso_limit_cone_parallelPair_of_eq (h₀ : f = g) {c : Fork f g} (h : IsLimit c) :
    IsIso c.ι :=
  Iso.isIso_hom <| IsLimit.conePointUniqueUpToIso h <| isLimitIdFork h₀

Limit cone over equal parallel morphisms yields isomorphism

Informal description

Let $f, g : X \to Y$ be parallel morphisms in a category $\mathcal{C}$ such that $f = g$. For any fork $c$ over $(f, g)$ that is a limit cone, the morphism $\iota_c : c.\mathrm{pt} \to X$ is an isomorphism.

CategoryTheory.Limits.equalizer.ι_of_eq theorem

[HasEqualizer f g] (h : f = g) : IsIso (equalizer.ι f g)

Full source

/-- The equalizer of `(f, g)`, where `f = g`, is an isomorphism. -/
theorem equalizer.ι_of_eq [HasEqualizer f g] (h : f = g) : IsIso (equalizer.ι f g) :=
  isIso_limit_cone_parallelPair_of_eq h <| limit.isLimit _

Equalizer inclusion is an isomorphism when $f = g$

Informal description

Let $f, g : X \to Y$ be parallel morphisms in a category $\mathcal{C}$ such that $f = g$, and assume $\mathcal{C}$ has an equalizer for $(f, g)$. Then the inclusion morphism $\iota : \mathrm{equalizer}(f, g) \to X$ is an isomorphism.

CategoryTheory.Limits.isIso_limit_cone_parallelPair_of_self theorem

{c : Fork f f} (h : IsLimit c) : IsIso c.ι

Full source

/-- Every equalizer of `(f, f)` is an isomorphism. -/
theorem isIso_limit_cone_parallelPair_of_self {c : Fork f f} (h : IsLimit c) : IsIso c.ι :=
  isIso_limit_cone_parallelPair_of_eq rfl h

Limit cone over identical parallel morphisms yields isomorphism

Informal description

For any fork $c$ over a parallel pair $(f, f)$ in a category $\mathcal{C}$, if $c$ is a limit cone, then the morphism $\iota_c : c.\mathrm{pt} \to X$ is an isomorphism.

CategoryTheory.Limits.isIso_limit_cone_parallelPair_of_epi theorem

{c : Fork f g} (h : IsLimit c) [Epi c.ι] : IsIso c.ι

Full source

/-- An equalizer that is an epimorphism is an isomorphism. -/
theorem isIso_limit_cone_parallelPair_of_epi {c : Fork f g} (h : IsLimit c) [Epi c.ι] : IsIso c.ι :=
  isIso_limit_cone_parallelPair_of_eq ((cancel_epi _).1 (Fork.condition c)) h

Epimorphic Equalizer Implies Isomorphism

Informal description

Let $f, g : X \to Y$ be parallel morphisms in a category $\mathcal{C}$, and let $c$ be a fork over $(f, g)$ that is a limit cone. If the inclusion morphism $\iota_c : c.\mathrm{pt} \to X$ is an epimorphism, then $\iota_c$ is an isomorphism.

CategoryTheory.Limits.hasEqualizer_of_self instance

: HasEqualizer f f

Full source

instance hasEqualizer_of_self : HasEqualizer f f :=
  HasLimit.mk
    { cone := idFork rfl
      isLimit := isLimitIdFork rfl }

Existence of Equalizer for a Morphism with Itself

Informal description

For any morphism $f : X \to Y$ in a category $\mathcal{C}$, the pair $(f, f)$ has an equalizer.

CategoryTheory.Limits.equalizer.ι_of_self instance

: IsIso (equalizer.ι f f)

Full source

/-- The equalizer inclusion for `(f, f)` is an isomorphism. -/
instance equalizer.ι_of_self : IsIso (equalizer.ι f f) :=
  equalizer.ι_of_eq rfl

Equalizer Inclusion Isomorphism for Self-Parallel Morphism

Informal description

For any morphism $f : X \to Y$ in a category $\mathcal{C}$, the inclusion morphism $\iota : \mathrm{equalizer}(f, f) \to X$ is an isomorphism.

CategoryTheory.Limits.equalizer.isoSourceOfSelf definition

: equalizer f f ≅ X

Full source

/-- The equalizer of a morphism with itself is isomorphic to the source. -/
noncomputable def equalizer.isoSourceOfSelf : equalizerequalizer f f ≅ X :=
  asIso (equalizer.ι f f)

Equalizer of a morphism with itself is isomorphic to source

Informal description

The equalizer of a morphism $f : X \to Y$ with itself is isomorphic to its source object $X$, with the isomorphism given by the equalizer inclusion morphism $\iota : \mathrm{equalizer}(f, f) \to X$.

CategoryTheory.Limits.equalizer.isoSourceOfSelf_hom theorem

: (equalizer.isoSourceOfSelf f).hom = equalizer.ι f f

Full source

@[simp]
theorem equalizer.isoSourceOfSelf_hom : (equalizer.isoSourceOfSelf f).hom = equalizer.ι f f :=
  rfl

Homomorphism of Equalizer-Source Isomorphism is the Inclusion

Informal description

The homomorphism component of the isomorphism $\mathrm{equalizer}(f, f) \cong X$ is equal to the inclusion morphism $\iota : \mathrm{equalizer}(f, f) \to X$.

CategoryTheory.Limits.equalizer.isoSourceOfSelf_inv theorem

: (equalizer.isoSourceOfSelf f).inv = equalizer.lift (𝟙 X) (by simp)

Full source

@[simp]
theorem equalizer.isoSourceOfSelf_inv :
    (equalizer.isoSourceOfSelf f).inv = equalizer.lift (𝟙 X) (by simp) := by
  ext
  simp [equalizer.isoSourceOfSelf]

Inverse of Equalizer-Source Isomorphism for Self-Parallel Morphism

Informal description

The inverse morphism of the isomorphism $\mathrm{equalizer}(f, f) \cong X$ is given by the equalizer's universal property applied to the identity morphism $\mathrm{id}_X : X \to X$ (which trivially satisfies $\mathrm{id}_X \circ f = \mathrm{id}_X \circ f$).

CategoryTheory.Limits.HasCoequalizer abbrev

Full source

/-- `HasCoequalizer f g` represents a particular choice of colimiting cocone
for the parallel pair of morphisms `f` and `g`.
-/
abbrev HasCoequalizer :=
  HasColimit (parallelPair f g)

Existence of a coequalizer for parallel morphisms

Informal description

A category $\mathcal{C}$ is said to *have a coequalizer* for a pair of parallel morphisms $f, g : X \to Y$ if there exists a colimiting cocone over the diagram formed by $f$ and $g$. This means there exists an object $Q$ in $\mathcal{C}$ and a morphism $\pi : Y \to Q$ such that $\pi \circ f = \pi \circ g$, and this pair $(Q, \pi)$ is universal among all such pairs.

CategoryTheory.Limits.coequalizer abbrev

: C

Full source

/-- If a coequalizer of `f` and `g` exists, we can access an arbitrary choice of such by
    saying `coequalizer f g`. -/
noncomputable abbrev coequalizer : C :=
  colimit (parallelPair f g)

Universal Categorical Coequalizer of Parallel Morphisms

Informal description

Given two parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$, the coequalizer $\text{coequalizer}(f, g)$ is an object in $\mathcal{C}$ that serves as the universal coequalizing object for $f$ and $g$. It comes equipped with a morphism $\pi : Y \to \text{coequalizer}(f, g)$ satisfying $\pi \circ f = \pi \circ g$, and is universal among all such objects.

CategoryTheory.Limits.coequalizer.π abbrev

: Y ⟶ coequalizer f g

Full source

/-- If a coequalizer of `f` and `g` exists, we can access the corresponding projection by
    saying `coequalizer.π f g`. -/
noncomputable abbrev coequalizer.π : Y ⟶ coequalizer f g :=
  colimit.ι (parallelPair f g) one

Universal Coequalizer Projection $\pi$ for Parallel Morphisms $f$ and $g$

Informal description

Given two parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$, the coequalizer projection $\pi : Y \to \text{coequalizer}(f, g)$ is the universal morphism satisfying $\pi \circ f = \pi \circ g$.

CategoryTheory.Limits.coequalizer.cofork abbrev

: Cofork f g

Full source

/-- An arbitrary choice of coequalizer cocone for a parallel pair `f` and `g`.
-/
noncomputable abbrev coequalizer.cofork : Cofork f g :=
  colimit.cocone (parallelPair f g)

Cofork Construction for the Coequalizer of Parallel Morphisms

Informal description

Given two parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$, the cofork associated with their coequalizer is a cocone over the parallel pair diagram, consisting of an object $Q$ (the coequalizer) and a morphism $\pi : Y \to Q$ such that $\pi \circ f = \pi \circ g$.

CategoryTheory.Limits.coequalizer.cofork_π theorem

: (coequalizer.cofork f g).π = coequalizer.π f g

Full source

@[simp]
theorem coequalizer.cofork_π : (coequalizer.cofork f g).π = coequalizer.π f g :=
  rfl

Cofork Projection Equals Coequalizer Projection

Informal description

For parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$, the projection morphism $\pi$ of the cofork associated with their coequalizer is equal to the universal coequalizer projection $\pi : Y \to \text{coequalizer}(f, g)$. That is, $\pi_{\text{cofork}(f,g)} = \pi_{f,g}$.

CategoryTheory.Limits.coequalizer.cofork_ι_app_one theorem

: (coequalizer.cofork f g).ι.app one = coequalizer.π f g

Full source

theorem coequalizer.cofork_ι_app_one : (coequalizer.cofork f g).ι.app one = coequalizer.π f g :=
  rfl

Cofork Component at Terminal Object Equals Coequalizer Projection

Informal description

For parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$, the component of the cofork's natural transformation at the terminal object of the walking parallel pair category equals the coequalizer projection $\pi : Y \to \text{coequalizer}(f, g)$. That is, $\iota_{\text{one}} = \pi$ where $\iota$ is the natural transformation of the cofork and $\text{one}$ is the terminal object of the walking parallel pair category.

CategoryTheory.Limits.coequalizer.condition theorem

: f ≫ coequalizer.π f g = g ≫ coequalizer.π f g

Full source

@[reassoc]
theorem coequalizer.condition : f ≫ coequalizer.π f g = g ≫ coequalizer.π f g :=
  Cofork.condition <| colimit.cocone <| parallelPair f g

Coequalizer Condition: $f \circ \pi = g \circ \pi$

Informal description

For any two parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$, the composition of $f$ with the coequalizer projection $\pi : Y \to \text{coequalizer}(f, g)$ equals the composition of $g$ with $\pi$, i.e., $f \circ \pi = g \circ \pi$.

CategoryTheory.Limits.coequalizerIsCoequalizer definition

: IsColimit (Cofork.ofπ (coequalizer.π f g) (coequalizer.condition f g))

Full source

/-- The cofork built from `coequalizer.π f g` is colimiting. -/
noncomputable def coequalizerIsCoequalizer :
    IsColimit (Cofork.ofπ (coequalizer.π f g) (coequalizer.condition f g)) :=
  IsColimit.ofIsoColimit (colimit.isColimit _) (Cofork.ext (Iso.refl _) (by simp))

Cofork from coequalizer projection is colimiting

Informal description

The cofork built from the coequalizer projection $\pi : Y \to \text{coequalizer}(f, g)$ and the coequalizer condition $f \circ \pi = g \circ \pi$ is a colimiting cofork, meaning it satisfies the universal property of coequalizers.

CategoryTheory.Limits.coequalizer.desc abbrev

{W : C} (k : Y ⟶ W) (h : f ≫ k = g ≫ k) : coequalizer f g ⟶ W

Full source

/-- Any morphism `k : Y ⟶ W` satisfying `f ≫ k = g ≫ k` factors through the coequalizer of `f`
    and `g` via `coequalizer.desc : coequalizer f g ⟶ W`. -/
noncomputable abbrev coequalizer.desc {W : C} (k : Y ⟶ W) (h : f ≫ k = g ≫ k) :
    coequalizercoequalizer f g ⟶ W :=
  colimit.desc (parallelPair f g) (Cofork.ofπ k h)

Universal Property of the Coequalizer Morphism

Informal description

Given a morphism $k \colon Y \to W$ in a category $\mathcal{C}$ such that $f \circ k = g \circ k$, there exists a unique morphism $\text{coequalizer.desc}\, k\, h \colon \text{coequalizer}(f, g) \to W$ factoring $k$ through the coequalizer of $f$ and $g$.

CategoryTheory.Limits.coequalizer.π_desc theorem

{W : C} (k : Y ⟶ W) (h : f ≫ k = g ≫ k) : coequalizer.π f g ≫ coequalizer.desc k h = k

Full source

@[reassoc]
theorem coequalizer.π_desc {W : C} (k : Y ⟶ W) (h : f ≫ k = g ≫ k) :
    coequalizer.πcoequalizer.π f g ≫ coequalizer.desc k h = k :=
  colimit.ι_desc _ _

Composition of coequalizer projection with induced morphism equals original morphism

Informal description

Given two parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$ and a morphism $k : Y \to W$ such that $f \circ k = g \circ k$, the composition of the coequalizer projection $\pi : Y \to \text{coequalizer}(f, g)$ with the induced morphism $\text{coequalizer.desc}\, k\, h$ equals $k$, i.e., $\pi \circ (\text{coequalizer.desc}\, k\, h) = k$.

CategoryTheory.Limits.coequalizer.π_colimMap_desc theorem

 {X' Y' Z : C} (f' g' : X' ⟶ Y') [HasCoequalizer f' g'] (p : X ⟶ X') (q : Y ⟶ Y') (wf : f ≫ q = p ≫ f')
  (wg : g ≫ q = p ≫ g') (h : Y' ⟶ Z) (wh : f' ≫ h = g' ≫ h) :
  coequalizer.π f g ≫ colimMap (parallelPairHom f g f' g' p q wf wg) ≫ coequalizer.desc h wh = q ≫ h

Full source

theorem coequalizer.π_colimMap_desc {X' Y' Z : C} (f' g' : X' ⟶ Y') [HasCoequalizer f' g']
    (p : X ⟶ X') (q : Y ⟶ Y') (wf : f ≫ q = p ≫ f') (wg : g ≫ q = p ≫ g') (h : Y' ⟶ Z)
    (wh : f' ≫ h = g' ≫ h) :
    coequalizer.πcoequalizer.π f g ≫ colimMap (parallelPairHom f g f' g' p q wf wg) ≫ coequalizer.desc h wh =
      q ≫ h := by
  rw [ι_colimMap_assoc, parallelPairHom_app_one, coequalizer.π_desc]

Composition Identity for Categorical Coequalizers via Parallel Pair Homomorphism

Informal description

Given two pairs of parallel morphisms $(f, g : X \to Y)$ and $(f', g' : X' \to Y')$ in a category $\mathcal{C}$, with morphisms $p : X \to X'$ and $q : Y \to Y'$ such that the diagrams commute ($f \circ q = p \circ f'$ and $g \circ q = p \circ g'$), and a morphism $h : Y' \to Z$ satisfying $f' \circ h = g' \circ h$, the following composition holds: \[ \pi_{f,g} \circ \text{colimMap}(\text{parallelPairHom}(f, g, f', g', p, q, wf, wg)) \circ \text{coequalizer.desc}(h, wh) = q \circ h \] where $\pi_{f,g} : Y \to \text{coequalizer}(f, g)$ is the coequalizer projection and $\text{coequalizer.desc}(h, wh)$ is the induced morphism from the universal property of the coequalizer of $f'$ and $g'$.

CategoryTheory.Limits.coequalizer.desc' definition

{W : C} (k : Y ⟶ W) (h : f ≫ k = g ≫ k) : { l : coequalizer f g ⟶ W // coequalizer.π f g ≫ l = k }

Full source

/-- Any morphism `k : Y ⟶ W` satisfying `f ≫ k = g ≫ k` induces a morphism
    `l : coequalizer f g ⟶ W` satisfying `coequalizer.π ≫ g = l`. -/
noncomputable def coequalizer.desc' {W : C} (k : Y ⟶ W) (h : f ≫ k = g ≫ k) :
    { l : coequalizer f g ⟶ W // coequalizer.π f g ≫ l = k } :=
  ⟨coequalizer.desc k h, coequalizer.π_desc _ _⟩

Universal property of coequalizer morphism

Informal description

Given two parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$ and a morphism $k : Y \to W$ such that $f \circ k = g \circ k$, there exists a unique morphism $l : \text{coequalizer}(f, g) \to W$ satisfying $\pi \circ l = k$, where $\pi : Y \to \text{coequalizer}(f, g)$ is the coequalizer projection.

CategoryTheory.Limits.coequalizer.hom_ext theorem

{W : C} {k l : coequalizer f g ⟶ W} (h : coequalizer.π f g ≫ k = coequalizer.π f g ≫ l) : k = l

Full source

/-- Two maps from a coequalizer are equal if they are equal when composed with the coequalizer
    map -/
@[ext]
theorem coequalizer.hom_ext {W : C} {k l : coequalizercoequalizer f g ⟶ W}
    (h : coequalizer.πcoequalizer.π f g ≫ k = coequalizer.πcoequalizer.π f g ≫ l) : k = l :=
  Cofork.IsColimit.hom_ext (colimit.isColimit _) h

Uniqueness of Morphisms from Coequalizer via Projection Equality

Informal description

Let $f, g : X \to Y$ be parallel morphisms in a category $\mathcal{C}$ with a coequalizer $\text{coequalizer}(f, g)$. For any object $W$ and any pair of morphisms $k, l : \text{coequalizer}(f, g) \to W$, if the compositions $\pi \circ k$ and $\pi \circ l$ are equal (where $\pi : Y \to \text{coequalizer}(f, g)$ is the coequalizer projection), then $k = l$.

CategoryTheory.Limits.coequalizer.existsUnique theorem

{W : C} (k : Y ⟶ W) (h : f ≫ k = g ≫ k) : ∃! d : coequalizer f g ⟶ W, coequalizer.π f g ≫ d = k

Full source

theorem coequalizer.existsUnique {W : C} (k : Y ⟶ W) (h : f ≫ k = g ≫ k) :
    ∃! d : coequalizer f g ⟶ W, coequalizer.π f g ≫ d = k :=
  Cofork.IsColimit.existsUnique (colimit.isColimit _) _ h

Universal Property of Coequalizer (Unique Existence)

Informal description

Given two parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$ with a coequalizer $\text{coequalizer}(f, g)$, for any object $W$ and morphism $k : Y \to W$ satisfying $f \circ k = g \circ k$, there exists a unique morphism $d : \text{coequalizer}(f, g) \to W$ such that $\pi \circ d = k$, where $\pi : Y \to \text{coequalizer}(f, g)$ is the coequalizer projection.

CategoryTheory.Limits.coequalizer.π_epi instance

: Epi (coequalizer.π f g)

Full source

/-- A coequalizer morphism is an epimorphism -/
instance coequalizer.π_epi : Epi (coequalizer.π f g) where
  left_cancellation _ _ w := coequalizer.hom_ext w

Coequalizer Projection is Epimorphic

Informal description

For any two parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$, the coequalizer projection $\pi : Y \to \text{coequalizer}(f, g)$ is an epimorphism.

CategoryTheory.Limits.epi_of_isColimit_cofork theorem

{c : Cofork f g} (i : IsColimit c) : Epi c.π

Full source

/-- The coequalizer morphism in any colimit cocone is an epimorphism. -/
theorem epi_of_isColimit_cofork {c : Cofork f g} (i : IsColimit c) : Epi c.π :=
  { left_cancellation := fun _ _ w => Cofork.IsColimit.hom_ext i w }

Cofork Projection is Epimorphic in Colimit Cofork

Informal description

For any cofork $c$ of parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$, if $c$ is a colimit cocone, then the cofork projection morphism $\pi_c : Y \to c.\mathrm{pt}$ is an epimorphism.

CategoryTheory.Limits.idCofork definition

(h : f = g) : Cofork f g

Full source

/-- The identity determines a cocone on the coequalizer diagram of `f` and `g`, if `f = g`. -/
def idCofork (h : f = g) : Cofork f g :=
  Cofork.ofπ (𝟙 Y) <| h ▸ rfl

Identity Cofork for Equal Parallel Morphisms

Informal description

Given two parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$ such that $f = g$, the identity morphism $\text{id}_Y$ on $Y$ forms a cocone over the parallel pair $(f, g)$. This cocone is called the identity cofork.

CategoryTheory.Limits.isColimitIdCofork definition

(h : f = g) : IsColimit (idCofork h)

Full source

/-- The identity on `Y` is a coequalizer of `(f, g)`, where `f = g`. -/
def isColimitIdCofork (h : f = g) : IsColimit (idCofork h) :=
  Cofork.IsColimit.mk _ (fun s => Cofork.π s) (fun _ => Category.id_comp _) fun s m h => by
    convert h
    exact (Category.id_comp _).symm

Identity cofork is a colimit cocone for equal parallel morphisms

Informal description

Given two parallel morphisms $ f, g : X \to Y $ in a category $\mathcal{C}$ such that $ f = g $, the identity cofork (formed by the identity morphism $\text{id}_Y$) is a colimit cocone for the parallel pair $(f, g)$. This means that the identity morphism on $ Y $ is the coequalizer of $ f $ and $ g $ when they are equal.

CategoryTheory.Limits.isIso_colimit_cocone_parallelPair_of_eq theorem

(h₀ : f = g) {c : Cofork f g} (h : IsColimit c) : IsIso c.π

Full source

/-- Every coequalizer of `(f, g)`, where `f = g`, is an isomorphism. -/
theorem isIso_colimit_cocone_parallelPair_of_eq (h₀ : f = g) {c : Cofork f g} (h : IsColimit c) :
    IsIso c.π :=
  Iso.isIso_hom <| IsColimit.coconePointUniqueUpToIso (isColimitIdCofork h₀) h

Cofork projection is isomorphism when parallel morphisms are equal and cocone is colimit

Informal description

Let $f, g : X \to Y$ be parallel morphisms in a category $\mathcal{C}$ such that $f = g$. For any cofork $c$ of $(f, g)$ that is a colimit cocone, the morphism $\pi_c : Y \to c.\mathrm{pt}$ is an isomorphism.

CategoryTheory.Limits.coequalizer.π_of_eq theorem

[HasCoequalizer f g] (h : f = g) : IsIso (coequalizer.π f g)

Full source

/-- The coequalizer of `(f, g)`, where `f = g`, is an isomorphism. -/
theorem coequalizer.π_of_eq [HasCoequalizer f g] (h : f = g) : IsIso (coequalizer.π f g) :=
  isIso_colimit_cocone_parallelPair_of_eq h <| colimit.isColimit _

Coequalizer Projection Isomorphism for Equal Parallel Morphisms

Informal description

Given two parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$ with a coequalizer, if $f = g$, then the coequalizer projection $\pi : Y \to \text{coequalizer}(f, g)$ is an isomorphism.

CategoryTheory.Limits.isIso_colimit_cocone_parallelPair_of_self theorem

{c : Cofork f f} (h : IsColimit c) : IsIso c.π

Full source

/-- Every coequalizer of `(f, f)` is an isomorphism. -/
theorem isIso_colimit_cocone_parallelPair_of_self {c : Cofork f f} (h : IsColimit c) : IsIso c.π :=
  isIso_colimit_cocone_parallelPair_of_eq rfl h

Cofork projection is isomorphism for self-parallel morphisms with colimit cocone

Informal description

For any cofork $c$ of the parallel pair $(f, f)$ in a category $\mathcal{C}$, if $c$ is a colimit cocone, then the cofork projection $\pi_c : Y \to c.\mathrm{pt}$ is an isomorphism.

CategoryTheory.Limits.isIso_limit_cocone_parallelPair_of_epi theorem

{c : Cofork f g} (h : IsColimit c) [Mono c.π] : IsIso c.π

Full source

/-- A coequalizer that is a monomorphism is an isomorphism. -/
theorem isIso_limit_cocone_parallelPair_of_epi {c : Cofork f g} (h : IsColimit c) [Mono c.π] :
    IsIso c.π :=
  isIso_colimit_cocone_parallelPair_of_eq ((cancel_mono _).1 (Cofork.condition c)) h

Monomorphic coequalizer projection is an isomorphism

Informal description

Let $f, g : X \to Y$ be parallel morphisms in a category $\mathcal{C}$. Given a cofork $c$ of $(f, g)$ that is a colimit cocone, if the projection morphism $\pi_c : Y \to c.\mathrm{pt}$ is a monomorphism, then $\pi_c$ is an isomorphism.

CategoryTheory.Limits.hasCoequalizer_of_self instance

: HasCoequalizer f f

Full source

instance hasCoequalizer_of_self : HasCoequalizer f f :=
  HasColimit.mk
    { cocone := idCofork rfl
      isColimit := isColimitIdCofork rfl }

Existence of Cofork for Equal Parallel Morphisms

Informal description

For any pair of parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$ where $f = g$, the pair $(f, g)$ has a coequalizer.

CategoryTheory.Limits.coequalizer.π_of_self instance

: IsIso (coequalizer.π f f)

Full source

/-- The coequalizer projection for `(f, f)` is an isomorphism. -/
instance coequalizer.π_of_self : IsIso (coequalizer.π f f) :=
  coequalizer.π_of_eq rfl

Coequalizer Projection Isomorphism for Identical Morphisms

Informal description

For any parallel morphisms $f, f : X \to Y$ in a category $\mathcal{C}$, the coequalizer projection $\pi : Y \to \text{coequalizer}(f, f)$ is an isomorphism.

CategoryTheory.Limits.coequalizer.isoTargetOfSelf definition

: coequalizer f f ≅ Y

Full source

/-- The coequalizer of a morphism with itself is isomorphic to the target. -/
noncomputable def coequalizer.isoTargetOfSelf : coequalizercoequalizer f f ≅ Y :=
  (asIso (coequalizer.π f f)).symm

Coequalizer of a morphism with itself is isomorphic to its target

Informal description

The coequalizer of a morphism $f : X \to Y$ with itself is isomorphic to its target object $Y$. Specifically, the isomorphism is given by the inverse of the coequalizer projection $\pi : Y \to \text{coequalizer}(f, f)$, which is an isomorphism in this case.

CategoryTheory.Limits.coequalizer.isoTargetOfSelf_hom theorem

: (coequalizer.isoTargetOfSelf f).hom = coequalizer.desc (𝟙 Y) (by simp)

Full source

@[simp]
theorem coequalizer.isoTargetOfSelf_hom :
    (coequalizer.isoTargetOfSelf f).hom = coequalizer.desc (𝟙 Y) (by simp) := by
  ext
  simp [coequalizer.isoTargetOfSelf]

Homomorphism of Coequalizer Self-Isomorphism is Universal Descend

Informal description

The homomorphism component of the isomorphism $\text{coequalizer}(f, f) \cong Y$ is equal to the coequalizer's universal morphism $\text{coequalizer.desc}$ applied to the identity morphism $\text{id}_Y$ on $Y$.

CategoryTheory.Limits.coequalizer.isoTargetOfSelf_inv theorem

: (coequalizer.isoTargetOfSelf f).inv = coequalizer.π f f

Full source

@[simp]
theorem coequalizer.isoTargetOfSelf_inv : (coequalizer.isoTargetOfSelf f).inv = coequalizer.π f f :=
  rfl

Inverse of Coequalizer Self-Isomorphism Equals Projection

Informal description

The inverse of the isomorphism $\text{coequalizer.isoTargetOfSelf}(f) : \text{coequalizer}(f, f) \cong Y$ is equal to the coequalizer projection $\pi : Y \to \text{coequalizer}(f, f)$.

CategoryTheory.Limits.equalizerComparison definition

[HasEqualizer f g] [HasEqualizer (G.map f) (G.map g)] : G.obj (equalizer f g) ⟶ equalizer (G.map f) (G.map g)

Full source

/-- The comparison morphism for the equalizer of `f,g`.
This is an isomorphism iff `G` preserves the equalizer of `f,g`; see
`CategoryTheory/Limits/Preserves/Shapes/Equalizers.lean`
-/
noncomputable def equalizerComparison [HasEqualizer f g] [HasEqualizer (G.map f) (G.map g)] :
    G.obj (equalizer f g) ⟶ equalizer (G.map f) (G.map g) :=
  equalizer.lift (G.map (equalizer.ι _ _))
    (by simp only [← G.map_comp]; rw [equalizer.condition])

Comparison morphism for equalizers under functor $G$

Informal description

Given a functor $G : \mathcal{C} \to \mathcal{D}$ and two parallel morphisms $f, g : X \to Y$ in $\mathcal{C}$, the comparison morphism $\mathrm{equalizerComparison}(f, g, G)$ is the unique morphism from $G(\mathrm{equalizer}(f, g))$ to $\mathrm{equalizer}(G(f), G(g))$ in $\mathcal{D}$ that makes the following diagram commute: \[ G(\mathrm{equalizer}(f, g)) \xrightarrow{\mathrm{equalizerComparison}(f, g, G)} \mathrm{equalizer}(G(f), G(g)) \] This morphism is an isomorphism if and only if $G$ preserves the equalizer of $f$ and $g$.

CategoryTheory.Limits.equalizerComparison_comp_π theorem

 [HasEqualizer f g] [HasEqualizer (G.map f) (G.map g)] :
  equalizerComparison f g G ≫ equalizer.ι (G.map f) (G.map g) = G.map (equalizer.ι f g)

Full source

@[reassoc (attr := simp)]
theorem equalizerComparison_comp_π [HasEqualizer f g] [HasEqualizer (G.map f) (G.map g)] :
    equalizerComparisonequalizerComparison f g G ≫ equalizer.ι (G.map f) (G.map g) = G.map (equalizer.ι f g) :=
  equalizer.lift_ι _ _

Commutativity of Equalizer Comparison with Inclusion Morphisms

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories with equalizers, and let $G : \mathcal{C} \to \mathcal{D}$ be a functor. Given two parallel morphisms $f, g : X \to Y$ in $\mathcal{C}$, the composition of the equalizer comparison morphism $\mathrm{equalizerComparison}(f, g, G)$ with the inclusion morphism $\iota$ of the equalizer of $G(f)$ and $G(g)$ equals the image under $G$ of the inclusion morphism $\iota$ of the equalizer of $f$ and $g$. That is, the following diagram commutes: \[ \mathrm{equalizerComparison}(f, g, G) \circ \iota_{G(f), G(g)} = G(\iota_{f, g}) \]

CategoryTheory.Limits.map_lift_equalizerComparison theorem

 [HasEqualizer f g] [HasEqualizer (G.map f) (G.map g)] {Z : C} {h : Z ⟶ X} (w : h ≫ f = h ≫ g) :
  G.map (equalizer.lift h w) ≫ equalizerComparison f g G = equalizer.lift (G.map h) (by simp only [← G.map_comp, w])

Full source

@[reassoc (attr := simp)]
theorem map_lift_equalizerComparison [HasEqualizer f g] [HasEqualizer (G.map f) (G.map g)] {Z : C}
    {h : Z ⟶ X} (w : h ≫ f = h ≫ g) :
    G.map (equalizer.lift h w) ≫ equalizerComparison f g G =
      equalizer.lift (G.map h) (by simp only [← G.map_comp, w]) := by
  apply equalizer.hom_ext
  simp [← G.map_comp]

Functoriality of Equalizer Lifting: $G(\mathrm{lift}(h)) \circ \mathrm{comp}(G) = \mathrm{lift}(G(h))$

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories with equalizers, and let $G : \mathcal{C} \to \mathcal{D}$ be a functor. Given two parallel morphisms $f, g : X \to Y$ in $\mathcal{C}$ and a morphism $h : Z \to X$ such that $h \circ f = h \circ g$, the following diagram commutes: \[ G(\mathrm{equalizer.lift}(h, w)) \circ \mathrm{equalizerComparison}(f, g, G) = \mathrm{equalizer.lift}(G(h), \text{by simp only } [\leftarrow G.map_comp, w]) \] where $w$ is the proof that $h$ equalizes $f$ and $g$.

CategoryTheory.Limits.coequalizerComparison definition

[HasCoequalizer f g] [HasCoequalizer (G.map f) (G.map g)] : coequalizer (G.map f) (G.map g) ⟶ G.obj (coequalizer f g)

Full source

/-- The comparison morphism for the coequalizer of `f,g`. -/
noncomputable def coequalizerComparison [HasCoequalizer f g] [HasCoequalizer (G.map f) (G.map g)] :
    coequalizercoequalizer (G.map f) (G.map g) ⟶ G.obj (coequalizer f g) :=
  coequalizer.desc (G.map (coequalizer.π _ _))
    (by simp only [← G.map_comp]; rw [coequalizer.condition])

Coequalizer comparison morphism under a functor

Informal description

Given a functor $G \colon \mathcal{C} \to \mathcal{D}$ and two parallel morphisms $f, g \colon X \to Y$ in $\mathcal{C}$, the coequalizer comparison morphism is the unique morphism from the coequalizer of $G(f)$ and $G(g)$ in $\mathcal{D}$ to the image under $G$ of the coequalizer of $f$ and $g$ in $\mathcal{C}$. This morphism is induced by the universal property of the coequalizer in $\mathcal{D}$ applied to $G$ of the coequalizer projection in $\mathcal{C}$.

CategoryTheory.Limits.ι_comp_coequalizerComparison theorem

 [HasCoequalizer f g] [HasCoequalizer (G.map f) (G.map g)] :
  coequalizer.π _ _ ≫ coequalizerComparison f g G = G.map (coequalizer.π _ _)

Full source

@[reassoc (attr := simp)]
theorem ι_comp_coequalizerComparison [HasCoequalizer f g] [HasCoequalizer (G.map f) (G.map g)] :
    coequalizer.πcoequalizer.π _ _ ≫ coequalizerComparison f g G = G.map (coequalizer.π _ _) :=
  coequalizer.π_desc _ _

Commutativity of coequalizer projection with comparison morphism under a functor

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories with coequalizers, and let $G \colon \mathcal{C} \to \mathcal{D}$ be a functor. Given two parallel morphisms $f, g \colon X \to Y$ in $\mathcal{C}$, the composition of the coequalizer projection $\pi \colon Y \to \text{coequalizer}(f, g)$ with the coequalizer comparison morphism $\text{coequalizerComparison}\, f\, g\, G$ equals the image under $G$ of the coequalizer projection in $\mathcal{C}$, i.e., \[ \pi \circ \text{coequalizerComparison}\, f\, g\, G = G(\pi). \]

CategoryTheory.Limits.coequalizerComparison_map_desc theorem

 [HasCoequalizer f g] [HasCoequalizer (G.map f) (G.map g)] {Z : C} {h : Y ⟶ Z} (w : f ≫ h = g ≫ h) :
  coequalizerComparison f g G ≫ G.map (coequalizer.desc h w) =
    coequalizer.desc (G.map h) (by simp only [← G.map_comp, w])

Full source

@[reassoc (attr := simp)]
theorem coequalizerComparison_map_desc [HasCoequalizer f g] [HasCoequalizer (G.map f) (G.map g)]
    {Z : C} {h : Y ⟶ Z} (w : f ≫ h = g ≫ h) :
    coequalizerComparisoncoequalizerComparison f g G ≫ G.map (coequalizer.desc h w) =
      coequalizer.desc (G.map h) (by simp only [← G.map_comp, w]) := by
  apply coequalizer.hom_ext
  simp [← G.map_comp]

Commutativity of coequalizer comparison with descent morphism under a functor

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories with coequalizers, and let $G \colon \mathcal{C} \to \mathcal{D}$ be a functor. Given two parallel morphisms $f, g \colon X \to Y$ in $\mathcal{C}$ and a morphism $h \colon Y \to Z$ such that $f \circ h = g \circ h$, the composition of the coequalizer comparison morphism $\text{coequalizerComparison}\, f\, g\, G$ with $G$ applied to the coequalizer descent morphism $\text{coequalizer.desc}\, h\, w$ equals the coequalizer descent morphism of $G(h)$ in $\mathcal{D}$. That is, \[ \text{coequalizerComparison}\, f\, g\, G \circ G(\text{coequalizer.desc}\, h\, w) = \text{coequalizer.desc}\, G(h)\, w'. \]

CategoryTheory.Limits.HasEqualizers abbrev

Full source

/-- `HasEqualizers` represents a choice of equalizer for every pair of morphisms -/
abbrev HasEqualizers :=
  HasLimitsOfShape WalkingParallelPair C

Existence of Equalizers in a Category

Informal description

A category $\mathcal{C}$ has equalizers if for every pair of parallel morphisms $f, g : X \to Y$ in $\mathcal{C}$, there exists a limit cone over the diagram formed by $f$ and $g$. This means there exists an object $E$ and a morphism $\iota : E \to X$ such that $\iota$ equalizes $f$ and $g$ (i.e., $\iota \circ f = \iota \circ g$), and $E$ is universal with this property.

CategoryTheory.Limits.HasCoequalizers abbrev

Full source

/-- `HasCoequalizers` represents a choice of coequalizer for every pair of morphisms -/
abbrev HasCoequalizers :=
  HasColimitsOfShape WalkingParallelPair C

Existence of Coequalizers in a Category

Informal description

A category $\mathcal{C}$ is said to *have coequalizers* if for every pair of parallel morphisms $f, g: X \to Y$ in $\mathcal{C}$, there exists a coequalizer object $Q$ and a morphism $q: Y \to Q$ such that $f \circ q = g \circ q$, and $q$ is universal with this property (i.e., any other morphism $h: Y \to Z$ satisfying $f \circ h = g \circ h$ factors uniquely through $q$).

CategoryTheory.Limits.hasEqualizers_of_hasLimit_parallelPair theorem

[∀ {X Y : C} {f g : X ⟶ Y}, HasLimit (parallelPair f g)] : HasEqualizers C

Full source

/-- If `C` has all limits of diagrams `parallelPair f g`, then it has all equalizers -/
theorem hasEqualizers_of_hasLimit_parallelPair
    [∀ {X Y : C} {f g : X ⟶ Y}, HasLimit (parallelPair f g)] : HasEqualizers C :=
  { has_limit := fun F => hasLimit_of_iso (diagramIsoParallelPair F).symm }

Existence of Equalizers from Limits of Parallel Pairs

Informal description

If a category $\mathcal{C}$ has all limits of diagrams of the form $\text{parallelPair}(f,g)$ for every pair of parallel morphisms $f, g : X \to Y$ in $\mathcal{C}$, then $\mathcal{C}$ has all equalizers.

CategoryTheory.Limits.hasCoequalizers_of_hasColimit_parallelPair theorem

[∀ {X Y : C} {f g : X ⟶ Y}, HasColimit (parallelPair f g)] : HasCoequalizers C

Full source

/-- If `C` has all colimits of diagrams `parallelPair f g`, then it has all coequalizers -/
theorem hasCoequalizers_of_hasColimit_parallelPair
    [∀ {X Y : C} {f g : X ⟶ Y}, HasColimit (parallelPair f g)] : HasCoequalizers C :=
  { has_colimit := fun F => hasColimit_of_iso (diagramIsoParallelPair F) }

Existence of Coequalizers from Colimits of Parallel Pairs

Informal description

If a category $\mathcal{C}$ has all colimits of diagrams formed by parallel pairs of morphisms $f, g: X \to Y$, then $\mathcal{C}$ has all coequalizers.

CategoryTheory.Limits.coneOfIsSplitMono definition

: Fork (𝟙 Y) (retraction f ≫ f)

Full source

/-- A split mono `f` equalizes `(retraction f ≫ f)` and `(𝟙 Y)`.
Here we build the cone, and show in `isSplitMonoEqualizes` that it is a limit cone.
-/
-- @[simps (config := { rhsMd := semireducible })] Porting note: no semireducible
@[simps!]
noncomputable def coneOfIsSplitMono : Fork (𝟙 Y) (retractionretraction f ≫ f) :=
  Fork.ofι f (by simp)

Cone for a split monomorphism as a fork over (id, retraction f ∘ f)

Informal description

Given a split monomorphism $f : X \to Y$ in a category $\mathcal{C}$, the cone $\text{coneOfIsSplitMono}\, f$ is a fork over the parallel pair consisting of the identity morphism $\text{id}_Y$ and the composition of the retraction of $f$ with $f$ itself, i.e., $\text{retraction}\, f \circ f$. The morphism from the vertex of this fork to $X$ is $f$ itself, satisfying the condition $f \circ \text{id}_Y = f \circ (\text{retraction}\, f \circ f)$ (which holds by definition of a retraction).

CategoryTheory.Limits.coneOfIsSplitMono_ι theorem

: (coneOfIsSplitMono f).ι = f

Full source

@[simp]
theorem coneOfIsSplitMono_ι : (coneOfIsSplitMono f).ι = f :=
  rfl

Inclusion morphism of split mono cone equals $f$

Informal description

For a split monomorphism $f : X \to Y$ in a category $\mathcal{C}$, the inclusion morphism $\iota$ of the cone $\text{coneOfIsSplitMono}\, f$ is equal to $f$ itself.

CategoryTheory.Limits.isSplitMonoEqualizes definition

{X Y : C} (f : X ⟶ Y) [IsSplitMono f] : IsLimit (coneOfIsSplitMono f)

Full source

/-- A split mono `f` equalizes `(retraction f ≫ f)` and `(𝟙 Y)`.
-/
noncomputable def isSplitMonoEqualizes {X Y : C} (f : X ⟶ Y) [IsSplitMono f] :
    IsLimit (coneOfIsSplitMono f) :=
  Fork.IsLimit.mk' _ fun s =>
    ⟨s.ι ≫ retraction f, by
      dsimp
      rw [Category.assoc, ← s.condition]
      apply Category.comp_id, fun hm => by simp [← hm]⟩

Split monomorphism equalizes (id, retraction f ∘ f)

Informal description

Given a split monomorphism $f : X \to Y$ in a category $\mathcal{C}$, the fork $\text{coneOfIsSplitMono}\, f$ is a limit cone for the parallel pair consisting of the identity morphism $\text{id}_Y$ and the composition $\text{retraction}\, f \circ f$.

CategoryTheory.Limits.splitMonoOfEqualizer definition

 {X Y : C} {f : X ⟶ Y} {r : Y ⟶ X} (hr : f ≫ r ≫ f = f)
  (h : IsLimit (Fork.ofι f (hr.trans (Category.comp_id _).symm : f ≫ r ≫ f = f ≫ 𝟙 Y))) : SplitMono f

Full source

/-- We show that the converse to `isSplitMonoEqualizes` is true:
Whenever `f` equalizes `(r ≫ f)` and `(𝟙 Y)`, then `r` is a retraction of `f`. -/
def splitMonoOfEqualizer {X Y : C} {f : X ⟶ Y} {r : Y ⟶ X} (hr : f ≫ r ≫ f = f)
    (h : IsLimit (Fork.ofι f (hr.trans (Category.comp_id _).symm : f ≫ r ≫ f = f ≫ 𝟙 Y))) :
    SplitMono f where
  retraction := r
  id := Fork.IsLimit.hom_ext h ((Category.assoc _ _ _).trans <| hr.trans (Category.id_comp _).symm)

Split monomorphism from equalizer condition

Informal description

Given a morphism $f : X \to Y$ in a category $\mathcal{C}$ and a morphism $r : Y \to X$ such that $f \circ r \circ f = f$, if the fork formed by $f$ and the identity morphism on $Y$ is a limit cone, then $f$ is a split monomorphism with retraction $r$.

CategoryTheory.Limits.isEqualizerCompMono definition

 {c : Fork f g} (i : IsLimit c) {Z : C} (h : Y ⟶ Z) [hm : Mono h] :
  have : Fork.ι c ≫ f ≫ h = Fork.ι c ≫ g ≫ h :=
    by
    simp only [← Category.assoc]
    exact congrArg (· ≫ h) c.condition
  IsLimit (Fork.ofι c.ι (by simp [this]) : Fork (f ≫ h) (g ≫ h))

Full source

/-- The fork obtained by postcomposing an equalizer fork with a monomorphism is an equalizer. -/
def isEqualizerCompMono {c : Fork f g} (i : IsLimit c) {Z : C} (h : Y ⟶ Z) [hm : Mono h] :
    have : Fork.ιFork.ι c ≫ f ≫ h = Fork.ιFork.ι c ≫ g ≫ h := by
      simp only [← Category.assoc]
      exact congrArg (· ≫ h) c.condition
    IsLimit (Fork.ofι c.ι (by simp [this]) : Fork (f ≫ h) (g ≫ h)) :=
  Fork.IsLimit.mk' _ fun s =>
    let s' : Fork f g := Fork.ofι s.ι (by apply hm.right_cancellation; simp [s.condition])
    let l := Fork.IsLimit.lift' i s'.ι s'.condition
    ⟨l.1, l.2, fun hm => by
      apply Fork.IsLimit.hom_ext i; rw [Fork.ι_ofι] at hm; rw [hm]; exact l.2.symm⟩

Limit fork remains limit after postcomposing with a monomorphism

Informal description

Given a limit fork $c$ of parallel morphisms $f, g : X \to Y$ in a category $\mathcal{C}$, and a monomorphism $h : Y \to Z$, the fork obtained by postcomposing $f$ and $g$ with $h$ is also a limit fork. Specifically, the fork with vertex $c.\mathrm{pt}$ and inclusion morphism $c.\iota$ is a limit cone for the parallel pair $(f \circ h, g \circ h)$.

CategoryTheory.Limits.hasEqualizer_comp_mono theorem

[HasEqualizer f g] {Z : C} (h : Y ⟶ Z) [Mono h] : HasEqualizer (f ≫ h) (g ≫ h)

Full source

@[instance]
theorem hasEqualizer_comp_mono [HasEqualizer f g] {Z : C} (h : Y ⟶ Z) [Mono h] :
    HasEqualizer (f ≫ h) (g ≫ h) :=
  ⟨⟨{   cone := _
        isLimit := isEqualizerCompMono (limit.isLimit _) h }⟩⟩

Existence of Equalizer for Postcomposed Parallel Morphisms with a Monomorphism

Informal description

If a category $\mathcal{C}$ has an equalizer for the parallel morphisms $f, g : X \to Y$, and $h : Y \to Z$ is a monomorphism, then $\mathcal{C}$ also has an equalizer for the postcomposed morphisms $f \circ h, g \circ h : X \to Z$.

CategoryTheory.Limits.splitMonoOfIdempotentOfIsLimitFork definition

{X : C} {f : X ⟶ X} (hf : f ≫ f = f) {c : Fork (𝟙 X) f} (i : IsLimit c) : SplitMono c.ι

Full source

/-- An equalizer of an idempotent morphism and the identity is split mono. -/
@[simps]
def splitMonoOfIdempotentOfIsLimitFork {X : C} {f : X ⟶ X} (hf : f ≫ f = f) {c : Fork (𝟙 X) f}
    (i : IsLimit c) : SplitMono c.ι where
  retraction := i.lift (Fork.ofι f (by simp [hf]))
  id := by
    letI := mono_of_isLimit_fork i
    rw [← cancel_mono_id c.ι, Category.assoc, Fork.IsLimit.lift_ι, Fork.ι_ofι, ← c.condition]
    exact Category.comp_id c.ι

Split monomorphism from an idempotent equalizer

Informal description

Given an idempotent morphism $f : X \to X$ (i.e., $f \circ f = f$) in a category $\mathcal{C}$ and a fork $c$ over the parallel pair $(1_X, f)$ that is a limit cone, the morphism $\iota_c : c.\text{pt} \to X$ is a split monomorphism. This means there exists a retraction $r : X \to c.\text{pt}$ such that $r \circ \iota_c = \text{id}_{c.\text{pt}}$.

CategoryTheory.Limits.splitMonoOfIdempotentEqualizer definition

{X : C} {f : X ⟶ X} (hf : f ≫ f = f) [HasEqualizer (𝟙 X) f] : SplitMono (equalizer.ι (𝟙 X) f)

Full source

/-- The equalizer of an idempotent morphism and the identity is split mono. -/
noncomputable def splitMonoOfIdempotentEqualizer {X : C} {f : X ⟶ X} (hf : f ≫ f = f)
    [HasEqualizer (𝟙 X) f] : SplitMono (equalizer.ι (𝟙 X) f) :=
  splitMonoOfIdempotentOfIsLimitFork _ hf (limit.isLimit _)

Split monomorphism from an idempotent equalizer

Informal description

Given an idempotent morphism $ f : X \to X $ (i.e., $ f \circ f = f $) in a category $ \mathcal{C} $ where the equalizer of the identity morphism $ \mathbb{1}_X $ and $ f $ exists, the inclusion morphism $ \iota : \mathrm{equalizer}(\mathbb{1}_X, f) \to X $ is a split monomorphism. This means there exists a retraction $ r : X \to \mathrm{equalizer}(\mathbb{1}_X, f) $ such that $ r \circ \iota = \text{id}_{\mathrm{equalizer}(\mathbb{1}_X, f)} $.

CategoryTheory.Limits.coconeOfIsSplitEpi definition

: Cofork (𝟙 X) (f ≫ section_ f)

Full source

/-- A split epi `f` coequalizes `(f ≫ section_ f)` and `(𝟙 X)`.
Here we build the cocone, and show in `isSplitEpiCoequalizes` that it is a colimit cocone.
-/
-- @[simps (config := { rhsMd := semireducible })] Porting note: no semireducible
@[simps!]
noncomputable def coconeOfIsSplitEpi : Cofork (𝟙 X) (f ≫ section_ f) :=
  Cofork.ofπ f (by simp)

Cofork construction for a split epimorphism

Informal description

Given a split epimorphism $f : X \to Y$ in a category $\mathcal{C}$, the construction `coconeOfIsSplitEpi` produces a cofork on the parallel pair consisting of the identity morphism $\mathbb{1}_X$ and the composition $f \circ s$, where $s$ is a section of $f$. The cocone has $Y$ as its vertex and $f$ as the cofork morphism, satisfying the coequalizer condition $f \circ \mathbb{1}_X = f \circ (f \circ s)$.

CategoryTheory.Limits.coconeOfIsSplitEpi_π theorem

: (coconeOfIsSplitEpi f).π = f

Full source

@[simp]
theorem coconeOfIsSplitEpi_π : (coconeOfIsSplitEpi f).π = f :=
  rfl

Cofork Projection of Split Epimorphism Equals Itself

Informal description

For a split epimorphism $f : X \to Y$ in a category $\mathcal{C}$, the cofork projection morphism $\pi$ of the cocone constructed from $f$ is equal to $f$ itself.

CategoryTheory.Limits.isSplitEpiCoequalizes definition

{X Y : C} (f : X ⟶ Y) [IsSplitEpi f] : IsColimit (coconeOfIsSplitEpi f)

Full source

/-- A split epi `f` coequalizes `(f ≫ section_ f)` and `(𝟙 X)`.
-/
noncomputable def isSplitEpiCoequalizes {X Y : C} (f : X ⟶ Y) [IsSplitEpi f] :
    IsColimit (coconeOfIsSplitEpi f) :=
  Cofork.IsColimit.mk' _ fun s =>
    ⟨section_ f ≫ s.π, by
      dsimp
      rw [← Category.assoc, ← s.condition, Category.id_comp], fun hm => by simp [← hm]⟩

Split epimorphism coequalizes its section composition with identity

Informal description

Given a split epimorphism $f : X \to Y$ in a category $\mathcal{C}$, the cocone constructed from $f$ (with vertex $Y$ and morphism $f$) is a colimit cocone for the parallel pair consisting of the identity morphism $\mathbb{1}_X$ and the composition $f \circ s$, where $s$ is a section of $f$.

CategoryTheory.Limits.splitEpiOfCoequalizer definition

 {X Y : C} {f : X ⟶ Y} {s : Y ⟶ X} (hs : f ≫ s ≫ f = f)
  (h :
    IsColimit
      (Cofork.ofπ f ((Category.assoc _ _ _).trans <| hs.trans (Category.id_comp f).symm : (f ≫ s) ≫ f = 𝟙 X ≫ f))) :
  SplitEpi f

Full source

/-- We show that the converse to `isSplitEpiEqualizes` is true:
Whenever `f` coequalizes `(f ≫ s)` and `(𝟙 X)`, then `s` is a section of `f`. -/
def splitEpiOfCoequalizer {X Y : C} {f : X ⟶ Y} {s : Y ⟶ X} (hs : f ≫ s ≫ f = f)
    (h :
      IsColimit
        (Cofork.ofπ f
          ((Category.assoc _ _ _).trans <| hs.trans (Category.id_comp f).symm :
            (f ≫ s) ≫ f = 𝟙𝟙 X ≫ f))) :
    SplitEpi f where
  section_ := s
  id := Cofork.IsColimit.hom_ext h (hs.trans (Category.comp_id _).symm)

Split epimorphism from coequalizer condition

Informal description

Given morphisms $f : X \to Y$ and $s : Y \to X$ in a category $\mathcal{C}$ such that $f \circ s \circ f = f$, and given that the cofork formed by $f$ is a colimit, then $f$ is a split epimorphism with section $s$.

CategoryTheory.Limits.isCoequalizerEpiComp definition

 {c : Cofork f g} (i : IsColimit c) {W : C} (h : W ⟶ X) [hm : Epi h] :
  have : (h ≫ f) ≫ Cofork.π c = (h ≫ g) ≫ Cofork.π c :=
    by
    simp only [Category.assoc]
    exact congrArg (h ≫ ·) c.condition
  IsColimit (Cofork.ofπ c.π (this) : Cofork (h ≫ f) (h ≫ g))

Full source

/-- The cofork obtained by precomposing a coequalizer cofork with an epimorphism is
a coequalizer. -/
def isCoequalizerEpiComp {c : Cofork f g} (i : IsColimit c) {W : C} (h : W ⟶ X) [hm : Epi h] :
    have : (h ≫ f) ≫ Cofork.π c = (h ≫ g) ≫ Cofork.π c := by
      simp only [Category.assoc]
      exact congrArg (h ≫ ·) c.condition
    IsColimit (Cofork.ofπ c.π (this) : Cofork (h ≫ f) (h ≫ g)) :=
  Cofork.IsColimit.mk' _ fun s =>
    let s' : Cofork f g :=
      Cofork.ofπ s.π (by apply hm.left_cancellation; simp_rw [← Category.assoc, s.condition])
    let l := Cofork.IsColimit.desc' i s'.π s'.condition
    ⟨l.1, l.2, fun hm => by
      apply Cofork.IsColimit.hom_ext i; rw [Cofork.π_ofπ] at hm; rw [hm]; exact l.2.symm⟩

Colimit cofork preserved under precomposition with an epimorphism

Informal description

Given a cofork $ c $ of parallel morphisms $ f, g : X \to Y $ in a category $ \mathcal{C} $, if $ c $ is a colimit cofork and $ h : W \to X $ is an epimorphism, then the cofork obtained by precomposing $ f $ and $ g $ with $ h $ (i.e., $ h \circ f $ and $ h \circ g $) is also a colimit cofork. Specifically, the cofork formed by the projection $ \pi_c : Y \to c.\text{pt} $ remains a colimit under this composition.

CategoryTheory.Limits.hasCoequalizer_epi_comp theorem

[HasCoequalizer f g] {W : C} (h : W ⟶ X) [Epi h] : HasCoequalizer (h ≫ f) (h ≫ g)

Full source

theorem hasCoequalizer_epi_comp [HasCoequalizer f g] {W : C} (h : W ⟶ X) [Epi h] :
    HasCoequalizer (h ≫ f) (h ≫ g) :=
  ⟨⟨{   cocone := _
        isColimit := isCoequalizerEpiComp (colimit.isColimit _) h }⟩⟩

Existence of coequalizer preserved under precomposition with an epimorphism

Informal description

Let $\mathcal{C}$ be a category with a coequalizer for a pair of parallel morphisms $f, g : X \to Y$. Given an epimorphism $h : W \to X$, the pair of morphisms $h \circ f, h \circ g : W \to Y$ also has a coequalizer in $\mathcal{C}$.

CategoryTheory.Limits.splitEpiOfIdempotentOfIsColimitCofork definition

{X : C} {f : X ⟶ X} (hf : f ≫ f = f) {c : Cofork (𝟙 X) f} (i : IsColimit c) : SplitEpi c.π

Full source

/-- A coequalizer of an idempotent morphism and the identity is split epi. -/
@[simps]
def splitEpiOfIdempotentOfIsColimitCofork {X : C} {f : X ⟶ X} (hf : f ≫ f = f) {c : Cofork (𝟙 X) f}
    (i : IsColimit c) : SplitEpi c.π where
  section_ := i.desc (Cofork.ofπ f (by simp [hf]))
  id := by
    letI := epi_of_isColimit_cofork i
    rw [← cancel_epi_id c.π, ← Category.assoc, Cofork.IsColimit.π_desc, Cofork.π_ofπ, ←
      c.condition]
    exact Category.id_comp _

Split epimorphism from idempotent cofork colimit

Informal description

Given an idempotent morphism $f : X \to X$ (i.e., $f \circ f = f$) in a category $\mathcal{C}$, and a cofork $c$ of the identity morphism $\text{id}_X$ and $f$ that is a colimit, the projection morphism $\pi_c : X \to c.\text{pt}$ is a split epimorphism. This means there exists a section (right inverse) for $\pi_c$.

CategoryTheory.Limits.splitEpiOfIdempotentCoequalizer definition

{X : C} {f : X ⟶ X} (hf : f ≫ f = f) [HasCoequalizer (𝟙 X) f] : SplitEpi (coequalizer.π (𝟙 X) f)

Full source

/-- The coequalizer of an idempotent morphism and the identity is split epi. -/
noncomputable def splitEpiOfIdempotentCoequalizer {X : C} {f : X ⟶ X} (hf : f ≫ f = f)
    [HasCoequalizer (𝟙 X) f] : SplitEpi (coequalizer.π (𝟙 X) f) :=
  splitEpiOfIdempotentOfIsColimitCofork _ hf (colimit.isColimit _)

Split epimorphism from idempotent coequalizer

Informal description

Given an idempotent morphism $f : X \to X$ (i.e., $f \circ f = f$) in a category $\mathcal{C}$ that has a coequalizer of the identity morphism $\text{id}_X$ and $f$, the coequalizer projection $\pi : X \to \text{coequalizer}(\text{id}_X, f)$ is a split epimorphism. This means there exists a section (right inverse) for $\pi$.

Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Main definitions

Main statements

Implementation notes

References