Retract

📁 Source: Mathlib/CategoryTheory/Retract.lean

Statistics

Metric	Count
Definitions retract, retractArrowApp, Retract, i, map, ofIso, op, r, refl, splitEpi, splitMono, trans, RetractArrow, left, map, op, right, unop	18
Theorems retract_i, retract_r, retractArrowApp_i, retractArrowApp_r, instIsSplitEpiR, instIsSplitMonoI, map_i, map_r, op_i, op_r, refl_i, refl_r, retract, retract_assoc, splitEpi_section_, splitMono_retraction, trans_i, trans_r, i_w, i_w_assoc, instIsSplitEpiLeftRArrow, instIsSplitEpiRightRArrow, instIsSplitMonoLeftIArrow, instIsSplitMonoRightIArrow, left_i, left_r, map_i_left, map_i_right, map_r_left, map_r_right, op_i_left, op_i_right, op_r_left, op_r_right, r_w, r_w_assoc, retract_left, retract_left_assoc, retract_right, retract_right_assoc, right_i, right_r, unop_i_left, unop_i_right, unop_r_left, unop_r_right	46
Total	64

CategoryTheory

Definitions

Name	Category	Theorems
Retract 📖	CompData	1 math math: ObjectProperty.prop_retractClosure_iff
RetractArrow 📖	CompOp	—

CategoryTheory.Iso

Definitions

Name	Category	Theorems
retract 📖	CompOp	2 math math: retract_r, retract_i

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
retract_i 📖	mathematical	—	CategoryTheory.Retract.i retract hom	—	—
retract_r 📖	mathematical	—	CategoryTheory.Retract.r retract inv	—	—

CategoryTheory.NatTrans

Definitions

Name	Category	Theorems
retractArrowApp 📖	CompOp	2 math math: retractArrowApp_r, retractArrowApp_i

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
retractArrowApp_i 📖	mathematical	—	CategoryTheory.Retract.i CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.obj app retractArrowApp CategoryTheory.Arrow.homMk CategoryTheory.Functor.map	—	—
retractArrowApp_r 📖	mathematical	—	CategoryTheory.Retract.r CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.obj app retractArrowApp CategoryTheory.Arrow.homMk CategoryTheory.Functor.map	—	—

CategoryTheory.Retract

Definitions

