# Zulip Chat Archive

## Stream: maths

### Topic: Normed spaces

#### Heather Macbeth (May 16 2020 at 01:07):

This continues a discussion from the new members stream. I would like to discuss some possible changes to `normed_space.basic`

. Here is the branch (not yet PR'd).

#### Heather Macbeth (May 16 2020 at 01:07):

- Implement
`normed_algebra.to_normed_space`

, prior discussion

#### Heather Macbeth (May 16 2020 at 01:07):

- Implement a class
`normed_module`

(axiom`norm_smul_le`

,`∥c • x∥ ≤ ∥c∥ ∥x∥`

), and prove that a normed module over a field is a normed space (axiom`norm_smul`

,`∥c • x∥ = ∥c∥ ∥x∥`

). By the way, I am not sure that a "normed module" is a particularly standard object, but it seemed to me like a useful way to abstract out the norm-respecting property of the C(a, k)-module C(a, E) (for E a normed k-space).

#### Heather Macbeth (May 16 2020 at 01:08):

Changes that I considered but did not currently implement:

#### Heather Macbeth (May 16 2020 at 01:08):

- Add [@simp] attribute to
`norm_smul`

(`∥c • x∥ = ∥c∥ ∥x∥`

) and related lemmas, prior discussion. I think this is possibly a good idea in principle, but it breaks a few existing proofs in`normed_space.operator_norm`

,`normed_space.banach`

etc.

#### Heather Macbeth (May 16 2020 at 01:08):

- Introduce consistency among naming in

`instance normed_top_monoid : topological_add_monoid α := ...`

`instance normed_top_group : topological_add_group α := ...`

`instance normed_top_ring : topological_ring α :=`

`instance normed_space.topological_vector_space : topological_vector_space α E := ...`

#### Heather Macbeth (May 16 2020 at 01:09):

Comments on any of these would be welcome. Regarding 2, it was suggested in the previous thread that once `normed_module`

is added, `normed_space`

should cease to exist except as an abbreviation for a normed module over a field.

#### Heather Macbeth (May 16 2020 at 01:09):

Sebastien Gouezel said:

I think

`vector_space`

is just an abbreviation for`module`

. We could have`normed_module`

, and then`normed_space`

as an abbreviation of`normed_module`

.

Johan Commelin said:

Sure. And

`norm_smul`

would be a lemma with the assumption`[normed_field k]`

#### Heather Macbeth (May 16 2020 at 01:09):

I did not implement this yet, because, if I understand correctly, this would require going through the library to all existing instances of normed spaces, and modifying the existing construction (using the axiom `norm_smul`

) to instead check the new axiom (`norm_smul_le`

). Correct? Thoughts?

#### Bryan Gin-ge Chen (May 16 2020 at 01:23):

I haven't been following this, but @Yury G. Kudryashov recently opened #2693 which seems quite relevant.

#### Heather Macbeth (May 16 2020 at 01:28):

Oops, looks like @Yury G. Kudryashov and I both took the same lesson from our discussion yesterday ...

#### Heather Macbeth (May 16 2020 at 01:29):

Sorry Yury, do you want to incorporate my other changes into your refactor? Or vice versa?

#### Yury G. Kudryashov (May 16 2020 at 02:33):

Feel free to take over this

#### Yury G. Kudryashov (May 16 2020 at 02:33):

I'm sorry for starting this without announcing here.

#### Yury G. Kudryashov (May 16 2020 at 02:36):

Note that I simplified several proofs in `bounded_continuous_function`

#### Heather Macbeth (May 16 2020 at 02:37):

Yes, I think this is likely to be one advantage of replacing `norm_smul`

with `norm_smul_le`

.

#### Heather Macbeth (May 16 2020 at 02:38):

Off the top of your head, are there other instances of normed spaces whose construction will be simplified by this?

#### Yury G. Kudryashov (May 16 2020 at 02:38):

`operator_norm`

?

#### Heather Macbeth (May 16 2020 at 02:39):

Also, do you agree with @Johan Commelin / @Sebastien Gouezel 's proposal to make `normed_space`

an abbreviation for `normed_module`

over a field?

#### Heather Macbeth (May 16 2020 at 02:39):

`normed_module`

having the `norm_smul_le`

axiom

#### Yury G. Kudryashov (May 16 2020 at 02:39):

Yes.

#### Heather Macbeth (May 16 2020 at 02:40):

And do you have any opinion on the other possible changes? https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Normed.20spaces/near/197768469

#### Yury G. Kudryashov (May 16 2020 at 02:41):

1, 2, 3: sure

4: I don't care about instance names

#### Heather Macbeth (May 16 2020 at 02:43):

Ok great.

#### Heather Macbeth (May 16 2020 at 02:50):

Your PR has nicer code than mine. If you like I can finish chasing down the things that your PR breaks (because of the `norm_smul`

to `norm_smul_le`

change.)

#### Heather Macbeth (May 16 2020 at 02:51):

Then when that is merged, make the `space`

to `module`

change as a second PR.

#### Yury G. Kudryashov (May 16 2020 at 02:52):

Whatever is more convenient for you.

#### Yury G. Kudryashov (May 16 2020 at 02:53):

Your PR has nicer code than mine.

I have a bit more (~1 year) experience with Lean and mathlib.

#### Heather Macbeth (May 16 2020 at 05:42):

Johan Commelin said:

Yup, that's right. So all their constructions should be prepended with

`normed_space.mk'`

or some other name that provided a second constructor.

@Yury G. Kudryashov , what do you think of incorporating this suggestion (a second constructor) into your PR, so that there are not a bunch of `le_of_eq`

's added to the library from normed space constructions for which the equality is more natural than the inequality? (I can make the change, just wanted to check your opinion.)

#### Sebastien Gouezel (May 16 2020 at 08:29):

@Heather Macbeth , @Yury G. Kudryashov Do you mind if I work a little on Yury's branch, incorporating your definition of a normed module and registering a normed space as an abbreviation of a normed module?

#### Yury G. Kudryashov (May 16 2020 at 08:45):

I don't mind.

#### Yury G. Kudryashov (May 16 2020 at 08:46):

Note that @Heather Macbeth has this definition in her branch.

#### Heather Macbeth (May 16 2020 at 08:48):

Sure, go ahead!

#### Heather Macbeth (May 16 2020 at 08:53):

@Yury G. Kudryashov my branch did it the old way, with a normed space as a separate class with `to`

and `of`

methods; no point keeping it.

#### Sebastien Gouezel (May 16 2020 at 09:17):

I have started playing with it, and I have broken everything :) More precisely, I have stumbled on an issue with typeclass inference that reminds me very strongly of the issue we had with `pi_instance`

