Documentation

TauCeti.Analysis.Normed.Module.StrictGenerators

Finite strict generating systems of normed submodules #

Let N be a submodule of a normed module M over a seminormed ring A. A finite set F of nonzero elements of N generates N strictly when every y ∈ N is a combination ∑ x ∈ F, a x • x with ‖a x‖ * ‖x‖ ≤ ‖y‖, so that no cancellation between the terms is needed to represent y.

Because F is finite and consists of nonzero elements, the coefficients a x of such a representation are bounded by (∑ x ∈ F, ‖x‖⁻¹) * ‖y‖. The linear-combination map (F → A) → N therefore has uniformly norm-bounded lifts, making it an open quotient map onto N with its subspace topology (TauCeti.isOpenMap_of_exists_norm_le). Consequently:

When the norm of A is multiplicative and ultrametric, the action of A on M multiplies norms, and the norm of every nonzero element of N is the norm of a unit of A, each generator can be divided by such a unit. This gives a strict generating system of elements of norm one, with coefficients bounded by ‖y‖ (Submodule.exists_finset_norm_eq_one_of_exists_finset_eq_sum_smul). For ideals and submodules of finite free modules over a Tate algebra at unit polyradius the units used for this normalisation can be chosen to be nonzero constants, whose norms are all the values of the Gauss norm.

source
theorem Submodule.isModuleTopology_of_exists_finset_eq_sum_smul {A : Type u_1} {M : Type u_2} [SeminormedRing A] [NormedAddCommGroup M] [Module A M] [IsBoundedSMul A M] {N : Submodule A M} (hN : ∃ (F : Finset M), (∀ x ∈ F, x ∈ N ∧ x ≠ 0) ∧ ∀ y ∈ N, ∃ (a : M → A), y = ∑ x ∈ F, a x • x ∧ ∀ x ∈ F, ‖a x‖ * ‖x‖ ≤ ‖y‖) :
IsModuleTopology A ↥N

Subspace module topology from strict generators. If a submodule N of a normed module M over a seminormed ring A has a finite strict generating system, its subspace topology is the module topology over A. Neither completeness nor commutativity of A is needed.

source
theorem LinearMap.exists_preimage_norm_le_of_exists_finset_eq_sum_smul {A : Type u_1} {M : Type u_2} [SeminormedRing A] [NormedAddCommGroup M] [Module A M] {M₀ : Type u_3} [SeminormedAddCommGroup M₀] [Module A M₀] [IsBoundedSMul A M₀] (f : M₀ →ₗ[A] M) (hr : ∃ (F : Finset M), (∀ y ∈ F, y ∈ f.range ∧ y ≠ 0) ∧ ∀ z ∈ f.range, ∃ (a : M → A), z = ∑ y ∈ F, a y • y ∧ ∀ y ∈ F, ‖a y‖ * ‖y‖ ≤ ‖z‖) :
∃ (C : ℝ), 0 < C ∧ ∀ z ∈ f.range, ∃ (x : M₀), f x = z ∧ ‖x‖ ≤ C * ‖z‖

Uniformly bounded preimages from strict generators of the range. If the range of a linear map f : M₀ →ₗ[A] M from a seminormed A-module into a normed A-module has a finite strict generating system, there is C > 0 such that every z ∈ LinearMap.range f has a preimage x : M₀ with ‖x‖ ≤ C * ‖z‖. Neither continuity of f nor completeness of A or M₀ is needed.

source
theorem LinearMap.exists_preimage_norm_le_quotient_of_exists_finset_eq_sum_smul {A : Type u_1} {M : Type u_2} [SeminormedRing A] [NormedAddCommGroup M] [Module A M] {M₀ : Type u_3} [SeminormedAddCommGroup M₀] [Module A M₀] [IsBoundedSMul A M₀] {N : Submodule A M} (f : M₀ →ₗ[A] M ⧸ N) (hrep : ∀ q ∈ f.range, ∃ (w : M), Submodule.Quotient.mk w = q ∧ ‖w‖ = ‖q‖) (hr : ∃ (F : Finset M), (∀ y ∈ F, y ∈ Submodule.comap N.mkQ f.range ∧ y ≠ 0) ∧ ∀ z ∈ Submodule.comap N.mkQ f.range, ∃ (a : M → A), z = ∑ y ∈ F, a y • y ∧ ∀ y ∈ F, ‖a y‖ * ‖y‖ ≤ ‖z‖) :
∃ (C : ℝ), 0 < C ∧ ∀ q ∈ f.range, ∃ (x : M₀), f x = q ∧ ‖x‖ ≤ C * ‖q‖

