Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 9 commits into
base: main
Choose a base branch
from
Open

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
2ac10b1
First commit
WilliamCoram Oct 3, 2025
11d4685
lake exe mk_all
WilliamCoram Oct 3, 2025
0e941d4
docustrings
WilliamCoram Oct 3, 2025
0a10753
post quick review changes
WilliamCoram Oct 7, 2025
22a9248
new docustring needed?
WilliamCoram Oct 7, 2025
69408dc
new files
WilliamCoram Nov 4, 2025
a01c2f3
fun_prop
WilliamCoram Nov 4, 2025
7d20737
docustring
WilliamCoram Nov 4, 2025
7eec90c
docustring
WilliamCoram Nov 4, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions FLT.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,6 +54,7 @@ import FLT.Mathlib.Algebra.Algebra.Tower
import FLT.Mathlib.Algebra.FixedPoints.Basic
import FLT.Mathlib.Algebra.IsQuaternionAlgebra
import FLT.Mathlib.Algebra.Module.LinearMap.Defs
import FLT.Mathlib.Algebra.Module.Prod
import FLT.Mathlib.Algebra.Module.Submodule.Basic
import FLT.Mathlib.Algebra.Order.AbsoluteValue.Basic
import FLT.Mathlib.Analysis.Normed.Ring.WithAbs
Expand Down Expand Up @@ -108,6 +109,7 @@ import FLT.Mathlib.Topology.Algebra.Valued.ValuationTopology
import FLT.Mathlib.Topology.Algebra.Valued.WithVal
import FLT.Mathlib.Topology.Algebra.Valued.WithZeroMulInt
import FLT.Mathlib.Topology.Constructions
import FLT.Mathlib.Topology.Constructions.SumProd
import FLT.Mathlib.Topology.HomToDiscrete
import FLT.Mathlib.Topology.Homeomorph
import FLT.Mathlib.Topology.Instances.Matrix
Expand Down
38 changes: 38 additions & 0 deletions FLT/Mathlib/Algebra/Module/Prod.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,38 @@
import Mathlib.Algebra.Module.Defs
Copy link
Collaborator

@kbuzzard kbuzzard Nov 8, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

import Mathlib.Algebra.Ring.Prod
import Mathlib.Algebra.Module.Prod

/-
I am not fully convinced what the naming should be for this instance, or if this is where it belongs
as it conflicts with Prod.instModule ... also will there be a diamond when S = R?
Copy link
Collaborator

@kbuzzard kbuzzard Nov 8, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

-/
namespace ModuleProd

variable {R S M N : Type*}

/-- The (R × S)-module structure on (M × N). -/
local instance instModuleProd [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid N]
Copy link
Collaborator

@kbuzzard kbuzzard Nov 8, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

[Module R M] [Module S N] : Module (R × S) (M × N) where
smul rs mn := (rs.1 • mn.1, rs.2 • mn.2)
one_smul mn := by cases mn; ext; exacts [one_smul R _, one_smul S _]
mul_smul rs rs' mn := by
cases rs; cases rs'; cases mn
Comment on lines +18 to +19
Copy link
Collaborator

@kbuzzard kbuzzard Nov 8, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

ext <;>
exact mul_smul _ _ _
smul_zero rs := by cases rs; ext <;> exact smul_zero _
smul_add rs mn mn' := by
cases rs; cases mn; cases mn'
ext <;>
exact smul_add _ _ _
add_smul rs rs' mn := by
cases rs; cases rs'; cases mn
ext <;>
exact add_smul _ _ _
zero_smul mn := by cases mn; ext <;> exact zero_smul _ _

/-- Product map of the scalar multiplications defined on the product `R × M` and `S × N`. -/
def smul [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid N]
[Module R M] [Module S N] : (R × M) × (S × N) → (M × N) :=
Prod.map (fun (r, m) => r • m) (fun (s, n) => s • n)

