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.
: (A → B) → Type _
is-antisurjective {B = B} f = ∃[ b ∈ B ] (¬ (fibre f b)) is-antisurjective
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!
: (A → B) → Type _
split-antisurjective {B = B} f = Σ[ b ∈ B ] (¬ (fibre f b)) split-antisurjective
As the name suggests, antisurjective functions are not surjective.
split-antisurj→not-surjective: {f : A → B}
→ split-antisurjective f
→ ¬ (is-surjective f)
(b , ¬fib) f-s =
split-antisurj→not-surjective (λ a p → ¬fib (a , p)) (f-s b)
rec!
is-antisurj→not-surjective: {f : A → B}
→ is-antisurjective f
→ ¬ (is-surjective f)
=
is-antisurj→not-surjective f-as (λ b ¬fib → split-antisurj→not-surjective (b , ¬fib)) f-as rec!
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)
{g = g} (c , ¬fib) = c , ¬fib ∘ Σ-map g (λ p → p)
split-antisurj-∘l
is-antisurj-∘l: {f : B → C} {g : A → B}
→ is-antisurjective f
→ is-antisurjective (f ∘ g)
{f = f} {g = g} = ∥-∥-map split-antisurj-∘l is-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)
{f = f} f-inj (b , ¬fib) =
inj+split-antisurj→split-antisurj
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 (inj+split-antisurj→split-antisurj f-inj) ∥-∥-map
split-antisurj-cancelr: {f : B → C} {g : A → B}
→ is-surjective g
→ split-antisurjective (f ∘ g)
→ split-antisurjective f
{f = f} {g = g} surj (c , ¬fib) =
split-antisurj-cancelr λ b p → rec! (λ a q → ¬fib (a , ap f q ∙ p)) (surj b)
c , rec!
is-antisurj-cancelr: {f : B → C} {g : A → B}
→ is-surjective g
→ is-antisurjective (f ∘ g)
→ is-antisurjective f
= ∥-∥-map (split-antisurj-cancelr surj) is-antisurj-cancelr surj