Yoneda

📁 Source: Mathlib/CategoryTheory/Linear/Yoneda.lean

Statistics

Metric	Count
Definitions linearCoyoneda, linearYoneda	2
Theorems faithful_linearCoyoneda, faithful_linearYoneda, full_linearCoyoneda, full_linearYoneda, linearCoyoneda_map_app, linearCoyoneda_obj_additive, linearCoyoneda_obj_map, linearCoyoneda_obj_obj_carrier, linearCoyoneda_obj_obj_isAddCommGroup, linearCoyoneda_obj_obj_isModule, linearYoneda_map_app, linearYoneda_obj_additive, linearYoneda_obj_map, linearYoneda_obj_obj_carrier, linearYoneda_obj_obj_isAddCommGroup, linearYoneda_obj_obj_isModule, whiskering_linearCoyoneda, whiskering_linearCoyoneda₂, whiskering_linearYoneda, whiskering_linearYoneda₂	20
Total	22

CategoryTheory

Definitions

Name	Category	Theorems
linearCoyoneda 📖	CompOp	10 math math: linearCoyoneda_obj_additive, linearCoyoneda_map_app, linearCoyoneda_obj_obj_carrier, whiskering_linearCoyoneda, linearCoyoneda_obj_obj_isAddCommGroup, whiskering_linearCoyoneda₂, full_linearCoyoneda, faithful_linearCoyoneda, linearCoyoneda_obj_map, linearCoyoneda_obj_obj_isModule
linearYoneda 📖	CompOp	11 math math: linearYoneda_obj_map, linearYoneda_obj_obj_carrier, faithful_linearYoneda, linearYoneda_map_app, linearYoneda_obj_obj_isAddCommGroup, whiskering_linearYoneda, linearYoneda_obj_additive, full_linearYoneda, linearYoneda_obj_obj_isModule, whiskering_linearYoneda₂, ChainComplex.linearYonedaObj_X

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
faithful_linearCoyoneda 📖	mathematical	—	Functor.Faithful Opposite Category.opposite Functor ModuleCat ModuleCat.moduleCategory Functor.category linearCoyoneda	—	Functor.Faithful.of_comp_eq Coyoneda.coyoneda_faithful whiskering_linearCoyoneda
faithful_linearYoneda 📖	mathematical	—	Functor.Faithful Functor Opposite Category.opposite ModuleCat ModuleCat.moduleCategory Functor.category linearYoneda	—	Functor.Faithful.of_comp_eq Yoneda.yoneda_faithful whiskering_linearYoneda
full_linearCoyoneda 📖	mathematical	—	Functor.Full Opposite Category.opposite Functor ModuleCat ModuleCat.moduleCategory Functor.category linearCoyoneda	—	Coyoneda.coyoneda_full Functor.Full.of_comp_faithful Functor.faithful_whiskeringRight_obj instFaithfulForget
full_linearYoneda 📖	mathematical	—	Functor.Full Functor Opposite Category.opposite ModuleCat ModuleCat.moduleCategory Functor.category linearYoneda	—	Yoneda.yoneda_full Functor.Full.of_comp_faithful Functor.faithful_whiskeringRight_obj instFaithfulForget
linearCoyoneda_map_app 📖	mathematical	—	NatTrans.app ModuleCat ModuleCat.moduleCategory ModuleCat.of Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Opposite.unop Preadditive.homGroup Linear.homModule Ring.toSemiring ModuleCat.ofHom Linear.rightComp Functor.map Opposite Category.opposite Functor Functor.category linearCoyoneda Linear.leftComp Quiver.Hom.unop	—	—
linearCoyoneda_obj_additive 📖	mathematical	—	Functor.Additive ModuleCat ModuleCat.moduleCategory ModuleCat.instPreadditive Functor.obj Opposite Category.opposite Functor Functor.category linearCoyoneda	—	ModuleCat.hom_ext LinearMap.ext Preadditive.comp_add
linearCoyoneda_obj_map 📖	mathematical	—	Functor.map ModuleCat ModuleCat.moduleCategory Functor.obj Opposite Category.opposite Functor Functor.category linearCoyoneda ModuleCat.ofHom Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Opposite.unop Preadditive.homGroup Linear.homModule Ring.toSemiring Linear.rightComp	—	—
linearCoyoneda_obj_obj_carrier 📖	mathematical	—	ModuleCat.carrier Functor.obj ModuleCat ModuleCat.moduleCategory Opposite Category.opposite Functor Functor.category linearCoyoneda Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Opposite.unop	—	—
linearCoyoneda_obj_obj_isAddCommGroup 📖	mathematical	—	ModuleCat.isAddCommGroup Functor.obj ModuleCat ModuleCat.moduleCategory Opposite Category.opposite Functor Functor.category linearCoyoneda Preadditive.homGroup Opposite.unop	—	—
linearCoyoneda_obj_obj_isModule 📖	mathematical	—	ModuleCat.isModule Functor.obj ModuleCat ModuleCat.moduleCategory Opposite Category.opposite Functor Functor.category linearCoyoneda Linear.homModule Ring.toSemiring Opposite.unop	—	—
linearYoneda_map_app 📖	mathematical	—	NatTrans.app Opposite Category.opposite ModuleCat ModuleCat.moduleCategory ModuleCat.of Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Opposite.unop Preadditive.homGroup Linear.homModule Ring.toSemiring ModuleCat.ofHom Linear.leftComp Quiver.Hom.unop Functor.map Functor Functor.category linearYoneda Linear.rightComp	—	—
linearYoneda_obj_additive 📖	mathematical	—	Functor.Additive Opposite ModuleCat Category.opposite ModuleCat.moduleCategory instPreadditiveOpposite ModuleCat.instPreadditive Functor.obj Functor Functor.category linearYoneda	—	ModuleCat.hom_ext LinearMap.ext Preadditive.add_comp
linearYoneda_obj_map 📖	mathematical	—	Functor.map Opposite Category.opposite ModuleCat ModuleCat.moduleCategory Functor.obj Functor Functor.category linearYoneda ModuleCat.ofHom Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Opposite.unop Preadditive.homGroup Linear.homModule Ring.toSemiring Linear.leftComp Quiver.Hom.unop	—	—
linearYoneda_obj_obj_carrier 📖	mathematical	—	ModuleCat.carrier Functor.obj Opposite Category.opposite ModuleCat ModuleCat.moduleCategory Functor Functor.category linearYoneda Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Opposite.unop	—	—
linearYoneda_obj_obj_isAddCommGroup 📖	mathematical	—	ModuleCat.isAddCommGroup Functor.obj Opposite Category.opposite ModuleCat ModuleCat.moduleCategory Functor Functor.category linearYoneda Preadditive.homGroup Opposite.unop	—	—
linearYoneda_obj_obj_isModule 📖	mathematical	—	ModuleCat.isModule Functor.obj Opposite Category.opposite ModuleCat ModuleCat.moduleCategory Functor Functor.category linearYoneda Linear.homModule Ring.toSemiring Opposite.unop	—	—
whiskering_linearCoyoneda 📖	mathematical	—	Functor.comp Opposite Category.opposite Functor ModuleCat ModuleCat.moduleCategory Functor.category types linearCoyoneda Functor.obj Functor.whiskeringRight forget LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier coyoneda	—	—
whiskering_linearCoyoneda₂ 📖	mathematical	—	Functor.comp Opposite Category.opposite Functor ModuleCat ModuleCat.moduleCategory Functor.category AddCommGrpCat AddCommGrpCat.instCategory linearCoyoneda Functor.obj Functor.whiskeringRight forget₂ LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier ModuleCat.hasForgetToAddCommGroup preadditiveCoyoneda	—	—
whiskering_linearYoneda 📖	mathematical	—	Functor.comp Functor Opposite Category.opposite ModuleCat ModuleCat.moduleCategory Functor.category types linearYoneda Functor.obj Functor.whiskeringRight forget LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier yoneda	—	—
whiskering_linearYoneda₂ 📖	mathematical	—	Functor.comp Functor Opposite Category.opposite ModuleCat ModuleCat.moduleCategory Functor.category AddCommGrpCat AddCommGrpCat.instCategory linearYoneda Functor.obj Functor.whiskeringRight forget₂ LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier ModuleCat.hasForgetToAddCommGroup preadditiveYoneda	—	—

---

← Back to Index