Quantitative mapping theorems over Tate rings

TauCeti.HasZeroSequenceOfUnits.isOpenMap proves Henkel's topological open mapping theorem for surjective equivariant additive maps out of a complete first-countable non-archimedean group into a Baire target over any scalar ring admitting a zero sequence of units. When the scalar ring is a Tate normed ring (TauCeti.NormedRing.IsTate), the powers of a multiplicative pseudo-uniformiser supply that zero sequence of units, and exact scaling by integer powers of the pseudo-uniformiser turns topological openness into quantitative linear preimage bounds.

This file develops those quantitative mapping theorems and their finite-free consequences over any Tate seminormed ring R (no commutativity or ultrametric hypothesis on R is needed unless R^n itself serves as the ultrametric domain):

• Quantitative preimage bounds from openness: if ϖ is a multiplicative pseudo-uniformiser on R and the image of ball (0 : M) R₀ under f : M →ₗ[R] N contains ball (0 : N) δ with ‖(ϖ.unit : R)‖ ^ k < δ, then f is surjective onto the normed module N and every y : N admits a preimage x with ‖x‖ ≤ R₀ * (‖(ϖ.unit : R)‖ ^ (k + 1))⁻¹ * ‖y‖ (TauCeti.NormedRing.PseudoUniformizer.exists_preimage_norm_le_of_ball_subset). Consequently, any open linear map into a normed module over a Tate ring is surjective with a linear preimage bound (LinearMap.exists_preimage_norm_le_of_isOpenMap).
• Quantitative Banach open mapping: a surjective continuous linear map f : M →L[R] N from a complete ultrametric seminormed module to a complete normed module over a Tate ring is an open quotient map and admits a constant C > 0 such that every y : N lifts to x : M with ‖x‖ ≤ C * ‖y‖ (ContinuousLinearMap.exists_preimage_norm_le_of_isTate).
• Closed-range strictness and antilipschitz criteria: a continuous linear map with closed range from a complete ultrametric seminormed module to a complete normed module over a Tate ring is strict and admits linear preimage bounds on its range; if it is also injective, it is antilipschitz and induces a ContinuousLinearEquiv onto its range (ContinuousLinearMap.isClosed_range_iff_antilipschitz_of_injective_of_isTate, ContinuousLinearMap.equivRangeOfIsTate).
• Bounded inverse and closed graph theorems packaged for ContinuousLinearEquiv and ContinuousLinearMap over Tate rings (LinearEquiv.toContinuousLinearEquivOfContinuousOfIsTate, ContinuousLinearEquiv.ofBijectiveOfIsTate, ContinuousLinearMap.isUnit_iff_bijective_of_isTate, LinearMap.continuous_of_isClosed_graph_of_isTate, LinearMap.continuous_of_seq_closed_graph_of_isTate, ContinuousLinearMap.ofIsClosedGraphOfIsTate, and ContinuousLinearMap.ofSeqClosedGraphOfIsTate).
• Quantitative finite spanning: any finite family v : ι → N satisfying Submodule.span R (Set.range v) = ⊤ in a complete normed module over a complete ultrametric Tate ring admits a constant C > 0 representing every y : N as ∑ i, c i • v i with ‖c‖ ≤ C * ‖y‖ (TauCeti.exists_linearCombination_eq_and_norm_le).

The API and the bounded-inverse, range-equivalence, bijective-map, unit and closed-graph packaging are adapted from Mathlib/Analysis/Normed/Operator/Banach.lean, in particular LinearEquiv.continuous_symm, LinearEquiv.toContinuousLinearEquivOfContinuous, ContinuousLinearMap.equivRange, ContinuousLinearMap.isClosed_range_iff_antilipschitz_of_injective, ContinuousLinearEquiv.ofBijective, ContinuousLinearMap.isUnit_iff_bijective, ContinuousLinearMap.ofIsClosedGraph and ContinuousLinearMap.ofSeqClosedGraph.

References

• K. Buzzard, The Analytic Continuation of p-adic Modular Forms (eigenbook), §2.
• L. Henkel, An Open Mapping Theorem for rings which have a zero sequence of units, arXiv:1407.5647.
• C. Johansson and J. Newton, Extended eigenvarieties for overconvergent cohomology, arXiv:1604.07739, §2.1.
• P. Schneider, Nonarchimedean Functional Analysis, Springer, 2002, §8.

