Spectrification

[Alizter]

Here is a branch of mine that has the colimits and EM spaces branches merged. I have changed the definition of Build_Spectrum so that it will demand all the data. The original Build_Spectrum has been renamed Build_Spectrum'.

It has been commonly suggested that spectrification should be defined as a colimit. I have yet to see this being checked formally anywhere. The Lean (Spectral) library doesn't have spectrification, they leave it as (the equivalent of) admitted.

Here is what the code looks like so far:

Require Import Basics.
Require Import Types.
Require Import Pointed.
Require Import Spectrum.
Require Import Colimits.Colimit.
Require Import Diagrams.Cocone.
Require Import Diagrams.Sequence.
Require Import Spaces.Nat.

Local Open Scope pointed_scope.
Local Open Scope nat_scope.

(** Spectrification defined as a sequential colimit *)

Section Spectrification.

  (* The diagram we will be taking a colimit of *)
  (* We write k + n so that 0 + n is definitionally n *)
  Definition Seq (Y : Prespectrum) (n : nat) : Sequence.
  Proof.
    serapply Build_Sequence.
    { intro k.
      exact (iterated_loops k (Y (k + n))). }
    intros k x.
    refine (transport _ (unfold_iterated_loops k _)^ _).
    revert x.
    refine (iterated_loops_functor k _).
    apply glue.
  Defined.

  Definition L (Y : Prespectrum) (n : nat) : pType.
  Proof.
    serapply Build_pType.
    1: exact (Colimit (Seq Y n)).
    serapply colim; cbn.
    1: exact 0.
    apply ispointed_type.
  Defined.

  Definition glueL {Y : Prespectrum} (n : nat)
    : L Y n ->* loops (L Y n.+1).
  Proof.
  Admitted.

  Global Instance isequiv_glueL {Y : Prespectrum} {n : nat}
    : IsEquiv (@glueL Y n).
  Proof.
  Admitted.

  Definition Spectrification (Y : Prespectrum) : Spectrum.
  Proof.
    serapply Build_Spectrum.
    + by apply L.
    + apply glueL.
    + intro n.
      exact _.
  Defined.

End Spectrification.

All the hard work lies in defining glueL and showing it is an equivalence.

Here is my attempt at glueL:

  Definition glueL {Y : Prespectrum} (n : nat)
    : L Y n ->* loops (L Y n.+1).
  Proof.
    serapply Build_pMap.
    { serapply Colimit_rec.
      serapply Build_Cocone; cbn.
      { intro k.

  Admitted.

Now the goal reads as:

1 subgoal
Y : Prespectrum
n, k : nat
______________________________________(1/1)
iterated_loops k (Y (k + n)) ->
colim 0 (ispointed_type (Y n.+1)) = colim 0 (ispointed_type (Y n.+1))

My first instinct was to go about like this:

  Definition glueL {Y : Prespectrum} (n : nat)
    : L Y n ->* loops (L Y n.+1).
  Proof.
    serapply Build_pMap.
    { serapply Colimit_rec.
      serapply Build_Cocone; cbn.
      { intro k.
        intro x.
        apply ap.
        induction k.
        { apply glue, x. }
        apply IHk.
        apply unfold_iterated_loops' in x.
        revert x.
        apply iterated_loops_functor.

  Admitted.

Which gives us this goal:

1 subgoal
Y : Prespectrum
n, k : nat
IHk : iterated_loops k (Y (k + n)) ->
      ispointed_type (Y n.+1) = ispointed_type (Y n.+1)
______________________________________(1/1)
loops (Y (k.+1 + n)) ->* Y (k + n)

What would go great here is the inverse of glue. But to have that we would need Y to be a spectrum already, which is exactly what we are trying to achieve.

Hence I think there is a clever thing we need to do with the colims but I haven't been able to work out. Hence I am writing this issue.

What do you think needs to be done?

[mikeshulman]

What's needed is that sequential colimits commute with path-spaces. For a while it was an open problem to deal with all the coherence involved in proving that by encode-decode. I can't remember for sure but I think that perhaps it's been solved now? Maybe ask Egbert? I don't see it explicitly in his lecture notes on sequential colimits but maybe it can be deduced from his descent or flattening theorems.

[Alizter]

@mikeshulman So given any dependent diagram, if it is equifibered we have a flattening lemma for it. Given any sequence A, there is an equifibered sequence A' and a map of diagrams A -> A' such that colim A <~> colim A'. In general I would expect this to hold for some notion of k-filtered A. Edit: I am being a bit sloppy, A is also dependent but this can be worked out.

What's nice about this is now we can apply the flattening lemma to filtered diagrams. We can then construct a family P : colim A -> Type, whose total space is contractible by the flattening lemma. This means that the fibers of P are equivalent to the identity type. The construction of P is a bit involved (even for sequential diagrams) so I won't write it here. What we get at the end is a series of equivalences induced by the filteredness of the diagram, which allows us to prove that the loop space of a colimit of pointed types is equivalent to the colimit of loop spaces.

If I am to formalise this argument, I will stick to sequential colimits since filtered colimits are a bit too hopeful for now. The construction of P is detailed on pg 64 of Floris' thesis and pg 146 of Egbert's thesis.

I am probably missing a crucial step here that makes the above argument much harder than it seems currently.

[Alizter]

FTR we currently have a formalized proof of colimits commuting with path spaces however the path algebra involved is quite tricky from the last time I tried it. It ought to be possible however if somebody is willing to have a go.