Retracts

Defines retracts of objects and morphisms.

structure CategoryTheory.Retract {C : Type u} [CategoryTheory.Category.{v, u} C] (X Y : C) : Type v

An object X is a retract of Y if there are morphisms i : X ⟶ Y and r : Y ⟶ X such that i ≫ r = 𝟙 X.

• i : X ⟶ Y

  the split monomorphism

• r : Y ⟶ X

  the split epimorphism

• retract : CategoryTheory.CategoryStruct.comp self.i self.r = CategoryTheory.CategoryStruct.id X

@[simp]

theorem CategoryTheory.Retract.retract_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (self : CategoryTheory.Retract X Y) {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp self.i (CategoryTheory.CategoryStruct.comp self.r h) = h

def CategoryTheory.Retract.map {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {X Y : C} (h : CategoryTheory.Retract X Y) (F : CategoryTheory.Functor C D) : CategoryTheory.Retract (F.obj X) (F.obj Y)

If X is a retract of Y, then F.obj X is a retract of F.obj Y.

Equations

• h.map F = { i := F.map h.i, r := F.map h.r, retract := ⋯ }

@[simp]

theorem CategoryTheory.Retract.map_i {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {X Y : C} (h : CategoryTheory.Retract X Y) (F : CategoryTheory.Functor C D) : (h.map F).i = F.map h.i

@[simp]

theorem CategoryTheory.Retract.map_r {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {X Y : C} (h : CategoryTheory.Retract X Y) (F : CategoryTheory.Functor C D) : (h.map F).r = F.map h.r

def CategoryTheory.Retract.splitEpi {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (h : CategoryTheory.Retract X Y) : CategoryTheory.SplitEpi h.r

a retract determines a split epimorphism.

Equations

• h.splitEpi = { section_ := h.i, id := ⋯ }

@[simp]

theorem CategoryTheory.Retract.splitEpi_section_ {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (h : CategoryTheory.Retract X Y) : h.splitEpi.section_ = h.i

def CategoryTheory.Retract.splitMono {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (h : CategoryTheory.Retract X Y) : CategoryTheory.SplitMono h.i

a retract determines a split monomorphism.

Equations

• h.splitMono = { retraction := h.r, id := ⋯ }

@[simp]

theorem CategoryTheory.Retract.splitMono_retraction {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (h : CategoryTheory.Retract X Y) : h.splitMono.retraction = h.r

instance CategoryTheory.Retract.instIsSplitEpiR {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (h : CategoryTheory.Retract X Y) : CategoryTheory.IsSplitEpi h.r

instance CategoryTheory.Retract.instIsSplitMonoI {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (h : CategoryTheory.Retract X Y) : CategoryTheory.IsSplitMono h.i

@[reducible, inline]

abbrev CategoryTheory.RetractArrow {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z W : C} (f : X ⟶ Y) (g : Z ⟶ W) : Type v

  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.

Equations

• CategoryTheory.RetractArrow f g = CategoryTheory.Retract (CategoryTheory.Arrow.mk f) (CategoryTheory.Arrow.mk g)

theorem CategoryTheory.RetractArrow.i_w {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : CategoryTheory.RetractArrow f g) : CategoryTheory.CategoryStruct.comp h.i.left g = CategoryTheory.CategoryStruct.comp f h.i.right

theorem CategoryTheory.RetractArrow.i_w_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : CategoryTheory.RetractArrow f g) {Z✝ : C} (h✝ : W ⟶ Z✝) : CategoryTheory.CategoryStruct.comp h.i.left (CategoryTheory.CategoryStruct.comp g h✝) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp h.i.right h✝)

theorem CategoryTheory.RetractArrow.r_w {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : CategoryTheory.RetractArrow f g) : CategoryTheory.CategoryStruct.comp h.r.left f = CategoryTheory.CategoryStruct.comp g h.r.right

theorem CategoryTheory.RetractArrow.r_w_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : CategoryTheory.RetractArrow f g) {Z✝ : C} (h✝ : Y ⟶ Z✝) : CategoryTheory.CategoryStruct.comp h.r.left (CategoryTheory.CategoryStruct.comp f h✝) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp h.r.right h✝)

def CategoryTheory.RetractArrow.left {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : CategoryTheory.RetractArrow f g) : CategoryTheory.Retract X Z

The top of a retract diagram of morphisms determines a retract of objects.

Equations

• h.left = CategoryTheory.Retract.map h CategoryTheory.Arrow.leftFunc

@[simp]

theorem CategoryTheory.RetractArrow.left_i {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : CategoryTheory.RetractArrow f g) : h.left.i = h.i.left

@[simp]

theorem CategoryTheory.RetractArrow.left_r {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : CategoryTheory.RetractArrow f g) : h.left.r = h.r.left

def CategoryTheory.RetractArrow.right {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : CategoryTheory.RetractArrow f g) : CategoryTheory.Retract Y W

The bottom of a retract diagram of morphisms determines a retract of objects.

Equations

• h.right = CategoryTheory.Retract.map h CategoryTheory.Arrow.rightFunc

@[simp]

theorem CategoryTheory.RetractArrow.right_i {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : CategoryTheory.RetractArrow f g) : h.right.i = h.i.right

@[simp]

theorem CategoryTheory.RetractArrow.right_r {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : CategoryTheory.RetractArrow f g) : h.right.r = h.r.right

@[simp]

theorem CategoryTheory.RetractArrow.retract_left {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : CategoryTheory.RetractArrow f g) : CategoryTheory.CategoryStruct.comp h.i.left h.r.left = CategoryTheory.CategoryStruct.id X

@[simp]

theorem CategoryTheory.RetractArrow.retract_left_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : CategoryTheory.RetractArrow f g) {Z✝ : C} (h✝ : (CategoryTheory.Arrow.mk f).left ⟶ Z✝) : CategoryTheory.CategoryStruct.comp h.i.left (CategoryTheory.CategoryStruct.comp h.r.left h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id X) h✝

@[simp]

theorem CategoryTheory.RetractArrow.retract_right {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : CategoryTheory.RetractArrow f g) : CategoryTheory.CategoryStruct.comp h.i.right h.r.right = CategoryTheory.CategoryStruct.id Y

@[simp]

theorem CategoryTheory.RetractArrow.retract_right_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : CategoryTheory.RetractArrow f g) {Z✝ : C} (h✝ : (CategoryTheory.Arrow.mk f).right ⟶ Z✝) : CategoryTheory.CategoryStruct.comp h.i.right (CategoryTheory.CategoryStruct.comp h.r.right h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id Y) h✝

instance CategoryTheory.RetractArrow.instIsSplitEpiLeftRArrow {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : CategoryTheory.RetractArrow f g) : CategoryTheory.IsSplitEpi h.r.left

instance CategoryTheory.RetractArrow.instIsSplitEpiRightRArrow {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : CategoryTheory.RetractArrow f g) : CategoryTheory.IsSplitEpi h.r.right

instance CategoryTheory.RetractArrow.instIsSplitMonoLeftIArrow {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : CategoryTheory.RetractArrow f g) : CategoryTheory.IsSplitMono h.i.left

instance CategoryTheory.RetractArrow.instIsSplitMonoRightIArrow {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : CategoryTheory.RetractArrow f g) : CategoryTheory.IsSplitMono h.i.right