Kernel span diagrams of maps

Content created by Egbert Rijke.

Created on 2024-01-28.
Last modified on 2024-01-28.

module foundation.kernel-span-diagrams-of-maps where
Imports 
open import foundation.dependent-pair-types
open import foundation.span-diagrams
open import foundation.spans
open import foundation.universe-levels

open import foundation-core.function-types
open import foundation-core.identity-types

Idea

Consider a map f : A → B. The kernel span diagram of f is the span diagram

      pr1                           pr1 ∘ pr2
  A <----- Σ (x y : A), f x ＝ f y -----------> A.

We call this the kernel span diagram, since the pair (pr1 , pr1 ∘ pr2) is often called the kernel pair of a map.

Definitions

Kernel span diagrams of maps

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

  spanning-type-kernel-span : UU (l1 ⊔ l2)
  spanning-type-kernel-span =
    Σ A (λ x → Σ A (λ y → f x ＝ f y))

  left-map-kernel-span :
    spanning-type-kernel-span → A
  left-map-kernel-span = pr1

  right-map-kernel-span :
    spanning-type-kernel-span → A
  right-map-kernel-span = pr1 ∘ pr2

  kernel-span : span (l1 ⊔ l2) A A
  pr1 kernel-span =
    spanning-type-kernel-span
  pr1 (pr2 kernel-span) =
    left-map-kernel-span
  pr2 (pr2 kernel-span) =
    right-map-kernel-span

  domain-kernel-span-diagram : UU l1
  domain-kernel-span-diagram = A

  codomain-kernel-span-diagram : UU l1
  codomain-kernel-span-diagram = A

  kernel-span-diagram : span-diagram l1 l1 (l1 ⊔ l2)
  pr1 kernel-span-diagram = domain-kernel-span-diagram
  pr1 (pr2 kernel-span-diagram) = codomain-kernel-span-diagram
  pr2 (pr2 kernel-span-diagram) = kernel-span

Recent changes