# Zulip Chat Archive

## 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
#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 (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
(@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 (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]
#check (star_ring_aut : ring_aut R).to_add_monoid_hom.isometry_of_norm
```

#### 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:17):

Or docs#continuous_linear_map.comp_left_continuous_bounded

#### 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

#### Frédéric Dupuis (Dec 01 2021 at 04:35):

(deleted)

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

(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