Mathlib.CategoryTheory.Retract

CategoryTheory.Retract structure

(X Y : C)

Full source

/-- An object `X` is a retract of `Y` if there are morphisms `i : X ⟶ Y` and `r : Y ⟶ X` such
that `i ≫ r = 𝟙 X`. -/
structure Retract (X Y : C) where
  /-- the split monomorphism -/
  i : X ⟶ Y
  /-- the split epimorphism -/
  r : Y ⟶ X
  retract : i ≫ r = 𝟙 X := by aesop_cat

Retract in a category

Informal description

An object $X$ is a retract of an object $Y$ in a category $\mathcal{C}$ if there exist morphisms $i \colon X \to Y$ and $r \colon Y \to X$ such that their composition $i \circ r$ is the identity morphism on $X$.

CategoryTheory.Retract.map definition

(F : C ⥤ D) : Retract (F.obj X) (F.obj Y)

Full source

/-- If `X` is a retract of `Y`, then `F.obj X` is a retract of `F.obj Y`. -/
@[simps]
def map (F : C ⥤ D) : Retract (F.obj X) (F.obj Y) where
  i := F.map h.i
  r := F.map h.r
  retract := by rw [← F.map_comp h.i h.r, h.retract, F.map_id]

Retract under a functor

Informal description

Given a functor $ F \colon \mathcal{C} \to \mathcal{D} $ and a retract $ h $ between objects $ X $ and $ Y $ in $ \mathcal{C} $, the image of $ X $ under $ F $ is a retract of the image of $ Y $ under $ F $ in $ \mathcal{D} $. Specifically, the morphisms $ F(h.i) \colon F(X) \to F(Y) $ and $ F(h.r) \colon F(Y) \to F(X) $ satisfy $ F(h.i) \circ F(h.r) = \text{id}_{F(X)} $.

CategoryTheory.Retract.splitEpi definition

: SplitEpi h.r

Full source

/-- a retract determines a split epimorphism. -/
@[simps] def splitEpi : SplitEpi h.r where
  section_ := h.i

Split epimorphism from a retract

Informal description

Given a retract $h$ in a category $\mathcal{C}$, the morphism $r \colon Y \to X$ associated with the retract is a split epimorphism, meaning there exists a section $i \colon X \to Y$ such that $r \circ i = \text{id}_X$.

CategoryTheory.Retract.splitMono definition

: SplitMono h.i

Full source

/-- a retract determines a split monomorphism. -/
@[simps] def splitMono : SplitMono h.i where
  retraction := h.r

Split monomorphism from a retract

Informal description

Given a retract $h$ in a category $\mathcal{C}$, the morphism $i \colon X \to Y$ associated with the retract is a split monomorphism, meaning there exists a retraction $r \colon Y \to X$ such that $r \circ i = \text{id}_X$.

CategoryTheory.Retract.instIsSplitEpiR instance

: IsSplitEpi h.r

Full source

instance : IsSplitEpi h.r := ⟨⟨h.splitEpi⟩⟩

Retraction Morphism of a Retract is a Split Epimorphism

Informal description

For any retract $h$ in a category $\mathcal{C}$, the retraction morphism $r \colon Y \to X$ is a split epimorphism.

CategoryTheory.Retract.instIsSplitMonoI instance

: IsSplitMono h.i

Full source

instance : IsSplitMono h.i := ⟨⟨h.splitMono⟩⟩

Inclusion Morphism of a Retract is a Split Monomorphism

Informal description

For any retract $h$ in a category $\mathcal{C}$, the inclusion morphism $i \colon X \to Y$ is a split monomorphism.

CategoryTheory.Retract.refl definition

: Retract X X

Full source

/-- Any object is a retract of itself. -/
@[simps]
def refl : Retract X X where
  i := 𝟙 X
  r := 𝟙 X

Reflexivity of retracts

Informal description

For any object $X$ in a category $\mathcal{C}$, $X$ is a retract of itself, with the inclusion and retraction morphisms both given by the identity morphism $\mathrm{id}_X \colon X \to X$.

CategoryTheory.Retract.trans definition

