rescale_preserves_limits_of_shape_discrete_quotient

Stream: condensed mathematics

[Kevin Buzzard]

In condensed/rescale.lean there's the following claim:

instance rescale_preserves_limits_of_shape_discrete_quotient
  (X : Profinite.{u}) (c : ℝ≥0) [fact (0 < c)] :
  limits.preserves_limits_of_shape.{u u u u u+1 u+1} (discrete_quotient.{u} ↥X) (rescale.{u u} c) :=
sorry

How about this for an approach: rescale c is an equivalence of categories, and equivalences preserve all limits -- but I can't find the latter. Do we have it? I'm working on the equivalence. Not sure if it's the quickest way but it seems nice to formalise.

[Johan Commelin]

Yeah, I think that's a very sensible way of proving this.

[Adam Topaz]

I'm sure we have it. Maybe docs#category_theory.equivalence_preserves_limits

[Kevin Buzzard]

Oh nice. I looked in all the preserves files but not at adjunctions

[Kevin Buzzard]

This is so messed up. is_equivalence isn't a Prop! Why can't we use is for props and has for data?

[Adam Topaz]

It's because the essential inverse of an equivalence is only unique up to isomorphism.

[Adam Topaz]

Same goes for things like is_right_adjoint

[Kevin Buzzard]

sure, but here we just need existence of an essential inverse.

[Adam Topaz]

That's true. I guess we could mimic what we have for limits, where has_limit is a prop, which is then used to get the noncomputable limit F, while we also have is_limit saying that a certain cone is a limit cone, and a bunch of API giving us the canonical isomorphisms.

[Adam Topaz]

That would be a significant refactor though

[Scott Morrison]

Oh dear, it never even occurred to me that is_limit and has_limit might be backwards by Kevin's rubric!

[Kevin Buzzard]

Maybe I'm fusing about nothing! I just have this dream that in the algebra hierarchy and beyond you can guess how to make eg Dedekind domains by assuming a base typeclass like comm_ring and then putting Prop-valued typeclasses all called is_something on top

[Kevin Buzzard]

OK I pushed a proof of rescale_preserves_limits_of_shape_discrete_quotient. Basically I had to learn how to steer this stuff; once I got the hang of it all proofs were short. The idea is that when mapping between different rescales every map is id but if you write it as λ m, (rescale.of (rescale.of (rescale.of.symm m))), or whatever (this is how to get from rescale (a * b) M to rescale b (rescale a M)) then you don't get any eq.recs in definitions and things come out really nicely.

So out of interest, the abstract situation here is that we have an nnreal-indexed family of endofunctors F r : C -> C from a category to itself, and the things I needed to explicitly define were: morphisms in both directions between F 1 M and M, morphisms in both directions between F r (F s M) and F (s * r) M, and finally if r = s a morphism from F r M to F s M. All of these maps are the identity on the underlying type (rescaling is moving around some of the other structure on the type), but it took me a while to understand how to prove that they played well with e.g. the topologies. Once I had these maps I could just compose them together to prove that F r and F r^{-1} were equivalences. There is probably some general story going on here -- monoids acting on categories? Not that it matters, it's all working now.

[Adam Topaz]

This stuff can be considered as a monoidal functor from the positive reals (considered as a monoidal category) to the monoidal category of endofunctors. This is actually very similar to how docs#category_theory.has_shift is defined.

[Adam Topaz]

In fact, we could probably package these rescale functors into a has_shift instance with nnreal (although has_shift wants an additive monoids whereas here we would use the multiplicative monoid)

[Scott Morrison]

I dare you to write @[to_additive] in front of has_shift and see what happens. :-)