category of metric spaces with ∞ allowed

  • notation: Met∞\mathbf{Met}_{\infty}
  • objects: metric spaces, where the metric is allowed to assume the value ∞\infty
  • morphisms: non-expansive maps ff, meaning d(f(x),f(y))≤d(x,y)d(f(x),f(y)) \leq d(x,y) for all x,yx,y
  • nLab Link
  • Related categories: Met\mathbf{Met}, Metc\mathbf{Met}_c

The fact that we allow ∞\infty means that universal constructions work much better.

Properties

Properties from the database

Deduced properties

  • is locally essentially small
    Since it is locally small, we deduce that it is locally essentially small.
  • has coproducts
    Since it has disjoint coproducts, we deduce that it has coproducts.
  • has disjoint finite coproducts
    Since it has disjoint coproducts, we deduce that it has disjoint finite coproducts.
  • has finite coproducts
    Since it has disjoint finite coproducts, we deduce that it has finite coproducts.
  • has finite products
    Since it is infinitary distributive, we deduce that it has finite products.
  • is distributive
    Since it is infinitary distributive, we deduce that it is distributive.
  • has a strict initial object
    Since it is distributive, we deduce that it has a strict initial object.
  • is locally presentable
    Since it is locally ℵ₁-presentable, we deduce that it is locally presentable.
  • has countable coproducts
    Since it has coproducts, we deduce that it has countable coproducts.
  • has an initial object
    Since it has finite coproducts, we deduce that it has an initial object.
  • has binary coproducts
    Since it has finite coproducts, we deduce that it has binary coproducts.
  • is connected
    Since it has an initial object, we deduce that it is connected.
  • is inhabited
    Since it has a cogenerator, we deduce that it is inhabited.
  • has a terminal object
    Since it has finite products, we deduce that it has a terminal object.
  • has binary products
    Since it has finite products, we deduce that it has binary products.
  • is well-powered
    Since it is locally presentable, we deduce that it is well-powered.
  • is well-copowered
    Since it is locally presentable, we deduce that it is well-copowered.
  • is complete
    Since it is locally presentable, we deduce that it is complete.
  • is cocomplete
    Since it is locally presentable, we deduce that it is cocomplete.
  • has a generator
    Since it is locally presentable, we deduce that it has a generator.
  • is finitely cocomplete
    Since it is cocomplete, we deduce that it is finitely cocomplete.
  • has filtered colimits
    Since it is cocomplete, we deduce that it has filtered colimits.
  • has wide pushouts
    Since it is cocomplete, we deduce that it has wide pushouts.
  • has connected colimits
    Since it is cocomplete, we deduce that it has connected colimits.
  • has coequalizers
    Since it is cocomplete, we deduce that it has coequalizers.
  • has pushouts
    Since it has binary coproducts and has coequalizers, we deduce that it has pushouts.
  • is Cauchy complete
    Since it has coequalizers, we deduce that it is Cauchy complete.
  • has sequential colimits
    Since it has coequalizers and has countable coproducts, we deduce that it has sequential colimits.
  • is finitely complete
    Since it is complete, we deduce that it is finitely complete.
  • has filtered limits
    Since it is complete, we deduce that it has filtered limits.
  • has wide pullbacks
    Since it is complete, we deduce that it has wide pullbacks.
  • has connected limits
    Since it is complete, we deduce that it has connected limits.
  • has products
    Since it is complete, we deduce that it has products.
  • has equalizers
    Since it is complete, we deduce that it has equalizers.
  • has countable products
    Since it has products, we deduce that it has countable products.
  • has pullbacks
    Since it has binary products and has equalizers, we deduce that it has pullbacks.
  • has sequential limits
    Since it has equalizers and has countable products, we deduce that it has sequential limits.

Non-Properties

Non-Properties from the database

