Odd roots of real numbers

Content created by Louis Wasserman.

Created on 2026-02-07.
Last modified on 2026-02-07.

{-# OPTIONS --lossy-unification #-}

module real-numbers.odd-roots-real-numbers where
Imports 
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.parity-natural-numbers

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

open import real-numbers.cofinal-and-coinitial-strictly-increasing-pointwise-epsilon-delta-continuous-endomaps-real-numbers
open import real-numbers.dedekind-real-numbers
open import real-numbers.increasing-endomaps-real-numbers
open import real-numbers.powers-real-numbers
open import real-numbers.strictly-increasing-endomaps-real-numbers

Idea

For odd , the function x ↦ \root{n}{x} is defined on the real numbers as the inverse function to the power operation .

Definition

module _
  (l : Level)
  (n : ℕ)
  (odd-n : is-odd-ℕ n)
  where

  cofinal-and-coinitial-strictly-increasing-pointwise-ε-δ-continuous-endomap-power-is-odd-exponent-ℝ :
    cofinal-and-coinitial-strictly-increasing-pointwise-ε-δ-continuous-endomap-ℝ
      ( l)
      ( l)
  cofinal-and-coinitial-strictly-increasing-pointwise-ε-δ-continuous-endomap-power-is-odd-exponent-ℝ =
    ( ( pointwise-ε-δ-continuous-power-ℝ l n ,
        is-strictly-increasing-power-is-odd-exponent-ℝ l n odd-n) ,
      is-cofinal-power-is-odd-exponent-ℝ l n odd-n ,
      is-coinitial-power-is-odd-exponent-ℝ l n odd-n)

  aut-power-is-odd-exponent-ℝ : Aut (ℝ l)
  aut-power-is-odd-exponent-ℝ =
    aut-cofinal-and-coinitial-strictly-increasing-pointwise-ε-δ-continuous-endomap-ℝ
      ( cofinal-and-coinitial-strictly-increasing-pointwise-ε-δ-continuous-endomap-power-is-odd-exponent-ℝ)

root-is-odd-exponent-ℝ : {l : Level} (n : ℕ) → is-odd-ℕ n → ℝ l → ℝ l
root-is-odd-exponent-ℝ {l} n odd-n =
  map-inv-equiv (aut-power-is-odd-exponent-ℝ l n odd-n)

Properties

For odd n, nth roots are the inverse operation to nth powers

module _
  {l : Level}
  (n : ℕ)
  (odd-n : is-odd-ℕ n)
  (x : ℝ l)
  where

  abstract
    is-section-root-is-odd-exponent-ℝ :
      power-ℝ n (root-is-odd-exponent-ℝ n odd-n x) ＝ x
    is-section-root-is-odd-exponent-ℝ =
      is-section-map-inv-equiv (aut-power-is-odd-exponent-ℝ l n odd-n) x

    is-retraction-root-is-odd-exponent-ℝ :
      root-is-odd-exponent-ℝ n odd-n (power-ℝ n x) ＝ x
    is-retraction-root-is-odd-exponent-ℝ =
      is-retraction-map-inv-equiv (aut-power-is-odd-exponent-ℝ l n odd-n) x

For odd n, the nth root operation preserves strict inequality

module _
  {l : Level}
  (n : ℕ)
  (odd-n : is-odd-ℕ n)
  where

  abstract
    is-strictly-increasing-root-is-odd-exponent-ℝ :
      is-strictly-increasing-endomap-ℝ (root-is-odd-exponent-ℝ {l} n odd-n)
    is-strictly-increasing-root-is-odd-exponent-ℝ =
      is-strictly-increasing-map-inv-cofinal-and-coinitial-strictly-increasing-pointwise-ε-δ-continuous-endomap-ℝ
        ( cofinal-and-coinitial-strictly-increasing-pointwise-ε-δ-continuous-endomap-power-is-odd-exponent-ℝ
          ( l)
          ( n)
          ( odd-n))

For odd n, the nth root operation preserves inequality

module _
  {l : Level}
  (n : ℕ)
  (odd-n : is-odd-ℕ n)
  where

  abstract
    is-increasing-root-is-odd-exponent-ℝ :
      is-increasing-endomap-ℝ (root-is-odd-exponent-ℝ {l} n odd-n)
    is-increasing-root-is-odd-exponent-ℝ =
      is-increasing-is-strictly-increasing-endomap-ℝ
        ( root-is-odd-exponent-ℝ n odd-n)
        ( is-strictly-increasing-root-is-odd-exponent-ℝ n odd-n)

Recent changes