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
- 2023-09-12. Egbert Rijke. Factoring out whiskering (#756).
- 2023-08-07. Egbert Rijke. Normalizers, normal closures, normal cores, and centralizers (#693).
- 2023-06-25. Fredrik Bakke, louismntnu, fernabnor, Egbert Rijke and Julian KG. Posets are categories, and refactor binary relations (#665).
- 2023-06-15. Egbert Rijke. Replace
isretr
withis-retraction
andissec
withis-section
(#659). - 2023-06-10. Egbert Rijke. cleaning up transport and dependent identifications files (#650).