Pseudofunctor

📁 Source: Mathlib/Algebra/Category/ModuleCat/Pseudofunctor.lean

Statistics

Metric	Count
Definitions moduleCatExtendScalarsPseudofunctor, moduleCatRestrictScalarsPseudofunctor, moduleCatRestrictScalarsPseudofunctor	3
Theorems moduleCatExtendScalarsPseudofunctor_map, moduleCatExtendScalarsPseudofunctor_mapComp, moduleCatExtendScalarsPseudofunctor_mapId, moduleCatExtendScalarsPseudofunctor_obj, moduleCatRestrictScalarsPseudofunctor_map, moduleCatRestrictScalarsPseudofunctor_mapComp, moduleCatRestrictScalarsPseudofunctor_mapId, moduleCatRestrictScalarsPseudofunctor_obj, moduleCatRestrictScalarsPseudofunctor_map, moduleCatRestrictScalarsPseudofunctor_mapComp, moduleCatRestrictScalarsPseudofunctor_mapId, moduleCatRestrictScalarsPseudofunctor_obj	12
Total	15

CommRingCat

Definitions

Name	Category	Theorems
moduleCatExtendScalarsPseudofunctor 📖	CompOp	4 math math: moduleCatExtendScalarsPseudofunctor_map, moduleCatExtendScalarsPseudofunctor_obj, moduleCatExtendScalarsPseudofunctor_mapComp, moduleCatExtendScalarsPseudofunctor_mapId
moduleCatRestrictScalarsPseudofunctor 📖	CompOp	4 math math: moduleCatRestrictScalarsPseudofunctor_mapComp, moduleCatRestrictScalarsPseudofunctor_mapId, moduleCatRestrictScalarsPseudofunctor_map, moduleCatRestrictScalarsPseudofunctor_obj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
moduleCatExtendScalarsPseudofunctor_map 📖	mathematical	—	Prefunctor.map CategoryTheory.LocallyDiscrete CommRingCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory instCategory CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor moduleCatExtendScalarsPseudofunctor CategoryTheory.Functor.toCatHom ModuleCat carrier CategoryTheory.LocallyDiscrete.as CommRing.toRing commRing ModuleCat.moduleCategory ModuleCat.extendScalars Hom.hom CategoryTheory.Discrete.as	—	—
moduleCatExtendScalarsPseudofunctor_mapComp 📖	mathematical	—	CategoryTheory.Pseudofunctor.mapComp CategoryTheory.LocallyDiscrete CommRingCat CategoryTheory.locallyDiscreteBicategory instCategory CategoryTheory.Cat CategoryTheory.Cat.bicategory moduleCatExtendScalarsPseudofunctor CategoryTheory.Cat.Hom.isoMk ModuleCat carrier CategoryTheory.LocallyDiscrete.as CommRing.toRing commRing ModuleCat.moduleCategory ModuleCat.extendScalars RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Hom.hom CategoryTheory.Discrete.as Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.comp CategoryTheory.Cat.str CategoryTheory.Cat.of ModuleCat.extendScalarsComp	—	—
moduleCatExtendScalarsPseudofunctor_mapId 📖	mathematical	—	CategoryTheory.Pseudofunctor.mapId CategoryTheory.LocallyDiscrete CommRingCat CategoryTheory.locallyDiscreteBicategory instCategory CategoryTheory.Cat CategoryTheory.Cat.bicategory moduleCatExtendScalarsPseudofunctor CategoryTheory.Cat.Hom.isoMk ModuleCat carrier CategoryTheory.LocallyDiscrete.as CommRing.toRing commRing ModuleCat.moduleCategory ModuleCat.extendScalars RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.Functor.id CategoryTheory.Cat.str CategoryTheory.Cat.of ModuleCat.extendScalarsId	—	—
moduleCatExtendScalarsPseudofunctor_obj 📖	mathematical	—	Prefunctor.obj CategoryTheory.LocallyDiscrete CommRingCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory instCategory CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor moduleCatExtendScalarsPseudofunctor CategoryTheory.Cat.of ModuleCat carrier CategoryTheory.LocallyDiscrete.as CommRing.toRing commRing ModuleCat.moduleCategory	—	—
moduleCatRestrictScalarsPseudofunctor_map 📖	mathematical	—	Prefunctor.map CategoryTheory.LocallyDiscrete Opposite CommRingCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite instCategory CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor moduleCatRestrictScalarsPseudofunctor CategoryTheory.Functor.toCatHom ModuleCat carrier Opposite.unop CategoryTheory.LocallyDiscrete.as CommRing.toRing commRing ModuleCat.moduleCategory ModuleCat.restrictScalars Hom.hom Quiver.Hom.unop CategoryTheory.Discrete.as	—	—
moduleCatRestrictScalarsPseudofunctor_mapComp 📖	mathematical	—	CategoryTheory.Pseudofunctor.mapComp CategoryTheory.LocallyDiscrete Opposite CommRingCat CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite instCategory CategoryTheory.Cat CategoryTheory.Cat.bicategory moduleCatRestrictScalarsPseudofunctor CategoryTheory.Cat.Hom.isoMk ModuleCat carrier Opposite.unop CategoryTheory.LocallyDiscrete.as CommRing.toRing commRing ModuleCat.moduleCategory ModuleCat.restrictScalars RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Hom.hom Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Discrete.as Quiver.Hom CategoryTheory.Functor.comp CategoryTheory.Cat.str CategoryTheory.Cat.of ModuleCat.restrictScalarsComp	—	—
moduleCatRestrictScalarsPseudofunctor_mapId 📖	mathematical	—	CategoryTheory.Pseudofunctor.mapId CategoryTheory.LocallyDiscrete Opposite CommRingCat CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite instCategory CategoryTheory.Cat CategoryTheory.Cat.bicategory moduleCatRestrictScalarsPseudofunctor CategoryTheory.Cat.Hom.isoMk ModuleCat carrier Opposite.unop CategoryTheory.LocallyDiscrete.as CommRing.toRing commRing ModuleCat.moduleCategory ModuleCat.restrictScalars RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.Functor.id CategoryTheory.Cat.str CategoryTheory.Cat.of ModuleCat.restrictScalarsId	—	—
moduleCatRestrictScalarsPseudofunctor_obj 📖	mathematical	—	Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CommRingCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite instCategory CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor moduleCatRestrictScalarsPseudofunctor CategoryTheory.Cat.of ModuleCat carrier Opposite.unop CategoryTheory.LocallyDiscrete.as CommRing.toRing commRing ModuleCat.moduleCategory	—	—