Name	Category	Theorems
i 📖	CompOp	34 math math: refl_i, CategoryTheory.RetractArrow.retract_left_assoc, op_i, splitEpi_section_, retract, CategoryTheory.RetractArrow.i_w, splitMono_retraction, CategoryTheory.RetractArrow.op_r_right, CategoryTheory.Iso.retract_i, CategoryTheory.RetractArrow.right_i, CategoryTheory.RetractArrow.retract_left, CategoryTheory.RetractArrow.retract_right_assoc, CategoryTheory.RetractArrow.op_i_right, CategoryTheory.RetractArrow.retract_right, CategoryTheory.RetractArrow.unop_r_right, CategoryTheory.Idempotents.Karoubi.retract_i_f, instIsSplitMonoI, CategoryTheory.RetractArrow.map_i_left, CategoryTheory.RetractArrow.op_r_left, CategoryTheory.RetractArrow.op_i_left, CategoryTheory.RetractArrow.map_i_right, CategoryTheory.RetractArrow.instIsSplitMonoRightIArrow, AlgebraicGeometry.instIsClosedImmersionISchemeOfSubsingletonCarrierCarrierCommRingCat, CategoryTheory.RetractArrow.unop_i_left, CategoryTheory.RetractArrow.unop_i_right, CategoryTheory.RetractArrow.left_i, retract_assoc, CategoryTheory.RetractArrow.i_w_assoc, CategoryTheory.RetractArrow.unop_r_left, CategoryTheory.RetractArrow.instIsSplitMonoLeftIArrow, map_i, op_r, CategoryTheory.NatTrans.retractArrowApp_i, trans_i
map 📖	CompOp	2 math math: map_r, map_i
ofIso 📖	CompOp	—
op 📖	CompOp	2 math math: op_i, op_r
r 📖	CompOp	33 math math: refl_r, CategoryTheory.RetractArrow.right_r, CategoryTheory.RetractArrow.retract_left_assoc, CategoryTheory.RetractArrow.left_r, op_i, splitEpi_section_, CategoryTheory.RetractArrow.r_w_assoc, retract, CategoryTheory.RetractArrow.map_r_right, splitMono_retraction, CategoryTheory.Idempotents.Karoubi.retract_r_f, CategoryTheory.RetractArrow.op_r_right, CategoryTheory.Iso.retract_r, CategoryTheory.RetractArrow.r_w, CategoryTheory.RetractArrow.retract_left, map_r, CategoryTheory.RetractArrow.retract_right_assoc, CategoryTheory.RetractArrow.op_i_right, CategoryTheory.RetractArrow.retract_right, CategoryTheory.RetractArrow.map_r_left, CategoryTheory.RetractArrow.unop_r_right, CategoryTheory.NatTrans.retractArrowApp_r, instIsSplitEpiR, CategoryTheory.RetractArrow.instIsSplitEpiRightRArrow, CategoryTheory.RetractArrow.op_r_left, trans_r, CategoryTheory.RetractArrow.op_i_left, CategoryTheory.RetractArrow.unop_i_left, CategoryTheory.RetractArrow.unop_i_right, retract_assoc, CategoryTheory.RetractArrow.instIsSplitEpiLeftRArrow, CategoryTheory.RetractArrow.unop_r_left, op_r
refl 📖	CompOp	2 math math: refl_r, refl_i
splitEpi 📖	CompOp	1 math math: splitEpi_section_
splitMono 📖	CompOp	1 math math: splitMono_retraction
trans 📖	CompOp	2 math math: trans_r, trans_i

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsSplitEpiR 📖	mathematical	—	CategoryTheory.IsSplitEpi r	—	—
instIsSplitMonoI 📖	mathematical	—	CategoryTheory.IsSplitMono i	—	—
map_i 📖	mathematical	—	i CategoryTheory.Functor.obj map CategoryTheory.Functor.map	—	—
map_r 📖	mathematical	—	r CategoryTheory.Functor.obj map CategoryTheory.Functor.map	—	—
op_i 📖	mathematical	—	i Opposite CategoryTheory.Category.opposite Opposite.op op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct r	—	—
op_r 📖	mathematical	—	r Opposite CategoryTheory.Category.opposite Opposite.op op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct i	—	—
refl_i 📖	mathematical	—	i refl CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
refl_r 📖	mathematical	—	r refl CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
retract 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct i r CategoryTheory.CategoryStruct.id	—	—
retract_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct i r	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' retract
splitEpi_section_ 📖	mathematical	—	CategoryTheory.SplitEpi.section_ r splitEpi i	—	—
splitMono_retraction 📖	mathematical	—	CategoryTheory.SplitMono.retraction i splitMono r	—	—
trans_i 📖	mathematical	—	i trans CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
trans_r 📖	mathematical	—	r trans CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—

CategoryTheory.RetractArrow

Definitions

