Repetitions of values

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Victor Blanchi.

Created on 2023-04-08.
Last modified on 2024-04-11.

module univalent-combinatorics.repetitions-of-values where

open import foundation.repetitions-of-values public
Imports 
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.well-ordering-principle-standard-finite-types

open import foundation.cartesian-product-types
open import foundation.decidable-types
open import foundation.identity-types
open import foundation.injective-maps
open import foundation.negated-equality
open import foundation.negation
open import foundation.sets

open import univalent-combinatorics.decidable-dependent-function-types
open import univalent-combinatorics.decidable-propositions
open import univalent-combinatorics.dependent-pair-types
open import univalent-combinatorics.equality-standard-finite-types
open import univalent-combinatorics.standard-finite-types

Idea

A repetition of values of a function f : A → B consists of a pair a a' : A such that a ≠ a' and f a ＝ f a'.

Properties

If f : Fin k → Fin l is not injective, then it has a repetition of values

b

repetition-of-values-is-not-injective-Fin :
  (k l : ℕ) (f : Fin k → Fin l) →
  is-not-injective f → repetition-of-values f
repetition-of-values-is-not-injective-Fin k l f N =
  pair (pair x (pair y (pr2 w))) (pr1 w)
  where
  u : Σ (Fin k) (λ x → ¬ ((y : Fin k) → f x ＝ f y → x ＝ y))
  u =
    exists-not-not-for-all-Fin k
      ( λ x →
        is-decidable-Π-Fin k
          ( λ y →
            is-decidable-function-type
              ( has-decidable-equality-Fin l (f x) (f y))
              ( has-decidable-equality-Fin k x y)))
      ( λ f → N (λ {x} {y} → f x y))
  x : Fin k
  x = pr1 u
  H : ¬ ((y : Fin k) → f x ＝ f y → x ＝ y)
  H = pr2 u
  v : Σ (Fin k) (λ y → ¬ (f x ＝ f y → x ＝ y))
  v = exists-not-not-for-all-Fin k
      ( λ y →
        is-decidable-function-type
          ( has-decidable-equality-Fin l (f x) (f y))
          ( has-decidable-equality-Fin k x y))
      ( H)
  y : Fin k
  y = pr1 v
  K : ¬ (f x ＝ f y → x ＝ y)
  K = pr2 v
  w : (f x ＝ f y) × (x ≠ y)
  w = exists-not-not-for-all-count
      ( λ _ → Id x y)
      ( λ _ →
        has-decidable-equality-Fin k x y)
      ( count-is-decidable-is-prop
        ( is-set-Fin l (f x) (f y))
        ( has-decidable-equality-Fin l (f x) (f y)))
      ( K)

On the standard finite sets, is-repetition-of-values f x is decidable

is-decidable-is-repetition-of-values-Fin :
  {k l : ℕ} (f : Fin k → Fin l) (x : Fin k) →
  is-decidable (is-repetition-of-values f x)
is-decidable-is-repetition-of-values-Fin f x =
  is-decidable-Σ-Fin
    ( λ y →
      is-decidable-product
        ( is-decidable-neg (has-decidable-equality-Fin x y))
        ( has-decidable-equality-Fin (f x) (f y)))

On the standard finite sets, is-repeated-value f x is decidable

is-decidable-is-repeated-value-Fin :
  (k l : ℕ) (f : Fin k → Fin l) (x : Fin k) →
  is-decidable (is-repeated-value f x)
is-decidable-is-repeated-value-Fin k l f x =
  is-decidable-Σ-Fin k
    ( λ y →
      is-decidable-product
        ( is-decidable-neg (has-decidable-equality-Fin k x y))
        ( has-decidable-equality-Fin l (f x) (f y)))

The predicate that f maps two different elements to the same value

This remains to be defined. #748

On the standard finite sets, has-repetition-of-values f is decidable

is-decidable-has-repetition-of-values-Fin :
  (k l : ℕ) (f : Fin k → Fin l) → is-decidable (has-repetition-of-values f)
is-decidable-has-repetition-of-values-Fin k l f =
  is-decidable-Σ-Fin k (is-decidable-is-repetition-of-values-Fin k l f)

If f is not injective, then it has a repetition-of-values

is-injective-map-Fin-zero-Fin :
  {k : ℕ} (f : Fin zero-ℕ → Fin k) → is-injective f
is-injective-map-Fin-zero-Fin f {()}

is-injective-map-Fin-one-Fin : {k : ℕ} (f : Fin 1 → Fin k) → is-injective f
is-injective-map-Fin-one-Fin f {inr star} {inr star} p = refl

has-repetition-of-values-is-not-injective-Fin :
  (k l : ℕ) (f : Fin l → Fin k) →
  is-not-injective f → has-repetition-of-values f
has-repetition-of-values-is-not-injective-Fin k zero-ℕ f H =
  ex-falso (H (is-injective-map-Fin-zero-Fin {k} f))
has-repetition-of-values-is-not-injective-Fin k (succ-ℕ l) f H with
  is-decidable-is-repetition-of-values-Fin (succ-ℕ l) k f (inr star)
... | inl r = pair (inr star) r
... | inr g =
  α (has-repetition-of-values-is-not-injective-Fin k l (f ∘ inl) K)
  where
  K : is-not-injective (f ∘ inl)
  K I = H (λ {x} {y} → J x y)
    where
    J : (x y : Fin (succ-ℕ l)) → Id (f x) (f y) → Id x y
    J (inl x) (inl y) p = ap inl (I p)
    J (inl x) (inr star) p =
      ex-falso (g (triple (inl x) (Eq-Fin-eq (succ-ℕ l)) (inv p)))
    J (inr star) (inl y) p =
      ex-falso (g (triple (inl y) (Eq-Fin-eq (succ-ℕ l)) p))
    J (inr star) (inr star) p = refl
    α : has-repetition-of-values (f ∘ inl) → has-repetition-of-values f
    α (pair x (pair y (pair h q))) =
      pair (inl x) (pair (inl y) (pair (λ r → h (is-injective-inl r)) q))

Recent changes