Isomorphisms in TopModuleCat with a discrete target

A morphism of topological modules whose target carries the discrete topology is an isomorphism of TopModuleCat R as soon as the underlying morphism of modules is one (TopModuleCat.isIso_of_isIso_forget₂_map), in particular as soon as it is bijective (TopModuleCat.isIso_of_bijective): the inverse is continuous because its source is discrete. This is the counterpart, for the forgetful functor to ModuleCat R and under discreteness of the target, of Mathlib's (forget₂ (TopModuleCat R) TopCat).ReflectsIsomorphisms. It turns Mathlib's invertibility results for the homology of forgotten cochain complexes into isomorphisms of discrete cohomology modules.

@[simp]

theorem TopModuleCat.hom_forget₂_ModuleCat_map {R : Type u_1} [Ring R] [TopologicalSpace R] {X Y : TopModuleCat R} (f : X ⟶ Y) : ModuleCat.Hom.hom ((CategoryTheory.forget₂ (TopModuleCat R) (ModuleCat R)).map f) = ↑(Hom.hom f)

The forgetful functor to ModuleCat R acts on a morphism as its underlying linear map, the counterpart of Mathlib's TopModuleCat.hom_forget₂_TopCat_map for the other forgetful functor.

@[simp]

theorem TopModuleCat.ofIso_hom {R : Type u_1} [Ring R] [TopologicalSpace R] {X Y : TopModuleCat R} (e : ↑X.toModuleCat ≃L[R] ↑Y.toModuleCat) : (ofIso e).hom = ofHom ↑e

The forward morphism of TopModuleCat.ofIso e is e as a continuous linear map.

theorem TopModuleCat.isIso_of_bijective {R : Type u_1} [Ring R] [TopologicalSpace R] {X Y : TopModuleCat R} [DiscreteTopology ↑Y.toModuleCat] (f : X ⟶ Y) (hf : Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom f)) : CategoryTheory.IsIso f

A bijective morphism of topological modules into a discrete module is an isomorphism: the inverse is continuous because its source is discrete.

theorem TopModuleCat.isIso_of_isIso_forget₂_map {R : Type u_1} [Ring R] [TopologicalSpace R] {X Y : TopModuleCat R} [DiscreteTopology ↑Y.toModuleCat] (f : X ⟶ Y) [CategoryTheory.IsIso ((CategoryTheory.forget₂ (TopModuleCat R) (ModuleCat R)).map f)] : CategoryTheory.IsIso f

A morphism of topological modules into a discrete module is an isomorphism as soon as its underlying morphism of modules is one: that morphism is then bijective.