Name	Category	Theorems
left 📖	CompOp	2 math math: left_r, left_i
map 📖	CompOp	4 math math: map_r_right, map_r_left, map_i_left, map_i_right
op 📖	CompOp	4 math math: op_r_right, op_i_right, op_r_left, op_i_left
right 📖	CompOp	2 math math: right_r, right_i
unop 📖	CompOp	4 math math: unop_r_right, unop_i_left, unop_i_right, unop_r_left

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
i_w 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.CommaMorphism.left CategoryTheory.Retract.i CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Comma.right CategoryTheory.CommaMorphism.right	—	CategoryTheory.CommaMorphism.w
i_w_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.CommaMorphism.left CategoryTheory.Retract.i CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.CommaMorphism.right	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' i_w
instIsSplitEpiLeftRArrow 📖	mathematical	—	CategoryTheory.IsSplitEpi CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.CommaMorphism.left CategoryTheory.Retract.r CategoryTheory.Arrow CategoryTheory.instCategoryArrow	—	—
instIsSplitEpiRightRArrow 📖	mathematical	—	CategoryTheory.IsSplitEpi CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.CommaMorphism.right CategoryTheory.Retract.r CategoryTheory.Arrow CategoryTheory.instCategoryArrow	—	—
instIsSplitMonoLeftIArrow 📖	mathematical	—	CategoryTheory.IsSplitMono CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.CommaMorphism.left CategoryTheory.Retract.i CategoryTheory.Arrow CategoryTheory.instCategoryArrow	—	—
instIsSplitMonoRightIArrow 📖	mathematical	—	CategoryTheory.IsSplitMono CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.CommaMorphism.right CategoryTheory.Retract.i CategoryTheory.Arrow CategoryTheory.instCategoryArrow	—	—
left_i 📖	mathematical	—	CategoryTheory.Retract.i left CategoryTheory.CommaMorphism.left CategoryTheory.Functor.id CategoryTheory.Arrow CategoryTheory.instCategoryArrow	—	—
left_r 📖	mathematical	—	CategoryTheory.Retract.r left CategoryTheory.CommaMorphism.left CategoryTheory.Functor.id CategoryTheory.Arrow CategoryTheory.instCategoryArrow	—	—
map_i_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.mapArrow CategoryTheory.Retract.i CategoryTheory.Functor.map map	—	—
map_i_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.mapArrow CategoryTheory.Retract.i CategoryTheory.Functor.map map	—	—
map_r_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.mapArrow CategoryTheory.Retract.r CategoryTheory.Functor.map map	—	—
map_r_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.mapArrow CategoryTheory.Retract.r CategoryTheory.Functor.map map	—	—
op_i_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.id Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Retract.i CategoryTheory.Arrow CategoryTheory.instCategoryArrow op CategoryTheory.Comma.right CategoryTheory.CommaMorphism.right CategoryTheory.Retract.r	—	—
op_i_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.id Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Retract.i CategoryTheory.Arrow CategoryTheory.instCategoryArrow op CategoryTheory.Comma.left CategoryTheory.CommaMorphism.left CategoryTheory.Retract.r	—	—
op_r_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.id Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Retract.r CategoryTheory.Arrow CategoryTheory.instCategoryArrow op CategoryTheory.Comma.right CategoryTheory.CommaMorphism.right CategoryTheory.Retract.i	—	—
op_r_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.id Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Retract.r CategoryTheory.Arrow CategoryTheory.instCategoryArrow op CategoryTheory.Comma.left CategoryTheory.CommaMorphism.left CategoryTheory.Retract.i	—	—
r_w 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.CommaMorphism.left CategoryTheory.Retract.r CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Comma.right CategoryTheory.CommaMorphism.right	—	CategoryTheory.CommaMorphism.w
r_w_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.CommaMorphism.left CategoryTheory.Retract.r CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.CommaMorphism.right	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' r_w
retract_left 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.CommaMorphism.left CategoryTheory.Retract.i CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Retract.r CategoryTheory.CategoryStruct.id	—	CategoryTheory.Retract.retract
retract_left_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.CommaMorphism.left CategoryTheory.Retract.i CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Retract.r CategoryTheory.CategoryStruct.id	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' retract_left
retract_right 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.CommaMorphism.right CategoryTheory.Retract.i CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Retract.r CategoryTheory.CategoryStruct.id	—	CategoryTheory.Retract.retract
retract_right_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.CommaMorphism.right CategoryTheory.Retract.i CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Retract.r CategoryTheory.CategoryStruct.id	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' retract_right
right_i 📖	mathematical	—	CategoryTheory.Retract.i right CategoryTheory.CommaMorphism.right CategoryTheory.Functor.id CategoryTheory.Arrow CategoryTheory.instCategoryArrow	—	—
right_r 📖	mathematical	—	CategoryTheory.Retract.r right CategoryTheory.CommaMorphism.right CategoryTheory.Functor.id CategoryTheory.Arrow CategoryTheory.instCategoryArrow	—	—
unop_i_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Functor.id Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Retract.i CategoryTheory.Arrow CategoryTheory.instCategoryArrow unop CategoryTheory.Comma.right Opposite CategoryTheory.Category.opposite CategoryTheory.CommaMorphism.right CategoryTheory.Retract.r	—	—
unop_i_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Functor.id Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Retract.i CategoryTheory.Arrow CategoryTheory.instCategoryArrow unop CategoryTheory.Comma.left Opposite CategoryTheory.Category.opposite CategoryTheory.CommaMorphism.left CategoryTheory.Retract.r	—	—
unop_r_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Functor.id Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Retract.r CategoryTheory.Arrow CategoryTheory.instCategoryArrow unop CategoryTheory.Comma.right Opposite CategoryTheory.Category.opposite CategoryTheory.CommaMorphism.right CategoryTheory.Retract.i	—	—
unop_r_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Functor.id Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Retract.r CategoryTheory.Arrow CategoryTheory.instCategoryArrow unop CategoryTheory.Comma.left Opposite CategoryTheory.Category.opposite CategoryTheory.CommaMorphism.left CategoryTheory.Retract.i	—	—

---

← Back to Index