# Rational commutative monoids

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-09-13.

module group-theory.rational-commutative-monoids where

Imports
open import elementary-number-theory.natural-numbers

open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.identity-types
open import foundation.propositions
open import foundation.universe-levels

open import group-theory.commutative-monoids
open import group-theory.monoids
open import group-theory.powers-of-elements-commutative-monoids


## Idea

A rational commutative monoid is a commutative monoid (M,0,+) in which the map x ↦ nx is invertible for every natural number n > 0. This condition implies that we can invert the natural numbers in M, which are the elements of the form n1 in M.

Note: Since we usually write commutative monoids multiplicatively, the condition that a commutative monoid is rational is that the map x ↦ xⁿ is invertible for every natural number n > 0. However, for rational commutative monoids we will write the binary operation additively.

## Definition

### The predicate of being a rational commutative monoid

module _
{l : Level} (M : Commutative-Monoid l)
where

is-rational-prop-Commutative-Monoid : Prop l
is-rational-prop-Commutative-Monoid =
Π-Prop ℕ
( λ n →
is-equiv-Prop (power-Commutative-Monoid M (succ-ℕ n)))

is-rational-Commutative-Monoid : UU l
is-rational-Commutative-Monoid =
type-Prop is-rational-prop-Commutative-Monoid

is-prop-is-rational-Commutative-Monoid :
is-prop is-rational-Commutative-Monoid
is-prop-is-rational-Commutative-Monoid =
is-prop-type-Prop is-rational-prop-Commutative-Monoid


### Rational commutative monoids

Rational-Commutative-Monoid : (l : Level) → UU (lsuc l)
Rational-Commutative-Monoid l =
Σ (Commutative-Monoid l) is-rational-Commutative-Monoid

module _
{l : Level} (M : Rational-Commutative-Monoid l)
where

commutative-monoid-Rational-Commutative-Monoid : Commutative-Monoid l
commutative-monoid-Rational-Commutative-Monoid = pr1 M

monoid-Rational-Commutative-Monoid : Monoid l
monoid-Rational-Commutative-Monoid =
monoid-Commutative-Monoid commutative-monoid-Rational-Commutative-Monoid

type-Rational-Commutative-Monoid : UU l
type-Rational-Commutative-Monoid =
type-Commutative-Monoid commutative-monoid-Rational-Commutative-Monoid

(x y : type-Rational-Commutative-Monoid) →
type-Rational-Commutative-Monoid
mul-Commutative-Monoid commutative-monoid-Rational-Commutative-Monoid

zero-Rational-Commutative-Monoid : type-Rational-Commutative-Monoid
zero-Rational-Commutative-Monoid =
unit-Commutative-Monoid commutative-monoid-Rational-Commutative-Monoid

(x y z : type-Rational-Commutative-Monoid) →
( z) ＝
( x)
associative-mul-Commutative-Monoid
commutative-monoid-Rational-Commutative-Monoid

(x : type-Rational-Commutative-Monoid) →
left-unit-law-mul-Commutative-Monoid
commutative-monoid-Rational-Commutative-Monoid

(x : type-Rational-Commutative-Monoid) →
right-unit-law-mul-Commutative-Monoid
commutative-monoid-Rational-Commutative-Monoid

multiple-Rational-Commutative-Monoid :
ℕ → type-Rational-Commutative-Monoid → type-Rational-Commutative-Monoid
multiple-Rational-Commutative-Monoid =
power-Commutative-Monoid commutative-monoid-Rational-Commutative-Monoid

is-rational-Rational-Commutative-Monoid :
is-rational-Commutative-Monoid
commutative-monoid-Rational-Commutative-Monoid
is-rational-Rational-Commutative-Monoid = pr2 M