Zulip Chat Archive

Stream: condensed mathematics

Topic: sigma bounded above


Johan Commelin (Jun 23 2022 at 06:46):

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 (Jun 23 2022 at 06:47):

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

Adam Topaz (Jun 23 2022 at 12:16):

There must be something...

Adam Topaz (Jun 23 2022 at 12:16):

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

Johan Commelin (Jun 24 2022 at 06:47):

Thanks. This is now done.


Last updated: Dec 20 2023 at 11:08 UTC