theorem TauCeti.NormedRing.PseudoUniformizer.exists_preimage_norm_le_of_ball_subset {R : Type u_1} {M : Type u_2} {N : Type u_3} [SeminormedRing R] [SeminormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [NormedAddCommGroup N] [Module R N] [IsBoundedSMul R N] (ϖ : PseudoUniformizer R) (f : M →ₗ[R] N) {δ R₀ : ℝ} (k : ℤ) (hδ : ‖↑ϖ.unit‖ ^ k < δ) (hball : Metric.ball 0 δ ⊆ ⇑f '' Metric.ball 0 R₀) (y : N) : ∃ (x : M), f x = y ∧ ‖x‖ ≤ R₀ * (‖↑ϖ.unit‖ ^ (k + 1))⁻¹ * ‖y‖

Quantitative preimage bound from ball containment. If ϖ is a multiplicative pseudo-uniformiser on R, ‖(ϖ.unit : R)‖ ^ k < δ, and ball (0 : N) δ ⊆ f '' ball (0 : M) R₀, then every y : N admits x : M with f x = y and ‖x‖ ≤ R₀ * (‖(ϖ.unit : R)‖ ^ (k + 1))⁻¹ * ‖y‖.

theorem LinearMap.exists_preimage_norm_le_of_nhds_zero {R : Type u_1} {M : Type u_2} {N : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [NormedAddCommGroup N] [Module R N] [IsBoundedSMul R N] (f : M →ₗ[R] N) (hnhds : ⇑f '' Metric.ball 0 1 ∈ nhds 0) : ∃ C > 0, ∀ (y : N), ∃ (x : M), f x = y ∧ ‖x‖ ≤ C * ‖y‖

If the image of the unit ball under f : M →ₗ[R] N is a neighbourhood of 0 in a normed module N over a Tate ring R, then f is surjective and admits a constant C > 0 such that every y : N lifts to x : M with ‖x‖ ≤ C * ‖y‖.

theorem LinearMap.exists_preimage_norm_le_of_isOpenMap {R : Type u_1} {M : Type u_2} {N : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [NormedAddCommGroup N] [Module R N] [IsBoundedSMul R N] (f : M →ₗ[R] N) (hopen : IsOpenMap ⇑f) : ∃ C > 0, ∀ (y : N), ∃ (x : M), f x = y ∧ ‖x‖ ≤ C * ‖y‖

Any open linear map into a normed module over a Tate ring is surjective and admits a linear preimage bound ‖x‖ ≤ C * ‖y‖ with C > 0.

theorem LinearMap.isOpenMap_of_isTate {R : Type u_1} {M : Type u_2} {N : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup M] [IsUltrametricDist M] [CompleteSpace M] [Module R M] [IsBoundedSMul R M] [NormedAddCommGroup N] [CompleteSpace N] [Module R N] [IsBoundedSMul R N] (f : M →ₗ[R] N) (hf : Continuous ⇑f) (hsurj : Function.Surjective ⇑f) : IsOpenMap ⇑f

Open Mapping Theorem for normed modules over a Tate ring. A surjective continuous linear map from a complete ultrametric seminormed module to a complete normed module over a Tate ring is an open map.

theorem LinearMap.exists_preimage_norm_le_of_surjective {R : Type u_1} {M : Type u_2} {N : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup M] [IsUltrametricDist M] [CompleteSpace M] [Module R M] [IsBoundedSMul R M] [NormedAddCommGroup N] [CompleteSpace N] [Module R N] [IsBoundedSMul R N] (f : M →ₗ[R] N) (hf : Continuous ⇑f) (hsurj : Function.Surjective ⇑f) : ∃ C > 0, ∀ (y : N), ∃ (x : M), f x = y ∧ ‖x‖ ≤ C * ‖y‖

Quantitative Open Mapping Theorem for linear maps over a Tate ring: every surjective continuous linear map from a complete ultrametric seminormed module to a complete normed module admits a constant C > 0 such that every y : N lifts to x : M with ‖x‖ ≤ C * ‖y‖.

theorem LinearEquiv.continuous_symm_of_isTate {R : Type u_1} {M : Type u_2} {N : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup M] [IsUltrametricDist M] [CompleteSpace M] [Module R M] [IsBoundedSMul R M] [NormedAddCommGroup N] [CompleteSpace N] [Module R N] [IsBoundedSMul R N] (e : M ≃ₗ[R] N) (he : Continuous ⇑e) : Continuous ⇑e.symm

Bounded Inverse Theorem for linear equivalences over a Tate ring: the inverse of a continuous linear equivalence from a complete ultrametric seminormed module to a complete normed module is continuous.

def LinearEquiv.toContinuousLinearEquivOfContinuousOfIsTate {R : Type u_1} {M : Type u_2} {N : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup M] [IsUltrametricDist M] [CompleteSpace M] [Module R M] [IsBoundedSMul R M] [NormedAddCommGroup N] [CompleteSpace N] [Module R N] [IsBoundedSMul R N] (e : M ≃ₗ[R] N) (he : Continuous ⇑e) : M ≃L[R] N

Promote a continuous linear equivalence e : M ≃ₗ[R] N from a complete ultrametric seminormed module to a complete normed module over a Tate ring to a bundled ContinuousLinearEquiv.

@[simp]

theorem LinearEquiv.toLinearEquiv_toContinuousLinearEquivOfContinuousOfIsTate {R : Type u_1} {M : Type u_2} {N : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup M] [IsUltrametricDist M] [CompleteSpace M] [Module R M] [IsBoundedSMul R M] [NormedAddCommGroup N] [CompleteSpace N] [Module R N] [IsBoundedSMul R N] (e : M ≃ₗ[R] N) (he : Continuous ⇑e) : ↑(e.toContinuousLinearEquivOfContinuousOfIsTate he) = e

@[simp]

theorem LinearEquiv.coeFn_toContinuousLinearEquivOfContinuousOfIsTate {R : Type u_1} {M : Type u_2} {N : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup M] [IsUltrametricDist M] [CompleteSpace M] [Module R M] [IsBoundedSMul R M] [NormedAddCommGroup N] [CompleteSpace N] [Module R N] [IsBoundedSMul R N] (e : M ≃ₗ[R] N) (he : Continuous ⇑e) : ⇑(e.toContinuousLinearEquivOfContinuousOfIsTate he) = ⇑e

@[simp]

theorem LinearEquiv.coeFn_toContinuousLinearEquivOfContinuousOfIsTate_symm {R : Type u_1} {M : Type u_2} {N : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup M] [IsUltrametricDist M] [CompleteSpace M] [Module R M] [IsBoundedSMul R M] [NormedAddCommGroup N] [CompleteSpace N] [Module R N] [IsBoundedSMul R N] (e : M ≃ₗ[R] N) (he : Continuous ⇑e) : ⇑(e.toContinuousLinearEquivOfContinuousOfIsTate he).symm = ⇑e.symm

@[simp]

theorem LinearEquiv.toContinuousLinearEquivOfContinuousOfIsTate_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup M] [IsUltrametricDist M] [CompleteSpace M] [Module R M] [IsBoundedSMul R M] [NormedAddCommGroup N] [CompleteSpace N] [Module R N] [IsBoundedSMul R N] (e : M ≃ₗ[R] N) (he : Continuous ⇑e) (x : M) : (e.toContinuousLinearEquivOfContinuousOfIsTate he) x = e x

@[simp]

theorem LinearEquiv.toContinuousLinearEquivOfContinuousOfIsTate_symm_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup M] [IsUltrametricDist M] [CompleteSpace M] [Module R M] [IsBoundedSMul R M] [NormedAddCommGroup N] [CompleteSpace N] [Module R N] [IsBoundedSMul R N] (e : M ≃ₗ[R] N) (he : Continuous ⇑e) (y : N) : (e.toContinuousLinearEquivOfContinuousOfIsTate he).symm y = e.symm y

noncomputable def ContinuousLinearEquiv.ofBijectiveOfIsTate {R : Type u_1} {M : Type u_2} {N : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup M] [IsUltrametricDist M] [CompleteSpace M] [Module R M] [IsBoundedSMul R M] [NormedAddCommGroup N] [CompleteSpace N] [Module R N] [IsBoundedSMul R N] (f : M →L[R] N) (hf : Function.Bijective ⇑f) : M ≃L[R] N

Bounded Inverse Theorem: a bijective continuous linear map from a complete ultrametric seminormed module to a complete normed module over a Tate ring is a continuous linear equivalence.

@[simp]

theorem ContinuousLinearEquiv.coeFn_ofBijectiveOfIsTate {R : Type u_1} {M : Type u_2} {N : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup M] [IsUltrametricDist M] [CompleteSpace M] [Module R M] [IsBoundedSMul R M] [NormedAddCommGroup N] [CompleteSpace N] [Module R N] [IsBoundedSMul R N] (f : M →L[R] N) (hf : Function.Bijective ⇑f) : ⇑(ofBijectiveOfIsTate f hf) = ⇑f

@[simp]

theorem ContinuousLinearEquiv.coe_ofBijectiveOfIsTate {R : Type u_1} {M : Type u_2} {N : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup M] [IsUltrametricDist M] [CompleteSpace M] [Module R M] [IsBoundedSMul R M] [NormedAddCommGroup N] [CompleteSpace N] [Module R N] [IsBoundedSMul R N] (f : M →L[R] N) (hf : Function.Bijective ⇑f) : ↑(ofBijectiveOfIsTate f hf) = f

@[simp]

theorem ContinuousLinearEquiv.ofBijectiveOfIsTate_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup M] [IsUltrametricDist M] [CompleteSpace M] [Module R M] [IsBoundedSMul R M] [NormedAddCommGroup N] [CompleteSpace N] [Module R N] [IsBoundedSMul R N] (f : M →L[R] N) (hf : Function.Bijective ⇑f) (x : M) : (ofBijectiveOfIsTate f hf) x = f x

