Documentation

Mathlib.Topology.Maps.Strict.Module

Strict linear maps #

In this file, we study continuous linear maps which are strict in the sense of Topology.IsStrictMap. So far, all the results in this file are direct adaptations from the theory of strict homomorphisms of topological additive groups.

source
theorem LinearMap.isStrictMap_iff_isEmbedding_liftQ_ker {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [Ring R] [Ring S] {σ : R →+* S} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module S N] {f : M →ₛₗ[σ] N} [TopologicalSpace M] [TopologicalSpace N] :
Topology.IsStrictMap ⇑f ↔ Topology.IsEmbedding ⇑(f.ker.liftQ f ⋯)

A linear map f : M → N is strict if and only if the induced map M ⧸ f.ker → N is an embedding.

source
theorem LinearMap.isStrictMap_iff_isHomeomorph_quotKerEquivRange {R : Type u_1} {M : Type u_3} {Nₗ : Type u_5} [Ring R] [AddCommGroup M] [AddCommGroup Nₗ] [Module R M] [Module R Nₗ] {fₗ : M →ₗ[R] Nₗ} [TopologicalSpace M] [TopologicalSpace Nₗ] :
Topology.IsStrictMap ⇑fₗ ↔ IsHomeomorph ⇑fₗ.quotKerEquivRange

A linear map f : M → N is strict if and only if the canonical isomorphism M ⧸ f.ker ≃ f.range is a homeomorphism.

source
noncomputable def ContinuousLinearEquiv.quotKerEquivRange {R : Type u_1} {M : Type u_3} {Nₗ : Type u_5} [Ring R] [AddCommGroup M] [AddCommGroup Nₗ] [Module R M] [Module R Nₗ] {fₗ : M →ₗ[R] Nₗ} [TopologicalSpace M] [TopologicalSpace Nₗ] (hf : Topology.IsStrictMap ⇑fₗ) :
(M ⧸ fₗ.ker) ≃L[R] ↥fₗ.range

The isomorphism of topological modules M ⧸ f.ker ≃ f.range given by a strict linear map f : M → N. This is an avatar of the first isomorphism theorem.

Equations
Instances For
    source
    theorem LinearMap.isStrictMap_iff_isOpenQuotientMap_rangeRestrict {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [Ring R] [Ring S] {σ : R →+* S} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module S N] {f : M →ₛₗ[σ] N} [TopologicalSpace M] [TopologicalSpace N] [IsTopologicalAddGroup M] [RingHomSurjective σ] :
    Topology.IsStrictMap ⇑f ↔ IsOpenQuotientMap ⇑f.rangeRestrict

    A linear map is strict if and only if its rangeRestrict is an open quotient map.

    source
    theorem LinearMap.isStrictMap_prodMap_iff {R : Type u_1} {M : Type u_3} {Nₗ : Type u_5} {M' : Type u_6} {Nₗ' : Type u_7} [Ring R] [AddCommGroup M] [AddCommGroup Nₗ] [AddCommGroup M'] [AddCommGroup Nₗ'] [Module R M] [Module R Nₗ] [Module R M'] [Module R Nₗ'] {fₗ : M →ₗ[R] Nₗ} {gₗ : M' →ₗ[R] Nₗ'} [TopologicalSpace M] [TopologicalSpace Nₗ] [IsTopologicalAddGroup M] [TopologicalSpace M'] [IsTopologicalAddGroup M'] [TopologicalSpace Nₗ'] :
    Topology.IsStrictMap ⇑(fₗ.prodMap gₗ) ↔ Topology.IsStrictMap ⇑fₗ ∧ Topology.IsStrictMap ⇑gₗ

    The product (in the sense of LinearMap.prodMap) of linear maps is strict if and only if both maps are strict.

    source
    theorem LinearMap.isStrictMap_prodMap {R : Type u_1} {M : Type u_3} {Nₗ : Type u_5} {M' : Type u_6} {Nₗ' : Type u_7} [Ring R] [AddCommGroup M] [AddCommGroup Nₗ] [AddCommGroup M'] [AddCommGroup Nₗ'] [Module R M] [Module R Nₗ] [Module R M'] [Module R Nₗ'] {fₗ : M →ₗ[R] Nₗ} {gₗ : M' →ₗ[R] Nₗ'} [TopologicalSpace M] [TopologicalSpace Nₗ] [IsTopologicalAddGroup M] [TopologicalSpace M'] [IsTopologicalAddGroup M'] [TopologicalSpace Nₗ'] (hf : Topology.IsStrictMap ⇑fₗ) (hg : Topology.IsStrictMap ⇑gₗ) :
    Topology.IsStrictMap ⇑(fₗ.prodMap gₗ)

    The product (in the sense of LinearMap.prodMap) of strict linear maps is strict.