Fibers of maps between finite types

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

Created on 2022-03-31.
Last modified on 2023-09-11.

module univalent-combinatorics.fibers-of-maps where

open import foundation.fibers-of-maps public
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.sums-of-natural-numbers

open import foundation.contractible-types
open import foundation.decidable-types
open import foundation.equality-dependent-pair-types
open import foundation.equivalences
open import foundation.functoriality-dependent-pair-types
open import foundation.identity-types
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.sections
open import foundation.transport-along-identifications
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.universe-levels

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


The fibers of maps between finite types are finite.


If A and B can be counted, then the fibers of a map f : A → B can be counted

count-fiber :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A  B) 
  count A  count B  (y : B)  count (fiber f y)
count-fiber f count-A count-B =
    ( count-B)
    ( count-equiv' (equiv-total-fiber f) count-A)

  sum-number-of-elements-count-fiber :
    {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A  B) 
    (count-A : count A) (count-B : count B) 
      ( sum-count-ℕ count-B
        ( λ x  number-of-elements-count (count-fiber f count-A count-B x)))
      ( number-of-elements-count count-A)
  sum-number-of-elements-count-fiber f count-A count-B =
    sum-number-of-elements-count-fiber-count-Σ count-B
      ( count-equiv' (equiv-total-fiber f) count-A)

  double-counting-fiber :
    {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A  B) (count-A : count A) 
    (count-B : count B) (count-fiber-f : (y : B)  count (fiber f y)) (y : B) 
      ( number-of-elements-count (count-fiber-f y))
      ( number-of-elements-count (count-fiber f count-A count-B y))
  double-counting-fiber f count-A count-B count-fiber-f y =
    double-counting (count-fiber-f y) (count-fiber f count-A count-B y)

Fibers of maps between finite types are finite

  is-finite-fiber :
    {l1 l2 : Level} {X : UU l1} {Y : UU l2} (f : X  Y) 
    is-finite X  is-finite Y  (y : Y)  is-finite (fiber f y)
  is-finite-fiber f is-finite-X is-finite-Y y =
      ( is-finite-X)
      ( is-finite-Prop (fiber f y))
      ( λ H 
          ( is-finite-Y)
          ( is-finite-Prop (fiber f y))
          ( λ K  unit-trunc-Prop (count-fiber f H K y)))

fiber-𝔽 :
  {l1 l2 : Level} (X : 𝔽 l1) (Y : 𝔽 l2) (f : type-𝔽 X  type-𝔽 Y) 
  type-𝔽 Y  𝔽 (l1  l2)
pr1 (fiber-𝔽 X Y f y) = fiber f y
pr2 (fiber-𝔽 X Y f y) =
  is-finite-fiber f (is-finite-type-𝔽 X) (is-finite-type-𝔽 Y) y

  is-finite-fiber-map-section-family :
    {l1 l2 : Level} {A : UU l1} {B : A  UU l2} (b : (x : A)  B x) 
    is-finite (Σ A B)  ((x : A)  is-finite (B x)) 
    (t : Σ A B)  is-finite (fiber (map-section-family b) t)
  is-finite-fiber-map-section-family {l1} {l2} {A} {B} b f g (pair y z) =
      ( ( ( left-unit-law-Σ-is-contr
            ( is-contr-total-path' y)
            ( pair y refl)) ∘e
          ( inv-associative-Σ A
            ( λ x  Id x y)
            ( λ t  Id (tr B (pr2 t) (b (pr1 t))) z))) ∘e
        ( equiv-tot  x  equiv-pair-eq-Σ (pair x (b x)) (pair y z))))
      ( is-finite-eq (has-decidable-equality-is-finite (g y)))

The fibers of maps between finite types are decidable

is-decidable-fiber-count :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A  B) 
  count A  count B  (y : B)  is-decidable (fiber f y)
is-decidable-fiber-count f count-A count-B y =
  is-decidable-count (count-fiber f count-A count-B y)

is-decidable-fiber-Fin :
  {k l : } (f : Fin k  Fin l)  (y : Fin l)  is-decidable (fiber f y)
is-decidable-fiber-Fin {k} {l} f y =
  is-decidable-fiber-count f (count-Fin k) (count-Fin l) y

If f : A → B and B is finite, then A is finite if and only if the fibers of f are finite

equiv-is-finite-domain-is-finite-fiber :
  {l1 l2 : Level} {A : UU l1} 
  (B : 𝔽 l2) (f : A  (type-𝔽 B)) 
  ((b : type-𝔽 B)  is-finite (fiber f b))  is-finite A
equiv-is-finite-domain-is-finite-fiber {A = A} B f =
    ( is-prop-Π  b  is-prop-is-finite (fiber f b)))
    ( is-prop-is-finite A)
    ( λ P 
        ( equiv-total-fiber f)
        ( is-finite-Σ (is-finite-type-𝔽 B) P))
    ( λ P  is-finite-fiber f P ( is-finite-type-𝔽 B))

Recent changes