@[simp]

theorem ContinuousLinearEquiv.ofBijectiveOfIsTate_symm_apply_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup M] [IsUltrametricDist M] [CompleteSpace M] [Module R M] [IsBoundedSMul R M] [NormedAddCommGroup N] [CompleteSpace N] [Module R N] [IsBoundedSMul R N] (f : M →L[R] N) (hf : Function.Bijective ⇑f) (x : M) : (ofBijectiveOfIsTate f hf).symm (f x) = x

@[simp]

theorem ContinuousLinearEquiv.ofBijectiveOfIsTate_apply_symm_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup M] [IsUltrametricDist M] [CompleteSpace M] [Module R M] [IsBoundedSMul R M] [NormedAddCommGroup N] [CompleteSpace N] [Module R N] [IsBoundedSMul R N] (f : M →L[R] N) (hf : Function.Bijective ⇑f) (y : N) : f ((ofBijectiveOfIsTate f hf).symm y) = y

theorem ContinuousLinearMap.isOpenMap_of_isTate {R : Type u_1} {M : Type u_2} {N : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup M] [IsUltrametricDist M] [CompleteSpace M] [Module R M] [IsBoundedSMul R M] [NormedAddCommGroup N] [CompleteSpace N] [Module R N] [IsBoundedSMul R N] (f : M →L[R] N) (hsurj : Function.Surjective ⇑f) : IsOpenMap ⇑f

