Properties of coproducts in category of types

Stream: Is there code for X?

[Christian Merten]

Is there some criterion somewhere when the inclusion morphisms into a coproduct are monomorphisms? More specifically, is there the following result for the category of types?
Also is there the statement that in types, the inclusions into a coproduct are jointly surjective?

import Mathlib

universe u

open CategoryTheory Limits

lemma Types.mono_of_inclusionCoproduct (ι : Type*) (F : Discrete ι ⥤ Type u)
    (t : ColimitCocone F) (i : ι) : Mono (t.cocone.ι.app ⟨i⟩) :=
  sorry

lemma Types.jointlySurjective_inclusionsCoproduct (ι : Type*)
    (F : Discrete ι ⥤ Type u) (t : ColimitCocone F)
    (x : t.cocone.pt) : ∃ (i : ι) (y : F.obj ⟨i⟩), t.cocone.ι.app ⟨i⟩ y = x :=
  sorry

[Junyan Xu]

The second one is docs#CategoryTheory.Limits.Types.jointly_surjective

[Christian Merten]

Junyan Xu said:

The second one is docs#CategoryTheory.Limits.Types.jointly_surjective

I keep loogling for ColimitCocone, instead of searching for IsColimit. ColimitCocone is not used very often it seems.

[Adam Topaz]

That's right. We use Cocone and IsColimit instead of ColimitCocone most of the time. Actually, in most cases you should just use the colimit (or coproduct in this case) without referring to any cocones.

[Christian Merten]

Adam Topaz said:

That's right. We use Cocone and IsColimit instead of ColimitCocone most of the time. Actually, in most cases you should just use the colimit (or coproduct in this case) without referring to any cocones.

So you are saying that X ≅ colimit F is preferrable over (t : ColimitCocone F) (h : t.cocone.pt = X)? The latter seems closer to what I would say on a piece of paper, but I realised that it leads to repeated eqToHom h terms when working with it (to prevent casting hell caused by rw [h]).

[Christian Merten]

I found docs#CategoryTheory.Limits.MonoCoprod which is essentially what I want, although I need to conclude from MonoCoprod C for a category C, that inclusions in arbitrary (existing) coproducts are injective (at least if C has all coproducts). This does not seem to be anywhere. @Joël Riou: you wrote the linked file, did I overlook something?

[Joël Riou]

When #8242 is merged, I can add this property of categories C satisfying [MonoCoprod C].

[Dagur Asgeirsson]

@Christian Merten since you're working in the category of types, for your Types.mono_of_inclusionCoproduct for now you can use a combination of docs#CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso, docs#CategoryTheory.Limits.Types.coproductIso, and docs#sigma_mk_injective

[Christian Merten]

Thanks, that worked, at least for coproducts indexed by ι : Type u and f : ι → Type u, i.e. the universe levels need to match. That is because docs#CategoryTheory.Limits.Types.coproductIso is only defined for agreeing universe levels. Can I circumvent that? Or is there a reason why these are only formulated for agreeing universe levels?

[Dagur Asgeirsson]

It's probably a typo that coproductIso only works for matching universe levels. I don't see why it shouldn't work for input of the form {J : Type v} (F : J → Type u) [UnivLE.{v, u}] like productIso

[Dagur Asgeirsson]

#8421 allows for different universe levels (the TypeMax version)