Type ? vs. Type (max ? ?)

Stream: general

[Jireh Loreaux]

Can someone explain why the first two of these typecheck, but the last one doesn't. It has something to do with universes, but I don't understand. Is there a way I can make this work?

import analysis.normed.group.basic
import algebra.star.basic

#check star_ring_aut.to_add_monoid_hom
-- ring_equiv.to_add_monoid_hom star_ring_aut : ?M_1 →+ ?M_1
#check add_monoid_hom.isometry_of_norm
-- add_monoid_hom.isometry_of_norm : ∀ (f : ?M_1 →+ ?M_2),
-- (∀ (x : ?M_1), ∥⇑f x∥ = ∥x∥) → isometry ⇑f
#check star_ring_aut.to_add_monoid_hom.isometry_of_norm
/-
type mismatch at application
  (ring_equiv.to_add_monoid_hom star_ring_aut).isometry_of_norm
term
  ring_equiv.to_add_monoid_hom star_ring_aut
has type
  ?m_1 →+ ?m_1 : Type ?
but is expected to have type
  ?m_1 →+ ?m_2 : Type (max ? ?)
-/

[Heather Macbeth]

Not answering your question, but what are you using isometry_of_norm for? In general I would expect starₗᵢ to provide facts about the isometry more efficiently.

[Mario Carneiro]

I don't think the error is actually about universes. Run it with set_option pp.all true?

[Jireh Loreaux]

with set_option pp.all true ...

type mismatch at application
  @add_monoid_hom.isometry_of_norm.{?l_1 ?l_2} ?m_3 ?m_4 ?m_5 ?m_6
    (@ring_equiv.to_add_monoid_hom.{?l_7 ?l_7} ?m_8 ?m_8
       (@semiring.to_non_assoc_semiring.{?l_7} ?m_8 (@comm_semiring.to_semiring.{?l_7} ?m_8 ?m_9))
       (@semiring.to_non_assoc_semiring.{?l_7} ?m_8 (@comm_semiring.to_semiring.{?l_7} ?m_8 ?m_9))
       (@star_ring_aut.{?l_7} ?m_8 ?m_9 ?m_10))
term
  @ring_equiv.to_add_monoid_hom.{?l_1 ?l_1} ?m_2 ?m_2
    (@semiring.to_non_assoc_semiring.{?l_1} ?m_2 (@comm_semiring.to_semiring.{?l_1} ?m_2 ?m_3))
    (@semiring.to_non_assoc_semiring.{?l_1} ?m_2 (@comm_semiring.to_semiring.{?l_1} ?m_2 ?m_3))
    (@star_ring_aut.{?l_1} ?m_2 ?m_3 ?m_4)
has type
  @add_monoid_hom.{?l_1 ?l_1} ?m_2 ?m_2
    (@add_monoid.to_add_zero_class.{?l_1} ?m_2
       (@add_comm_monoid.to_add_monoid.{?l_1} ?m_2
          (@non_unital_non_assoc_semiring.to_add_comm_monoid.{?l_1} ?m_2
             (@non_assoc_semiring.to_non_unital_non_assoc_semiring.{?l_1} ?m_2
                (@semiring.to_non_assoc_semiring.{?l_1} ?m_2 (@comm_semiring.to_semiring.{?l_1} ?m_2 ?m_3))))))
    (@add_monoid.to_add_zero_class.{?l_1} ?m_2
       (@add_comm_monoid.to_add_monoid.{?l_1} ?m_2
          (@non_unital_non_assoc_semiring.to_add_comm_monoid.{?l_1} ?m_2
             (@non_assoc_semiring.to_non_unital_non_assoc_semiring.{?l_1} ?m_2
                (@semiring.to_non_assoc_semiring.{?l_1} ?m_2
                   (@comm_semiring.to_semiring.{?l_1} ?m_2 ?m_3)))))) : Type ?l_1
