Normed spaces

Stream: maths

[Heather Macbeth]

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]

1. Implement normed_algebra.to_normed_space, prior discussion

[Heather Macbeth]

2. 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]

Changes that I considered but did not currently implement:

[Heather Macbeth]

3. 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]

4. 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]

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]

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]

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]

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

[Heather Macbeth]

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

[Heather Macbeth]

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

[Yury G. Kudryashov]

Feel free to take over this

[Yury G. Kudryashov]

I'm sorry for starting this without announcing here.

[Yury G. Kudryashov]

Note that I simplified several proofs in bounded_continuous_function

[Heather Macbeth]

Yes, I think this is likely to be one advantage of replacing norm_smul with norm_smul_le.

[Heather Macbeth]

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

[Yury G. Kudryashov]

operator_norm?

[Heather Macbeth]

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]

normed_module having the norm_smul_le axiom

[Yury G. Kudryashov]

Yes.

[Heather Macbeth]

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]

1, 2, 3: sure
4: I don't care about instance names

[Heather Macbeth]

Ok great.

[Heather Macbeth]

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]

Then when that is merged, make the space to module change as a second PR.

[Yury G. Kudryashov]

Whatever is more convenient for you.

[Yury G. Kudryashov]

Your PR has nicer code than mine.

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

[Heather Macbeth]

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]

@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]

I don't mind.

[Yury G. Kudryashov]

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

[Heather Macbeth]

Sure, go ahead!

[Heather Macbeth]

@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]

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]

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

[Sebastien Gouezel]

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]

@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]

Go ahead.

[Sebastien Gouezel]

@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]

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]

With tactic.transparency.instances, everything works.

[Mario Carneiro]

This sounds like "working as intended" though

[Mario Carneiro]

reflexivity reducible is supposed to unfold only reducible definitions, not instances

[Mario Carneiro]

doesn't simp have a canonize_instances option that is supposed to fix issues like this?

[Sebastien Gouezel]

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]

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

[Mario Carneiro]

it is not using instance reducibility for some subproblems

[Mario Carneiro]

does simp fix it?

[Sebastien Gouezel]

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]

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]

I guess you could locally hide a bad instance?

[Mario Carneiro]

like I doubt you need local rings for this

[Sebastien Gouezel]

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]

We need the Zulip developers to implement deferred pings.

[Sebastien Gouezel]

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

[Yury G. Kudryashov]

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]

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

[Heather Macbeth]

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

[Yury G. Kudryashov]

Good idea!

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Heather Macbeth]

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

[Heather Macbeth]

Or do you mean an internal change to normed_space regarding normed rings?

[Yury G. Kudryashov]

I mean this instance

[Heather Macbeth]

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

[Yury G. Kudryashov]

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

[Heather Macbeth]

But keep it!

[Yury G. Kudryashov]

then normed_algebra

[Yury G. Kudryashov]

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

[Heather Macbeth]

Just checked .. I have algebra but not yet normed_algebra

[Heather Macbeth]

That was why I caught the missing normed_algebra.to_normed_spaceinstance

[Heather Macbeth]

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

[Yury G. Kudryashov]

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]

Great, will do.

[Yury G. Kudryashov]

I can fix merge conflicts once norm_smul will be merged.

[Yury G. Kudryashov]

reverted This means that we shouldn't merge norm-smul into bcf-normed-algebra.

[Yury G. Kudryashov]

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]

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

[Heather Macbeth]

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

[Heather Macbeth]

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]

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]

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

[Heather Macbeth]

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

[Yury G. Kudryashov]

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

[Heather Macbeth]

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

[Heather Macbeth]

To get inverse and implicit function theorems in arbitrary differentiability

[Yury G. Kudryashov]

Do we need f to be strictly differentiable k times?

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

See this lemma

[Heather Macbeth]

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]

The plan is rather to work on reals or complexes, where C^k functions are automatically strictly differentiable.

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Yury G. Kudryashov]

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]

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

[Kenny Lau]

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

[Kevin Buzzard]

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]

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

[Yury G. Kudryashov]

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

[Kevin Buzzard]

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]

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]

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]

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]

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

[Kevin Buzzard]

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

[Heather Macbeth]

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]

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

[Kevin Buzzard]

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

[Reid Barton]

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

[Kevin Buzzard]

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

[Heather Macbeth]

Yes, I think that's fine.

[Reid Barton]

Isn't it not proper?

[Kevin Buzzard]

Oh maybe I don't know what proper means

[Reid Barton]

Maybe I don't know!

[Heather Macbeth]

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

[Heather Macbeth]

I think that's fine here.

[Heather Macbeth]

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

[Reid Barton]

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

[Kevin Buzzard]

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

[Reid Barton]

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]

Heather Macbeth said:

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

Just skimming the proof .

[Heather Macbeth]

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

[Heather Macbeth]

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]

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]

Ask @Kenny Lau

[Heather Macbeth]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

and building that structure will involve actually checking all the axioms

[Kevin Buzzard]

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

[Heather Macbeth]

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]

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

[Heather Macbeth]

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

[Kevin Buzzard]

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

[Heather Macbeth]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

And diff geom is harder :-)

[Reid Barton]

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

[Kevin Buzzard]

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]

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

[Reid Barton]

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

[Reid Barton]

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

[Patrick Massot]

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]

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]

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]

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]

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]

OK, makes sense!

[Heather Macbeth]

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]

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

[Heather Macbeth]

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

[Heather Macbeth]

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

[Kevin Buzzard]

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]

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

[Yury G. Kudryashov]

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

[Heather Macbeth]

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]

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

[Heather Macbeth]

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

[Kevin Buzzard]

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

[Reid Barton]

instance [nonempty α] : normed_algebra ...

[Heather Macbeth]

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]

Is this impossible to fix without implementing a theory of normed_comm_ring which unifies comm_ring and normed_ring?

[Yury G. Kudryashov]

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

[Heather Macbeth]

PR'd, #2722

[Heather Macbeth]

I decided not to make normed_comm_ring, that can wait for a future refactor of normed_space.basic