nLab ring setoid

Redirected from "braided ring setoid".

Context

Algebra

Category theory

Relations

Constructivism, Realizability, Computability

Contents

Idea

A setoid or Bishop set whose quotient set is a ring. Equivalently, a thin ring groupoid, or in foundations where groupoids are univalent by default, a thin ring pregroupoid.

“Ring setoid” and “Bishop ring” are placeholder names for a concept which may or may not have another name in the mathematics literature.

Definition

A ring setoid or Bishop ring is a setoid (A,)(A, \sim) with elements 0A0 \in A and 1A1 \in A and functions α:A×AA\alpha:A \times A \to A, ν:AA\nu:A \to A, and μ:A×AA\mu:A \times A \to A, such that

  • (A,,0,α,ν)(A, \sim, 0, \alpha, \nu) is a braided groupal setoid

  • (A,,1,μ)(A, \sim, 1, \mu) is a monoidal setoid

  • μ\mu distributes over α\alpha up to the equivalence relation: for all elements aAa \in A, bAb \in A, and cAc \in A,

    μ(a,α(b,c))α(μ(a,b),μ(a,c))andμ(α(a,b),c)α(μ(a,c),μ(b,c))\mu(a, \alpha(b, c)) \sim \alpha(\mu(a, b), \mu(a, c)) \quad \mathrm{and} \quad \mu(\alpha(a, b), c) \sim \alpha(\mu(a, c), \mu(b, c))

AA is commutative or symmetric or braided if additionally for all elements aAa \in A and bAb \in A, μ(a,b)μ(b,a)\mu(a, b) \sim \mu(b, a).

Examples

Ring setoid homomorphisms

A ring setoid homomorphism or Bishop ring homomorphism between two ring setoids AA and BB is a function h:ABh:A \to B such that

  • ff preserves the equivalence relation: for all aAa \in A and bAb \in A, a Aba \sim_A b implies f(a) Bf(b)f(a) \sim_B f(b)

  • ff preserves the groupal unit up to equivalence relation: f(0 A) B0 Bf(0_A) \sim_B 0_B

  • ff preserves the groupal product up to equivalence relation: for all aAa \in A and bAb \in A,

    f(α A(a,b)) Bα B(f(a),f(b))f(\alpha_A(a, b)) \sim_B \alpha_B(f(a), f(b))
  • ff preserves the groupal inverse up to equivalence relation: for all aAa \in A,

    f(ν A(a)) Bν B(f(a))f(\nu_A(a)) \sim_B \nu_B(f(a))
  • ff preserves the monoidal unit up to equivalence relation: f(1 A) B1 Bf(1_A) \sim_B 1_B

  • ff preserves the monoidal product up to equivalence relation: for all aAa \in A and bAb \in A,

    f(μ A(a,b)) Bμ B(f(a),f(b))f(\mu_A(a, b)) \sim_B \mu_B(f(a), f(b))

Theorem

Let AA be a ring setoid, and let A/A / \sim be its quotient set. Then the function []:A(A/)[-]:A \to (A / \sim) which takes an element of AA to its equivalence class is a ring setoid homomorphism.

Last revised on August 19, 2024 at 14:59:11. See the history of this page for a list of all contributions to it.