feat (Fujisakis): Module topology on a product is the product of the module topologies

[WilliamCoram]

For an R module M and an S module N, we show the R x S module topology on M x N is equal to the product of the module topologies.

[kbuzzard]

I'll look at this more carefully later, but here are some initial comments.

[WilliamCoram]

awaiting-review

[kbuzzard]

These variables should move after the local instance, and should only be introduced as you need them, and should be introduced in the right generality. For example I should think that the instance will work fine for semirings.

[kbuzzard]

This namespace does not conform at all to the naming conventions. Is is not in the naming conventions at all as far as I know, and Top means something else. How about ModuleProd?

[kbuzzard]

You are misusing variables. They should never have been added at this point; you have too many and you don't need them.

[kbuzzard]

This has nothing to do with ring theory, should be in another file, should be tagged @[fun_prop], and you might want to PR it directly to mathlib. Note that in your code it's in the wrong namespace (this has nothing to do with modules).

@[fun_prop]
lemma Equiv.continuous_prodProdProdComm : Continuous (Equiv.prodProdProdComm R S M N) :=
  show Continuous fun abcd : (R × S) × M × N ↦ ((abcd.1.1, abcd.2.1), abcd.1.2, abcd.2.2) by
  fun_prop

[WilliamCoram]

awaiting-review

[kbuzzard]

Can you add a copyright header? I want to start moving towards this as a convention.

[kbuzzard]

The thread is here #mathlib4 > product of modules over product of rings @ 💬 and in the comment (which could be a module docstring) you could link to it and also give the following example:

example [CommRing R] : (inferInstance : Module (R × R) ((R × R) × (R × R))) =
    instModuleProd := by
  ext ⟨a, b⟩ ⟨⟨c, d⟩, e, f⟩
  · rfl
  · simp [SMul.smul, instModuleProd]
    -- ⊢ b * d = a * d
    sorry
  · simp [SMul.smul, instModuleProd]
    -- ⊢ a * e = b * e
    sorry
  · rfl

This is why the instance won't be allowed in mathlib. It's fine to make it a definition; but after reading the discussion about instance names I now understand that you shouldn't call it inst-anything because it's not an instance. And moreover you shouldn't make it a local instance in this fie because there's no point -- the file compiles fine without it. This is the sort of thing which you can just temporarily switch on in other files as needed.

[kbuzzard]

Suggested change

	local instance instModuleProd [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid N]
	def Prod.moduleProd [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid N]

How about that for a name?

[kbuzzard]

Suggested change

	mul_smul rs rs' mn := by
	cases rs; cases rs'; cases mn
	mul_smul := by
	rintro ⟨r, s⟩ ⟨r', s'⟩ ⟨m, n⟩

is slightly shorter but I'm not suggesting this because I think you should change it, I'm just showing you the trick; what you have is fine.

[kbuzzard]

Of course we have this already: it's AddMonoidHom.inl (a group homomorphism, but it will have a coercion to function), so I would definitely not define this. Each definition comes with a cost, which is that you have to make API for the definition, and the API is already made for AddMonoidHom.inl.

[kbuzzard]

After this heroic effort you can deduce this much cleaner statement:

lemma induced_continuous_add'' [TopologicalSpace M] [TopologicalSpace (M × N)]
    [IsModuleTopology (R × S) (M × N)] (hM : Topology.IsInducing (AddMonoidHom.inl M N)) :
    ContinuousAdd M := by
  obtain ⟨rfl⟩ := hM
  have := eq_moduleTopology (R × S) (M × N)
  convert induced_continuous_add

Your proof is pretty horrible because it's full of @s. What I want to know is: is my variant above actually enough for your purposes? Because if so I would recommend proving my version instead of your version, just because it's cleaner to state so will be cleaner to use.

