3
$\begingroup$

Question 0: How do injective envelopes work in constructive mathematics?

For example,

Question 1: How strong is it to assert internally that there are enough injectives (in the category of sets, say)? (Externally, every topos has enough injectives thanks to the subobject classifier.)

Question 2: How about injective envelopes?

The usual way to construct injective envelopes is quite choice-y. And their notorious lack of functoriality certainly suggests that their existence is probably some sort of choice principle.

An example I have in mind is that in the topos of simplicial sets, $\Delta^1$ is probably the injective envelope of $Bool$, smaller than the "canonical" injective resolution given by $\Omega$. The two embeddings $=0, =1 : \Delta^1 \rightrightarrows \Omega$ are indicative of the non-canonical nature of the construction. This example suggests to me that asserting the existence of an injective envelope of Bool might even be a nice axiom for synthetic domain theory.... (especially since injectivity is often a completeness condition. For example, the injective posets are exaclty the complete lattices...)

Improve this question
$\endgroup$
3
  • 2
    $\begingroup$ $\Delta^1$ is not an injective object... $\endgroup$ Commented Apr 25 at 21:14
  • 1
    $\begingroup$ I think Martin Escardo has some work on injective objects in homotopy type theory (given the tags). $\endgroup$ Commented Apr 25 at 23:43
  • $\begingroup$ @ZhenLin ah you’re right. To be honest I was thinking about Cat, where complete lattices are still injective with respect to fully faithful functors. In sSet, $\Delta^1$ is injective with respect to decidable monos, and more generally with respect to the analogs of fully faithful functors (the right orthogonal complement of bijective-on-vertices functors). $\endgroup$ Commented Apr 26 at 12:46

1 Answer 1

Reset to default
5
$\begingroup$

Injective in the category of sets are still fairly abundant constructively, at least impredicatively: In the category of sets, and in any topos, you can embedded every set X into its power set, or the subset of its power set of subsingleton (i.e. subset of X with at most one element) and these are always injective object constructives.

I'm not quite sure what injective hull mean in a non additive setting, but If by injective enveloppes you just mean a mono to an injective, then the construction above provide one.

Improve this answer
$\endgroup$
6
  • 1
    $\begingroup$ Yes, this is the construction of enough objectives in a topos which I alluded to in a topos. It’s not clear to me that this construction validates the internal statement “$X \to \Omega^X$ is a mono to an injective”. Well, to be honest the issue is really that objectivity quantifies over objects so it’s not clear what it means internally. For injective envelopes, I do mean more than a mono to an injective. It should be an essential mono to an injective. See nlab $\endgroup$ Commented Apr 26 at 12:39
  • $\begingroup$ I don't know what an essential mono mean in the category of sets. the notion uses zero object, and the way it interact with injectivity has to do with the "f is a mono" iff ker(f)=0. If you replace "non zero" by inhabited in the defintion then the only essential mono are isomorphisms so the answer is trivially no. $\endgroup$ Commented Apr 26 at 12:48
  • $\begingroup$ But yes, this construction of injective envelope works in constructive setting as well and set is still a topos constructively so this is true. and from an external point of view, yes the statment that $X \to \Omega^X$ is an embedding to an injective is internally true. $\endgroup$ Commented Apr 26 at 12:50
  • $\begingroup$ Thanks. The notion of $\mathcal E$-essential mono is sufficiently well-studied (without serious contenders materializing for a notion of “generalized essential mono) that I think it’s more likely I want to vary the notion of monomorphism rather than the notion of essentiality… But OTOH the injective resolution we’ve been discussing relies on the impredicative subobject classifier. This can’t be the end of the story of constructive injective resolutions! $\endgroup$ Commented Apr 27 at 3:24
  • 1
    $\begingroup$ I think the only small injective set that you can build in a predicative setting is the terminal one, this sketch argument. $\endgroup$ Commented Apr 27 at 12:30

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.