Define Submodule.IsTopologicalCompl

[ADedecker]

Right now, Mathlib defines Submodule.ClosedComplemented: a submodule has a closed complement if it is the range of some (continuous) projection. However, this definition allows for no control on the kernel of such a projection.

This more precise version is: S and T are topological complements if there exists a (necessarily unique) f : E →L[𝕜] E which is the identity on S and vanishes on E. I am open to slight modifications of the definitions, e.g taking f : E →L[𝕜] S instead, or replacing the "there exists" by "this specific linear map is continuous". I am also open to other names, but I don't like IsClosedCompl.

Here is a rough sketch of the API I would expect :

• symmetry in S and T (easy)
• Submodule.prodEquivOfClosedCompl should be generalized to this setup (this is also an alternative definitions).
• Same for Submodule.linearProjOfClosedCompl
• ContinuousLinearMap.ker_closedComplemented_of_finiteDimensional_range and its brother Submodule.ClosedComplemented.of_quotient_finiteDimensional should be extended to arbitrary TVSs, and strengthened to say that any algebraic complement of a closed finite-codimension space is a topological complement
• the file Mathlib.Analysis.Normed.Module.Complemented should be refactored so that the main theorem is that, for closed subspaces of a Banach space, IsCompl implies IsTopologicalCompl

This is probably way too much for a single PR, but the first three points above would be good enough to get things started!

[ADedecker]

Actually I think I'm going to work on this myself, because I'm going to need this API quite soon 😅

[sharky564]

Hey, would you be interested in some help here? I am interested in helping out with this and the downstream issues to build up Fredholm operators.

Also I think potentially the formulation should be IsTopologicalCompl S T definitionally is IsCompl S T ^ (continuity condition). The definition to use probably should be "the linear map S × T → E given by addition is a homeomorphism, from which the continuous projection is a theorem, and the other two projected versions should follow from something like isTopologicalCompl_iff_exists_proj. We also get the symmetry lemma easily from Homeomorph.prodComm I think.

Happy to defer to your preference though.

[ADedecker]

Thanks for offering help! As I said I decided to start working on this myself, you can see the first PR at #38547. I ended up going for "the subspaces are complements and one of the projections is continuous" because I suspect it would be the most convenient condition to prove in practice (and symmetry is still quite trivial). One slight disadvantage is that the definition is no longer an "and", because you need to know that the two subspaces are complements to talk about the projection.

Your proposal is nice in that it doesn't require this (and in fact I believe you don't even need to include IsCompl, it will follow from bijectivity of the addition map), but I worry that proving isHomeomorph would be a pain in practice (especially since we really only need the backwards continuity). I'm open to change though!

Also, I wrote down the definition, but my PR does not contain all the API we want, so there will definitely be some work left to do.

[sharky564]

Your formulation worked well as the starting point - here's where I got with the first TODO (the prodEquiv bundling). Code below - happy to open this as a follow-up PR after yours lands, or you can pull it in here, whichever you prefer.

Two design questions I'd want your input on first:

1. I needed Equiv.isHomeomorph_iff and LinearEquiv.isHomeomorph_iff, neither of which seems to exist. Worth a separate prerequisite PR to Topology.Homeomorph.Lemmas and Topology.Algebra.Module.Equiv?
2. I added Submodule.continuous_prodEquivOfIsCompl as a standalone lemma since it gets used in a few places - does that fit the API you have in mind?

I also started on quotientEquiv but my proof is fighting the abstraction - I think the clean version goes through mkQ being a quotient map (Continuous (quotientEquiv) ↔ Continuous (quotientEquiv ∘ mkQ), then identifying the composite with q.linearProjOfIsCompl p h.symm). Couldn't find the right name for the quotient-map fact about mkQ. Happy to share what I have if useful, or defer it to you.

section ContinuousLinearEquiv

variable [IsTopologicalAddGroup M]