some time ago. Here is a MWE:

```
import analysis.normed_space.basic
section normed_module
set_option default_priority 100 -- see Note [default priority]
class normed_module (α : Type*) (β : Type*) [normed_ring α] [normed_group β]
extends module α β :=
(norm_smul_le : ∀ (a:α) (b:β), ∥a • b∥ ≤ ∥a∥ * ∥b∥)
end normed_module
variables {𝕜 : Type} {n : ℕ} {E : fin n → Type}
[A : normed_field 𝕜] [N : ∀i, normed_group (E i)] [∀i, normed_module 𝕜 (E i)]
-- Two different ways to say: Π (i : fin n), module 𝕜 (E i)
lemma all_right :
Π (i : fin n),
@module.{0} 𝕜 (E i)
(@normed_ring.to_ring.{0} 𝕜
(@normed_field.to_normed_ring.{0} 𝕜 A))
(@normed_group.to_add_comm_group.{0} (E i) (N i)) :=
by apply_instance
lemma fails :
Π (i : fin n),
@module.{0} 𝕜 (E i)
(@comm_ring.to_ring.{0} 𝕜
(@nonzero_comm_ring.to_comm_ring.{0} 𝕜
(@local_ring.to_nonzero_comm_ring.{0} 𝕜
(@field.local_ring.{0} 𝕜
(@normed_field.to_field.{0} 𝕜 A)))))
(@normed_group.to_add_comm_group.{0} (E i) (N i)) :=
by apply_instance -- fails
-- all_right -- works
```

I defined normed modules, and then I express in two ways that if you know that you have normed module structures on every `E i`

with respect to some normed field, then you have module structures on the `E i`

with respect to this normed field. The difference is that the instance paths from normed field to ring are different in the two lemmas. In one of them, `by apply_instance`

works, in the other one it fails. But the two lemmas are defeq.

#### Yury G. Kudryashov (May 16 2020 at 09:50):

And I guess Lean picks up the wrong path. What do you think about leaving this change to another PR?

#### Sebastien Gouezel (May 16 2020 at 09:56):

You mean the introduction of normed modules? Yes, sure, it can wait for another PR. Still, I think the problem above is important, and should be fixed instead of worked around: this is probably not specific to normed spaces, and could bite us in many places. @Mario Carneiro , @Gabriel Ebner , what do you think?