end ModuleProd
284 changes: 284 additions & 0 deletions FLT/Mathlib/Topology/Algebra/Module/ModuleTopology.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,8 @@ import Mathlib.Topology.Algebra.Module.ModuleTopology
import Mathlib.Topology.Algebra.Algebra.Equiv
import FLT.Mathlib.Algebra.Algebra.Tower
import FLT.Deformations.ContinuousRepresentation.IsTopologicalModule
import FLT.Mathlib.Algebra.Module.Prod
import FLT.Mathlib.Topology.Constructions.SumProd

theorem ModuleTopology.isModuleTopology (R : Type*) [TopologicalSpace R] (S : Type*) [Add S]
[SMul R S] : @IsModuleTopology R _ S _ _ (moduleTopology R S) where
Expand Down Expand Up @@ -470,6 +472,288 @@ instance instProd' : IsModuleTopology (A × B) (M × N) := inferInstance

end Prod

section ModuleProd

/- This should probably replace the Prod section above ... reduces CommRing → Ring. -/

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

/-- The R × S module structure on M × N. -/
local instance : Module (R × S) (M × N) := ModuleProd.instModuleProd
Copy link
Collaborator

@kbuzzard kbuzzard Nov 8, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.


/-- Inclusion `M → M × N` by `a ↦ (a, 0)`. -/
abbrev incl1 : M → M × N :=
fun a => (a, 0)
Copy link
Collaborator

@kbuzzard kbuzzard Nov 8, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.


/-- Inclusion `N → M × N` by `a ↦ (0, a)`. -/
abbrev incl2 : N → M × N :=
fun b => (0 , b)

lemma induced_continuous_add : @ContinuousAdd M
(TopologicalSpace.induced (incl1) (moduleTopology (R × S) (M × N))) _ := by
suffices h : @Continuous (M × M) (M × N) (@instTopologicalSpaceProd M M
(TopologicalSpace.induced (incl1) (moduleTopology (R × S) (M × N)))
(TopologicalSpace.induced (incl1) (moduleTopology (R × S) (M × N))))
((moduleTopology (R × S) (M × N))) (fun (a : M × M) => (a.1 + a.2, (0 : N))) by
convert (@Topology.IsInducing.continuous_iff (M × M) M (M × N) (fun (a : M × M) ↦ a.1 + a.2)
(incl1) (TopologicalSpace.induced (incl1) (moduleTopology (R × S) (M × N)))
(@instTopologicalSpaceProd M M
(TopologicalSpace.induced (incl1) (moduleTopology (R × S) (M × N)))
(TopologicalSpace.induced (incl1) (moduleTopology (R × S) (M × N))))
(moduleTopology (R × S) (M × N)) _).mpr h
· constructor <;> intro h
· exact ContinuousAdd.continuous_add
· rw [continuous_def] at h
use h
· rw [@Topology.isInducing_iff]
have h : (fun (a : M × M) => (a.1 + a.2, (0 : N))) =
(fun (b : (M × N) × (M × N)) => (b.1.1 + b.2.1, b.1.2 + b.2.2)) ∘
(fun (a : M × M ) => (((a.1, 0) : (M × N)) , (((a.2, 0)) : (M × N)))) := by
ext a
all_goals simp
rw [h]
refine @Continuous.comp (M × M) ((M × N) × M × N) (M × N) (@instTopologicalSpaceProd M M
Copy link
Collaborator

@kbuzzard kbuzzard Nov 8, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

(TopologicalSpace.induced (incl1) (moduleTopology (R × S) (M × N)))
(TopologicalSpace.induced (incl1) (moduleTopology (R × S) (M × N))))
(@instTopologicalSpaceProd (M × N) (M × N) (moduleTopology (R × S) (M × N))
(moduleTopology (R × S) (M × N))) (moduleTopology (R × S) (M × N))
(f := (fun (a : M × M ) => (((a.1, 0) : (M × N)) , (((a.2, 0)) : (M × N)))))
(g := (fun (b : (M × N) × (M × N)) => (b.1.1 + b.2.1, b.1.2 + b.2.2))) ?_ ?_
· convert ContinuousAdd.continuous_add
exact ModuleTopology.continuousAdd (R × S) (M × N)
· refine @Continuous.prodMap (M × N) (M × N) M M (moduleTopology (R × S) (M × N))
(moduleTopology (R × S) (M × N))
(TopologicalSpace.induced (incl1) (moduleTopology (R × S) (M × N)))
(TopologicalSpace.induced (incl1) (moduleTopology (R × S) (M × N)))
(f := incl1) (g := incl1) ?_ ?_
all_goals exact continuous_iff_le_induced.mpr fun U a ↦ a
Copy link
Collaborator