A surjective continuous linear map from a complete ultrametric seminormed module to a complete normed module over a Tate ring is an open map.

theorem ContinuousLinearMap.isQuotientMap_of_isTate {R : Type u_1} {M : Type u_2} {N : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup M] [IsUltrametricDist M] [CompleteSpace M] [Module R M] [IsBoundedSMul R M] [NormedAddCommGroup N] [CompleteSpace N] [Module R N] [IsBoundedSMul R N] (f : M →L[R] N) (hsurj : Function.Surjective ⇑f) : Topology.IsQuotientMap ⇑f

A surjective continuous linear map from a complete ultrametric seminormed module to a complete normed module over a Tate ring is a quotient map.

theorem ContinuousLinearMap.exists_preimage_norm_le_of_isTate {R : Type u_1} {M : Type u_2} {N : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup M] [IsUltrametricDist M] [CompleteSpace M] [Module R M] [IsBoundedSMul R M] [NormedAddCommGroup N] [CompleteSpace N] [Module R N] [IsBoundedSMul R N] (f : M →L[R] N) (hsurj : Function.Surjective ⇑f) : ∃ C > 0, ∀ (y : N), ∃ (x : M), f x = y ∧ ‖x‖ ≤ C * ‖y‖

Quantitative Open Mapping Theorem: for a surjective continuous linear map f : M →L[R] N from a complete ultrametric seminormed module to a complete normed module over a Tate ring, there exists C > 0 such that every y : N lifts to x : M with ‖x‖ ≤ C * ‖y‖.