#### Heather Macbeth (May 16 2020 at 16:23):

@Yury G. Kudryashov do you mind if I also incorporate the change 1 I mentioned above? (`normed_algebra.to_normed_space`

). It's unrelated, but only a few lines:

```
instance to_normed_space {𝕜 : Type*} (𝕜' : Type*) [normed_field 𝕜] [normed_ring 𝕜']
[h : normed_algebra 𝕜 𝕜'] : normed_space 𝕜 𝕜' :=
{ norm_smul_le := begin
intros s x,
calc ∥s • x∥ = ∥((algebra_map 𝕜 𝕜') s) * x∥ : by {rw h.smul_def', exact rfl}
... ≤ ∥algebra_map 𝕜 𝕜' s∥ * ∥x∥ : normed_ring.norm_mul _ _
... = ∥s∥ * ∥x∥ : by rw norm_algebra_map_eq,
end,
..h }
```

#### Yury G. Kudryashov (May 16 2020 at 18:14):

Go ahead.

#### Sebastien Gouezel (May 16 2020 at 20:18):

@Mario Carneiro , since you're here, did you have time to have a look at https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Normed.20spaces/near/197786186?

#### Sebastien Gouezel (May 16 2020 at 20:22):

It's really a weird behavior. I have investigated it a bit further, and it behaves exactly like the example we had with `pi_instance`

some time ago. There are two terms that are definitionally equal (even with the attribute `tactic.transparency.reducible`

), but `apply_instance`

fails to spot this. The outer terms are proved equal with the attribute `tactic.transparency.reducible`

, but not inner terms. More precisely,

```
lemma outer_works :
(Π (i : fin n),
@module.{0} 𝕜 (E i)
(@normed_ring.to_ring.{0} 𝕜
(@normed_field.to_normed_ring.{0} 𝕜 A))
(@normed_group.to_add_comm_group.{0} (E i) (N i)))
=
(Π (i : fin n),
@module.{0} 𝕜 (E i)
(@comm_ring.to_ring.{0} 𝕜
(@nonzero_comm_ring.to_comm_ring.{0} 𝕜
(@local_ring.to_nonzero_comm_ring.{0} 𝕜
(@field.local_ring.{0} 𝕜
(@normed_field.to_field.{0} 𝕜 A)))))
(@normed_group.to_add_comm_group.{0} (E i) (N i))) :=
by tactic.reflexivity tactic.transparency.reducible -- works
lemma inner_fails :
(@normed_ring.to_ring.{0} 𝕜
(@normed_field.to_normed_ring.{0} 𝕜 A))
=
(@comm_ring.to_ring.{0} 𝕜
(@nonzero_comm_ring.to_comm_ring.{0} 𝕜
(@local_ring.to_nonzero_comm_ring.{0} 𝕜
(@field.local_ring.{0} 𝕜
(@normed_field.to_field.{0} 𝕜 A))))) :=
by tactic.reflexivity tactic.transparency.reducible -- fails
```

#### Sebastien Gouezel (May 16 2020 at 20:23):

With `tactic.transparency.instances`

, everything works.

#### Mario Carneiro (May 16 2020 at 20:50):

This sounds like "working as intended" though

#### Mario Carneiro (May 16 2020 at 20:50):

`reflexivity reducible`

is supposed to unfold only reducible definitions, not instances

#### Mario Carneiro (May 16 2020 at 20:53):

doesn't `simp`

have a `canonize_instances`

option that is supposed to fix issues like this?

#### Sebastien Gouezel (May 16 2020 at 20:56):

I don't think it works as intended. You have

```
lemma all_right :
Π (i : fin n),
@module.{0} 𝕜 (E i)
(@normed_ring.to_ring.{0} 𝕜
(@normed_field.to_normed_ring.{0} 𝕜 A))
(@normed_group.to_add_comm_group.{0} (E i) (N i)) :=
by apply_instance
lemma fails :
Π (i : fin n),
@module.{0} 𝕜 (E i)
(@comm_ring.to_ring.{0} 𝕜
(@nonzero_comm_ring.to_comm_ring.{0} 𝕜
(@local_ring.to_nonzero_comm_ring.{0} 𝕜
(@field.local_ring.{0} 𝕜
(@normed_field.to_field.{0} 𝕜 A)))))
(@normed_group.to_add_comm_group.{0} (E i) (N i)) :=
by apply_instance -- fails
-- all_right -- works
lemma outer_works :
(Π (i : fin n),
@module.{0} 𝕜 (E i)
(@normed_ring.to_ring.{0} 𝕜
(@normed_field.to_normed_ring.{0} 𝕜 A))
(@normed_group.to_add_comm_group.{0} (E i) (N i)))
=
(Π (i : fin n),
@module.{0} 𝕜 (E i)
(@comm_ring.to_ring.{0} 𝕜
(@nonzero_comm_ring.to_comm_ring.{0} 𝕜
(@local_ring.to_nonzero_comm_ring.{0} 𝕜
(@field.local_ring.{0} 𝕜
(@normed_field.to_field.{0} 𝕜 A)))))
(@normed_group.to_add_comm_group.{0} (E i) (N i))) :=
by tactic.reflexivity tactic.transparency.instances
```

