Basic

📁 Source: Mathlib/CategoryTheory/Dialectica/Basic.lean

Statistics

Metric	Count
Definitions Dial, F, f, instCategory, isoMk, rel, src, tgt	8
Theorems ext, ext_iff, le, comp_F, comp_f, comp_le_lemma, hom_ext, hom_ext_iff, id_F, id_f, isoMk_hom_F, isoMk_hom_f, isoMk_inv_F, isoMk_inv_f	14
Total	22

CategoryTheory

Definitions

Name	Category	Theorems
Dial 📖	CompData	60 math math: Dial.braiding_inv_f, Dial.leftUnitor_naturality, Dial.tensorUnit_src, Dial.rightUnitor_hom_f, Dial.rightUnitor_naturality, Dial.rightUnitorImpl_inv_f, Dial.tensorHom_F, Dial.triangle, Dial.braiding_naturality_right, Dial.associator_hom_F, Dial.associatorImpl_inv_F, Dial.leftUnitor_hom_f, Dial.rightUnitor_hom_F, Dial.rightUnitorImpl_inv_F, Dial.whiskerRight_f, Dial.tensorObj_src, Dial.rightUnitorImpl_hom_F, Dial.leftUnitor_inv_f, Dial.hexagon_reverse, Dial.braiding_inv_F, Dial.associator_inv_f, Dial.braiding_hom_f, Dial.rightUnitor_inv_f, Dial.associatorImpl_hom_F, Dial.leftUnitor_hom_F, Dial.whiskerRight_F, Dial.hexagon_forward, Dial.tensorObj_tgt, Dial.associator_naturality, Dial.tensorUnit_rel, Dial.comp_F, Dial.isoMk_inv_F, Dial.associator_inv_F, Dial.isoMk_hom_f, Dial.tensorUnit_tgt, Dial.leftUnitorImpl_hom_F, Dial.pentagon, Dial.comp_f, Dial.id_f, Dial.isoMk_hom_F, Dial.symmetry, Dial.whiskerLeft_f, Dial.braiding_hom_F, Dial.leftUnitor_inv_F, Dial.associatorImpl_inv_f, Dial.tensorHom_f, Dial.whiskerLeft_F, Dial.associator_hom_f, Dial.leftUnitorImpl_inv_f, Dial.braiding_naturality_left, Dial.associatorImpl_hom_f, Dial.rightUnitor_inv_F, Dial.id_F, Dial.id_tensorHom_id, Dial.tensorHom_comp_tensorHom, Dial.isoMk_inv_f, Dial.leftUnitorImpl_hom_f, Dial.rightUnitorImpl_hom_f, Dial.leftUnitorImpl_inv_F, Dial.tensorObj_rel

CategoryTheory.Dial

Definitions

