Split Surjectivity

src/1Lab/Classical.lagda.md

@@ -122,7 +122,7 @@ Surjections-split =
   ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → is-set A → is-set B
   → (f : A → B)
   → is-surjective f
-  → ∥ (∀ b → fibre f b) ∥
+  → is-split-surjective f
 ```
 
 We show that these two statements are logically equivalent^[they are also

src/1Lab/Equiv.lagda.md

@@ -71,8 +71,9 @@ Here in the 1Lab, we formalise three acceptable notions of equivalence:
 <!--
 ```agda
 private variable
-  ℓ₁ ℓ₂ : Level
+  ℓ ℓ₁ ℓ₂ : Level
   A B C : Type ℓ₁
+  P : A → Type ℓ
 ```
 -->
 
@@ -1086,7 +1087,37 @@ infix  3 _≃∎
 infix 21 _≃_
 
 syntax ≃⟨⟩-syntax x q p = x ≃⟨ p ⟩ q
+```
+-->
+
+## Some useful equivalences
 
+We can extend `subst`{.Agda} to an equivalence between `Σ[ y ∈ A ] (y ≡ x × P y)`
+and `P x` for every `x : A` and `P : A → Type`.
+
+```agda
+subst≃
+  : (x : A) → (Σ[ y ∈ A ] (y ≡ x × P y)) ≃ P x
+subst≃ {A = A} {P = P} x = Iso→Equiv (to , iso from invr invl)
+  where
+    to : Σ[ y ∈ A ] (y ≡ x × P y) → P x
+    to (y , y=x , py) = subst P y=x py
+
+    from : P x → Σ[ y ∈ A ] (y ≡ x × P y)
+    from px = x , refl , px
+
+    invr : is-right-inverse from to
+    invr = transport-refl
+
+    invl : is-left-inverse from to
+    invl (y , y=x , py) i =
+      (y=x (~ i)) ,
+      (λ j → y=x (~ i ∨ j)) ,
+      transp (λ j → P (y=x (~ i ∧ j))) i py
+```
+
+<!--
+```agda
 lift-inj
   : ∀ {ℓ ℓ'} {A : Type ℓ} {a b : A}
   → lift {ℓ = ℓ'} a ≡ lift {ℓ = ℓ'} b → a ≡ b

src/1Lab/Function/Surjection.lagda.md

@@ -4,7 +4,9 @@ open import 1Lab.Function.Embedding
 open import 1Lab.Reflection.HLevel
 open import 1Lab.HIT.Truncation
 open import 1Lab.HLevel.Closure
+open import 1Lab.Type.Sigma
 open import 1Lab.Inductive
+open import 1Lab.Type.Pi
 open import 1Lab.HLevel
 open import 1Lab.Equiv
 open import 1Lab.Path
@@ -22,8 +24,10 @@ module 1Lab.Function.Surjection where
 <!--
 ```agda
 private variable
-  ℓ ℓ' : Level
+  ℓ ℓ' ℓ'' : Level
   A B C : Type ℓ
+  P Q : A → Type ℓ'
+  f g : A → B
 ```
 -->
 
@@ -99,6 +103,19 @@ is-equiv→is-surjective : {f : A → B} → is-equiv f → is-surjective f
 is-equiv→is-surjective eqv x = inc (eqv .is-eqv x .centre)
 ```
 
+Surjections also are closed under a weaker form of [[two-out-of-three]]:
+if $f circ g$ is surjective, then $f$ must also be surjective.
+
+```agda
+is-surjective-cancelr
+  : {f : B → C} {g : A → B}
+  → is-surjective (f ∘ g)
+  → is-surjective f
+is-surjective-cancelr {g = g} fgs c = do
+  (fg*x , p) ← fgs c
+  pure (g fg*x , p)
+```
+
 <!--
 ```agda
 Equiv→Cover : A ≃ B → A ↠ B
@@ -144,3 +161,263 @@ injective-surjective→is-equiv! =
   injective-surjective→is-equiv (hlevel 2)
 ```
 -->
