Sections

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Julian KG, fernabnor and louismntnu.

Created on 2022-02-04.
Last modified on 2023-09-12.

module foundation-core.sections where
Imports 
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import foundation-core.function-types
open import foundation-core.homotopies
open import foundation-core.whiskering-homotopies

Idea

A section is a map that has a left inverse, i.e. a retraction. Thus, s : B → A is a section of f : A → B if the composition f ∘ s is homotopic to the identity at B.

For example, every dependent function induces a section of the projection map.

Definition

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

  section : UU (l1 ⊔ l2)
  section = Σ (B → A) (λ s → (f ∘ s) ~ id)

  map-section : section → B → A
  map-section = pr1

  is-section-map-section : (s : section) → (f ∘ map-section s) ~ id
  is-section-map-section = pr2

Properties

If g ∘ f has a section then g has a section

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

  section-left-factor :
    (g : B → X) (h : A → B) → section (g ∘ h) → section g
  pr1 (section-left-factor g h section-gh) = h ∘ (pr1 section-gh)
  pr2 (section-left-factor g h section-gh) = pr2 section-gh

  section-left-factor-htpy' :
    (f : A → X) (g : B → X) (h : A → B) (H' : (g ∘ h) ~ f) →
    section f → section g
  pr1 (section-left-factor-htpy' f g h H' section-f) =
    h ∘ (pr1 section-f)
  pr2 (section-left-factor-htpy' f g h H' section-f) =
    (H' ·r pr1 section-f) ∙h (pr2 section-f)

  section-left-factor-htpy :
    (f : A → X) (g : B → X) (h : A → B) (H : f ~ (g ∘ h)) →
    section f → section g
  section-left-factor-htpy f g h H section-f =
    section-left-factor-htpy' f g h (inv-htpy H) section-f

Composites of sections are sections

  section-comp :
    (g : B → X) (h : A → B) → section h → section g → section (g ∘ h)
  pr1 (section-comp g h section-h section-g) = pr1 section-h ∘ pr1 section-g
  pr2 (section-comp g h section-h section-g) =
    (g ·l (pr2 section-h ·r (pr1 section-g))) ∙h (pr2 section-g)

  section-comp-htpy :
    (f : A → X) (g : B → X) (h : A → B) (H : f ~ (g ∘ h)) →
    section h → section g → section f
  pr1 (section-comp-htpy f g h H section-h section-g) =
    pr1 (section-comp g h section-h section-g)
  pr2 (section-comp-htpy f g h H section-h section-g) =
    (H ·r pr1 (section-comp g h section-h section-g)) ∙h
    (pr2 (section-comp g h section-h section-g))

  inv-triangle-section :
    (f : A → X) (g : B → X) (h : A → B) (H : f ~ (g ∘ h))
    (section-h : section h) → (f ∘ (pr1 section-h)) ~ g
  inv-triangle-section h g f H section-h =
    (H ·r (pr1 section-h)) ∙h (g ·l (pr2 section-h))

  triangle-section :
    (f : A → X) (g : B → X) (h : A → B) (H : f ~ (g ∘ h))
    (section-h : section h) → g ~ (f ∘ (pr1 section-h))
  triangle-section h g f H section-h =
    inv-htpy (inv-triangle-section h g f H section-h)

Recent changes