module 1Lab.Function.Surjection where
Surjectionsπ
A function is a surjection if, for each we have that is, all of its fibres are inhabited. Using the notation for mere existence, we may write this as
which is evidently the familiar notion of surjection.
is-surjective : (A β B) β Type _ is-surjective f = β b β β₯ fibre f b β₯
To abbreviate talking about surjections, we will use the notation pronounced β covers β.
_β _ : Type β β Type β' β Type (β β β') A β B = Ξ£[ f β (A β B) ] is-surjective f
The notion of surjection is intimately connected with that of quotient, and in particular with the elimination principle into propositions. We think of a surjection as expressing that can be βglued togetherβ by introducing paths between the elements of Since any family of propositions respects these new paths, we can prove a property of by showing it for the βgeneratorsβ coming from
is-surjectiveβelim-prop : (f : A β B) β β {β} (P : B β Type β) β (β x β is-prop (P x)) β (β a β P (f .fst a)) β β x β P x is-surjectiveβelim-prop (f , surj) P pprop pfa x = β₯-β₯-rec (pprop _) (Ξ» (x , p) β subst P p (pfa x)) (surj x)
When the type is a set, we can actually take this analogy all the way to its conclusion: Given any cover we can produce an equivalence between and the quotient of under the congruence induced by See surjections are quotient maps.
Closure propertiesπ
The class of surjections contains the identity β and thus every equivalence β and is closed under composition.
β-is-surjective : {f : B β C} {g : A β B} β is-surjective f β is-surjective g β is-surjective (f β g) β-is-surjective {f = f} fs gs x = do (f*x , p) β fs x (g*fx , q) β gs f*x pure (g*fx , ap f q β p) id-is-surjective : is-surjective {A = A} id id-is-surjective x = inc (x , refl) 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)
Relationship with equivalencesπ
We have defined equivalences to be the maps with contractible fibres; and surjections to be the maps with inhabited fibres. It follows that a surjection is an equivalence precisely if its fibres are also propositions; in other words, if it is an embedding.
embedding-surjectiveβis-equiv : {f : A β B} β is-embedding f β is-surjective f β is-equiv f embedding-surjectiveβis-equiv f-emb f-surj .is-eqv x = β₯-β₯-out! do pt β f-surj x pure $ is-propββis-contr (f-emb x) pt
injective-surjectiveβis-equiv : {f : A β B} β is-set B β injective f β is-surjective f β is-equiv f injective-surjectiveβis-equiv b-set f-inj = embedding-surjectiveβis-equiv (injectiveβis-embedding b-set _ f-inj) injective-surjectiveβis-equiv! : {f : A β B} β¦ b-set : H-Level B 2 β¦ β injective f β is-surjective f β is-equiv f injective-surjectiveβis-equiv! = injective-surjectiveβis-equiv (hlevel 2)