In the first lemma, the instance is found. In the second lemma, the instance is not found. But from the point of view of instance resolution, these two things should be the same as the third lemma shows that they are equal for ` tactic.reflexivity tactic.transparency.instances`

.

#### Mario Carneiro (May 16 2020 at 20:58):

This is apparently an issue with typeclass inference, and I'm not qualified to fix it in the C++

#### Mario Carneiro (May 16 2020 at 20:58):

it is not using instance reducibility for some subproblems

#### Mario Carneiro (May 16 2020 at 20:59):

does `simp`

fix it?

#### Sebastien Gouezel (May 16 2020 at 21:00):

In my use case, the instance has to be inferred automatically even to let me state my lemma, so `simp`

is not really an option...

#### Sebastien Gouezel (May 16 2020 at 21:01):

So, your guess if that `apply_instance`

is passing the flag `tactic.transparency.reducibility`

instead of `tactic.transparency.instances`

somewhere. Yes, that would perfectly explain the behavior I am seeing.

#### Mario Carneiro (May 16 2020 at 21:02):

I guess you could locally hide a bad instance?

#### Mario Carneiro (May 16 2020 at 21:02):

like I doubt you need local rings for this

#### Sebastien Gouezel (May 16 2020 at 21:05):

Yes, I could certainly do that. But we have already been bitten by this with the `pi_instance`

issue (where it was solved by cleaning up the tactic to make sure that it generates diamonds that are solved with `tactic.transparency.reducibility`

), so I am afraid it will come up again later. If you think this is a C++ problem, all I can do is invoke @Gabriel Ebner (but not now, it's the week-end) and pray :)

#### Patrick Massot (May 16 2020 at 21:12):

We need the Zulip developers to implement deferred pings.

#### Sebastien Gouezel (May 16 2020 at 21:18):

I have opened an issue with all the details, and I'll do the manual pinging later.

#### Yury G. Kudryashov (May 17 2020 at 00:37):

BTW, @Heather Macbeth what is your goal with the `normed_space`

/`normed_algebra`

PRs? I mean, do you want to formalize something specific or just filling in a hole in the library?

#### Heather Macbeth (May 17 2020 at 02:52):

When I noticed these things, I was trying to prove that under appropriate hypotheses C(X, 𝕜) is a Banach algebra.

#### Heather Macbeth (May 17 2020 at 02:52):

I am not sure what I will try next, maybe Holder spaces.

#### Yury G. Kudryashov (May 17 2020 at 03:01):

Good idea!

#### Yury G. Kudryashov (May 17 2020 at 03:02):

I pushed `normed_ring`

instance, then realized that now we do two loosely related changes in one PR.

#### Yury G. Kudryashov (May 17 2020 at 03:03):

So possibly this part should be reverted and moved to another PR. Do you have a `normed_algebra`

instance?

#### Heather Macbeth (May 17 2020 at 03:04):

Do you mean, that C(X, 𝕜) is a normed ring?

#### Heather Macbeth (May 17 2020 at 03:04):

Or do you mean an internal change to `normed_space`

regarding normed rings?

#### Yury G. Kudryashov (May 17 2020 at 03:07):

I mean this instance

#### Heather Macbeth (May 17 2020 at 03:08):

Ah great. Yes, I had some draft code doing approximately that :)

#### Yury G. Kudryashov (May 17 2020 at 03:08):

The next instance should be something like `instance [nonempty α] {R : Type*} [normed_algebra 𝕜 R] : algebra 𝕜 (α →ᵇ R)`

.

#### Heather Macbeth (May 17 2020 at 03:08):

But keep it!

#### Yury G. Kudryashov (May 17 2020 at 03:08):

then `normed_algebra`

#### Yury G. Kudryashov (May 17 2020 at 03:08):

Do you have these instances, or I should write&push mine?

#### Heather Macbeth (May 17 2020 at 03:12):