@kbuzzard kbuzzard Nov 8, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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).


lemma induced_continuous_smul : @ContinuousSMul R M _ _
(TopologicalSpace.induced (incl1) (moduleTopology (R × S) (M × N))) := by
suffices h : @Continuous (R × M) (M × N) (@instTopologicalSpaceProd R M _
(TopologicalSpace.induced (incl1) (moduleTopology (R × S) (M × N))))
((moduleTopology (R × S) (M × N))) (fun (a : R × M) => (a.1 • a.2, (0 : N))) by
convert (@Topology.IsInducing.continuous_iff (R × M) M (M × N) (fun (a : R × M) ↦ a.1 • a.2)
(incl1) (TopologicalSpace.induced (incl1) (moduleTopology (R × S) (M × N)))
(@instTopologicalSpaceProd R M _
(TopologicalSpace.induced (incl1) (moduleTopology (R × S) (M × N))))
(moduleTopology (R × S) (M × N)) _).mpr h
· constructor <;> intro h
· exact ContinuousSMul.continuous_smul
· rw [continuous_def] at h
use h
· rw [@Topology.isInducing_iff]
have : (fun (a : R × M) ↦ (a.1 • a.2, 0)) =
(fun (c : (R × S) × (M × N)) => (c.1.1 • c.2.1, c.1.2 • c.2.2)) ∘
(fun (b : R × M × N) => ((b.1, (0 : S)), (b.2.1, b.2.2))) ∘
(fun (a : R × M) => (a.1, a.2, (0 : N))) := by
ext a
· rfl
· simp only [Prod.mk.eta, Function.comp_apply, smul_zero]
rw [this]
refine @Continuous.comp (R × M) ((R × S) × M × N) (M × N) (@instTopologicalSpaceProd R M _
(TopologicalSpace.induced (incl1) (moduleTopology (R × S) (M × N))))
(@instTopologicalSpaceProd (R × S) (M × N) _ (moduleTopology (R × S) (M × N)))
(moduleTopology (R × S) (M × N))
(f := (fun (b : R × M × N) => ((b.1, (0 : S)), (b.2.1, b.2.2))) ∘
(fun (a : R × M) => (a.1, a.2, (0 : N))))
(g := (fun (c : (R × S) × (M × N)) => (c.1.1 • c.2.1, c.1.2 • c.2.2))) ?_ ?_
· exact ContinuousSMul.continuous_smul
· refine @Continuous.comp (R × M) (R × M × N) ((R × S) × M × N) (@instTopologicalSpaceProd R M _
(TopologicalSpace.induced (incl1) (moduleTopology (R × S) (M × N))))
(@instTopologicalSpaceProd R (M × N) _ (moduleTopology (R × S) (M × N)))
(@instTopologicalSpaceProd (R × S) (M × N) _ (moduleTopology (R × S) (M × N)))
(f := (fun (a : R × M) => (a.1, a.2, (0 : N))))
(g := (fun (b : R × M × N) => ((b.1, (0 : S)), (b.2.1, b.2.2)))) ?_ ?_
· simp only [Prod.mk.eta, continuous_prodMk]
· constructor
· constructor
· exact @continuous_fst R (M × N) _ (moduleTopology (R × S) (M × N))
· rw [continuous_def] --is there a better way?
intro s hs
have : ((fun (x : R × M × N) ↦ 0) ⁻¹' s) = ∅ ∨
((fun (x : R × M × N) ↦ 0) ⁻¹' s = Set.univ) := by
rcases (Classical.em (0 ∈ s)) with h | h
all_goals aesop
aesop
· exact @continuous_snd R (M × N) _ (moduleTopology (R × S) (M × N))
· simp only [continuous_prodMk]
constructor
· exact @continuous_fst R M _
(TopologicalSpace.induced (incl1) (moduleTopology (R × S) (M × N)))
· refine @Continuous.comp (R × M) M (M × N) (@instTopologicalSpaceProd R M _
(TopologicalSpace.induced (incl1) (moduleTopology (R × S) (M × N))))
(TopologicalSpace.induced (incl1) (moduleTopology (R × S) (M × N)))
(moduleTopology (R × S) (M × N))
(f := fun (a : R × M) => a.2) (g := incl1) ?_ ?_
· exact continuous_iff_le_induced.mpr fun U a ↦ a
· exact @continuous_snd R M _
(TopologicalSpace.induced (incl1) (moduleTopology (R × S) (M × N)))

lemma continuous_incl1 : @Continuous M (M × N) (moduleTopology R M) (moduleTopology (R × S) (M × N))
(incl1) := by
refine continuous_iff_le_induced.mpr ?_
refine sInf_le ?_
constructor
· exact induced_continuous_smul
· exact induced_continuous_add

lemma induced_continuous_add' : @ContinuousAdd N
(TopologicalSpace.induced (incl2) (moduleTopology (R × S) (M × N))) _ := by
Copy link
Collaborator

@kbuzzard kbuzzard Nov 9, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

suffices h : @Continuous (N × N) (M × N) (@instTopologicalSpaceProd N N
(TopologicalSpace.induced (incl2) (moduleTopology (R × S) (M × N)))
(TopologicalSpace.induced (incl2) (moduleTopology (R × S) (M × N))))
((moduleTopology (R × S) (M × N))) (fun (a : N × N) => ((0 : M), a.1 + a.2)) by
convert (@Topology.IsInducing.continuous_iff (N × N) N (M × N) (fun (a : N × N) ↦ a.1 + a.2)
(incl2) (TopologicalSpace.induced (incl2) (moduleTopology (R × S) (M × N)))
(@instTopologicalSpaceProd N N
(TopologicalSpace.induced (incl2) (moduleTopology (R × S) (M × N)))
(TopologicalSpace.induced (incl2) (moduleTopology (R × S) (M × N))))
(moduleTopology (R × S) (M × N)) _).mpr h
· constructor <;> intro h
· exact ContinuousAdd.continuous_add
· rw [continuous_def] at h
use h
· rw [@Topology.isInducing_iff]
have h : (fun (a : N × N) => ((0 : M), a.1 + a.2)) =
(fun (b : (M × N) × (M × N)) => (b.1.1 + b.2.1, b.1.2 + b.2.2)) ∘
(fun (a : N × N ) => (((0, a.1) : (M × N)) , (((0, a.2)) : (M × N)))) := by
ext a
all_goals simp
rw [h]
refine @Continuous.comp (N × N) ((M × N) × M × N) (M × N) (@instTopologicalSpaceProd N N
(TopologicalSpace.induced (incl2) (moduleTopology (R × S) (M × N)))
(TopologicalSpace.induced (incl2) (moduleTopology (R × S) (M × N))))
(@instTopologicalSpaceProd (M × N) (M × N) (moduleTopology (R × S) (M × N))
(moduleTopology (R × S) (M × N))) (moduleTopology (R × S) (M × N))
(f := (fun (a : N × N ) => (((0, a.1) : (M × N)) , (((0, a.2)) : (M × N)))))
(g := (fun (b : (M × N) × (M × N)) => (b.1.1 + b.2.1, b.1.2 + b.2.2))) ?_ ?_
· convert ContinuousAdd.continuous_add
exact ModuleTopology.continuousAdd (R × S) (M × N)
· refine @Continuous.prodMap (M × N) (M × N) N N (moduleTopology (R × S) (M × N))
(moduleTopology (R × S) (M × N))
(TopologicalSpace.induced (incl2) (moduleTopology (R × S) (M × N)))
(TopologicalSpace.induced (incl2) (moduleTopology (R × S) (M × N)))
(f := incl2) (g := incl2) ?_ ?_
all_goals exact continuous_iff_le_induced.mpr fun U a ↦ a

lemma induced_continuous_smul' : @ContinuousSMul S N _ _
(TopologicalSpace.induced (incl2) (moduleTopology (R × S) (M × N))) := by
suffices h : @Continuous (S × N) (M × N) (@instTopologicalSpaceProd S N _
(TopologicalSpace.induced (incl2) (moduleTopology (R × S) (M × N))))
((moduleTopology (R × S) (M × N))) (fun (a : S × N) => ((0 : M), a.1 • a.2)) by
convert (@Topology.IsInducing.continuous_iff (S × N) N (M × N) (fun (a : S × N) ↦ a.1 • a.2)
(incl2) (TopologicalSpace.induced (incl2) (moduleTopology (R × S) (M × N)))
(@instTopologicalSpaceProd S N _
(TopologicalSpace.induced (incl2) (moduleTopology (R × S) (M × N))))
(moduleTopology (R × S) (M × N)) _).mpr h
· constructor <;> intro h
· exact ContinuousSMul.continuous_smul
· rw [continuous_def] at h
use h
· rw [@Topology.isInducing_iff]
have : (fun (a : S × N) ↦ (0, a.1 • a.2)) =
(fun (c : (R × S) × (M × N)) => (c.1.1 • c.2.1, c.1.2 • c.2.2)) ∘
(fun (b : S × M × N) => (((0 : R), b.1), (b.2.1, b.2.2))) ∘
(fun (a : S × N) => (a.1, (0 : M), a.2)) := by
ext a
· aesop
· simp only [Prod.mk.eta, Function.comp_apply, smul_zero]
rw [this]
refine @Continuous.comp (S × N) ((R × S) × M × N) (M × N) (@instTopologicalSpaceProd S N _
(TopologicalSpace.induced (incl2) (moduleTopology (R × S) (M × N))))
(@instTopologicalSpaceProd (R × S) (M × N) _ (moduleTopology (R × S) (M × N)))
(moduleTopology (R × S) (M × N))
(f := (fun (b : S × M × N) => (((0 : R), b.1), (b.2.1, b.2.2))) ∘
(fun (a : S × N) => (a.1, (0 : M), a.2)))
(g := (fun (c : (R × S) × (M × N)) => (c.1.1 • c.2.1, c.1.2 • c.2.2))) ?_ ?_
· exact ContinuousSMul.continuous_smul
· refine @Continuous.comp (S × N) (S × M × N) ((R × S) × M × N) (@instTopologicalSpaceProd S N _
(TopologicalSpace.induced (incl2) (moduleTopology (R × S) (M × N))))
(@instTopologicalSpaceProd S (M × N) _ (moduleTopology (R × S) (M × N)))
(@instTopologicalSpaceProd (R × S) (M × N) _ (moduleTopology (R × S) (M × N)))
(f := (fun (a : S × N) => (a.1, (0 : M), a.2)))
(g := (fun (b : S × M × N) => (((0 : R), b.1), (b.2.1, b.2.2)))) ?_ ?_
· simp only [Prod.mk.eta, continuous_prodMk]
· constructor
· constructor
· rw [continuous_def]
intro s hs
have : ((fun (x : S × M × N) ↦ 0) ⁻¹' s) = ∅ ∨
((fun (x : S × M × N) ↦ 0) ⁻¹' s = Set.univ) := by
rcases (Classical.em (0 ∈ s)) with h | h
all_goals aesop
aesop
· exact @continuous_fst S (M × N) _ (moduleTopology (R × S) (M × N))
· exact @continuous_snd S (M × N) _ (moduleTopology (R × S) (M × N))
· simp only [continuous_prodMk]
constructor
· exact @continuous_fst S N _
(TopologicalSpace.induced (incl2) (moduleTopology (R × S) (M × N)))
· refine @Continuous.comp (S × N) N (M × N) (@instTopologicalSpaceProd S N _
(TopologicalSpace.induced (incl2) (moduleTopology (R × S) (M × N))))
(TopologicalSpace.induced (incl2) (moduleTopology (R × S) (M × N)))
(moduleTopology (R × S) (M × N))
(f := fun (a : S × N) => a.2) (g := incl2) ?_ ?_
· exact continuous_iff_le_induced.mpr fun U a ↦ a
· exact @continuous_snd S N _
(TopologicalSpace.induced (incl2) (moduleTopology (R × S) (M × N)))

lemma continuous_incl2 : @Continuous N (M × N) (moduleTopology S N) (moduleTopology (R × S) (M × N))
(incl2) := by
refine continuous_iff_le_induced.mpr ?_
refine sInf_le ?_
constructor
· exact induced_continuous_smul'
· exact induced_continuous_add'

lemma id_eq : @id (M × N) = ((incl1) ∘ (Prod.fst)) + ((incl2) ∘ (Prod.snd)) := by
ext a
all_goals simp

variable [TopologicalSpace M] [TopologicalSpace N] [IsModuleTopology R M] [IsModuleTopology S N]

lemma continuous_smul : ContinuousSMul (R × S) (M × N) where
continuous_smul := by
have : (fun p ↦ p.1 • p.2 : (R × S) × M × N → M × N) =
(ModuleProd.smul) ∘ (Equiv.prodProdProdComm R S M N) := by
ext a
all_goals simp only [Function.comp_apply, ModuleProd.smul]
all_goals rfl
rw [this]
refine Continuous.comp ?_ (continuous_prodProdProdComm R S M N)
· apply Continuous.prodMap
all_goals exact ContinuousSMul.continuous_smul

/-- If `M` has the `A`-module topology and `N` has the `B`-module topology
then `M × N` has the `(A × B)`-module topology. -/
instance instProd'' : IsModuleTopology (R × S) (M × N) := by
Copy link
Collaborator

@kbuzzard kbuzzard Nov 9, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Contributor Author

@WilliamCoram WilliamCoram Nov 9, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Collaborator

@kbuzzard kbuzzard Nov 9, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

haveI : ContinuousAdd M := IsModuleTopology.toContinuousAdd R M
haveI : ContinuousAdd N := IsModuleTopology.toContinuousAdd S N
have h2 := continuous_smul (R := R) (S := S) (M := M) (N := N)
refine IsModuleTopology.of_continuous_id ?_
rw [id_eq]
have a : @Continuous (M × N) (M × N) instTopologicalSpaceProd
(moduleTopology (R × S) (M × N)) ((incl1) ∘ (Prod.fst)) := by
refine @Continuous.comp (M × N) M (M × N) instTopologicalSpaceProd (moduleTopology R M)
(moduleTopology (R × S) (M × N)) (Prod.fst) (incl1) ?_ ?_
· exact continuous_incl1
· convert @continuous_fst M N (moduleTopology R M) (moduleTopology S N)
all_goals exact IsModuleTopology.eq_moduleTopology' -- maybe I need to be synthesising better?
have b : @Continuous (M × N) (M × N) instTopologicalSpaceProd
(moduleTopology (R × S) (M × N)) ((incl2) ∘ (Prod.snd)) := by
refine @Continuous.comp (M × N) N (M × N) instTopologicalSpaceProd (moduleTopology S N)
(moduleTopology (R × S) (M × N)) (Prod.snd) (incl2) ?_ ?_
· exact continuous_incl2
· convert @continuous_snd M N (moduleTopology R M) (moduleTopology S N)
all_goals exact IsModuleTopology.eq_moduleTopology'
exact @Continuous.add _ (moduleTopology (R × S) (M × N)) _
(ModuleTopology.continuousAdd (R × S) (M × N)) _ _ _ _ a b


end ModuleProd

section locally_compact

variable (R : Type*) [τR : TopologicalSpace R] [Ring R] [IsTopologicalRing R]
Expand Down
10 changes: 10 additions & 0 deletions FLT/Mathlib/Topology/Constructions/SumProd.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
import Mathlib.Topology.Constructions.SumProd

variable (R S M N : Type*) [TopologicalSpace R] [TopologicalSpace S] [TopologicalSpace M]
[TopologicalSpace N]

@[fun_prop]
lemma continuous_prodProdProdComm : Continuous (Equiv.prodProdProdComm R S M N) := by
unfold Equiv.prodProdProdComm
simp only [Equiv.coe_fn_mk]
fun_prop