If I understood better what you were doing (e.g. if you'd sketched a human-readable proof in comments in the longer proof above) then I might have a stab at proving this directly, but what I'm unclear about is whether it's enough for you because at this point I'm not entirely sure why you need these results (in the sense that I'm sure you've told me, but I've now forgotten because I've been working on CFT and top-down FLT for months and ignoring bottom-up FLT, and am only now getting back into it).

[kbuzzard]

With long proofs like this I would kind of prefer comments just briefly explaining the mathematical ideas, like I do in the module topology files in mathlib. It would make it much easier to golf the proofs if I knew what was going on.

[kbuzzard]

You should only switch this on when you need it. In fact you can even just switch it on in the definitions and theorems which need it by putting

attribute [local instance] ModuleProd.instModuleProd in

just before them.

[kbuzzard]

Woah woah woah, you've already proved this once for inl, you don't want to prove it again for inr, you want to deduce the result by symmetry. You can't just duplicate the code like that.

After having written that comment, I decided to do this myself. Because I am not entirely clear about whether we actually want your ugly statements with @s in or whether we can get away with my nicer statements like my induced_continuous_add'' above, I decided that I would just try and prove the .inr version of my clean version. My version (deduced from induced_continuous_add'') is this:

attribute [local instance] ModuleProd.instModuleProd in
lemma induced_continuous_add''' [TopologicalSpace N] [TopologicalSpace (M × N)]
    [IsModuleTopology (R × S) (M × N)] (hN : Topology.IsInducing (AddMonoidHom.inr M N)) :
    ContinuousAdd N := by
  let : TopologicalSpace (N × M) := .induced (Equiv.prodComm N M) inferInstance
  let e : (M × N) ≃SL[(RingEquiv.prodComm.toRingHom : R × S →+* S × R)] (N × M) := {
    __ := LinearEquiv.prodSwap R S M N
    continuous_toFun := by
      convert continuous_coinduced_rng
      exact congr($(Equiv.induced_symm (Equiv.prodComm M N)) _)
    continuous_invFun := continuous_induced_dom
  }
  have hN' : Topology.IsInducing (AddMonoidHom.inl N M) := by
    rw [← Topology.isInducing_iff_comp_continuousEquiv (AddMonoidHom.inl N M) e.symm.toHomeomorph]
    convert hN
  convert induced_continuous_add'' (R := S) (S := R) (M := N) (N := M) hN'
  apply ContinuousLinearEquiv.isModuleTopology _ _ continuous_swap continuous_swap e.symm

However, that version won't compile for you, because you are missing LinearEquiv.prodSwap
and Topology.isInducing_iff_comp_continuousEquiv and ContinuousLinearEquiv.isModuleTopology, all of which I had to write myself. And in writing them I found other missing things in mathlib. The below code has taken me many hours, but I firmly believe that this is the correct way to proceed rather tham the code duplication. The code can be inserted into the file just after your continuous_incl1, which I've restated to be about AddMonoidHom.inl _ _.

-- your code, around line 596
lemma continuous_incl1 : @Continuous M (M × N) (moduleTopology R M) (moduleTopology (R × S) (M × N))
    (AddMonoidHom.inl _ _) := by
  refine continuous_iff_le_induced.mpr ?_
  refine sInf_le ?_
  constructor
  · exact induced_continuous_smul
  · exact induced_continuous_add

-- new bit starts here. Start by exiting the namespace because this stuff should be elsewhere
end ModuleProd

end IsModuleTopology

-- I am amazed that this isn't in mathlib
lemma TopologicalSpace.induced_comp {X Y Z : Type*}
    (f : X → Y) (g : Y → Z) (τ : TopologicalSpace Z) :
    induced (g ∘ f) τ = induced f (induced g τ) := by
  ext U
  refine ⟨fun ⟨W, hW, hWU⟩ ↦ ⟨g⁻¹' W, isOpen_induced hW, hWU⟩,
      fun ⟨V, ⟨W, hW, hWV⟩, hVU⟩ ↦ ?_⟩
  subst hWV hVU
  exact ⟨W, hW, rfl⟩

lemma Topology.isInducing_iff_comp_continuousEquiv
    {X Y Z : Type*} [TopologicalSpace X] [TopologicalSpace Y]
    [TopologicalSpace Z] (f : X → Y) (e : Y ≃ₜ Z) :
    Topology.IsInducing (e ∘ f) ↔ Topology.IsInducing f := by
  simp only [Topology.isInducing_iff]
  apply Eq.congr_right
  rw [TopologicalSpace.induced_comp]
  congr
  exact (Homeomorph.induced_eq e)

lemma TopologicalSpace.induced_eq_iff_coinduced_eq {X Y : Type*}
    (x : TopologicalSpace X) (y : TopologicalSpace Y)
    {F : Type*} (e : F) [EquivLike F X Y] :
    TopologicalSpace.induced e y = x ↔ TopologicalSpace.coinduced e x = y := by
  refine ⟨?_, ?_⟩
  · rintro rfl
    convert show coinduced e (coinduced (Equiv.symm e) y) = y by
      simp [coinduced_compose, coinduced_id]
    exact (Equiv.coinduced_symm (e : X ≃ Y)).symm -- can't rewrite this earlier because ⇑↑e ≠ ⇑e
  · rintro rfl
    convert show coinduced (Equiv.symm e) (coinduced e x) = x by
      simp [coinduced_compose, coinduced_id]
    exact (Equiv.coinduced_symm (e : X ≃ Y)).symm

-- I am surprised that this isn't in mathlib but maybe there's a reason that
-- it's not
@[simp]
lemma LinearEquiv.self_comp_symm {A B M N : Type*}
    [Semiring A] [TopologicalSpace A]
    [Semiring B] [TopologicalSpace B]
    [AddCommMonoid M] [Module A M]
    [AddCommMonoid N] [Module B N] [TopologicalSpace N] [IsModuleTopology B N]
    (σ : A →+* B) (σ' : B →+* A) [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] (e : M ≃ₛₗ[σ] N) :
    ⇑e ∘ ⇑e.symm = id := by
  ext
  simp

-- variant of continuousAdd_induced for `AddEquivClass` where we can go both ways
lemma continuousAdd_induced_iff {M N : Type*} [AddCommMonoid M] [AddCommMonoid N]
    {F : Type*} [EquivLike F M N] [AddEquivClass F M N] (e : F)
    (t : TopologicalSpace N) :
    @ContinuousAdd M (.induced e t) _ ↔ ContinuousAdd N := by
  refine ⟨fun h ↦ ?_, fun h ↦ continuousAdd_induced e⟩
  let : TopologicalSpace M := .induced e t
  convert continuousAdd_induced (N := M) (e : M ≃+ N).symm
  subst this
  simp only [← TopologicalSpace.induced_comp] -- simp won't simplify `⇑e ∘ ⇑(↑e).symm`
  convert induced_id.symm
  ext
  simp

-- better than `continuousSMul_induced` because it lets me change rings
lemma continuousSMul_induced' {A B M N : Type*}
    [Semiring A] [TopologicalSpace A]
    [Semiring B] [TopologicalSpace B]
    [AddCommMonoid M] [Module A M]
    [AddCommMonoid N] [Module B N] [τN : TopologicalSpace N]
    {σ : A →+* B} (hσ : Continuous σ)
    (e : M →ₛₗ[σ] N) [ContinuousSMul B N] :
    @ContinuousSMul A M _ _ (τN.induced e) :=
  let _ : TopologicalSpace M := τN.induced e
  Topology.IsInducing.continuousSMul (N := A) (Y := M) (f := σ) (X := N) (g := e) ⟨rfl⟩ hσ
    (LinearMap.map_smulₛₗ e _ _)

-- version of `continuousSMul_induced` for `LinearEquiv`s where we can go both ways
lemma continuousSMul_induced_iff {A B M N : Type*}
    [Semiring A] [TopologicalSpace A]
    [Semiring B] [TopologicalSpace B]
    [AddCommMonoid M] [Module A M]
    [AddCommMonoid N] [Module B N] [τN : TopologicalSpace N] --[IsModuleTopology B N]
    {σ : A →+* B} {σ' : B →+* A} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ]
    (hσ : Continuous σ) (hσ' : Continuous σ')
    (e : M ≃ₛₗ[σ] N) :
    @ContinuousSMul A M _ _ (τN.induced e) ↔ ContinuousSMul B N := by
  refine ⟨fun h ↦ ?_, fun h ↦ continuousSMul_induced' hσ e.toLinearMap⟩
  let : TopologicalSpace M := τN.induced e
  convert continuousSMul_induced' hσ' e.symm.toLinearMap
  subst this
  simp only [LinearEquiv.coe_coe, ← TopologicalSpace.induced_comp]
  convert induced_id.symm -- missing simp lemma
  ext
  simp

-- `isModuleTopology` can be pulled back along a `ContinuousLinearEquiv`
lemma ContinuousLinearEquiv.isModuleTopology {A B M N : Type*}
    [Semiring A] [TopologicalSpace A]
    [Semiring B] [TopologicalSpace B]
    [AddCommMonoid M] [Module A M] [TopologicalSpace M]
    [AddCommMonoid N] [Module B N] [TopologicalSpace N] [IsModuleTopology B N]
    (σ : A →+* B) (σ' : B →+* A) [RingHomInvPair σ σ'] [RingHomInvPair σ' σ]
    (hσ : Continuous σ) (hσ' : Continuous σ')
    (e : M ≃SL[σ] N) :
    IsModuleTopology A M := by
  constructor
  simp_rw [← Homeomorph.induced_eq e.toHomeomorph, eq_moduleTopology B N, induced_sInf]
  congr
  let g : M ≃ₛₗ[σ] N := e
  let f : M ≃+ N := e
  ext t
  simp only [Set.mem_image, TopologicalSpace.induced_eq_iff_coinduced_eq, exists_eq_right']
  set u : TopologicalSpace N := TopologicalSpace.coinduced e t with hu
  have ht := (TopologicalSpace.induced_eq_iff_coinduced_eq t u e).2 hu.symm
  change u ∈ _ ↔ _
  rw [← ht]
  simp only [Set.mem_setOf_eq]
  apply and_congr
  · exact (continuousSMul_induced_iff hσ hσ' g).symm
  · exact (continuousAdd_induced_iff f u).symm

-- `isModuleTopology` can be pulled back and pushed forward along a `ContinuousLinearEquiv`
lemma ContinuousLinearEquiv.isModuleTopology_iff {A B M N : Type*}
    [Semiring A] [TopologicalSpace A]
    [Semiring B] [TopologicalSpace B]
    [AddCommMonoid M] [Module A M]
    [TopologicalSpace M]
    [AddCommMonoid N] [Module B N]
    [TopologicalSpace N]
    (σ : A →+* B) (σ' : B →+* A) [RingHomInvPair σ σ'] [RingHomInvPair σ' σ]
    (hσ : Continuous σ) (hσ' : Continuous σ')
    (e : M ≃SL[σ] N) :
    IsModuleTopology A M ↔ IsModuleTopology B N := by
  constructor <;> intro _
  · exact ContinuousLinearEquiv.isModuleTopology σ' σ hσ' hσ e.symm
  · exact ContinuousLinearEquiv.isModuleTopology σ σ' hσ hσ' e

-- no idea why this instance isn't there
instance {R S : Type*} [Semiring R] [Semiring S] :
    RingHomInvPair (R₁ := R × S) (R₂ := S × R) RingEquiv.prodComm.toRingHom
      RingEquiv.prodComm.toRingHom where
  comp_eq := by ext ⟨r, s⟩ <;> simp
  comp_eq₂ := by ext ⟨s, r⟩ <;> simp

-- the linear equivalence between `M × N` and `N × M` for your module structure,
-- lying over the ring isomorphism `RingEquiv.prodComm : R × S ≃+* S × R`
attribute [local instance] ModuleProd.instModuleProd in
def LinearEquiv.prodSwap (R S M N : Type*) [Semiring R] [Semiring S]
    [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module S N] :
    (M × N) ≃ₛₗ[(RingEquiv.prodComm.toRingHom : R × S →+* S × R)] (N × M) where
  __ := AddEquiv.prodComm (M := M) (N := N)
  map_smul' := by
    rintro ⟨r, s⟩ ⟨m, n⟩
    rfl

-- now we're back to the file itself; all the above should go in other files
-- and also in mathlib
namespace IsModuleTopology

section ModuleProd -- back in your section

-- your variables again
variable {R S M N : Type*} [Semiring R] [Semiring S] [TopologicalSpace R] [TopologicalSpace S]
    [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module S N]

-- my proof of the clean version of `induced_continuous_add` for `.inr`,
-- deduced from the clean `.inl` version using symmetry
attribute [local instance] ModuleProd.instModuleProd in
lemma induced_continuous_add''' [TopologicalSpace N] [TopologicalSpace (M × N)]
    [IsModuleTopology (R × S) (M × N)] (hN : Topology.IsInducing (AddMonoidHom.inr M N)) :
    ContinuousAdd N := by
  let : TopologicalSpace (N × M) := .induced (Equiv.prodComm N M) inferInstance
  let e : (M × N) ≃SL[(RingEquiv.prodComm.toRingHom : R × S →+* S × R)] (N × M) := {
    __ := LinearEquiv.prodSwap R S M N
    continuous_toFun := by
      convert continuous_coinduced_rng
      exact congr($(Equiv.induced_symm (Equiv.prodComm M N)) _)
    continuous_invFun := continuous_induced_dom
  }
  have hN' : Topology.IsInducing (AddMonoidHom.inl N M) := by
    rw [← Topology.isInducing_iff_comp_continuousEquiv (AddMonoidHom.inl N M) e.symm.toHomeomorph]
    convert hN
  convert induced_continuous_add'' (R := S) (S := R) hN'
  apply ContinuousLinearEquiv.isModuleTopology _ _ continuous_swap continuous_swap e.symm

-- etc etc

My main question to you is whether you can get away with the clean versions of the results (the double and triple primed versions) or whether you need to prove these messier versions (the noprime and single-primed versions in your file). In general I think IsModuleTopology is a more flexible assumption than just putting moduleTopology on everything; the Is version is a predicate so it's more flexible; basically [TopologicalSpace M] [IsModuleTopology R M] just lives entirely in the typeclass system so you don't have to fight it.

Actually, given that I have spent many hours today thinking about your stuff I may as well offer you my proof of the single-primed version:

attribute [local instance] ModuleProd.instModuleProd in
lemma induced_continuous_add' : @ContinuousAdd N
    (TopologicalSpace.induced (AddMonoidHom.inr _ _) (moduleTopology (R × S) (M × N))) _ := by
  let : TopologicalSpace N :=
    (TopologicalSpace.induced (AddMonoidHom.inr _ _) (moduleTopology (R × S) (M × N)))
  let : TopologicalSpace (M × N) := moduleTopology (R × S) (M × N)
  convert induced_continuous_add (R := S) (S := R) (M := N) (N := M)
  convert TopologicalSpace.induced_comp (AddMonoidHom.inl N M) Prod.swap
    (moduleTopology (R × S) (M × N))
  let : TopologicalSpace (N × M) :=
    TopologicalSpace.induced Prod.swap (moduleTopology (R × S) (M × N))
  have : IsModuleTopology (R × S) (M × N) := ⟨rfl⟩
  let e : (M × N) ≃SL[(RingEquiv.prodComm.toRingHom : R × S →+* S × R)] (N × M) := {
    __ := LinearEquiv.prodSwap R S M N
    continuous_toFun := by
      convert continuous_coinduced_rng
      exact congr($(Equiv.induced_symm (Equiv.prodComm M N)) _)
    continuous_invFun := continuous_induced_dom
  }
  obtain ⟨h⟩ := ContinuousLinearEquiv.isModuleTopology _ _
    continuous_swap continuous_swap e.symm
  exact h.symm

[kbuzzard]

Is this the point of these hundreds of lines? Is this the only thing you need or do you also need all these intermediate results? Can you sketch a maths proof?

[WilliamCoram]

This is the only thing I need (or needed, since I could just use the existing results with commring as opposed to ring). The whole file follows a proof you gave me August 1st over Zulip and I pretty much verbatim follow your proof outline. I believe I linked it in my previous message to you.

I agree all the @'s are horrible... but this was the only way I knew how to force the correct topologies (of which there are many) I wanted on every step. Because of this I was also unsure how to infer inr from inl, as although the method is 90% the same; the calling of each topology would be different and certain maps would swap order.

[kbuzzard]

I think you should detail the natural language proof in the Lean proof, there is no point keeping it secret. Can you try and figure out whether you can use my double and triple primed version of the results instead of your versions? Can you move some of the code I suggest above into separate files in FLT/Mathlib?