Hilbert ε-operators on maps

Content created by Fredrik Bakke.

Created on 2025-08-14.
Last modified on 2025-08-14.

module foundation.hilbert-epsilon-operators-maps where
Imports
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.hilberts-epsilon-operators
open import foundation.images
open import foundation.universe-levels

open import foundation-core.equivalences
open import foundation-core.fibers-of-maps
open import foundation-core.injective-maps
open import foundation-core.sections

Idea

A Hilbert ε-operator on a map is a family of Hilbert ε-operators on its fibers. I.e., for every y : B there is an operator

  ε_y : ║ fiber f y ║₋₁ → fiber f y.

Some authors also refer to this as split support [KECA17]. Contrary to Hilbert, we do not assume that such an operator exists for every map.

Definitions

The structure of a Hilbert ε-operator on a map

ε-operator-map :
  {l1 l2 : Level} {A : UU l1} {B : UU l2}  (A  B)  UU (l1  l2)
ε-operator-map {B = B} f = (y : B)  ε-operator-Hilbert (fiber f y)

Properties

ε-operators on maps are sections of the image-unit

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A  B}
  where

  map-section-map-unit-im-ε-operator-map : ε-operator-map f  im f  A
  map-section-map-unit-im-ε-operator-map ε (y , p) = pr1 (ε y p)

  is-section-map-section-map-unit-im-ε-operator-map :
    (ε : ε-operator-map f) 
    is-section (map-unit-im f) (map-section-map-unit-im-ε-operator-map ε)
  is-section-map-section-map-unit-im-ε-operator-map ε (y , p) =
    eq-Eq-im f _ _ (pr2 (ε y p))

  section-map-unit-im-ε-operator-map :
    ε-operator-map f  section (map-unit-im f)
  section-map-unit-im-ε-operator-map ε =
    ( map-section-map-unit-im-ε-operator-map ε ,
      is-section-map-section-map-unit-im-ε-operator-map ε)

Injective maps with ε-operators are embeddings

Proof. Given a map f : A → B equipped with an ε-operator, then we have a section of the image projection map A ↠ im f given by the Hilbert ε-operator. Now, by injectivity of f we the image projection map must be an equivalence. Hence, f is a composite of embeddings and so must be an embedding as well.

    im f
    ↟ ⋮   \
    │ ⋮ ~   \
    │ ↓       ∨
     A ──────→ B
          f
module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A  B}
  where

  is-emb-is-injective-ε-operator-map :
    ε-operator-map f  is-injective f  is-emb f
  is-emb-is-injective-ε-operator-map ε H =
    is-emb-comp
      ( inclusion-im f)
      ( map-unit-im f)
      ( is-emb-inclusion-im f)
      ( is-emb-is-equiv
        ( is-equiv-is-injective
          ( section-map-unit-im-ε-operator-map ε)
          ( is-injective-right-factor (inclusion-im f) (map-unit-im f) H)))

References

[KECA17]
Nicolai Kraus, Martín Escardó, Thierry Coquand, and Thorsten Altenkirch. Notions of Anonymous Existence in Martin-Löf Type Theory. Logical Methods in Computer Science, 03 2017. URL: https://lmcs.episciences.org/3217, arXiv:1610.03346, doi:10.23638/LMCS-13(1:15)2017.

Recent changes