Name	Category	Theorems
instCategory 📖	CompOp	60 math math: braiding_inv_f, leftUnitor_naturality, tensorUnit_src, rightUnitor_hom_f, rightUnitor_naturality, rightUnitorImpl_inv_f, tensorHom_F, triangle, braiding_naturality_right, associator_hom_F, associatorImpl_inv_F, leftUnitor_hom_f, rightUnitor_hom_F, rightUnitorImpl_inv_F, whiskerRight_f, tensorObj_src, rightUnitorImpl_hom_F, leftUnitor_inv_f, hexagon_reverse, braiding_inv_F, associator_inv_f, braiding_hom_f, rightUnitor_inv_f, associatorImpl_hom_F, leftUnitor_hom_F, whiskerRight_F, hexagon_forward, tensorObj_tgt, associator_naturality, tensorUnit_rel, comp_F, isoMk_inv_F, associator_inv_F, isoMk_hom_f, tensorUnit_tgt, leftUnitorImpl_hom_F, pentagon, comp_f, id_f, isoMk_hom_F, symmetry, whiskerLeft_f, braiding_hom_F, leftUnitor_inv_F, associatorImpl_inv_f, tensorHom_f, whiskerLeft_F, associator_hom_f, leftUnitorImpl_inv_f, braiding_naturality_left, associatorImpl_hom_f, rightUnitor_inv_F, id_F, id_tensorHom_id, tensorHom_comp_tensorHom, isoMk_inv_f, leftUnitorImpl_hom_f, rightUnitorImpl_hom_f, leftUnitorImpl_inv_F, tensorObj_rel
isoMk 📖	CompOp	4 math math: isoMk_inv_F, isoMk_hom_f, isoMk_hom_F, isoMk_inv_f
rel 📖	CompOp	6 math math: tensorObjImpl_rel, comp_le_lemma, Hom.le, tensorUnit_rel, tensorUnitImpl_rel, tensorObj_rel
src 📖	CompOp	48 math math: braiding_inv_f, tensorObjImpl_rel, tensorUnit_src, rightUnitor_hom_f, rightUnitorImpl_inv_f, tensorHom_F, associator_hom_F, associatorImpl_inv_F, leftUnitor_hom_f, rightUnitor_hom_F, rightUnitorImpl_inv_F, comp_le_lemma, whiskerRight_f, tensorObj_src, rightUnitorImpl_hom_F, leftUnitor_inv_f, braiding_inv_F, associator_inv_f, braiding_hom_f, rightUnitor_inv_f, tensorUnitImpl_src, associatorImpl_hom_F, Hom.le, leftUnitor_hom_F, whiskerRight_F, tensorHomImpl_F, comp_F, associator_inv_F, leftUnitorImpl_hom_F, tensorObjImpl_src, comp_f, id_f, tensorHomImpl_f, whiskerLeft_f, braiding_hom_F, leftUnitor_inv_F, associatorImpl_inv_f, tensorHom_f, whiskerLeft_F, associator_hom_f, leftUnitorImpl_inv_f, associatorImpl_hom_f, rightUnitor_inv_F, id_F, leftUnitorImpl_hom_f, rightUnitorImpl_hom_f, leftUnitorImpl_inv_F, tensorObj_rel
tgt 📖	CompOp	28 math math: tensorObjImpl_rel, tensorHom_F, tensorObjImpl_tgt, associator_hom_F, associatorImpl_inv_F, rightUnitor_hom_F, rightUnitorImpl_inv_F, comp_le_lemma, rightUnitorImpl_hom_F, braiding_inv_F, associatorImpl_hom_F, Hom.le, leftUnitor_hom_F, whiskerRight_F, tensorObj_tgt, tensorHomImpl_F, comp_F, associator_inv_F, tensorUnit_tgt, leftUnitorImpl_hom_F, braiding_hom_F, leftUnitor_inv_F, whiskerLeft_F, rightUnitor_inv_F, id_F, leftUnitorImpl_inv_F, tensorObj_rel, tensorUnitImpl_tgt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_F 📖	mathematical	—	Hom.F CategoryTheory.CategoryStruct.comp CategoryTheory.Dial CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Limits.prod src tgt CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.map Hom.f CategoryTheory.CategoryStruct.id	—	—
comp_f 📖	mathematical	—	Hom.f CategoryTheory.CategoryStruct.comp CategoryTheory.Dial CategoryTheory.Category.toCategoryStruct instCategory src	—	—
comp_le_lemma 📖	mathematical	—	CategoryTheory.Subobject CategoryTheory.Limits.prod src tgt CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.hasLimitsOfShape_discrete Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.pair Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Functor.obj Preorder.smallCategory CategoryTheory.Subobject.pullback CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.prod.map Hom.f CategoryTheory.CategoryStruct.id Hom.F rel	—	le_trans CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete Finite.of_fintype CategoryTheory.Subobject.pullback.congr_simp CategoryTheory.Limits.prod.comp_lift CategoryTheory.Limits.limit.lift_π LE.le.trans CategoryTheory.Functor.monotone Hom.le CategoryTheory.Limits.prod.lift_map CategoryTheory.Category.comp_id CategoryTheory.Limits.prod.map_fst CategoryTheory.Limits.prod.map_map
hom_ext 📖	—	Hom.f Hom.F	—	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete Finite.of_fintype Hom.ext
hom_ext_iff 📖	mathematical	—	Hom.f Hom.F	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete Finite.of_fintype hom_ext
id_F 📖	mathematical	—	Hom.F CategoryTheory.CategoryStruct.id CategoryTheory.Dial CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Limits.prod.snd src tgt	—	—
id_f 📖	mathematical	—	Hom.f CategoryTheory.CategoryStruct.id CategoryTheory.Dial CategoryTheory.Category.toCategoryStruct instCategory src	—	—
isoMk_hom_F 📖	mathematical	rel CategoryTheory.Functor.obj CategoryTheory.Subobject CategoryTheory.Limits.prod src tgt CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.hasLimitsOfShape_discrete Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.pair Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.pullback CategoryTheory.Limits.prod.map CategoryTheory.Iso.hom	Hom.F CategoryTheory.Dial instCategory isoMk CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.prod.snd CategoryTheory.Iso.inv	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete Finite.of_fintype
isoMk_hom_f 📖	mathematical	rel CategoryTheory.Functor.obj CategoryTheory.Subobject CategoryTheory.Limits.prod src tgt CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.hasLimitsOfShape_discrete Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.pair Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.pullback CategoryTheory.Limits.prod.map CategoryTheory.Iso.hom	Hom.f CategoryTheory.Dial instCategory isoMk	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete Finite.of_fintype
isoMk_inv_F 📖	mathematical	rel CategoryTheory.Functor.obj CategoryTheory.Subobject CategoryTheory.Limits.prod src tgt CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.hasLimitsOfShape_discrete Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.pair Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.pullback CategoryTheory.Limits.prod.map CategoryTheory.Iso.hom	Hom.F CategoryTheory.Iso.inv CategoryTheory.Dial instCategory isoMk CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.prod.snd	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete Finite.of_fintype
isoMk_inv_f 📖	mathematical	rel CategoryTheory.Functor.obj CategoryTheory.Subobject CategoryTheory.Limits.prod src tgt CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.hasLimitsOfShape_discrete Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.pair Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.pullback CategoryTheory.Limits.prod.map CategoryTheory.Iso.hom	Hom.f CategoryTheory.Iso.inv CategoryTheory.Dial instCategory isoMk	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete Finite.of_fintype