Uniformly bounded preimages into a quotient from strict generators and exact representatives. Let N be a submodule of a normed A-module M, and f : M₀ →ₗ[A] M ⧸ N a linear map from a seminormed A-module M₀. If every class in LinearMap.range f has a representative in M attaining its quotient norm, and (LinearMap.range f).comap N.mkQ ≤ M admits a finite strict generating system, then f has uniformly norm-bounded preimages on its range.

source
theorem Submodule.completeSpace_of_exists_finset_eq_sum_smul {A : Type u_1} {M : Type u_2} [SeminormedRing A] [NormedAddCommGroup M] [Module A M] [IsBoundedSMul A M] [CompleteSpace A] {N : Submodule A M} (hN : ∃ (F : Finset M), (∀ x ∈ F, x ∈ N ∧ x ≠ 0) ∧ ∀ y ∈ N, ∃ (a : M → A), y = ∑ x ∈ F, a x • x ∧ ∀ x ∈ F, ‖a x‖ * ‖x‖ ≤ ‖y‖) :
CompleteSpace ↥N

Completeness from strict generators. Over a complete seminormed ring, every submodule of a normed module admitting a finite strict generating system is complete in the induced norm.

source
theorem Submodule.isClosed_of_exists_finset_eq_sum_smul {A : Type u_1} {M : Type u_2} [SeminormedRing A] [NormedAddCommGroup M] [Module A M] [IsBoundedSMul A M] [CompleteSpace A] {N : Submodule A M} (hN : ∃ (F : Finset M), (∀ x ∈ F, x ∈ N ∧ x ≠ 0) ∧ ∀ y ∈ N, ∃ (a : M → A), y = ∑ x ∈ F, a x • x ∧ ∀ x ∈ F, ‖a x‖ * ‖x‖ ≤ ‖y‖) :
IsClosed ↑N

Closedness from strict generators. Over a complete seminormed ring, every submodule of a normed module admitting a finite strict generating system is closed.

source
theorem Submodule.exists_finset_norm_eq_one_of_exists_finset_eq_sum_smul {A : Type u_1} {M : Type u_2} [NormedRing A] [NormMulClass A] [IsUltrametricDist A] [SeminormedAddCommGroup M] [Module A M] [NormSMulClass A M] {N : Submodule A M} (hunit : ∀ x ∈ N, x ≠ 0 → ∃ (u : A), IsUnit u ∧ ‖u‖ = ‖x‖) (hN : ∃ (F : Finset M), (∀ x ∈ F, x ∈ N ∧ x ≠ 0) ∧ ∀ y ∈ N, ∃ (a : M → A), y = ∑ x ∈ F, a x • x ∧ ∀ x ∈ F, ‖a x‖ * ‖x‖ ≤ ‖y‖) :
∃ (F : Finset M), (∀ x ∈ F, x ∈ N ∧ ‖x‖ = 1) ∧ ∀ y ∈ N, ∃ (a : M → A), y = ∑ x ∈ F, a x • x ∧ ∀ x ∈ F, ‖a x‖ ≤ ‖y‖

Normalising a strict generating system. Let N be a submodule of a normed module over a ring with a multiplicative ultrametric norm, such that the norm of every nonzero element of N is the norm of a unit. If finitely many nonzero elements x of N generate it strictly, with each y ∈ N a combination ∑ x, a x • x with ‖a x‖ * ‖x‖ ≤ ‖y‖, then finitely many elements of N of norm one generate it with coefficients ‖a x‖ ≤ ‖y‖.