Retracts

Defines retracts of objects and morphisms.

structure CategoryTheory.Retract {C : Type u} [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 : CategoryStruct.comp self.i self.r = CategoryStruct.id X

@[simp]

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

def CategoryTheory.Retract.map {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {X Y : C} (h : Retract X Y) (F : Functor C D) : 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} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {X Y : C} (h : Retract X Y) (F : Functor C D) : (h.map F).i = F.map h.i

@[simp]

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

def CategoryTheory.Retract.splitEpi {C : Type u} [Category.{v, u} C] {X Y : C} (h : Retract X Y) : 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} [Category.{v, u} C] {X Y : C} (h : Retract X Y) : h.splitEpi.section_ = h.i

def CategoryTheory.Retract.splitMono {C : Type u} [Category.{v, u} C] {X Y : C} (h : Retract X Y) : 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} [Category.{v, u} C] {X Y : C} (h : Retract X Y) : h.splitMono.retraction = h.r

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

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

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

Any object is a retract of itself.

Equations

• CategoryTheory.Retract.refl X = { i := CategoryTheory.CategoryStruct.id X, r := CategoryTheory.CategoryStruct.id X, retract := ⋯ }

@[simp]

theorem CategoryTheory.Retract.refl_i {C : Type u} [Category.{v, u} C] (X : C) : (refl X).i = CategoryStruct.id X

@[simp]

theorem CategoryTheory.Retract.refl_r {C : Type u} [Category.{v, u} C] (X : C) : (refl X).r = CategoryStruct.id X

def CategoryTheory.Retract.trans {C : Type u} [Category.{v, u} C] {X Y : C} (h : Retract X Y) {Z : C} (h' : Retract Y Z) : Retract X Z

A retract of a retract is a retract.

Equations

• h.trans h' = { i := CategoryTheory.CategoryStruct.comp h.i h'.i, r := CategoryTheory.CategoryStruct.comp h'.r h.r, retract := ⋯ }

@[simp]

theorem CategoryTheory.Retract.trans_i {C : Type u} [Category.{v, u} C] {X Y : C} (h : Retract X Y) {Z : C} (h' : Retract Y Z) : (h.trans h').i = CategoryStruct.comp h.i h'.i

@[simp]

theorem CategoryTheory.Retract.trans_r {C : Type u} [Category.{v, u} C] {X Y : C} (h : Retract X Y) {Z : C} (h' : Retract Y Z) : (h.trans h').r = CategoryStruct.comp h'.r h.r

@[reducible, inline]

abbrev CategoryTheory.RetractArrow {C : Type u} [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} [Category.{v, u} C] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g) : CategoryStruct.comp h.i.left g = CategoryStruct.comp f h.i.right

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

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

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

def CategoryTheory.RetractArrow.left {C : Type u} [Category.{v, u} C] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g) : 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_r {C : Type u} [Category.{v, u} C] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g) : h.left.r = h.r.left

@[simp]

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

def CategoryTheory.RetractArrow.right {C : Type u} [Category.{v, u} C] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g) : 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} [Category.{v, u} C] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g) : h.right.i = h.i.right

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

def CategoryTheory.Iso.retract {C : Type u} [Category.{v, u} C] {X Y : C} (e : X ≅ Y) : Retract X Y

If X is isomorphic to Y, then X is a retract of Y.

Equations

• e.retract = { i := e.hom, r := e.inv, retract := ⋯ }

@[simp]

theorem CategoryTheory.Iso.retract_i {C : Type u} [Category.{v, u} C] {X Y : C} (e : X ≅ Y) : e.retract.i = e.hom

@[simp]

theorem CategoryTheory.Iso.retract_r {C : Type u} [Category.{v, u} C] {X Y : C} (e : X ≅ Y) : e.retract.r = e.inv