theorem ContinuousLinearMap.isStrictMap_of_isClosed_range_of_isTate {R : Type u_1} {M : Type u_2} {N : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup M] [IsUltrametricDist M] [CompleteSpace M] [Module R M] [IsBoundedSMul R M] [NormedAddCommGroup N] [CompleteSpace N] [Module R N] [IsBoundedSMul R N] (f : M →L[R] N) (hclosed : IsClosed (Set.range ⇑f)) : Topology.IsStrictMap ⇑f

A continuous linear map f : M →L[R] N with closed range from a complete ultrametric seminormed module to a complete normed module over a Tate ring is a strict morphism (Topology.IsStrictMap).

theorem ContinuousLinearMap.isOpenMap_rangeRestrict_of_isClosed_range_of_isTate {R : Type u_1} {M : Type u_2} {N : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup M] [IsUltrametricDist M] [CompleteSpace M] [Module R M] [IsBoundedSMul R M] [NormedAddCommGroup N] [CompleteSpace N] [Module R N] [IsBoundedSMul R N] (f : M →L[R] N) (hclosed : IsClosed (Set.range ⇑f)) : IsOpenMap ⇑f.rangeRestrict

A continuous linear map f : M →L[R] N with closed range from a complete ultrametric seminormed module to a complete normed module over a Tate ring is open onto its range.

theorem ContinuousLinearMap.exists_preimage_norm_le_of_isClosed_range_of_isTate {R : Type u_1} {M : Type u_2} {N : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup M] [IsUltrametricDist M] [CompleteSpace M] [Module R M] [IsBoundedSMul R M] [NormedAddCommGroup N] [CompleteSpace N] [Module R N] [IsBoundedSMul R N] (f : M →L[R] N) (hclosed : IsClosed (Set.range ⇑f)) : ∃ C > 0, ∀ y ∈ Set.range ⇑f, ∃ (x : M), f x = y ∧ ‖x‖ ≤ C * ‖y‖

Quantitative preimage bound for closed-range operators: if f : M →L[R] N from a complete ultrametric seminormed module to a complete normed module over a Tate ring has closed range, there exists C > 0 such that every y ∈ Set.range f lifts to x : M with f x = y and ‖x‖ ≤ C * ‖y‖.

theorem ContinuousLinearMap.exists_norm_le_of_injective_of_isClosed_range_of_isTate {R : Type u_1} {M : Type u_2} {N : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup M] [IsUltrametricDist M] [CompleteSpace M] [Module R M] [IsBoundedSMul R M] [NormedAddCommGroup N] [CompleteSpace N] [Module R N] [IsBoundedSMul R N] (f : M →L[R] N) (hinj : Function.Injective ⇑f) (hclosed : IsClosed (Set.range ⇑f)) : ∃ C > 0, ∀ (x : M), ‖x‖ ≤ C * ‖f x‖

If f : M →L[R] N from a complete ultrametric seminormed module to a complete normed module over a Tate ring is injective and has closed range, then ‖x‖ ≤ C * ‖f x‖ for some C > 0.

theorem ContinuousLinearMap.antilipschitz_of_injective_of_isClosed_range_of_isTate {R : Type u_1} {M : Type u_2} {N : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup M] [IsUltrametricDist M] [CompleteSpace M] [Module R M] [IsBoundedSMul R M] [NormedAddCommGroup N] [CompleteSpace N] [Module R N] [IsBoundedSMul R N] (f : M →L[R] N) (hinj : Function.Injective ⇑f) (hclosed : IsClosed (Set.range ⇑f)) : ∃ (K : NNReal), K ≠ 0 ∧ AntilipschitzWith K ⇑f

