Structures · Category theory
CategoryTheory.InitiallySmall
A category is InitiallySmall.{w} if there is an initial functor from a w-small category.
- Shape
- One type argument · adds initial_smallCategory
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances4
- CategoryTheory.Over
- CategoryTheory.Functor.Elements
- Prod
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by74
- CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiberMk
- CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiber
- CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered
- PresheafOfModules.ModuleColimit.homEquiv
- PresheafOfModules.ModuleColimit.map
- CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered
- CategoryTheory.GrothendieckTopology.Point.comap
- CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.functor
- CategoryTheory.fromInitialModel
- PresheafOfModules.ModuleColimit.map_apply
- CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered_naturality
- PresheafOfModules.colimitFunctor
- CategoryTheory.GrothendieckTopology.Point.skyscraperSheafFunctorCompSheafPushforwardContinuous
- PresheafOfModules.ModuleColimit.ιM_jointly_surjective
- CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered_w
- CategoryTheory.GrothendieckTopology.Point.sheafFiberComapIso
- PresheafOfModules.colimitAdjunction
- CategoryTheory.GrothendieckTopology.Point.presheafFiberOfIsCofilteredCocone
- PresheafOfModules.ModuleColimit.smul_eq
- PresheafOfModules.ModuleColimit.homEquiv_symm_apply
- CategoryTheory.InitiallySmall.exists_small_weakly_initial_set
- PresheafOfModules.ModuleColimit.homEquiv_naturality_left
- CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiber_map_fiberMk
- CategoryTheory.initiallySmall_of_initial_of_initiallySmall
- CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiberMk_map_comp
- PresheafOfModules.ModuleColimit.jointly_surjective₂
- PresheafOfModules.colimitAdjunction_homEquiv
- CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiberMk_map
- PresheafOfModules.ModuleColimit.map_id
- PresheafOfModules.ModuleColimit.ιR_jointly_surjective
- CategoryTheory.GrothendieckTopology.Point.sheafFiberComapIso_inv_app
- CategoryTheory.initial_fromInitialModel
- CategoryTheory.instFinallySmallOppositeOfInitiallySmall
- CategoryTheory.InitiallySmall.instIsCofilteredCofilteredInitialModel
- PresheafOfModules.ModuleColimit.map_smul_homEquiv'_iff
- CategoryTheory.GrothendieckTopology.Point.presheafFiberOfIsCofilteredCocone_ι_app
- CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.exists_of_fiberMk_eq_fiberMk
- CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.instIsCofilteredElementsFiber
- PresheafOfModules.ModuleColimit.ιM_jointly_surjective₃
- CategoryTheory.GrothendieckTopology.Point.presheafFiberOfIsCofilteredCocone_pt
- CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.instInitialElementsFiberFunctorOfIsCofiltered
- PresheafOfModules.ModuleColimit.instSMulCarrierPtOppositeRingCat
- CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.instInitiallySmallElementsFiberOfIsCofiltered
- CategoryTheory.GrothendieckTopology.Point.sheafFiberComapIso_hom_app
- CategoryTheory.InitiallySmall.fromCofilteredInitialModel
- PresheafOfModules.ModuleColimit.jointly_surjective₃'
- CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered_w_assoc
- CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered_fiber
- PresheafOfModules.ModuleColimit.homEquiv_naturality_right
- PresheafOfModules.ModuleColimit.homEquiv_naturality_left_symm
Ancestors0
No ancestors.