but is expected to have type
  @add_monoid_hom.{?l_1 ?l_2} ?m_3 ?m_4
    (@add_monoid.to_add_zero_class.{?l_1} ?m_3
       (@sub_neg_monoid.to_add_monoid.{?l_1} ?m_3
          (@add_group.to_sub_neg_monoid.{?l_1} ?m_3
             (@add_comm_group.to_add_group.{?l_1} ?m_3 (@semi_normed_group.to_add_comm_group.{?l_1} ?m_3 ?m_5)))))
    (@add_monoid.to_add_zero_class.{?l_2} ?m_4
       (@sub_neg_monoid.to_add_monoid.{?l_2} ?m_4
          (@add_group.to_sub_neg_monoid.{?l_2} ?m_4
             (@add_comm_group.to_add_group.{?l_2} ?m_4
                (@semi_normed_group.to_add_comm_group.{?l_2} ?m_4 ?m_6))))) : Type (max ?l_1 ?l_2)

[Mario Carneiro]

The given object is talking about a comm_semiring, but it seems to want a semi_normed_group

[Mario Carneiro]

the R argument of star_ring_aut should probably be explicit

[Jireh Loreaux]

ah, I see, yes that makes sense.

[Mario Carneiro]

I think this will work if you use some R which is both a comm_semiring and a semi_normed_group, although I don't know what the appropriate class is

[Heather Macbeth]

import analysis.normed_space.basic
import algebra.star.basic

variables {R : Type*} [normed_comm_ring R] [star_ring R]

#check (star_ring_aut : ring_aut R).to_add_monoid_hom.isometry_of_norm

[Mario Carneiro]

... I guess normed_comm_ring

[Heather Macbeth]

But, like I said, it's likely better to use starₗᵢ

[Jireh Loreaux]

Heather, I'm instantiating the bounded continuous functions (with appropriate hypotheses on the codomain) as a C^*-algebra. As part of this, I need to show that the star operation is a bounded continuous function, and I thought the best way to go would be to get an isometry to show that it's Lipschitz and then the composition of a bounded continuous function and lipschitz function is bounded continuous.

[Jireh Loreaux]

I'll have a look at starₗᵢ

[Heather Macbeth]

Ah! Check out docs#continuous_linear_map.comp_left_continuous maybe.

[Heather Macbeth]

Or docs#continuous_linear_map.comp_left_continuous_bounded

[Heather Macbeth]

I had to do something like this in the lemma docs#subalgebra.separates_points.complex_to_real to refer to (secretly) the star operation on bounded continuous functions.

[Jireh Loreaux]

Those are nice, but they seem to have too many hypotheses, like a nondiscrete_normed_field. In particular, it should be possible to show that if

variables [topological_space α] [normed_ring β] [star_ring β] [cstar_ring β]

then α →ᵇ β is a cstar_ring.

[Jireh Loreaux]

I already have a 5 line tactic proof of boundedness, but I was just trying to get better at golfing and using the library.

[Heather Macbeth]

Perhaps you can do the ring_hom analogue of those in the bounded continuous category. I added all the different algebraic structure variants in the continuous category before I got bored, including docs#ring_hom.comp_left_continuous

[Mario Carneiro]

If you think that starₗᵢ still holds in greater generality, by all means make a PR for it

[Frédéric Dupuis]

(deleted)

[Jireh Loreaux]

(deleted)

[Jireh Loreaux]

@Mario Carneiro if [normed_group E] [star_add_monoid E] [normed_star_monoid E], then star should be an isometric add_equiv, but I don't think we have a bundle for such things. I don't know of a case when something like that ever comes up.

[Jireh Loreaux]

Heather, I can work on those at some point soon.

[Heather Macbeth]

Feel free to do it the low-tech way (without building up these new algebraic constructions) if it's easier.

[Jireh Loreaux]

well, one reason it's a bit tricky to apply here is that star is an anti-automorphism.

[Heather Macbeth]

Yes, I am realizing now why you were using normed_add_hom at the start of the thread.

[Jireh Loreaux]

well, I wasn't because I was being silly. I think I should have been using star_add_equiv.