CategoryTheory.Dial.Hom

Definitions

Name	Category	Theorems
F 📖	CompOp	26 math math: CategoryTheory.Dial.tensorHom_F, CategoryTheory.Dial.associator_hom_F, CategoryTheory.Dial.associatorImpl_inv_F, CategoryTheory.Dial.rightUnitor_hom_F, CategoryTheory.Dial.rightUnitorImpl_inv_F, CategoryTheory.Dial.comp_le_lemma, CategoryTheory.Dial.rightUnitorImpl_hom_F, CategoryTheory.Dial.braiding_inv_F, CategoryTheory.Dial.associatorImpl_hom_F, le, CategoryTheory.Dial.leftUnitor_hom_F, CategoryTheory.Dial.whiskerRight_F, ext_iff, CategoryTheory.Dial.tensorHomImpl_F, CategoryTheory.Dial.comp_F, CategoryTheory.Dial.isoMk_inv_F, CategoryTheory.Dial.associator_inv_F, CategoryTheory.Dial.leftUnitorImpl_hom_F, CategoryTheory.Dial.isoMk_hom_F, CategoryTheory.Dial.braiding_hom_F, CategoryTheory.Dial.leftUnitor_inv_F, CategoryTheory.Dial.whiskerLeft_F, CategoryTheory.Dial.rightUnitor_inv_F, CategoryTheory.Dial.id_F, CategoryTheory.Dial.hom_ext_iff, CategoryTheory.Dial.leftUnitorImpl_inv_F
f 📖	CompOp	27 math math: CategoryTheory.Dial.braiding_inv_f, CategoryTheory.Dial.rightUnitor_hom_f, CategoryTheory.Dial.rightUnitorImpl_inv_f, CategoryTheory.Dial.leftUnitor_hom_f, CategoryTheory.Dial.comp_le_lemma, CategoryTheory.Dial.whiskerRight_f, CategoryTheory.Dial.leftUnitor_inv_f, CategoryTheory.Dial.associator_inv_f, CategoryTheory.Dial.braiding_hom_f, CategoryTheory.Dial.rightUnitor_inv_f, le, ext_iff, CategoryTheory.Dial.comp_F, CategoryTheory.Dial.isoMk_hom_f, CategoryTheory.Dial.comp_f, CategoryTheory.Dial.id_f, CategoryTheory.Dial.tensorHomImpl_f, CategoryTheory.Dial.whiskerLeft_f, CategoryTheory.Dial.associatorImpl_inv_f, CategoryTheory.Dial.tensorHom_f, CategoryTheory.Dial.associator_hom_f, CategoryTheory.Dial.leftUnitorImpl_inv_f, CategoryTheory.Dial.associatorImpl_hom_f, CategoryTheory.Dial.isoMk_inv_f, CategoryTheory.Dial.leftUnitorImpl_hom_f, CategoryTheory.Dial.rightUnitorImpl_hom_f, CategoryTheory.Dial.hom_ext_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	f F	—	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete Finite.of_fintype
ext_iff 📖	mathematical	—	f F	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete Finite.of_fintype ext
le 📖	mathematical	—	CategoryTheory.Subobject CategoryTheory.Limits.prod CategoryTheory.Dial.src CategoryTheory.Dial.tgt CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.hasLimitsOfShape_discrete Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.pair Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Functor.obj Preorder.smallCategory CategoryTheory.Subobject.pullback CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst F CategoryTheory.Dial.rel CategoryTheory.Limits.prod.map f CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—

---

← Back to Index