Unit similarity on the standard finite types

module elementary-number-theory.unit-similarity-standard-finite-types where

Imports

open import elementary-number-theory.congruence-natural-numbers
open import elementary-number-theory.modular-arithmetic-standard-finite-types
open import elementary-number-theory.multiplication-natural-numbers
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.unit-elements-standard-finite-types

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

open import univalent-combinatorics.standard-finite-types

Idea

Two elements x y : Fin k are said to be unit similar if there is a unit element u : Fin k such that mul-Fin u x = y. This relation gives a groupoid structure on Fin k.

Definition

Unit similarity in `Fin k`

sim-unit-Fin :
  (k : ℕ) → Fin k → Fin k → UU lzero
sim-unit-Fin k x y = Σ (unit-Fin k) (λ u → mul-Fin k (pr1 u) x ＝ y)

Unit similarity on `ℕ`

sim-unit-ℕ :
  (k : ℕ) → ℕ → ℕ → UU lzero
sim-unit-ℕ k x y =
  Σ (Σ ℕ (λ l → cong-ℕ k l 1)) (λ l → cong-ℕ k ((pr1 l) *ℕ x) y)

Congruence to `1`

sim-unit-one-ℕ : (k x : ℕ) → UU lzero
sim-unit-one-ℕ k x = Σ ℕ (λ l → cong-ℕ k (l *ℕ x) 1)

Properties

Unit similarity is an equivalence relation

refl-sim-unit-Fin :
  {k : ℕ} (x : Fin k) → sim-unit-Fin k x x
pr1 (refl-sim-unit-Fin {succ-ℕ k} x) = one-unit-Fin
pr2 (refl-sim-unit-Fin {succ-ℕ k} x) = left-unit-law-mul-Fin k x

symm-sim-unit-Fin :
  {k : ℕ} (x y : Fin k) → sim-unit-Fin k x y → sim-unit-Fin k y x
pr1 (symm-sim-unit-Fin {succ-ℕ k} x y (pair (pair u (pair v q)) p)) =
  inv-unit-Fin (pair u (pair v q))
pr2 (symm-sim-unit-Fin {succ-ℕ k} x y (pair (pair u (pair v q)) p)) =
  ( ( ( ap (mul-Fin (succ-ℕ k) v) (inv p)) ∙
        ( inv (associative-mul-Fin (succ-ℕ k) v u x))) ∙
      ( ap (mul-Fin' (succ-ℕ k) x) q)) ∙
    ( left-unit-law-mul-Fin k x)

trans-sim-unit-Fin :
  {k : ℕ} (x y z : Fin k) → sim-unit-Fin k x y → sim-unit-Fin k y z →
  sim-unit-Fin k x z
pr1 (trans-sim-unit-Fin {succ-ℕ k} x y z (pair u p) (pair v q)) =
  mul-unit-Fin (succ-ℕ k) v u
pr2 (trans-sim-unit-Fin {succ-ℕ k} x y z (pair u p) (pair v q)) =
  ( associative-mul-Fin (succ-ℕ k) (pr1 v) (pr1 u) x) ∙
  ( ap (mul-Fin (succ-ℕ k) (pr1 v)) p ∙ q)

A natural number `x` is congruent to `1` modulo `k+1` if and only if `[x]_{k+1}` is unit similar to `1`.

is-unit-similar-one-sim-unit-mod-succ-ℕ :
  (k x : ℕ) → sim-unit-Fin (succ-ℕ k) (mod-succ-ℕ k x) (one-Fin k) →
  sim-unit-one-ℕ (succ-ℕ k) x
pr1 (is-unit-similar-one-sim-unit-mod-succ-ℕ k x (pair u p)) =
  nat-Fin (succ-ℕ k) (pr1 u)
pr2 (is-unit-similar-one-sim-unit-mod-succ-ℕ k x (pair u p)) =
  cong-eq-mod-succ-ℕ k
    ( (nat-Fin (succ-ℕ k) (pr1 u)) *ℕ x)
    ( 1)
    ( ( eq-mod-succ-cong-ℕ k
        ( (nat-Fin (succ-ℕ k) (pr1 u)) *ℕ x)
        ( (nat-Fin (succ-ℕ k) (pr1 u)) *ℕ (nat-Fin (succ-ℕ k) (mod-succ-ℕ k x)))
        ( scalar-invariant-cong-ℕ
          ( succ-ℕ k)
          ( x)
          ( nat-Fin (succ-ℕ k) (mod-succ-ℕ k x))
          ( nat-Fin (succ-ℕ k) (pr1 u))
          ( symm-cong-ℕ
            ( succ-ℕ k)
            ( nat-Fin (succ-ℕ k) (mod-succ-ℕ k x))
            ( x)
            ( cong-nat-mod-succ-ℕ k x)))) ∙
      ( p))