Incorrect definition of essential surjectivity

[jonsterling]

To get the correct notion of surjection, it is very important that you use an existential quantifier / truncated dependent sum. Your definition means something, but it doesn't mean "surjection".

hStacks/src/S4_2_0013.ard

Line 128 in f589fa0

\func isEssentiallySurjective {A B : Precategory} (F : Functor A B) => \Pi (y : B) -> \Sigma (x : A) (F.F x ~= y)

Passing to the correct definition of essential surjectivity will have some consequences; you will not be able to prove the "full/faithfull/ess.surj. <=> equivalence" theorem for precategories, but it will remain true for univalent categories.

[tonyxty]

In HoTT book it's called split essentially surjective (Definition 9.4.4), and what I proved is Lemma 9.4.5. The truncated/category version you mentioned is Lemma 9.4.7.

Problem is, I'm not sure which one is actually being used in the rest of Stacks project - or how "constructive" Algebraic Geometry is - I guess we will be mostly dealing with split essential surjectivity; I might add Lemma 9.4.7 in the future if needs be, or if someone else proves it ;)

Moreover, the definition of "surjection" in Foundation/Set.ard also has this problem (and has an hPOV comment). Again this is not yet decided and depends on how constructive AG actually is (or can be).

About the choice of the terminology: for now I'm leaning towards reserving simpler names for the constructive/untruncated version and call the truncated version "merely surjective." This differs from HoTTbook usage but this project is still in its experimental stage, and there's intellij's refactor tool.

[jonsterling]

Good points! My perspective is:

1. Algebraic geometry is very classical and you should probably assume the axiom of choice.

2. I think it would still be best not to refer to this untruncated one as "essentially surjective", but you can then prove that every surjection is split (equivalent to the axiom of choice), and hence get the result you wanted about equivalences. Aside from keeping with ordinary terminology, my reason is also that one generally thinks of surjectivity as a property, whereas the space of splittings of a surjection is not generally contractible.

Anyway, good luck with your project! It is very ambitious.

[tonyxty]

Thanks! This reminded me that I'm violating the convention that isA is usually only used when A is a \Prop. I'll reconsider the choice of terminology.