English
If A and B are R-modules are homeomorphic via an R-linear homeomorphism, and A has the module topology, then B does as well.
Русский
Если A и B — R-модули, между ними существует R-линейная гомеоморфизм-изоморф, и A имеет модульную топологию, тогда B тоже имеет её.
LaTeX
$$$\text{iso}(e) : \ IsModuleTopology R B$$$
Lean4
/-- If `A` and `B` are `R`-modules, homeomorphic via an `R`-linear homeomorphism, and if
`A` has the module topology, then so does `B`. -/
theorem iso (e : A ≃L[R] B) : IsModuleTopology R B where
eq_moduleTopology' := by
-- get these in before I start putting new topologies on A and B and have to use `@`
let g : A →ₗ[R] B := e
let g' : B →ₗ[R] A := e.symm
let h : A →+ B := e
let h' : B →+ A := e.symm
simp_rw [e.toHomeomorph.symm.isInducing.1, eq_moduleTopology R A, moduleTopology, induced_sInf]
apply congr_arg
ext τ
rw [Set.mem_image]
constructor
· rintro ⟨σ, ⟨hσ1, hσ2⟩, rfl⟩
exact ⟨continuousSMul_induced g'.toMulActionHom, continuousAdd_induced h'⟩
· rintro ⟨h1, h2⟩
use τ.induced e
rw [induced_compose]
refine ⟨⟨continuousSMul_induced g.toMulActionHom, continuousAdd_induced h⟩, ?_⟩
nth_rw 2 [← induced_id (t := τ)]
simp
