Retracts #

Defines retracts of objects and morphisms.

source

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

Instances For

source

@[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

source

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

Retract (Opposite.op X) (Opposite.op Y)

Retracts are preserved when passing to the opposite category.

Equations

h.op = { i := h.r.op, r := h.i.op, retract := ⋯ }

Instances For

source

@[simp]

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

h.op.i = h.r.op

source

@[simp]

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

h.op.r = h.i.op

source

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 := ⋯ }

Instances For

source

@[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

source

@[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

source

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 := ⋯ }

Instances For

source

@[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

source

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 := ⋯ }

Instances For

source

@[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

source

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

IsSplitEpi h.r

source

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

IsSplitMono h.i

source

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 := ⋯ }

Instances For

source

@[simp]

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

(refl X).i = CategoryStruct.id X

source

@[simp]

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

(refl X).r = CategoryStruct.id X

source

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 := ⋯ }

Instances For

source

@[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

source

@[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

source

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

Retract X Y

If e : X ≅ Y, then X is a retract of Y.

Equations

CategoryTheory.Retract.ofIso e = { i := e.hom, r := e.inv, retract := ⋯ }

Instances For

source

@[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)

Instances For

source

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

source

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✝)

source

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

source

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✝)

source

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

Instances For

source

@[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

source

@[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

source

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

Instances For

source

@[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

source

@[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

source

@[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

source

@[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✝

source

@[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

source

@[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✝

source

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

source

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

source

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

source

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

source

def CategoryTheory.RetractArrow.map {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g) (F : Functor C D) :

RetractArrow (F.map f) (F.map g)

If a morphism f is a retract of g, then F.map f is a retract of F.map g for any functor F.

Equations

h.map F = CategoryTheory.Retract.map h F.mapArrow

Instances For

source

@[simp]

theorem CategoryTheory.RetractArrow.map_i_left {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g) (F : Functor C D) :

(h.map F).i.left = F.map h.i.left

source

@[simp]

theorem CategoryTheory.RetractArrow.map_i_right {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g) (F : Functor C D) :

(h.map F).i.right = F.map h.i.right

source

@[simp]

theorem CategoryTheory.RetractArrow.map_r_left {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g) (F : Functor C D) :

(h.map F).r.left = F.map h.r.left

source

@[simp]

theorem CategoryTheory.RetractArrow.map_r_right {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g) (F : Functor C D) :

(h.map F).r.right = F.map h.r.right

source

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

RetractArrow f.op g.op

If a morphism f is a retract of g, then f.op is a retract of g.op.

Equations

h.op = { i := { left := h.r.right.op, right := h.r.left.op, w := ⋯ }, r := { left := h.i.right.op, right := h.i.left.op, w := ⋯ }, retract := ⋯ }

Instances For

source

@[simp]

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

h.op.i.left = h.r.right.op

source

@[simp]

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

h.op.r.right = h.i.left.op

source

@[simp]

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

h.op.i.right = h.r.left.op

source

@[simp]

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

h.op.r.left = h.i.right.op

source

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

RetractArrow f.unop g.unop

If a morphism f in the opposite category is a retract of g, then f.unop is a retract of g.unop.

Equations

h.unop = { i := { left := h.r.right.unop, right := h.r.left.unop, w := ⋯ }, r := { left := h.i.right.unop, right := h.i.left.unop, w := ⋯ }, retract := ⋯ }

Instances For

source

@[simp]

theorem CategoryTheory.RetractArrow.unop_r_right {C : Type u} [Category.{v, u} C] {X Y Z W : Cᵒᵖ} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g) :

h.unop.r.right = h.i.left.unop

source

@[simp]

theorem CategoryTheory.RetractArrow.unop_i_left {C : Type u} [Category.{v, u} C] {X Y Z W : Cᵒᵖ} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g) :

h.unop.i.left = h.r.right.unop

source

@[simp]

theorem CategoryTheory.RetractArrow.unop_i_right {C : Type u} [Category.{v, u} C] {X Y Z W : Cᵒᵖ} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g) :

h.unop.i.right = h.r.left.unop

source

@[simp]

theorem CategoryTheory.RetractArrow.unop_r_left {C : Type u} [Category.{v, u} C] {X Y Z W : Cᵒᵖ} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g) :

h.unop.r.left = h.i.right.unop

source

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 := ⋯ }

Instances For

source

@[simp]

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

e.retract.i = e.hom

source

@[simp]

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

e.retract.r = e.inv

source

def CategoryTheory.NatTrans.retractArrowApp {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {F G : Functor C D} (τ : F ⟶ G) {X Y : C} (h : Retract X Y) :

RetractArrow (τ.app X) (τ.app Y)

If X is a retract of Y, then for any natural transformation τ, the natural transformation τ.app X is a retract of τ.app Y.

Equations

CategoryTheory.NatTrans.retractArrowApp τ h = { i := CategoryTheory.Arrow.homMk (F.map h.i) (G.map h.i) ⋯, r := CategoryTheory.Arrow.homMk (F.map h.r) (G.map h.r) ⋯, retract := ⋯ }

Instances For

source

@[simp]

theorem CategoryTheory.NatTrans.retractArrowApp_r {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {F G : Functor C D} (τ : F ⟶ G) {X Y : C} (h : Retract X Y) :

(retractArrowApp τ h).r = Arrow.homMk (F.map h.r) (G.map h.r) ⋯

source

@[simp]

theorem CategoryTheory.NatTrans.retractArrowApp_i {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {F G : Functor C D} (τ : F ⟶ G) {X Y : C} (h : Retract X Y) :

(retractArrowApp τ h).i = Arrow.homMk (F.map h.i) (G.map h.i) ⋯

Documentation

Mathlib.CategoryTheory.Retract

Retracts #