Skip to content

Refactor category support for morphisms (Hom is not a functorial construction!) #10668

@nthiery

Description

@nthiery

Before this ticket, Hom was implemented as a covariant functorial construction:

    sage: Rings().hom_category()
    Category of hom sets in Category of rings
    sage: Rings().hom_category().super_categories()
    [Category of hom sets in Category of sets]

The intention was to model the fact that a morphism in a category is
also a morphism in any super category, via the forgetful functor. With
the example above, if A and B are rings, then a ring morphism phi:
A->B is also a set morphism. However, at the level of parents, and as
noted in the documentation of sage.category.HomCategory, this is
mathematically plain wrong: if A and B are rings, then Hom(A,B) in the
category of rings does not coincide with Hom(A,B) in the category of
sets.

I, Nicolas, take full blame for this misfeature; it was just the
shortest route to implement some urgently needed features about
morphisms, and still get that huge chunk of category code done.

Status of the current reimplementation:

  • Add support for a MorphismsMethods subclass, similar to
    ElementMethods and ParentMethods. If Cat is a category, then
    Cat.MorphismMethods will provide generic methods for morphisms in
    Cat and in any subcategory. This can be achieved by:

    • Building of a hierarchy of abstract classes Cat.morphism_class,
      similar to Cat.element_class and Cat.parent_class (10 lines of
      code; see Category.element_class).

    • Having morphisms in Cat inherit from Cat.morphism_class; this
      is implemented by overriding Parent.morphism_class. An
      alternative would have been to override Category.element_class
      in HomsetsCategory.element_class.

  • Rename both HomCategory and hom_category to Homsets, for consistency
    with the other constructions like CartesianProducts, ...

  • Fix HomCategory: for Cat a category, the purpose of
    Cat.hom_category() shall be to provide mathematical information
    about its homsets (e.g. that a homset in the category of vector
    spaces is also a vector space). It is only a subcategory of the
    homsets of the full super categories of Cat (a homset in the
    category of finite groups is also a homset in the category of
    groups).

  • Remove HomCategory from the global namespace.

Potential further desirable features for a later ticket:

  • If CatA is a subcategory of CatB, add automatic coercion (or just
    conversion?) from Hom(A,B, CatA) to Hom(A, B, CatB), modeling the
    appropriate forgetful functor. There are too many such coercions
    for them to be registered explicitly. So this probably needs to be
    implemented through a specific CatB._has_coerce_map_from(A) for
    homsets.

  • Extend/use sage.categories.pushout to handle mixed morphism
    arithmetic (e.g. having the sum of an algebra morphism and a
    coalgebra morphism return a vector space morphism).

Depends on #16340

CC: @sagetrac-sage-combinat @simon-king-jena

Component: categories

Author: Nicolas M. Thiéry

Branch: a937938

Reviewer: Simon King

Issue created by migration from https://trac.sagemath.org/ticket/10668

Metadata

Metadata

Assignees

Type

No type

Projects

No projects

Milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions