## Stream: general

### Topic: Type ? vs. Type (max ? ?)

#### Jireh Loreaux (Dec 01 2021 at 03:57):

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

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


#### Heather Macbeth (Dec 01 2021 at 04:00):

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 (Dec 01 2021 at 04:02):

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

#### Jireh Loreaux (Dec 01 2021 at 04:04):

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
(@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
(@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
(@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))))))
(@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
(@semi_normed_group.to_add_comm_group.{?l_2} ?m_4 ?m_6))))) : Type (max ?l_1 ?l_2)


#### Mario Carneiro (Dec 01 2021 at 04:05):

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

#### Mario Carneiro (Dec 01 2021 at 04:06):

the R argument of star_ring_aut should probably be explicit

#### Jireh Loreaux (Dec 01 2021 at 04:07):

ah, I see, yes that makes sense.

#### Mario Carneiro (Dec 01 2021 at 04:09):

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 (Dec 01 2021 at 04:10):

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

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



#### Mario Carneiro (Dec 01 2021 at 04:10):

... I guess normed_comm_ring

#### Heather Macbeth (Dec 01 2021 at 04:11):

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

#### Jireh Loreaux (Dec 01 2021 at 04:12):

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 (Dec 01 2021 at 04:13):

I'll have a look at starₗᵢ

#### Heather Macbeth (Dec 01 2021 at 04:16):

Ah! Check out docs#continuous_linear_map.comp_left_continuous maybe.

#### Heather Macbeth (Dec 01 2021 at 04:18):

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 (Dec 01 2021 at 04:24):

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 (Dec 01 2021 at 04:27):

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 (Dec 01 2021 at 04:28):

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 (Dec 01 2021 at 04:28):

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

(deleted)

(deleted)

#### Jireh Loreaux (Dec 01 2021 at 05:05):

@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 (Dec 01 2021 at 05:06):

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

#### Heather Macbeth (Dec 01 2021 at 05:12):

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

#### Jireh Loreaux (Dec 01 2021 at 05:17):

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

#### Heather Macbeth (Dec 01 2021 at 05:31):

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

#### Jireh Loreaux (Dec 01 2021 at 05:35):

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

Last updated: Aug 03 2023 at 10:10 UTC