+
+## Surjectivity and images
+
+A map $f : A \to B$ if and only if the inclusion of the image of $f$ into $B$
+is an [[equivalence]].
+
+```agda
+surjective-iff-image-equiv
+  : ∀ {f : A → B}
+  → is-surjective f ≃ is-equiv {A = image f} fst
+```
+
+The forward direction is almost immediate: surjectivity of $f$ means
+that $B$ includes into its image, so it must be an equivalence. For the
+reverse direction, suppose that the inclusion of the image of $f$ is an
+equivalence. This lets us find some point in the image of $f$ for every $b : B$.
+Moreover, this point in the image must lie in a fibre of $b$, as the inclusion is
+an equivalence.
+
+```agda
+surjective-iff-image-equiv {f = f} = prop-ext! to from where
+
+  to : is-surjective f → is-equiv fst
+  to f-surj =
+    is-iso→is-equiv $
+      iso (λ b → b , f-surj b)
+        (λ _ → refl)
+        (λ _ → Σ-prop-path! refl)
+
+  from : is-equiv fst → is-surjective f
+  from im-eqv b = subst (λ b → ∥ fibre f b ∥) (equiv→counit im-eqv b) (snd (equiv→inverse im-eqv b))
+```
+
+# Split surjective functions
+
+:::{.definition #surjective-splitting}
+A **surjective splitting** of a function $f : A \to B$ consists of a designated
+element of the fibre $f^*b$ for each $b : B$.
+:::
+
+```agda
+surjective-splitting : (A → B) → Type _
+surjective-splitting f = ∀ b → fibre f b
+```
+
+Note that unlike "being surjective", a surjective splitting of $f$ is a *structure*
+on $f$, not a property. This difference becomes particularly striking when we
+look at functions into [[contractible]] types: if $B$ is contractible,
+then the type of surjective splittings of a function $f : A \to B$ is equivalent to $A$.
+
+```agda
+cod-contr→surjective-splitting≃dom
+  : (f : A → B)
+  → is-contr B
+  → surjective-splitting f ≃ A
+```
+
+First, recall that functions out of contractible types are equivalences, so
+a choice of fibres $(b : B) \to f^{-1}(b)$ is equivalent to a single fibre
+at the centre of contraction of $B$. Moreover, the type of paths in $B$ is
+also contractible, so the type of fibres of $f : A \to B$ is equivalent to $A$.
+
+```agda
+cod-contr→surjective-splitting≃dom {A = A} f B-contr =
+  (∀ b → fibre f b)         ≃⟨ Π-contr-eqv B-contr ⟩
+  fibre f (B-contr .centre) ≃⟨ Σ-contract (λ _ → Path-is-hlevel 0 B-contr) ⟩
+  A                         ≃∎
+```
+
+In contrast, if $B$ is contractible, then $f : A \to B$ is surjective if and only
+if $A$ is merely inhabited.
+
+```agda
+cod-contr→is-surjective-iff-dom-inhab
+  : (f : A → B)
+  → is-contr B
+  → is-surjective f ≃ ∥ A ∥
+cod-contr→is-surjective-iff-dom-inhab {A = A} f B-contr =
+  (∀ b → ∥ fibre f b ∥) ≃⟨ unique-choice≃ B-contr ⟩
+  ∥ (∀ b → fibre f b) ∥ ≃⟨ ∥-∥-ap (cod-contr→surjective-splitting≃dom f B-contr) ⟩
+  ∥ A ∥                 ≃∎
+```
+
+In light of this, we provide the following definition.
+
+:::{.definition #split-surjective}
+A function $f : A \to B$ is **split surjective** if there merely exists a
+surjective splitting of $f$.
+:::
+
+```agda
+is-split-surjective : (A → B) → Type _
+is-split-surjective f = ∥ surjective-splitting f ∥
+```
+
+Every split surjective map is surjective.
+
+```agda
+is-split-surjective→is-surjective : is-split-surjective f → is-surjective f
+is-split-surjective→is-surjective f-split-surj b = do
+  f-splitting ← f-split-surj
+  pure (f-splitting b)
+```
+
+Note that we do not have a converse to this constructively: the statement that
+every surjective function between [[sets]] splits is [[equivalent to the axiom of choice|axiom-of-choice]]!
+
+
+## Split surjective functions and sections
+
+The type of surjective splittings of a function $f : A \to B$ is equivalent
+to the type of sections of $f$, EG: functions $s : B \to A$ with $f \circ s = \id$.
+
+```agda
+section≃surjective-splitting
+  : (f : A → B)
+  → (Σ[ s ∈ (B → A) ] is-right-inverse s f) ≃ surjective-splitting f
+```
+
+Somewhat surprisingly, this is an immediate consequence of the fact that
+sigma types distribute over pi types!
+
+```agda
+section≃surjective-splitting {A = A} {B = B} f =
+  (Σ[ s ∈ (B → A) ] ((x : B) → f (s x) ≡ x)) ≃˘⟨ Σ-Π-distrib ⟩
+  ((b : B) → Σ[ a ∈ A ] f a ≡ b)             ≃⟨⟩
+  surjective-splitting f                     ≃∎
+```
+
+This means that a function $f$ is split surjective if and only if there
+[[merely]] exists some section of $f$.
+
+```agda
+exists-section-iff-split-surjective
+  : (f : A → B)
+  → (∃[ s ∈ (B → A) ] is-right-inverse s f) ≃ is-split-surjective f
+exists-section-iff-split-surjective f =
+  ∥-∥-ap (section≃surjective-splitting f)
+```
+
+## Closure properties of split surjective functions
+
+Like their non-split counterparts, split surjective functions are closed under composition.
+
+```agda
+∘-surjective-splitting
+  : surjective-splitting f
+  → surjective-splitting g
+  → surjective-splitting (f ∘ g)
+
+∘-is-split-surjective
+  : is-split-surjective f
+  → is-split-surjective g
+  → is-split-surjective (f ∘ g)
+```
+
+<details>
+<summary> The proof is essentially identical to the non-split case.
+</summary>
+```agda
+∘-surjective-splitting {f = f} f-split g-split c =
+  let (f*c , p) = f-split c
+      (g*f*c , q) = g-split f*c
+  in g*f*c , ap f q ∙ p
+
+∘-is-split-surjective fs gs = ⦇ ∘-surjective-splitting fs gs ⦈
+
+```
+</details>
+
+Every equivalence can be equipped with a surjective splitting, and
+is thus split surjective.
+
+```agda
+is-equiv→surjective-splitting
+  : is-equiv f
+  → surjective-splitting f
+
+is-equiv→is-split-surjective
+  : is-equiv f
+  → is-split-surjective f
+```
+
+This follows immediately from the definition of equivalences: if the
+type of fibres is contractible, then we can pluck the fibre we need
+out of the centre of contraction!
+
+```agda
+is-equiv→surjective-splitting f-equiv b =
+  f-equiv .is-eqv b .centre
+
+is-equiv→is-split-surjective f-equiv =
+  pure (is-equiv→surjective-splitting f-equiv)
+```
+
+Split surjective functions also satisfy left two-out-of-three.
+
+```agda
+surjective-splitting-cancelr
+  : surjective-splitting (f ∘ g)
+  → surjective-splitting f
+
+is-split-surjective-cancelr
+  : is-split-surjective (f ∘ g)
+  → is-split-surjective f
+```
+
+<details>
+<summary>These proofs are also essentially identical to the non-split versions.
+</summary>
+```agda
+surjective-splitting-cancelr {g = g} fg-split c =
+  let (fg*c , p) = fg-split c
+  in g fg*c , p
+
+is-split-surjective-cancelr fg-split =
+  map surjective-splitting-cancelr fg-split
+```
+</details>
+
+A function is an equivalence if and only if it is a split-surjective
+[[embedding]].
+
+```agda
+embedding-split-surjective≃is-equiv
+  : {f : A → B}
+  → (is-embedding f × is-split-surjective f) ≃ is-equiv f
+embedding-split-surjective≃is-equiv {f = f} =
+  prop-ext!
+    (λ (f-emb , f-split-surj) →
+      embedding-surjective→is-equiv
+        f-emb
+        (is-split-surjective→is-surjective f-split-surj))
+    (λ f-equiv → is-equiv→is-embedding f-equiv , is-equiv→is-split-surjective f-equiv)
+```
+
+# Surjectivity and connectedness
+
+If $f : A \to B$ is a function out of a [[contractible]] type $A$,
+then $f$ is surjective if and only if $B$ is a [[pointed connected type]], where
+the basepoint of $B$ is given by $f$ applied to the centre of contraction of $A$.
+
+```agda
+contr-dom-surjective-iff-connected-cod
+  : ∀ {f : A → B}
+  → (A-contr : is-contr A)
+  → is-surjective f ≃ ((x : B) → ∥ x ≡ f (A-contr .centre) ∥)
+```
+
+To see this, note that the type of fibres of $f$ over $x$ is equivalent
+to the type of paths $x = f(a_{bullet})$, where $a_{\bullet}$ is the centre
+of contraction of $A$.
+
+```agda
+contr-dom-surjective-iff-connected-cod {A = A} {B = B} {f = f} A-contr =
+  Π-cod≃ (λ b → ∥-∥-ap (Σ-contr-eqv A-contr ∙e sym-equiv))
+```
+
+This correspondence is not a coincidence: surjective maps are a special case
+of a more general family of maps called [[connected maps]].