Just checked .. I have `algebra`

but not yet `normed_algebra`

#### Heather Macbeth (May 17 2020 at 03:13):

That was why I caught the missing `normed_algebra.to_normed_space`

instance

#### Heather Macbeth (May 17 2020 at 03:13):

If you like I can finish tomorrow and push as part of the same PR

#### Yury G. Kudryashov (May 17 2020 at 03:17):

I've just created a new branch `bcf-normed-algebra`

. I'm going to revert some changes in the `norm-smul`

branch. It would be nice if you'll push the two missing instances to the new branch tomorrow, then open a new PR.

#### Heather Macbeth (May 17 2020 at 03:17):

Great, will do.

#### Yury G. Kudryashov (May 17 2020 at 03:18):

I can fix merge conflicts once `norm_smul`

will be merged.

#### Yury G. Kudryashov (May 17 2020 at 03:26):

reverted This means that we shouldn't merge `norm-smul`

into `bcf-normed-algebra`

.

#### Yury G. Kudryashov (May 17 2020 at 03:45):

I'd love to have the following fact about Hölder continuous functions in `mathlib`

: if `f : X → Y`

is Hölder continuous with exponent `α`

, then $\operatorname{dim}_H Y \le \frac{1}{α}\operatorname{dim}_H X$. This is an easy exercise but we have neither Hölder continuous functions nor Hausdorff dimension.

#### Heather Macbeth (May 17 2020 at 03:47):

Yes, I noticed that Hausdorff dimension is missing. Also a good project.

#### Heather Macbeth (May 17 2020 at 03:49):

I would like to try to get $C^{2,\alpha}$ estimates for the Newtonian potential

#### Heather Macbeth (May 17 2020 at 03:50):

Probably there are a lot of things missing before that can be done, but it would be a useful test to show what the library is missing.

#### Yury G. Kudryashov (May 17 2020 at 03:51):

Then you'll probably need FTC. We have an abandoned PR with it. I hope to take over this PR soon. Unfortunately, I'm getting distracted by other tasks.

#### Heather Macbeth (May 17 2020 at 03:51):

I saw that you are doing the implicit function theorem, that would be really great.

#### Heather Macbeth (May 17 2020 at 03:52):

People could make some examples of manifolds once you do that!

#### Yury G. Kudryashov (May 17 2020 at 03:53):

It's mostly done but I need complemented subspaces to write a good API.

#### Heather Macbeth (May 17 2020 at 03:56):

There also needs to be a theory of strict k-times-differentiable functions, right?

#### Heather Macbeth (May 17 2020 at 03:56):

To get inverse and implicit function theorems in arbitrary differentiability

#### Yury G. Kudryashov (May 17 2020 at 04:05):

Do we need `f`

to be strictly differentiable `k`

times?

#### Yury G. Kudryashov (May 17 2020 at 04:05):

Once we have the inverse function, its differentiability follows from differentiability of the original function.

#### Yury G. Kudryashov (May 17 2020 at 04:06):

See this lemma

#### Heather Macbeth (May 17 2020 at 04:15):

Maybe that's right. Then one ends up with manifolds whose structure groupoid (if I have learned the library's language correctly yet :slight_smile: ) consists of functions which are 1-time strictly differentiable, k-times differentiable?

#### Sebastien Gouezel (May 17 2020 at 07:07):

The plan is rather to work on reals or complexes, where `C^k`

functions are automatically strictly differentiable.

#### Kevin Buzzard (May 17 2020 at 08:26):

People could make some examples of manifolds once you do that!

There are no examples of anything in mathlib. We don't even have dihedral groups. For some reason examples don't form part of the philosophy. I would love to see examples. When we made schemes the computer scientists said we should make examples, and then we proved that the spectrum of a ring was a scheme and somehow this was enough because we can in theory make examples of rings

#### Yury G. Kudryashov (May 17 2020 at 08:46):

Some examples of manifolds are useful for general theory. E.g., there are theorems about $S^n$ and $\mathbb RP^n$.

#### Kevin Buzzard (May 17 2020 at 08:47):

I think Kenny made the scheme P^1 at some point but the gluing was hard work

#### Kevin Buzzard (May 17 2020 at 08:48):

I'm sure S^n would be straightforward once you have the basic theorems. How would you do projective space though?

#### Yury G. Kudryashov (May 17 2020 at 08:49):

It would be nice to have

