finite powers (biproducts)

Stream: condensed mathematics

[Johan Commelin]

@Scott Morrison Is there a good way to write down $M^n$ in some category with finite biproducts?

[Johan Commelin]

⨁ (λ (i : fin n), M)

is giving me universe issues :cry:

[Scott Morrison]

ulift the fin?

[Scott Morrison]

I don't think I've done this.

[Johan Commelin]

Aha.. so we need to setup some API. Because we don't want to mention those ulifts all the time.

[Scott Morrison]

Yeah, it would be nice to have some inequalities in the limits library, so you can take limits over even smaller categories.

[Scott Morrison]

Have to go!

[Johan Commelin]

Should we add an extra universe variable to the limit API? So that you can talk about limits of arbitrary size?
And then instances that say if you have all limits of shape D in universe v, then you also have all limits of shape D in universe 0.
Idem for going from v+1 to v.

[Johan Commelin]

And from max v₁ v₂ to v₁.

[Kevin Buzzard]

Just use Type and stop pandering to the computer scientists

[Kevin Buzzard]

There is a big disconnect between this multi-universe philosophy and the kind of concrete terms which we're defining such as int and fin n

[Kevin Buzzard]

If we're really supposed to be multi-universe then we should refactor nat and int and real and p-adic etc and make them all universe polymorphic

[Kevin Buzzard]

import tactic

universe u

-- if you truly believe in universe polymorphism then you should be doing this

inductive correct_nat : Type u
| zero : correct_nat
| succ : correct_nat → correct_nat


def correct_fin (n : correct_nat) : Type u := {x // x < n} -- failed to synthesize < on correct_nat

It will be a lot of work! But if they're telling us to be polymorphic then why aren't they making the correct objects themselves?

[Kevin Buzzard]

So just use Type for now, open an issue about how the definition of nat is wrong, and when someone fixes it we can go back to the silly multi-universe approach

[Johan Commelin]

@Kevin Buzzard That is not really an option.

[Johan Commelin]

section universes_are_necessary

set_option pp.universes true

def foo : category (Condensed.{0} Type) := by apply_instance

#print foo
/-
def foo : category.{1 1} (Condensed.{0 0 1} Type) :=
Condensed.category.{0 0 1} Type
-/

def test (f : fin 5 → Condensed.{0} Type) : Condensed.{0} Type := limit (discrete.functor f)
-- fails:
/-
expected type:
f: fin 5 → Condensed.{0 0 1} Type
⊢ discrete.{1} ⁇ ⥤ Condensed.{0 0 1} Type
Messages (2)
projective_replacement.lean:18:73
type mismatch at application
  discrete.functor.{1 1 1} f
term
  f
has type
  fin 5 → Condensed.{0 0 1} Type
but is expected to have type
  ?m_1 → Condensed.{0 0 1} Type
projective_replacement.lean:18:73
don't know how to synthesize placeholder
context:
f : fin 5 → Condensed.{0 0 1} Type
⊢ Type 1
-/

#print Condensed.category

end universes_are_necessary

[Johan Commelin]

The other option is to do all the $κ$-stuff that happens in Condensed.pdf

[Kevin Buzzard]

gaargh

[Johan Commelin]

That's a beautiful way of putting my feelings into words :wink:

[Kevin Buzzard]

OK so either we ulift or we make a polymorphic fin? Which would be less painful do you think? Or do they boil down to the same thing?

[Johan Commelin]

Given the current state of things: ulift

[Reid Barton]

Condensed.{0} Type is not the useful category, it should be Condensed.{0} (Type 1), but I don't think that will help

[Reid Barton]

Another way out is to add an inaccessible cardinal to Type with an axiom, but I'm not sure that is making things better overall

[Johan Commelin]

@Reid Barton Yep, I agree that you need to use Type 1. But as you say, that only makes the problem worse :expressionless:

[Reid Barton]

Kevin Buzzard said:

There is a big disconnect between this multi-universe philosophy and the kind of concrete terms which we're defining such as int and fin n

The reason that int and fin n and so on live in Type is because the other type formers like prod (and Pi, Sigma, ...) are "multi-universe" (e.g. prod : Type u -> Type v -> Type (max u v)). So if you use prod int int : Type 1, say, Lean would have no way to figure out which universe the ints each live in.

[Reid Barton]

There's another world you could imagine where every construction mentions exactly one universe, so int : Type u and prod : Type u -> Type u -> Type u. You would probably need some universe defaulting mechanism for examples like 0 = 1 : Prop (which int.{u} are we talking about?).

[Reid Barton]

(I don't mean literally every construction, but all the ones that aren't specifically "universe-aware")

[Adam Topaz]

I think a universe polymorphic fin would be particularly helpful in a lot of contexts such as simplicial objects.

[Adam Topaz]

Another option is to use S : Fintype.{u} and prove some induction principle for fintypes (I assume you want to use fin because you want to use induction somehow?). Not too long ago I made the skeleton of Fintype universe polymorphic, so in principle you could use that skeleton equivalence and usual Nat induction to prove such an induction principle.

[Kevin Buzzard]

Yes, I mentioned this issue to Oliver today at our weekly meeting and he suggested that maybe just using finite types would be easier than fin n, depending on what you were doing. Of course I am in general anti Fintype because it's constructive -- I'd prefer exists p : fintype X ;-)

[Johan Commelin]

What's the correct way to say that a functor preserves (binary) biproducts?

[Johan Commelin]

Should this reuse something about preserving products? Or should there be a new class?

[Adam Topaz]

[preserves_limits_of_shape walking_pair F] is one option