Closed subsets in Bishop topological groups

TL;DR

This paper introduces Bishop topological groups, defining closed subsets constructively without relying on classical topological notions or countable choice, emphasizing an algorithmic approach within constructive mathematics.

Contribution

It formalizes the concept of closed subsets in Bishop topological groups using a constructive, non-topological closure operator that avoids sequences and countable choice.

Findings

Defines Bishop topological groups with Bishop morphisms

Introduces a constructive closure operator for closed subsets

Provides algorithmic content aligned with constructive mathematics

Abstract

We introduce the notion of a Bishop topological group i.e., a group X equipped with a Bishop topology of functions F such that the group operations of X are Bishop morphisms with respect to F. A closed subset in the neighborhood structure of X induced by its Bishop topology F is defined in a positive way i.e., not as the complement of an open subset in X. The corresponding closure operator, although it is not topological, in the classical sense, does not involve sequences. As countable choice (CC) is avoided, and in agreement with Richman's critique on the use of CC in constructive mathematics, the fundamental facts on closed subsets in Bishop topological groups shown here have a clear algorithmic content. We work within Bishop's informal system of constructive mathematics BISH, without countable choice, equipped with inductive definitions with rules of countably many premises.