- ${\mathbb P}E$ for a vector space $E$;
- embedding of $\mathbb P^n$ into an affine space of larger dimension (don't remember if there is a general formula for this).

#### Kevin Buzzard (May 17 2020 at 08:51):

Do you have a plan for quotients? What I'm saying is that in alg geom they were a challenge

#### Kenny Lau (May 17 2020 at 08:51):

I thought about PE earlier (like a year ago maybe), and I decided that PE requires Grassmannian which requires linear algebra

#### Kevin Buzzard (May 17 2020 at 09:15):

Putting a manifold structure on the quotient of a manifold by a lie group action might be a challenge. Will there be underlying type theory problems which mathematicians don't usually notice?

#### Kevin Buzzard (May 17 2020 at 09:17):

I'm thinking $G/H$ with for example $G=GL_2(\mathbb{R})$ and $H$ the upper triangular matrices.

#### Yury G. Kudryashov (May 17 2020 at 09:18):

Specifically for the projective space we can come up with an explicit atlas

#### Kevin Buzzard (May 17 2020 at 09:42):

I would have said the same thing about the alg geom projective space but it was much easier said than done in practice

#### Patrick Massot (May 17 2020 at 09:55):

We'll need affine charts for projective spaces at some-point (but first we'll need affine spaces...). But this is not the morally correct way to put a manifold structure on them. We need quotient manifolds.

#### Heather Macbeth (May 17 2020 at 13:56):

Yury G. Kudryashov said:

It would be nice to have

- ${\mathbb P}E$ for a vector space $E$;
- embedding of $\mathbb P^n$ into an affine space of larger dimension (don't remember if there is a general formula for this).

I believe $\mathbb P^n$ embeds (non-holomorphically) into the space of Hermitian $(n+1)\times(n+1)$ matrices.

#### Heather Macbeth (May 17 2020 at 13:57):

But a non-holomorphic embedding only allows one to construct it (via the implicit function theorem) as a real manifold, not as a complex manifold.

#### Heather Macbeth (May 17 2020 at 13:59):

A bounded holomorphic function is constant, so there is no holomorphic embedding.

#### Kevin Buzzard (May 17 2020 at 14:00):

I think constructing projective n-space as a complex manifold might be quite challenging, given what we have.

#### Heather Macbeth (May 17 2020 at 14:02):

Kevin Buzzard said:

Putting a manifold structure on the quotient of a manifold by a lie group action might be a challenge. Will there be underlying type theory problems which mathematicians don't usually notice?

The right theorem is, the quotient by a free proper action is a manifold.

#### Heather Macbeth (May 17 2020 at 14:02):

I think, for this, one needs existence & uniqueness for ODEs

#### Kevin Buzzard (May 17 2020 at 14:03):

In Lean this will be a definition, not a theorem, and it might be challenging.

#### Reid Barton (May 17 2020 at 14:03):

But you also can't construct CP^n as a complex manifold this way, can you?

#### Kevin Buzzard (May 17 2020 at 14:03):

Not the $\mathbb{C}^\times$ action on a vector space of one dimension higher, minus the origin?

#### Heather Macbeth (May 17 2020 at 14:03):

Yes, I think that's fine.

#### Reid Barton (May 17 2020 at 14:03):

Isn't it not proper?

#### Kevin Buzzard (May 17 2020 at 14:03):

Oh maybe I don't know what proper means

#### Reid Barton (May 17 2020 at 14:04):

Maybe I don't know!

#### Heather Macbeth (May 17 2020 at 14:04):

Proper in this case means that the map $G\times M \to M \times M$ is proper.

#### Heather Macbeth (May 17 2020 at 14:05):

I think that's fine here.

#### Heather Macbeth (May 17 2020 at 14:05):

Anyway, even if not, one could take the quotient of $S^{2n+1}$ by $S^1$.

#### Reid Barton (May 17 2020 at 14:05):

Yes, I was just dimly recalling this definition. That's fine then.

#### Kevin Buzzard (May 17 2020 at 14:05):

Then Reid's point is that this doesn't give the complex structure

#### Reid Barton (May 17 2020 at 14:07):

The $(\mathbb{C}^{n+1} - \{0\})/\mathbb{C}^\times$ definition is fine though, I was just using the wrong definition of proper quotient.

#### Heather Macbeth (May 17 2020 at 14:09):

Heather Macbeth said:

The right theorem is, the quotient by a free proper action is a manifold.

Just skimming the proof .

#### Heather Macbeth (May 17 2020 at 14:10):

First, implicit function theorem to show that the G-orbits are properly embedded submanifolds

#### Heather Macbeth (May 17 2020 at 14:11):

Then, existence & uniqueness for ODEs, with smooth dependence on initial conditions, to put charts on the G-orbits via the exponential map, uniformly across a slice.

#### Heather Macbeth (May 17 2020 at 14:17):

Kevin Buzzard said:

I think constructing projective n-space as a complex manifold might be quite challenging, given what we have.

But why can projective n-space not currently be constructed from n+1 affine charts?

#### Kevin Buzzard (May 17 2020 at 14:17):

Ask @Kenny Lau

#### Heather Macbeth (May 17 2020 at 14:17):

Is it just that it's still a pain to differentiate actual functions?

#### Kevin Buzzard (May 17 2020 at 14:18):

The problem, I believe, is that quotients are very intuitive to mathematicians but my limited experience with using them in Lean to make complex objects has been extremely painful.

#### Kevin Buzzard (May 17 2020 at 14:19):

You have two copies of affine 1-space, and then you take the disjiont union, make the quotient, and now we have the underlying type

#### Kevin Buzzard (May 17 2020 at 14:19):

but now you need to actually make a structure which has been formalised but which is truly complicated

#### Kevin Buzzard (May 17 2020 at 14:19):

and building that structure will involve actually checking all the axioms

#### Kevin Buzzard (May 17 2020 at 14:20):

and Patrick's experience checking that various definitions of manifolds were equivalent was a lot more difficult than he expected.

#### Heather Macbeth (May 17 2020 at 14:20):

I see. So when you construct it from n+1 charts, you are not actually avoiding a quotient construction. You are just introducing a messier quotient construction.

#### Kevin Buzzard (May 17 2020 at 14:20):

Now we've gone with one. Maybe it was the best for making an API or something.

#### Heather Macbeth (May 17 2020 at 14:20):

disjoint union of n+1 copies of $\mathbb{C}^n$ via identification of points

#### Kevin Buzzard (May 17 2020 at 14:20):

But now let's see whether it's any good for making an example.

#### Heather Macbeth (May 17 2020 at 14:21):

rather than $\mathbb{C}^*$ quotient of $\mathbb{C}^{n+1}\setminus\{0\}$

#### Kevin Buzzard (May 17 2020 at 14:21):

Yes, making the underlying type is no problem. But now you have to hope that quotient topologies and quotient functions and quotient "I am differentiable" and everything all works fine

#### Kevin Buzzard (May 17 2020 at 14:21):

Glueing and quotienting by a group action are both quotients from the point of view of type theory

#### Kevin Buzzard (May 17 2020 at 14:22):

All I'm saying is that it might be painful but possible. This was what happened in alg geom anyway.

#### Kevin Buzzard (May 17 2020 at 14:22):

And diff geom is harder :-)