-- TODO: move to [Mathlib.Topology.Homeomorph.Lemmas] maybe
/-- A bijection between topological spaces is a homeomorphism if and only if it is continuous in
both directions. -/
theorem _root_.Equiv.isHomeomorph_iff {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
    (e : X ≃ Y) : IsHomeomorph e ↔ Continuous e ∧ Continuous e.symm := by
  rw [e.continuous_symm_iff]
  exact ⟨fun h ↦ ⟨h.continuous, h.isOpenMap⟩,
         fun ⟨hc, ho⟩ ↦ ⟨hc, ho, e.bijective⟩⟩

-- TODO: move to [Mathlib.Topology.Algebra.Module.Equiv] maybe
/-- A linear equivalence between topological modules is a homeomorphism if and only if it is
continuous in both directions. -/
theorem _root_.LinearEquiv.isHomeomorph_iff {R M N : Type*} [Semiring R]
    [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N]
    [TopologicalSpace M] [TopologicalSpace N] (e : M ≃ₗ[R] N) :
    IsHomeomorph e ↔ Continuous e ∧ Continuous e.symm :=
  e.toEquiv.isHomeomorph_iff

/-- Two submodules `p` and `q` are topological complements if and only if the algebraic equivalence
`p.prodEquivOfIsCompl q h` is continuous in the inverse direction. -/
theorem _root_.IsCompl.isTopCompl_iff_continuous_prodEquiv_symm (h : IsCompl p q) :
    IsTopCompl p q ↔ Continuous (p.prodEquivOfIsCompl q h).symm :=
  ⟨fun hTop ↦ (hTop.projectionOnto.prod hTop.symm.projectionOnto).continuous.congr fun x ↦
    (Submodule.prodEquivOfIsCompl_symm_apply h x).symm,
   fun hCont ↦ ⟨h, continuous_subtype_val.comp <| continuous_fst.comp hCont⟩⟩

/-- The algebraic equivalence `p.prodEquivOfIsCompl q h : p × q ≃ₗ[R] M` from a pair of
complementary submodules is always continuous as a map `p × q → M`. -/
theorem continuous_prodEquivOfIsCompl (h : IsCompl p q) :
    Continuous (p.prodEquivOfIsCompl q h) :=
  (continuous_subtype_val.comp continuous_fst).add
    (continuous_subtype_val.comp continuous_snd)

/-- Two submodules `p` and `q` are topological complements if and only if the algebraic equivalence
`p.prodEquivOfIsCompl q h` is a homeomorphism. -/
theorem _root_.IsCompl.isTopCompl_iff_isHomeomorph_prodEquiv (h : IsCompl p q) :
    IsTopCompl p q ↔ IsHomeomorph (p.prodEquivOfIsCompl q h) := by
  rw [(p.prodEquivOfIsCompl q h).isHomeomorph_iff, h.isTopCompl_iff_continuous_prodEquiv_symm,
      and_iff_right]
  exact continuous_prodEquivOfIsCompl h

/-- If two submodules `p` and `q` are topological complements, then the algebraic equivalence
`p.prodEquivOfIsCompl q h.isCompl` is a homeomorphism, bundled as a continuous linear equivalence.
-/
noncomputable def IsTopCompl.prodEquiv (h : IsTopCompl p q) : (p × q) ≃L[R] M :=
  { p.prodEquivOfIsCompl q h.isCompl with
    continuous_toFun := continuous_prodEquivOfIsCompl h.isCompl
    continuous_invFun := h.isCompl.isTopCompl_iff_continuous_prodEquiv_symm.mp h }

@[simp]
theorem IsTopCompl.coe_prodEquiv (h : IsTopCompl p q) :
    (h.prodEquiv : (p × q) →ₗ[R] M) = p.prodEquivOfIsCompl q h.isCompl :=
  rfl

@[simp]
theorem IsTopCompl.coe_prodEquiv_symm (h : IsTopCompl p q) :
    (h.prodEquiv.symm : M →ₗ[R] p × q) = (p.prodEquivOfIsCompl q h.isCompl).symm :=
  rfl

@[simp]
theorem IsTopCompl.prodEquiv_apply (h : IsTopCompl p q) (x : p × q) :
    h.prodEquiv x = (x.1 : M) + x.2 := rfl

@[simp]
theorem IsTopCompl.prodEquiv_symm_apply (h : IsTopCompl p q) (x : M) :
    h.prodEquiv.symm x = ((h.projectionOnto x, h.symm.projectionOnto x) : p × q) :=
  Submodule.prodEquivOfIsCompl_symm_apply h.isCompl x

end ContinuousLinearEquiv

No rush on any of this - happy to wait for your PR to land before doing anything.

[ADedecker]

I am running a bit out of time right now. I think my PR is large enough already, this should probably come after. Feel free to open a PR depending on mine if you want some more precise feedback.

The product part looks quite nice, I don't have much comments to make. IsHomeomorph is a quite recent addition to Mathlib, so it's not surprising to find some gaps in the API; I think you can PR them separately in the mean time.

Regarding the quotient part, I think the lemma you're searching for is QuotientGroup.isQuotientMap_mk. I realized recently that we don't seem to have Submodule.mkQ bundled as a continuous linear map at all (please double check though, because that is quite surprising). This would also make a good standalone PR.

[sharky564]

Alright I should be good to put out the PR merging in the first few points, once PR #38814 is in. Also, I've started thinking about the refactor - it should be relatively painless I think? Will let you know if I have any struggles.

[ADedecker]

You mean the refactor of Mathlib.Analysis.Normed.Module.Complemented? Yes that should be relatively straightfoward. Note that I've done a (very small) chunk of it in #38579