Skip to content

Target: apartness algebras and their antisubalgebras #1239

@djspacewhale

Description

@djspacewhale

For roughly the same reason as topologists like, say, Hausdorff groups, constructive algebraists like working with gadgets where the underlying set has a tight apartness relation. Examples in nature include RR^n and profinite groups such as Cantor space. As discussed at the nlab page on antisubalgebras, the more useful notion in such contexts is of an "antisubalgebra" rather than a subalgebra, again for roughly the same reason as topologists like closed subalgebras.

(Note 1: such work is only relevant to set-level algebra, as types with a tight relation are automatically sets; constructive higher algebra promises to be much trickier and likely out of the range of current technology without rapid progress in modal lands.)

This is potentially a lot of routine work but good ethical practice, then, to define the apartness-versions of groups, rings, modules, etc along with their antisubalgebras. Such work would be useful for investigating and formalizing further constructive algebra and promises to be a good onboarder for the budding constructive algebraist.

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions