module 1Lab.Function.Antisurjection where

Antisurjective functions🔗

A function is antisurjective if there merely exists some with an empty fibre. This is constructively stronger than being non-surjective, which states that it is not the case that all fibres are (merely) inhabited.

is-antisurjective : (A  B)  Type _
is-antisurjective {B = B} f = ∃[ b ∈ B ] (¬ (fibre f b))

Likewise, a function is split antisurjective if there is some with an empty fibre. Note that this is a structure on a function, not a property, as there may be many ways a function fails to be surjective!

split-antisurjective : (A  B)  Type _
split-antisurjective {B = B} f = Σ[ b ∈ B ] (¬ (fibre f b))

As the name suggests, antisurjective functions are not surjective.

split-antisurj→not-surjective
  : {f : A  B}
   split-antisurjective f
   ¬ (is-surjective f)
split-antisurj→not-surjective (b , ¬fib) f-s =
  rec!  a p  ¬fib (a , p)) (f-s b)

is-antisurj→not-surjective
  : {f : A  B}
   is-antisurjective f
   ¬ (is-surjective f)
is-antisurj→not-surjective f-as =
  rec!  b ¬fib  split-antisurj→not-surjective (b , ¬fib)) f-as

If is antisurjective and is an arbitrary function, then is also antisurjective.

split-antisurj-∘l
  : {f : B  C} {g : A  B}
   split-antisurjective f
   split-antisurjective (f ∘ g)
split-antisurj-∘l {g = g} (c , ¬fib) = c , ¬fib ∘ Σ-map g  p  p)

is-antisurj-∘l
  : {f : B  C} {g : A  B}
   is-antisurjective f
   is-antisurjective (f ∘ g)
is-antisurj-∘l {f = f} {g = g} = ∥-∥-map split-antisurj-∘l

If is injective and is antisurjective, then is also antisurjective.

inj+split-antisurj→split-antisurj
  : {f : B  C} {g : A  B}
   injective f
   split-antisurjective g
   split-antisurjective (f ∘ g)
inj+split-antisurj→split-antisurj {f = f} f-inj (b , ¬fib) =
  f b , ¬fib ∘ Σ-map₂ f-inj

inj+is-antisurj→is-antisurj
  : {f : B  C} {g : A  B}
   injective f
   is-antisurjective g
   is-antisurjective (f ∘ g)
inj+is-antisurj→is-antisurj f-inj =
  ∥-∥-map (inj+split-antisurj→split-antisurj f-inj)
split-antisurj-cancelr
  : {f : B  C} {g : A  B}
   is-surjective g
   split-antisurjective (f ∘ g)
   split-antisurjective f
split-antisurj-cancelr {f = f} {g = g} surj (c , ¬fib) =
  c , rec! λ b p  rec!  a q  ¬fib (a , ap f q ∙ p)) (surj b)

is-antisurj-cancelr
  : {f : B  C} {g : A  B}
   is-surjective g
   is-antisurjective (f ∘ g)
   is-antisurjective f
is-antisurj-cancelr surj = ∥-∥-map (split-antisurj-cancelr surj)