If f : M →L[R] N from a complete ultrametric seminormed module to a complete normed module over a Tate ring is injective and has closed range, then f is AntilipschitzWith K for some K ≠ 0.

theorem ContinuousLinearMap.isClosed_range_iff_antilipschitz_of_injective_of_isTate {R : Type u_1} {N : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [NormedAddCommGroup N] [CompleteSpace N] [Module R N] [IsBoundedSMul R N] {M' : Type u_4} [NormedAddCommGroup M'] [IsUltrametricDist M'] [CompleteSpace M'] [Module R M'] [IsBoundedSMul R M'] (f : M' →L[R] N) (hinj : Function.Injective ⇑f) : IsClosed (Set.range ⇑f) ↔ ∃ (K : NNReal), AntilipschitzWith K ⇑f

For an injective continuous linear map f : M' →L[R] N from a complete ultrametric normed module to a complete normed module over a Tate ring, the range of f is closed if and only if f is antilipschitz.

noncomputable def ContinuousLinearMap.equivRangeOfIsTate {R : Type u_1} {M : Type u_2} {N : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup M] [IsUltrametricDist M] [CompleteSpace M] [Module R M] [IsBoundedSMul R M] [NormedAddCommGroup N] [CompleteSpace N] [Module R N] [IsBoundedSMul R N] (f : M →L[R] N) (hinj : Function.Injective ⇑f) (hclosed : IsClosed (Set.range ⇑f)) : M ≃L[R] ↥(↑f).range

An injective continuous linear map with closed range from a complete ultrametric seminormed module to a complete normed module over a Tate ring induces a continuous linear equivalence onto its range.

@[simp]

theorem ContinuousLinearMap.coeFn_equivRangeOfIsTate {R : Type u_1} {M : Type u_2} {N : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup M] [IsUltrametricDist M] [CompleteSpace M] [Module R M] [IsBoundedSMul R M] [NormedAddCommGroup N] [CompleteSpace N] [Module R N] [IsBoundedSMul R N] (f : M →L[R] N) (hinj : Function.Injective ⇑f) (hclosed : IsClosed (Set.range ⇑f)) : ⇑(f.equivRangeOfIsTate hinj hclosed) = ⇑f.rangeRestrict

@[simp]

theorem ContinuousLinearMap.coe_equivRangeOfIsTate {R : Type u_1} {M : Type u_2} {N : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup M] [IsUltrametricDist M] [CompleteSpace M] [Module R M] [IsBoundedSMul R M] [NormedAddCommGroup N] [CompleteSpace N] [Module R N] [IsBoundedSMul R N] (f : M →L[R] N) (hinj : Function.Injective ⇑f) (hclosed : IsClosed (Set.range ⇑f)) : ↑(f.equivRangeOfIsTate hinj hclosed) = f.rangeRestrict

@[simp]

theorem ContinuousLinearMap.equivRangeOfIsTate_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup M] [IsUltrametricDist M] [CompleteSpace M] [Module R M] [IsBoundedSMul R M] [NormedAddCommGroup N] [CompleteSpace N] [Module R N] [IsBoundedSMul R N] (f : M →L[R] N) (hinj : Function.Injective ⇑f) (hclosed : IsClosed (Set.range ⇑f)) (x : M) : (f.equivRangeOfIsTate hinj hclosed) x = f.rangeRestrict x

@[simp]

theorem ContinuousLinearMap.equivRangeOfIsTate_symm_apply_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup M] [IsUltrametricDist M] [CompleteSpace M] [Module R M] [IsBoundedSMul R M] [NormedAddCommGroup N] [CompleteSpace N] [Module R N] [IsBoundedSMul R N] (f : M →L[R] N) (hinj : Function.Injective ⇑f) (hclosed : IsClosed (Set.range ⇑f)) (x : M) : (f.equivRangeOfIsTate hinj hclosed).symm ⟨f x, ⋯⟩ = x