#### Reid Barton (May 17 2020 at 14:22):

Both of these constructions are of course very important in general.

#### Kevin Buzzard (May 17 2020 at 14:28):

For me this was a shock. We had two rings A and B, an explicit isomorphism A[1/f]=B[1/g], where of course I'm using equality the way a mathematician does, but then to get the corresponding isomorphism of the locally ringed spaces is not immediate in dependent type theory, and a locally ringed space is a complex object. However I believe the objects you're dealing with are more complex

#### Heather Macbeth (May 17 2020 at 14:31):

Has someone done the quotient of a topological space by an equivalence relation, yet?

#### Reid Barton (May 17 2020 at 14:32):

Yes: https://github.com/leanprover-community/mathlib/blob/master/src/topology/constructions.lean#L45-L49

#### Reid Barton (May 17 2020 at 14:32):

(the second one, for an equivalence relation, but the construction is the same)

#### Patrick Massot (May 17 2020 at 17:12):

I'm sorry I missed the fun discussion. I haven't read very carefully all messages, but I have a couple of comments.

- Kevin likes to say differential geometry is harder than algebraic geometry but this is of course meaningless (and he knows it)
- There is no obstruction at all to defining projective spaces in currently mathlib, including the topology in the real or complex cases.
- There is no obstruction to build a manifold structure on projective space in the real and complex cases. We could do that in at most one day. But it would bring us nothing interesting.
- There is an obstruction to quickly do it right, because the natural proof requires machinery that would take time to build. This would be interesting.

#### Heather Macbeth (May 17 2020 at 17:17):

Kevin Buzzard said:

You have two copies of affine 1-space, and then you take the disjiont union, make the quotient, and now we have the underlying type

@Patrick Massot , are you saying that doing this for $\mathbb{P}^{n}$ using n+1 charts is not actually that hard?

