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
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


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.


Kernel span diagrams of maps

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

  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 =
  pr1 (pr2 kernel-span) =
  pr2 (pr2 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