theorem ContinuousLinearMap.isUnit_iff_bijective_of_isTate {R : Type u_1} {N : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [NormedAddCommGroup N] [CompleteSpace N] [Module R N] [IsBoundedSMul R N] [IsUltrametricDist N] (f : N →L[R] N) : IsUnit f ↔ Function.Bijective ⇑f

A continuous linear endomorphism of a complete ultrametric normed module over a Tate ring is a unit in N →L[R] N if and only if it is bijective.

Closed graph theorem

theorem LinearMap.continuous_of_isClosed_graph_of_isTate {R : Type u_1} {M : Type u_2} {N : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [NormedAddCommGroup M] [IsUltrametricDist M] [CompleteSpace M] [Module R M] [IsBoundedSMul R M] [SeminormedAddCommGroup N] [IsUltrametricDist N] [CompleteSpace N] [Module R N] [IsBoundedSMul R N] (f : M →ₗ[R] N) (hg : IsClosed ↑f.graph) : Continuous ⇑f

Closed Graph Theorem for normed modules over a Tate ring: a linear map from a complete ultrametric normed module to a complete ultrametric seminormed module whose graph is closed is continuous.

theorem LinearMap.continuous_of_seq_closed_graph_of_isTate {R : Type u_1} {M : Type u_2} {N : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [NormedAddCommGroup M] [IsUltrametricDist M] [CompleteSpace M] [Module R M] [IsBoundedSMul R M] [SeminormedAddCommGroup N] [IsUltrametricDist N] [CompleteSpace N] [Module R N] [IsBoundedSMul R N] (f : M →ₗ[R] N) (hg : ∀ (u : ℕ → M) (x : M) (y : N), Filter.Tendsto u Filter.atTop (nhds x) → Filter.Tendsto (⇑f ∘ u) Filter.atTop (nhds y) → y = f x) : Continuous ⇑f

Sequential Closed Graph Theorem for normed modules over a Tate ring: a linear map from a complete ultrametric normed module to a complete ultrametric seminormed module whose graph is sequentially closed is continuous.

def ContinuousLinearMap.ofIsClosedGraphOfIsTate {R : Type u_1} {M : Type u_2} {N : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [NormedAddCommGroup M] [IsUltrametricDist M] [CompleteSpace M] [Module R M] [IsBoundedSMul R M] [SeminormedAddCommGroup N] [IsUltrametricDist N] [CompleteSpace N] [Module R N] [IsBoundedSMul R N] {f : M →ₗ[R] N} (hg : IsClosed ↑f.graph) : M →L[R] N

Construct a bundled continuous linear map from a linear map with closed graph over a Tate ring.

@[simp]

theorem ContinuousLinearMap.coeFn_ofIsClosedGraphOfIsTate {R : Type u_1} {M : Type u_2} {N : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [NormedAddCommGroup M] [IsUltrametricDist M] [CompleteSpace M] [Module R M] [IsBoundedSMul R M] [SeminormedAddCommGroup N] [IsUltrametricDist N] [CompleteSpace N] [Module R N] [IsBoundedSMul R N] {f : M →ₗ[R] N} (hg : IsClosed ↑f.graph) : ⇑(ofIsClosedGraphOfIsTate hg) = ⇑f

@[simp]

theorem ContinuousLinearMap.coe_ofIsClosedGraphOfIsTate {R : Type u_1} {M : Type u_2} {N : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [NormedAddCommGroup M] [IsUltrametricDist M] [CompleteSpace M] [Module R M] [IsBoundedSMul R M] [SeminormedAddCommGroup N] [IsUltrametricDist N] [CompleteSpace N] [Module R N] [IsBoundedSMul R N] {f : M →ₗ[R] N} (hg : IsClosed ↑f.graph) : ↑(ofIsClosedGraphOfIsTate hg) = f

@[simp]

theorem ContinuousLinearMap.ofIsClosedGraphOfIsTate_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [NormedAddCommGroup M] [IsUltrametricDist M] [CompleteSpace M] [Module R M] [IsBoundedSMul R M] [SeminormedAddCommGroup N] [IsUltrametricDist N] [CompleteSpace N] [Module R N] [IsBoundedSMul R N] {f : M →ₗ[R] N} (hg : IsClosed ↑f.graph) (x : M) : (ofIsClosedGraphOfIsTate hg) x = f x

def ContinuousLinearMap.ofSeqClosedGraphOfIsTate {R : Type u_1} {M : Type u_2} {N : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [NormedAddCommGroup M] [IsUltrametricDist M] [CompleteSpace M] [Module R M] [IsBoundedSMul R M] [SeminormedAddCommGroup N] [IsUltrametricDist N] [CompleteSpace N] [Module R N] [IsBoundedSMul R N] {f : M →ₗ[R] N} (hg : ∀ (u : ℕ → M) (x : M) (y : N), Filter.Tendsto u Filter.atTop (nhds x) → Filter.Tendsto (⇑f ∘ u) Filter.atTop (nhds y) → y = f x) : M →L[R] N

Construct a bundled continuous linear map from a linear map with sequentially closed graph over a Tate ring.

@[simp]

theorem ContinuousLinearMap.coeFn_ofSeqClosedGraphOfIsTate {R : Type u_1} {M : Type u_2} {N : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [NormedAddCommGroup M] [IsUltrametricDist M] [CompleteSpace M] [Module R M] [IsBoundedSMul R M] [SeminormedAddCommGroup N] [IsUltrametricDist N] [CompleteSpace N] [Module R N] [IsBoundedSMul R N] {f : M →ₗ[R] N} (hg : ∀ (u : ℕ → M) (x : M) (y : N), Filter.Tendsto u Filter.atTop (nhds x) → Filter.Tendsto (⇑f ∘ u) Filter.atTop (nhds y) → y = f x) : ⇑(ofSeqClosedGraphOfIsTate hg) = ⇑f

@[simp]

theorem ContinuousLinearMap.coe_ofSeqClosedGraphOfIsTate {R : Type u_1} {M : Type u_2} {N : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [NormedAddCommGroup M] [IsUltrametricDist M] [CompleteSpace M] [Module R M] [IsBoundedSMul R M] [SeminormedAddCommGroup N] [IsUltrametricDist N] [CompleteSpace N] [Module R N] [IsBoundedSMul R N] {f : M →ₗ[R] N} (hg : ∀ (u : ℕ → M) (x : M) (y : N), Filter.Tendsto u Filter.atTop (nhds x) → Filter.Tendsto (⇑f ∘ u) Filter.atTop (nhds y) → y = f x) : ↑(ofSeqClosedGraphOfIsTate hg) = f

@[simp]

theorem ContinuousLinearMap.ofSeqClosedGraphOfIsTate_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [NormedAddCommGroup M] [IsUltrametricDist M] [CompleteSpace M] [Module R M] [IsBoundedSMul R M] [SeminormedAddCommGroup N] [IsUltrametricDist N] [CompleteSpace N] [Module R N] [IsBoundedSMul R N] {f : M →ₗ[R] N} (hg : ∀ (u : ℕ → M) (x : M) (y : N), Filter.Tendsto u Filter.atTop (nhds x) → Filter.Tendsto (⇑f ∘ u) Filter.atTop (nhds y) → y = f x) (x : M) : (ofSeqClosedGraphOfIsTate hg) x = f x

Quantitative finite spanning

theorem TauCeti.exists_linearCombination_eq_and_norm_le {R : Type u_1} {N : Type u_2} {ι : Type u_3} [Fintype ι] [SeminormedRing R] [IsUltrametricDist R] [CompleteSpace R] [NormedRing.IsTate R] [NormedAddCommGroup N] [CompleteSpace N] [Module R N] [IsBoundedSMul R N] (v : ι → N) (hspan : Submodule.span R (Set.range v) = ⊤) : ∃ C > 0, ∀ (y : N), ∃ (c : ι → R), ∑ i : ι, c i • v i = y ∧ ‖c‖ ≤ C * ‖y‖

Quantitative finite spanning over a complete ultrametric Tate ring. If a finite family v : ι → N spans a complete normed module N over a complete ultrametric Tate ring R, then there exists C > 0 such that every y : N can be written as ∑ i, c i • v i with ‖c‖ ≤ C * ‖y‖ (and hence ‖c i‖ ≤ C * ‖y‖ for every i).