sigma bounded above

Stream: condensed mathematics

[Johan Commelin]

Was this already done somewhere?

instance sigma_Qprime_int_bounded_above :
  ((homotopy_category.quotient (Condensed Ab) (complex_shape.up ℤ)).obj
    (∐ λ (k : ulift ℕ), (QprimeFP_int r' BD.data κ M).obj (ι k))).is_bounded_above :=
begin
  -- first pull the `∐` through the quotient functor
  -- then use something about `uniformly_bounded`??
  sorry,
end

[Johan Commelin]

(This is a sorry in Lbar/ext.lean)

[Adam Topaz]

There must be something...

[Adam Topaz]

Take a look at bounded_homotopy_category.cofan (I think?)

[Johan Commelin]

Thanks. This is now done.