matrix groups and Lie groups

Stream: Is there code for X?

[Winston Yin]

I'm just itching to contribute something to mathlib. I can't find that docs#matrix.general_linear_group is a Lie group, or the definitions of other common matrix Lie groups, or how to obtain a Lie algebra from a Lie group. Is somebody working on any of these, or should I try to tackle some of these? What would some missing prerequisites be?

[Eric Rodriguez]

cc @Oliver Nash

[Heather Macbeth]

@Winston Yin You should see the stub at this file
https://leanprover-community.github.io/mathlib_docs/geometry/manifold/instances/units_of_normed_algebra.html

[Heather Macbeth]

Your timing is good actually, because one of the prerequisites mentioned in the TODO,

cont_diff_mul (needs to be generalized from field to algebra)

was just completed last week, #15595

[Heather Macbeth]

So the main prerequisite is the other TODO mentioned,

• for an open embedding f, whose domain is equipped with the induced manifold structure f.singleton_smooth_manifold_with_corners, characterization of smoothness of functions to/from this manifold in terms of smoothness in the target space. See the pair of lemmas cont_mdiff_coe_sphere and cont_mdiff.cod_restrict_sphere for a model.

[Heather Macbeth]

After that, you should be well on the way to proving that GL(n) (in the form of the docs#units of docs#continuous_linear_map, not the form docs#matrix.general_linear_group you mentioned) is a Lie group.

[Winston Yin]

Thanks for the guide!

[Eric Wieser]

In case you missed it we also have docs#linear_map.general_linear_group, but that's not with continuity

[Heather Macbeth]

@Patrick Massot and I counted last week that there are at least five things in mathlib that could claim to be the general linear group. "Sameness" is difficult in formalization!

[Eric Wieser]

I'm curious what that list was, if you have it to hand

[Heather Macbeth]

I do, in fact:

• the group of automorphisms
• units of the ring of endomorphisms
• the group of bicontinuous automorphisms
• units of the ring of continuous endomorphisms
• matrix version

[Heather Macbeth]

Number 4 is the one which will be made a Lie group by the above strategy.

[Eric Wieser]

Oh of course, I forgot about the versions stated via equivs

[Johan Commelin]

Winston Yin said:

or how to obtain a Lie algebra from a Lie group

I think we have something in this direction, but I forgot where to find it :oops:

[Oliver Nash]

We have docs#left_invariant_derivation.lie_algebra which is one possible approach.

[Oliver Nash]

I think a valuable addition would be to construct the Lie bracket on smooth sections of docs#tangent_bundle (for any manifold).

[Winston Yin]

(deleted)

[Winston Yin]

Lie group of ring units in PR #15763. Still needs some cleanup

[Winston Yin]

Update: I've generalised the proofs so that smooth_mul and smooth_inv are now consequences of the theorem that the differentiability of a function g : M → M' between manifolds can be stated in terms of the differentiability of the corresponding function f : E → E' between the model vector spaces, given that there are open embeddings e : M → E and e' : M' → E', and that the extended charts on M and M' coincide with e and e', respectively.

[Winston Yin]

The actual file is still a mess. I'll need to wrestle with the type checker to find the least verbose arrangement of variables

[Winston Yin]

Because product manifolds are weird when formalised, there are two theorems, one more general (used to prove smooth_mul) but super verbose and the other only applying to manifolds made with singleton_smooth_manifold_with_corners (used to prove smooth_inv)

[Heather Macbeth]

Nice work! I would recommend dividing into two separate lemmas, though. One lemma should be just about when M', the target, is made from an open embedding e' : M' → E'. And the other lemma, which should cover everything you need about the domain, should be that when M is made from an open embedding e : M → E, then e itself is cont_mdiff.

[Heather Macbeth]

You can see what's done with docs#cont_mdiff.cod_restrict_sphere and docs#cont_mdiff_coe_sphere , respectively, as a model.

[Winston Yin]

I'm having some trouble using the sphere example as a model. What I'm trying to do is a generalisation of docs#cont_diff_on.cont_mdiff_on that can be used to show both smooth_mul and smooth_inv for ring units. While the inverse is a map from Rˣ to Rˣ, which is made from singleton_smooth_manifold_with_corners, the multiplication is a map from the product manifold Rˣ × Rˣ, whose manifold structure isn't defeq to the one induced from a single open embedding f : Rˣ × Rˣ → R × R.

The way I've generalised the lemma to take care of this case is to assume the model with corners I for the domain M to be an open map, and to assume that the extended chart at every point on the codomain M' to cover the whole space M'. These two assumptions are obviously true in the case of manifolds made with singleton_charted_space and model_with_corners_self.

...
{n : with_top ℕ} {f : E → E'} {g : M → M'}
(hI : is_open_map I) (hI' : ∀ x : M', (ext_chart_at I' x).source = set.univ)
(hf : ∀ x : M, cont_diff_on 𝕜 n f (ext_chart_at I x).target)
(hfg : ∀ x y, f ∘ (ext_chart_at I x) = (ext_chart_at I' y) ∘ g ) :
cont_mdiff I I' n g

If I'm understanding the suggestion correctly, we want the equivalent of docs#cont_mdiff_coe_sphere to show that the extended chart is smooth, and then the smoothness of g can be shown by first replacing it with (ext_chart_at I' y).symm ∘ f ∘ (ext_chart_at I x) and then using composition of smooth maps. However, the assumptions above appear to be too weak to show the smoothness of, say, (ext_chart_at I x) itself.

[Winston Yin]

I'd be happy to write some lemmas about the smoothness of open embeddings themselves, and they can certainly be used to show smooth_inv, but for the purpose of showing smooth_mul, the assumptions above seem to be relatively more general. Please let me know if I'm missing something!

[Winston Yin]

#15763 has a current version of the lemmas

[Heather Macbeth]

@Winston Yin Let's check we're on the same page. Here are the two lemmas I was proposing you write. The idea is that all manipulation of charts gets hidden inside them. Did you try something along these lines?

import geometry.manifold.cont_mdiff

noncomputable theory

variables
  {𝕜 : Type*} [nontrivially_normed_field 𝕜]
  {E : Type*} [normed_add_comm_group E] [normed_space 𝕜 E]
  {H : Type*} [topological_space H] (I : model_with_corners 𝕜 E H)
  {M : Type*} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M]
  (s : topological_space.opens M)

-- move this copy of `topological_space.opens.charted_space` to near the original lemma,
-- apparently need the variant because of the distinction between `↥s` and `↥↑s`
instance topological_space.opens.charted_space' : charted_space H (s : set M) :=
topological_space.opens.charted_space s

lemma cont_mdiff_coe_opens {m : with_top ℕ} : cont_mdiff I I m (coe : s → M) :=
sorry

variables
  {E' : Type*} [normed_add_comm_group E'] [normed_space 𝕜 E']
  {H' : Type*} [topological_space H'] {I' : model_with_corners 𝕜 E' H'}
  {M' : Type*} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M']

lemma cont_mdiff.cod_restrict_opens {m : with_top ℕ}
  {f : M' → M} (hf : cont_mdiff I' I m f) (hf' : ∀ x, f x ∈ s) :
  cont_mdiff I' I m (set.cod_restrict f s hf') :=
sorry

[Heather Macbeth]

You can also look at docs#circle.lie_group to see how the analogues of these two lemmas turn up in the proof that the circle is a Lie group.

[Heather Macbeth]

If you hit problems in the with-boundary case (there are certainly subtleties there with products, and I haven't thought about whether the lemmas should still be true), you can drop the H's and I's and just work with 𝓘(𝕜, E) or 𝓘(𝕜, E') as needed.

[Heather Macbeth]

@Winston Yin PS Sorry, I just noticed that in your use case the units are not literally an open subset of the algebra, but rather are some type with a natural embedding to that algebra. So you need the version of the above lemmas for an open embedding, rather than just subtype inclusion. This should do it (again modulo caveats in the with-boundary case):

import geometry.manifold.cont_mdiff

variables
  {𝕜 : Type*} [nontrivially_normed_field 𝕜]
  {E : Type*} [normed_add_comm_group E] [normed_space 𝕜 E]
  {H : Type*} [topological_space H] (I : model_with_corners 𝕜 E H)
  {M : Type*} [topological_space M]
  [nonempty M] {f : M → H} (h : open_embedding f)

lemma cont_mdiff_open_embedding {m : with_top ℕ} :
  @cont_mdiff _ _ _ _ _ _ _ I _ _ h.singleton_charted_space _ _ _ _ _ I _ _ _ m f :=
sorry

variables
  {E' : Type*} [normed_add_comm_group E'] [normed_space 𝕜 E']
  {H' : Type*} [topological_space H'] {I' : model_with_corners 𝕜 E' H'}
  {M' : Type*} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M']

lemma cont_mdiff.of_comp_open_embedding {m : with_top ℕ}
  {φ : M' → M} (hφ : cont_mdiff I' I m (f ∘ φ)) :
  @cont_mdiff _ _ _ _ _ _ _ I' _ _ _ _ _ _ _ _ I _ _ h.singleton_charted_space m φ :=
sorry

[Winston Yin]

Thanks for the detailed explanation. Suppose we have your cont_mdiff.of_comp_open_embedding. Is the strategy to then show cont_mdiff I' I m (f ∘ φ) by equivalently showing cont_mdiff I' I m (φ' ∘ f'), where f' : M' → H' is an open embedding and φ' is the "same" map as φ but on E' → E?

[Winston Yin]

Because the goal as I understand it is to express cont_mdiff on the manifolds in terms of the much simpler cont_diff on the model spaces, when there's an open embedding of the manifolds into the model space, on which a cont_diff lemma is already proven. A single theorem like docs#cont_diff_on.cont_mdiff_on but more general

[Winston Yin]

I'm sorry if I'm fundamentally misunderstanding the intended use case of your suggested lemmas

[Winston Yin]

In particular for inversion of ring units, your cont_mdiff.of_comp_open_embedding would leave us with the goal cont_mdiff 𝓘(𝕜, R) 𝓘(𝕜, R) ⊤ (coe ∘ λ (a : Rˣ), a⁻¹). A few more steps are still needed before docs#cont_diff_at_ring_inverse is applicable.

[Heather Macbeth]

@Winston Yin You can look at docs#circle.lie_group for a model. So, e.g., to show that inv : Rˣ → Rˣ is m-smooth

1. by cont_mdiff.of_comp_open_embedding it suffices to show that coe ∘ inv : Rˣ → R is m-smooth
2. the map coe ∘ inv : Rˣ → R is equal to ring.inverse ∘ coe (here docs#ring.inverse is this extended-by-junk-values "inverse")
3. by cont_mdiff_open_embedding the map coe : Rˣ → R is m-smooth
4. by docs#cont_diff_at_ring_inverse the map ring.inverse : R → R is smooth (on the needed domain) and therefore m-smooth
5. composition of m-smooth maps is m-smooth

[Winston Yin]

That coincides with my understanding. Thank you.

[Winston Yin]

This 5 step process is what I initially imagined the generalised lemmas to be, hence the ones I wrote in the linked PR

[Winston Yin]

I will further break them down and rephrase them. Stay tuned :)

[Heather Macbeth]

By the way, I'll be on holiday next week, and not replying quite so fast!

[Heather Macbeth]

@Winston Yin One more suggestion. The lemmas I suggested you route through are awkward, because of all the _. When you prove them you can make it less awkward within the proofs by starting with a line like,

letI := h.singleton_charted_space,

And afterwards, when you're using them, you can make it less awkward by restating them in the context when typeclass inference will be able to find the arguments:

variables
  {R : Type*} [normed_ring R] [complete_space R]
  {𝕜 : Type*} [nontrivially_normed_field 𝕜] [normed_algebra 𝕜 R]

lemma units.cont_mdiff_coe {m : with_top ℕ} : cont_mdiff 𝓘(𝕜, R) 𝓘(𝕜, R) m (coe : Rˣ → R) :=
cont_mdiff_open_embedding 𝓘(𝕜, R) units.open_embedding_coe

variables
  {E' : Type*} [normed_add_comm_group E'] [normed_space 𝕜 E']
  {H' : Type*} [topological_space H'] {I' : model_with_corners 𝕜 E' H'}
  {M' : Type*} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M']

lemma cont_mdiff.of_comp_units_coe {m : with_top ℕ}
  {φ : M' → Rˣ} (hφ : cont_mdiff I' 𝓘(𝕜, R) m (coe ∘ φ : M' → R)) :
  cont_mdiff I' 𝓘(𝕜, R) m φ :=
cont_mdiff.of_comp_open_embedding 𝓘(𝕜, R) units.open_embedding_coe hφ

[Winston Yin]

That’s good to know! Have a great holiday :)

[Winston Yin]

@Heather Macbeth Your suggested lemma statements required no modification. I was able to prove them and use them to show units.smooth_mul and units.smooth_inv. These are pushed to the PR. I'll also do a little more cleanup.

[Winston Yin]

My initial approach was conceptually complicated because when showing g : M → M' is cont_mdiff, in the step coe ∘ g = f ∘ coe', I was trying very hard to specify the factors on the RHS exactly, so that coe' must coincide with the manifold structure on M'. This requirement caused problems with product manifolds. I now see that one may freely choose the factorisation f ∘ coe' depending on what theorem already exists for f being cont_mdiff. So, thanks for clarifying this for me!