RingCat

Definitions

Name	Category	Theorems
moduleCatRestrictScalarsPseudofunctor 📖	CompOp	4 math math: moduleCatRestrictScalarsPseudofunctor_mapId, moduleCatRestrictScalarsPseudofunctor_map, moduleCatRestrictScalarsPseudofunctor_obj, moduleCatRestrictScalarsPseudofunctor_mapComp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
moduleCatRestrictScalarsPseudofunctor_map 📖	mathematical	—	Prefunctor.map CategoryTheory.LocallyDiscrete Opposite RingCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite instCategory CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor moduleCatRestrictScalarsPseudofunctor CategoryTheory.Functor.toCatHom ModuleCat carrier Opposite.unop CategoryTheory.LocallyDiscrete.as ring ModuleCat.moduleCategory ModuleCat.restrictScalars Hom.hom Quiver.Hom.unop CategoryTheory.Discrete.as	—	—
moduleCatRestrictScalarsPseudofunctor_mapComp 📖	mathematical	—	CategoryTheory.Pseudofunctor.mapComp CategoryTheory.LocallyDiscrete Opposite RingCat CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite instCategory CategoryTheory.Cat CategoryTheory.Cat.bicategory moduleCatRestrictScalarsPseudofunctor CategoryTheory.Cat.Hom.isoMk ModuleCat carrier Opposite.unop CategoryTheory.LocallyDiscrete.as ring ModuleCat.moduleCategory ModuleCat.restrictScalars RingHom.comp Semiring.toNonAssocSemiring Ring.toSemiring Hom.hom Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Discrete.as Quiver.Hom CategoryTheory.Functor.comp CategoryTheory.Cat.str CategoryTheory.Cat.of ModuleCat.restrictScalarsComp	—	—
moduleCatRestrictScalarsPseudofunctor_mapId 📖	mathematical	—	CategoryTheory.Pseudofunctor.mapId CategoryTheory.LocallyDiscrete Opposite RingCat CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite instCategory CategoryTheory.Cat CategoryTheory.Cat.bicategory moduleCatRestrictScalarsPseudofunctor CategoryTheory.Cat.Hom.isoMk ModuleCat carrier Opposite.unop CategoryTheory.LocallyDiscrete.as ring ModuleCat.moduleCategory ModuleCat.restrictScalars RingHom.id Semiring.toNonAssocSemiring Ring.toSemiring CategoryTheory.Functor.id CategoryTheory.Cat.str CategoryTheory.Cat.of ModuleCat.restrictScalarsId	—	—
moduleCatRestrictScalarsPseudofunctor_obj 📖	mathematical	—	Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite RingCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite instCategory CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor moduleCatRestrictScalarsPseudofunctor CategoryTheory.Cat.of ModuleCat carrier Opposite.unop CategoryTheory.LocallyDiscrete.as ring ModuleCat.moduleCategory	—	—

---

← Back to Index