#### Heather Macbeth (May 17 2020 at 17:18):

Heather Macbeth said:

Putting a manifold structure on the quotient of a manifold by a lie group action might be a challenge. Will there be underlying type theory problems which mathematicians don't usually notice?

The right theorem is, the quotient by a free proper action is a manifold.

And is this what you mean by "the right way"?

#### Patrick Massot (May 17 2020 at 17:24):

What Kevin wrote is not the right. The underlying type should be the natural one, without making any choice. Start with a vector space $E$ and define the obvious quotient of $E \setminus \{0\}$ to get $P(E)$. And then, assuming the base field is real or complex numbers there are two roads. In the first road you define affine charts (which will be very sad because we don't have affine spaces) and check transition maps are real or complex analytic (here I'm not sure whether Sébastien is totally ready, maybe I should say smooth instead of analytic). This is what I call the wrong way, but I'm exaggerating a bit when I write this would bring nothing good. What I call the right way is to setup the quotient manifold infrastructure.

#### Patrick Massot (May 17 2020 at 17:26):

Note that I never mention trying to get exactly $n+1$ charts (or finite dimensionality). I don't see what good it would do. Affine chart are defined as soon as you fix a hyperplane, and their canonical affine structure is much more apparent if you don't pollute things with coordinates.

#### Heather Macbeth (May 17 2020 at 17:30):

OK, makes sense!

#### Heather Macbeth (May 17 2020 at 17:32):

Even while the quotient infrastructure is not yet set up, people could work on defining Lie groups, Lie group actions, freeness and properness of Lie group actions

#### Heather Macbeth (May 17 2020 at 17:32):

And make a bunch of examples of $GL(n)$-actions and discrete group actions

#### Heather Macbeth (May 17 2020 at 17:33):

($GL(n)$ and discrete groups being the only Lie groups available without the implicit function theorem)

#### Heather Macbeth (May 17 2020 at 17:34):

So that as soon as the quotient manifold infrastructure is done, there are immediately several new examples of manifolds produced

#### Kevin Buzzard (May 17 2020 at 17:36):

Off topic: A poor man's definition of an automorphic form is a function on $GL(n,\mathbb{R})$ which satisfies certain differential equations (coming from the centre of the universal enveloping algebra of the Lie alegbra). I feel like we are slowly but surely converging to the point where we might be able to do this.

#### Patrick Massot (May 17 2020 at 17:38):

This is all part of the missing infrastructure, so yes, these are all steps in the right direction

#### Yury G. Kudryashov (May 17 2020 at 18:27):

@Heather Macbeth Merged master into `bcf-normed-algebra`

.

#### Heather Macbeth (May 17 2020 at 18:35):

Thanks, doing the rest now. I discovered that the `normed_algebra`

structure on bounded continuous functions only works when the domain is nonempty!

#### Heather Macbeth (May 17 2020 at 18:36):

It uses this lemma

`@[simp] lemma norm_const_eq [h : nonempty α] (b : β) : ∥const α b∥ = ∥b∥ `

#### Heather Macbeth (May 17 2020 at 18:37):

Is there a way to add a hypothesis to an instance?

#### Kevin Buzzard (May 17 2020 at 18:37):

The instance might never trigger, unless the hypothesis is itself a typeclass.

#### Reid Barton (May 17 2020 at 18:38):

`instance [nonempty α] : normed_algebra ...`

#### Heather Macbeth (May 17 2020 at 18:58):

Sorry, another question, very much like this one @Yury G. Kudryashov answered for me on Thursday. The following

```
import algebra.ring
import analysis.normed_space.basic
example {R : Type*} [comm_ring R] [normed_ring R] (a b : R) : a * b = b * a :=
begin
apply mul_comm,
end
```

fails with "invalid apply tactic, failed to unify `a * b = b * a`

with `?m_3 * ?m_4 = ?m_4 * ?m_3`

". (I discovered this while trying to get that $C(α, R)$ is commutative if $R$ is.)

#### Heather Macbeth (May 17 2020 at 18:59):

Is this impossible to fix without implementing a theory of `normed_comm_ring`

which unifies `comm_ring`

and `normed_ring`

?

#### Yury G. Kudryashov (May 17 2020 at 19:00):

I think you're right, you need one more typeclass.

#### Heather Macbeth (May 18 2020 at 04:29):

PR'd, #2722

#### Heather Macbeth (May 18 2020 at 04:32):

I decided not to make `normed_comm_ring`

, that can wait for a future refactor of `normed_space.basic`

Last updated: May 06 2021 at 18:20 UTC