{Z : C} (h' : Retract Y Z) : Retract X Z

Full source

/-- A retract of a retract is a retract. -/
@[simps]
def trans {Z : C} (h' : Retract Y Z) : Retract X Z where
  i := h.i ≫ h'.i
  r := h'.r ≫ h.r

Transitivity of Retracts in a Category

Informal description

Given objects $X$, $Y$, and $Z$ in a category $\mathcal{C}$, if $X$ is a retract of $Y$ and $Y$ is a retract of $Z$, then $X$ is a retract of $Z$. Specifically, the inclusion morphism $i \colon X \to Z$ is given by the composition $i_X \circ i_Y$, and the retraction morphism $r \colon Z \to X$ is given by the composition $r_Y \circ r_X$, where $i_X \colon X \to Y$, $r_X \colon Y \to X$, $i_Y \colon Y \to Z$, and $r_Y \colon Z \to Y$ are the respective inclusion and retraction morphisms.

CategoryTheory.Retract.ofIso definition

(e : X ≅ Y) : Retract X Y

Full source

/-- If `e : X ≅ Y`, then `X` is a retract of `Y`. -/
def ofIso (e : X ≅ Y) : Retract X Y where
  i := e.hom
  r := e.inv

Retract via isomorphism

Informal description

Given an isomorphism $e \colon X \cong Y$ in a category $\mathcal{C}$, the object $X$ is a retract of $Y$. Specifically, the inclusion morphism is given by the homomorphism $e_{\text{hom}} \colon X \to Y$ of the isomorphism, and the retraction morphism is given by the inverse $e_{\text{inv}} \colon Y \to X$ of the isomorphism.

CategoryTheory.RetractArrow abbrev

{X Y Z W : C} (f : X ⟶ Y) (g : Z ⟶ W)

Full source

/--
```
  X -------> Z -------> X
  |          |          |
  f          g          f
  |          |          |
  v          v          v
  Y -------> W -------> Y

```
A morphism `f : X ⟶ Y` is a retract of `g : Z ⟶ W` if there are morphisms `i : f ⟶ g`
and `r : g ⟶ f` in the arrow category such that `i ≫ r = 𝟙 f`. -/
abbrev RetractArrow {X Y Z W : C} (f : X ⟶ Y) (g : Z ⟶ W) := Retract (Arrow.mk f) (Arrow.mk g)

Retract of Morphisms in a Category

Informal description

A morphism $f \colon X \to Y$ is called a retract of a morphism $g \colon Z \to W$ in a category $\mathcal{C}$ if there exist morphisms $i \colon f \to g$ and $r \colon g \to f$ in the arrow category such that their composition satisfies $i \circ r = \mathrm{id}_f$. Here, the diagram commutes as follows: ``` X -------> Z -------> X | | | f g f | | | v v v Y -------> W -------> Y ```

CategoryTheory.RetractArrow.i_w theorem

: h.i.left ≫ g = f ≫ h.i.right

Full source

@[reassoc]
lemma i_w : h.i.left ≫ g = f ≫ h.i.right := h.i.w

Commutativity of Inclusion Components in a Retract of Morphisms

Informal description

Given a retract of morphisms $h$ from $f \colon X \to Y$ to $g \colon Z \to W$ in a category $\mathcal{C}$, the left component of the inclusion morphism $i$ satisfies the commutativity condition $i_{\text{left}} \circ g = f \circ i_{\text{right}}$, where $i_{\text{left}} \colon X \to Z$ and $i_{\text{right}} \colon Y \to W$ are the components of $i$.

CategoryTheory.RetractArrow.r_w theorem

: h.r.left ≫ f = g ≫ h.r.right

Full source

@[reassoc]
lemma r_w : h.r.left ≫ f = g ≫ h.r.right := h.r.w

Commutativity of Retraction Components in a Retract of Morphisms

Informal description

Given a retract of morphisms $h$ from $f \colon X \to Y$ to $g \colon Z \to W$ in a category $\mathcal{C}$, the left component of the retraction morphism $r$ satisfies the commutativity condition $r_{\text{left}} \circ f = g \circ r_{\text{right}}$, where $r_{\text{left}} \colon Z \to X$ and $r_{\text{right}} \colon W \to Y$ are the components of $r$.

CategoryTheory.RetractArrow.left definition

: Retract X Z

Full source

/-- The top of a retract diagram of morphisms determines a retract of objects. -/
@[simps!]
def left : Retract X Z := h.map Arrow.leftFunc

Retract of domain objects in a retract of morphisms

Informal description

Given a retract of morphisms $h$ from $f \colon X \to Y$ to $g \colon Z \to W$ in a category $\mathcal{C}$, the object $X$ is a retract of the object $Z$ via the left component of the retract diagram.

CategoryTheory.RetractArrow.right definition

: Retract Y W

Full source

/-- The bottom of a retract diagram of morphisms determines a retract of objects. -/
@[simps!]
def right : Retract Y W := h.map Arrow.rightFunc

Retract of codomain objects in a retract of morphisms

Informal description

Given a retract of morphisms $h$ from $f \colon X \to Y$ to $g \colon Z \to W$ in a category $\mathcal{C}$, the object $Y$ is a retract of the object $W$ via the right component of the retract diagram.

CategoryTheory.RetractArrow.retract_left theorem

: h.i.left ≫ h.r.left = 𝟙 X

Full source

@[reassoc (attr := simp)]
lemma retract_left : h.i.left ≫ h.r.left = 𝟙 X := h.left.retract

Left Retract Composition Yields Identity on Domain

Informal description

Given a retract of morphisms $h$ from $f \colon X \to Y$ to $g \colon Z \to W$ in a category $\mathcal{C}$, the composition of the left inclusion and left retraction morphisms equals the identity morphism on $X$, i.e., $h.i.left \circ h.r.left = \mathrm{id}_X$.

CategoryTheory.RetractArrow.retract_right theorem

: h.i.right ≫ h.r.right = 𝟙 Y

Full source

@[reassoc (attr := simp)]
lemma retract_right : h.i.right ≫ h.r.right = 𝟙 Y := h.right.retract

Right Retract Composition Yields Identity on Codomain

Informal description

Given a retract of morphisms $h$ from $f \colon X \to Y$ to $g \colon Z \to W$ in a category $\mathcal{C}$, the composition of the right inclusion and right retraction morphisms equals the identity morphism on $Y$, i.e., $h.i.right \circ h.r.right = \mathrm{id}_Y$.

CategoryTheory.RetractArrow.instIsSplitEpiLeftRArrow instance

: IsSplitEpi h.r.left

Full source

instance : IsSplitEpi h.r.left := ⟨⟨h.left.splitEpi⟩⟩

Split Epimorphism Property of the Left Retraction in a Retract of Morphisms

Informal description

Given a retract of morphisms $h$ from $f \colon X \to Y$ to $g \colon Z \to W$ in a category $\mathcal{C}$, the left component $h.r.left \colon Z \to X$ of the retraction morphism is a split epimorphism.

CategoryTheory.RetractArrow.instIsSplitEpiRightRArrow instance

: IsSplitEpi h.r.right

Full source

instance : IsSplitEpi h.r.right := ⟨⟨h.right.splitEpi⟩⟩

Split Epimorphism Property of the Right Retraction in a Retract of Morphisms

Informal description

Given a retract of morphisms $h$ from $f \colon X \to Y$ to $g \colon Z \to W$ in a category $\mathcal{C}$, the right component $h.r.right \colon W \to Y$ of the retraction morphism is a split epimorphism.

CategoryTheory.RetractArrow.instIsSplitMonoLeftIArrow instance

: IsSplitMono h.i.left

Full source

instance : IsSplitMono h.i.left := ⟨⟨h.left.splitMono⟩⟩

Split Monomorphism Property of the Left Inclusion in a Retract of Morphisms

Informal description

Given a retract of morphisms $h$ from $f \colon X \to Y$ to $g \colon Z \to W$ in a category $\mathcal{C}$, the left component $h.i.left \colon X \to Z$ of the inclusion morphism is a split monomorphism.

CategoryTheory.RetractArrow.instIsSplitMonoRightIArrow instance

: IsSplitMono h.i.right

Full source

instance : IsSplitMono h.i.right := ⟨⟨h.right.splitMono⟩⟩

Split Monomorphism Property of the Right Inclusion in a Retract of Morphisms

Informal description

Given a retract of morphisms $h$ from $f \colon X \to Y$ to $g \colon Z \to W$ in a category $\mathcal{C}$, the right component $h.i.right \colon Y \to W$ of the inclusion morphism is a split monomorphism.

CategoryTheory.Iso.retract definition

{X Y : C} (e : X ≅ Y) : Retract X Y

Full source

/-- If `X` is isomorphic to `Y`, then `X` is a retract of `Y`. -/
@[simps]
def retract {X Y : C} (e : X ≅ Y) : Retract X Y where
  i := e.hom
  r := e.inv

Retract via isomorphism

Informal description

Given an isomorphism $e \colon X \cong Y$ in a category $\mathcal{C}$, the object $X$ is a retract of $Y$ via the morphisms $e_{\text{hom}} \colon X \to Y$ and $e_{\text{inv}} \colon Y \to X$.