Deduced Non-Properties*

  • is not small
    Assume for a contradiction that it is small. Since it is small, we deduce that it is essentially small. Since it is essentially small and has products, we deduce that it is thin. Since it is essentially small and is thin and is complete and is infinitary distributive, we deduce that it is cartesian closed. This is a contradiction since we already know that it is not cartesian closed.
  • does not have zero morphisms
    Assume for a contradiction that it has zero morphisms. Since it has zero morphisms and has an initial object, we deduce that it is pointed. Since it has a strict initial object and is pointed, we deduce that it is trivial. Since it is trivial, we deduce that it is split abelian. Since it is split abelian, we deduce that it is abelian. Since it is abelian, we deduce that it is Malcev. This is a contradiction since we already know that it is not Malcev.
  • is not preadditive
    Assume for a contradiction that it is preadditive. Since it is preadditive, we deduce that it has zero morphisms. This is a contradiction since we already know that it does not have zero morphisms.
  • is not additive
    Assume for a contradiction that it is additive. Since it is additive, we deduce that it is preadditive. This is a contradiction since we already know that it is not preadditive.
  • is not abelian
    Assume for a contradiction that it is abelian. Since it is abelian, we deduce that it is additive. This is a contradiction since we already know that it is not additive.
  • is not pointed
    Assume for a contradiction that it is pointed. Since it is pointed, we deduce that it has zero morphisms. This is a contradiction since we already know that it does not have zero morphisms.
  • is not locally finitely presentable
    Assume for a contradiction that it is locally finitely presentable. Since it is locally finitely presentable, we deduce that it has exact filtered colimits. This is a contradiction since we already know that it does not have exact filtered colimits.
  • is not an elementary topos
    Assume for a contradiction that it is an elementary topos. Since it is an elementary topos, we deduce that it is cartesian closed. This is a contradiction since we already know that it is not cartesian closed.
  • is not a Grothendieck topos
    Assume for a contradiction that it is a Grothendieck topos. Since it is a Grothendieck topos, we deduce that it is an elementary topos. This is a contradiction since we already know that it is not an elementary topos.
  • is not self-dual
    Assume for a contradiction that it is self-dual. Since it is locally presentable and is self-dual, we deduce that it is thin. Since it is thin and is finitely complete, we deduce that it is Malcev. This is a contradiction since we already know that it is not Malcev.
  • is not a groupoid
    Assume for a contradiction that it is a groupoid. Since it is a groupoid, we deduce that it is self-dual. This is a contradiction since we already know that it is not self-dual.
  • is not essentially small
    Assume for a contradiction that it is essentially small. Since it is essentially small and has products, we deduce that it is thin. Since it is essentially small and is thin and is complete and is infinitary distributive, we deduce that it is cartesian closed. This is a contradiction since we already know that it is not cartesian closed.
  • is not thin
    Assume for a contradiction that it is thin. Since it is thin and is finitely complete, we deduce that it is Malcev. This is a contradiction since we already know that it is not Malcev.
  • is not discrete
    Assume for a contradiction that it is discrete. Since it is discrete, we deduce that it is skeletal. This is a contradiction since we already know that it is not skeletal.
  • is not essentially discrete
    Assume for a contradiction that it is essentially discrete. Since it is essentially discrete, we deduce that it is thin. This is a contradiction since we already know that it is not thin.
  • is not finitary algebraic
    Assume for a contradiction that it is finitary algebraic. Since it is finitary algebraic, we deduce that it is locally finitely presentable. This is a contradiction since we already know that it is not locally finitely presentable.
  • is not finite
    Assume for a contradiction that it is finite. Since it is finite, we deduce that it is small. This is a contradiction since we already know that it is not small.
  • is not essentially finite
    Assume for a contradiction that it is essentially finite. Since it is essentially finite and has finite products, we deduce that it is thin. This is a contradiction since we already know that it is not thin.
  • is not trivial
    Assume for a contradiction that it is trivial. Since it is trivial, we deduce that it is finitary algebraic. This is a contradiction since we already know that it is not finitary algebraic.
  • does not have a subobject classifier
    Assume for a contradiction that it has a subobject classifier. Since it has a subobject classifier, we deduce that it is mono-regular. Since it is mono-regular, we deduce that it is balanced. This is a contradiction since we already know that it is not balanced.
  • is not Grothendieck abelian
    Assume for a contradiction that it is Grothendieck abelian. Since it is Grothendieck abelian, we deduce that it is abelian. This is a contradiction since we already know that it is not abelian.
  • is not left cancellative
    Assume for a contradiction that it is left cancellative. Since it is left cancellative and has coequalizers, we deduce that it is thin. This is a contradiction since we already know that it is not thin.
  • is not right cancellative
    Assume for a contradiction that it is right cancellative. Since it is right cancellative and has equalizers, we deduce that it is thin. This is a contradiction since we already know that it is not thin.
  • is not split abelian
    Assume for a contradiction that it is split abelian. Since it is split abelian, we deduce that it is abelian. This is a contradiction since we already know that it is not abelian.
  • is not mono-regular
    Assume for a contradiction that it is mono-regular. Since it is mono-regular, we deduce that it is balanced. This is a contradiction since we already know that it is not balanced.
  • is not epi-regular
    Assume for a contradiction that it is epi-regular. Since it is epi-regular, we deduce that it is balanced. This is a contradiction since we already know that it is not balanced.

*This also uses the deduced properties.

Unknown properties

—

Special morphisms

  • Isomorphisms: bijective isometries
    easy
  • Monomorphisms: injective non-expansive maps
  • Epimorphisms: