Restricted series along a strict surjection

A bounded ring homomorphism φ : R → S of ultrametric normed rings, ‖φ r‖ ≤ C ‖r‖, maps restricted series to restricted series coefficientwise, giving a ring homomorphism R{X/c} → S{X/c}. If φ is moreover strictly surjective, that is, every s ∈ S lifts to some r with ‖r‖ ≤ C' ‖s‖, then lifting every coefficient shows that R{X/c} → S{X/c} is surjective. The norm control is what makes the lifted coefficients still tend to zero.

Combined with the identification R{X/c, Y/d} ≅ R{Y/d}{X/c} of TauCeti.MvPowerSeries.restrictedSumEquiv, this gives the form in which noetherianity passes to restricted series over a strict quotient of a ring of restricted series: if ψ : R{Y/d} → S is bounded and strictly surjective and R{X/c, Y/d} is noetherian, then S{X/c} is noetherian, being a quotient of R{Y/d}{X/c} ≅ R{X/c, Y/d}. This is how Kedlaya deduces the noetherianity of B^I{X/c} for the interval rings B^I of the Fargues–Fontaine curve from that of restricted series over the radius rings A^r (Kedlaya, Theorem 3.2), through presentations of B^I as strict quotients of A^r{Y} (Kedlaya, Lemma 4.9).

Main definitions

• TauCeti.MvPowerSeries.restrictedMap: the coefficientwise map R{X/c} →+* S{X/c} induced by a bounded ring homomorphism R →+* S.

Main results

• TauCeti.MvPowerSeries.restrictedMap_id and TauCeti.MvPowerSeries.restrictedMap_comp: restrictedMap is functorial.
• TauCeti.MvPowerSeries.restrictedMap_algebraMap: restrictedMap sends constants to constants.
• MvPowerSeries.restrictedMap_polynomialToRestricted: restrictedMap sends polynomials to their coefficientwise images.
• TauCeti.MvPowerSeries.restrictedMap_renameAlgEquiv: restrictedMap commutes with renaming the variables.
• TauCeti.MvPowerSeries.coe_restrictedSumEquiv_restrictedMap: restrictedMap commutes with the iteration R{X/c, Y/d} ≅ R{Y/d}{X/c}.
• TauCeti.MvPowerSeries.norm_restrictedMap_le: restrictedMap is bounded by the same constant.
• TauCeti.MvPowerSeries.norm_restrictedMap and TauCeti.MvPowerSeries.isometry_restrictedMap: a norm-preserving φ induces an isometry for the Gauss norms.
• TauCeti.MvPowerSeries.restrictedMap_eq_zero_iff: the coefficientwise kernel formula.
• TauCeti.MvPowerSeries.continuous_restrictedMap: continuity for the Gauss norm topologies.
• TauCeti.MvPowerSeries.exists_restrictedMap_eq_and_norm_coeff_le: coefficientwise bounded lifts.
• TauCeti.MvPowerSeries.restrictedMap_surjective: a strictly surjective φ induces a surjection R{X/c} → S{X/c}.
• TauCeti.MvPowerSeries.isNoetherianRing_isRestricted_subring_of_surjective: if R{X/c} is noetherian, so is S{X/c}.
• TauCeti.MvPowerSeries.isNoetherianRing_isRestricted_subring_of_surjective_of_sumElim: if ψ : R{Y/d} → S is bounded and strictly surjective and R{X/c, Y/d} is noetherian, then S{X/c} is noetherian.

References

• K. S. Kedlaya, Noetherian properties of Fargues–Fontaine curves, IMRN 2016, no. 8, 2544–2567; arXiv:1410.5160v3, Theorem 3.2, Lemma 4.9, Theorem 4.10 and Remark 4.11.

noncomputable def TauCeti.MvPowerSeries.restrictedMap {σ : Type u_1} {R : Type u_2} {S : Type u_3} [NormedRing R] [IsUltrametricDist R] [NormedRing S] [IsUltrametricDist S] {c : σ → ℝ} (φ : R →+* S) {C : ℝ} (hφ : ∀ (r : R), ‖φ r‖ ≤ C * ‖r‖) : ↥(MvPowerSeries.IsRestricted.subring c) →+* ↥(MvPowerSeries.IsRestricted.subring c)

The coefficientwise map R{X/c} →+* S{X/c} induced by a bounded ring homomorphism φ : R →+* S, ‖φ r‖ ≤ C ‖r‖.

theorem TauCeti.MvPowerSeries.coe_restrictedMap {σ : Type u_1} {R : Type u_2} {S : Type u_3} [NormedRing R] [IsUltrametricDist R] [NormedRing S] [IsUltrametricDist S] {c : σ → ℝ} (φ : R →+* S) {C : ℝ} (hφ : ∀ (r : R), ‖φ r‖ ≤ C * ‖r‖) (f : ↥(MvPowerSeries.IsRestricted.subring c)) : ↑((restrictedMap φ hφ) f) = (MvPowerSeries.map φ) ↑f

restrictedMap acts as MvPowerSeries.map on the underlying series.

@[simp]

theorem TauCeti.MvPowerSeries.coeff_restrictedMap {σ : Type u_1} {R : Type u_2} {S : Type u_3} [NormedRing R] [IsUltrametricDist R] [NormedRing S] [IsUltrametricDist S] {c : σ → ℝ} (φ : R →+* S) {C : ℝ} (hφ : ∀ (r : R), ‖φ r‖ ≤ C * ‖r‖) (f : ↥(MvPowerSeries.IsRestricted.subring c)) (t : σ →₀ ℕ) : (MvPowerSeries.coeff t) ↑((restrictedMap φ hφ) f) = φ ((MvPowerSeries.coeff t) ↑f)

restrictedMap acts on each coefficient by φ.

@[simp]

theorem TauCeti.MvPowerSeries.restrictedMap_eq_zero_iff {σ : Type u_1} {R : Type u_2} {S : Type u_3} [NormedRing R] [IsUltrametricDist R] [NormedRing S] [IsUltrametricDist S] {c : σ → ℝ} (φ : R →+* S) {C : ℝ} (hφ : ∀ (r : R), ‖φ r‖ ≤ C * ‖r‖) (f : ↥(MvPowerSeries.IsRestricted.subring c)) : (restrictedMap φ hφ) f = 0 ↔ ∀ (t : σ →₀ ℕ), φ ((MvPowerSeries.coeff t) ↑f) = 0

The kernel of a bounded coefficient map consists exactly of the series with every coefficient in the coefficient kernel.

@[simp]

theorem TauCeti.MvPowerSeries.restrictedMap_id {σ : Type u_1} {R : Type u_2} [NormedRing R] [IsUltrametricDist R] {c : σ → ℝ} {C : ℝ} (hC : ∀ (r : R), ‖(RingHom.id R) r‖ ≤ C * ‖r‖) : restrictedMap (RingHom.id R) hC = RingHom.id ↥(MvPowerSeries.IsRestricted.subring c)

The identity induces the identity on restricted series.

theorem TauCeti.MvPowerSeries.restrictedMap_comp {σ : Type u_1} {R : Type u_2} {S : Type u_3} [NormedRing R] [IsUltrametricDist R] [NormedRing S] [IsUltrametricDist S] {c : σ → ℝ} (φ : R →+* S) {C : ℝ} (hφ : ∀ (r : R), ‖φ r‖ ≤ C * ‖r‖) {T : Type u_4} [NormedRing T] [IsUltrametricDist T] (ψ : S →+* T) {C₂ C₃ : ℝ} (hψ : ∀ (s : S), ‖ψ s‖ ≤ C₂ * ‖s‖) (hψφ : ∀ (r : R), ‖(ψ.comp φ) r‖ ≤ C₃ * ‖r‖) : restrictedMap (ψ.comp φ) hψφ = (restrictedMap ψ hψ).comp (restrictedMap φ hφ)

The map induced by a composite is the composite of the induced maps.

@[simp]

theorem TauCeti.MvPowerSeries.restrictedMap_restrictedMap {σ : Type u_1} {R : Type u_2} {S : Type u_3} [NormedRing R] [IsUltrametricDist R] [NormedRing S] [IsUltrametricDist S] {c : σ → ℝ} (φ : R →+* S) {C : ℝ} (hφ : ∀ (r : R), ‖φ r‖ ≤ C * ‖r‖) {T : Type u_4} [NormedRing T] [IsUltrametricDist T] (ψ : S →+* T) {C₂ : ℝ} (hψ : ∀ (s : S), ‖ψ s‖ ≤ C₂ * ‖s‖) (f : ↥(MvPowerSeries.IsRestricted.subring c)) : (restrictedMap ψ hψ) ((restrictedMap φ hφ) f) = (restrictedMap (ψ.comp φ) ⋯) f

Applying two induced maps in turn is applying the map induced by the composite.

theorem TauCeti.MvPowerSeries.norm_restrictedMap_le {σ : Type u_1} {R : Type u_2} {S : Type u_3} [NormedRing R] [IsUltrametricDist R] [NormedRing S] [IsUltrametricDist S] {c : σ → ℝ} (φ : R →+* S) {C : ℝ} (hφ : ∀ (r : R), ‖φ r‖ ≤ C * ‖r‖) [∀ (i : σ), Fact (0 < c i)] (f : ↥(MvPowerSeries.IsRestricted.subring c)) : ‖(restrictedMap φ hφ) f‖ ≤ C * ‖f‖

restrictedMap does not increase the Gauss norm by more than the bound on φ.

@[simp]

theorem TauCeti.MvPowerSeries.norm_restrictedMap {σ : Type u_1} {R : Type u_2} {S : Type u_3} [NormedRing R] [IsUltrametricDist R] [NormedRing S] [IsUltrametricDist S] {c : σ → ℝ} (φ : R →+* S) {C : ℝ} (hφ : ∀ (r : R), ‖φ r‖ ≤ C * ‖r‖) [∀ (i : σ), Fact (0 < c i)] (hφ' : ∀ (r : R), ‖φ r‖ = ‖r‖) (f : ↥(MvPowerSeries.IsRestricted.subring c)) : ‖(restrictedMap φ hφ) f‖ = ‖f‖

A norm-preserving coefficient map preserves the Gauss norm.

theorem TauCeti.MvPowerSeries.isometry_restrictedMap {σ : Type u_1} {R : Type u_2} {S : Type u_3} [NormedRing R] [IsUltrametricDist R] [NormedRing S] [IsUltrametricDist S] {c : σ → ℝ} (φ : R →+* S) {C : ℝ} (hφ : ∀ (r : R), ‖φ r‖ ≤ C * ‖r‖) [∀ (i : σ), Fact (0 < c i)] (hφ' : ∀ (r : R), ‖φ r‖ = ‖r‖) : Isometry ⇑(restrictedMap φ hφ)

A norm-preserving coefficient map is an isometry for the Gauss norms.

theorem TauCeti.MvPowerSeries.lipschitzWith_restrictedMap {σ : Type u_1} {R : Type u_2} {S : Type u_3} [NormedRing R] [IsUltrametricDist R] [NormedRing S] [IsUltrametricDist S] {c : σ → ℝ} (φ : R →+* S) {C : ℝ} (hφ : ∀ (r : R), ‖φ r‖ ≤ C * ‖r‖) [∀ (i : σ), Fact (0 < c i)] : LipschitzWith C.toNNReal ⇑(restrictedMap φ hφ)

Bounded coefficient maps are Lipschitz for the Gauss norm.

theorem TauCeti.MvPowerSeries.continuous_restrictedMap {σ : Type u_1} {R : Type u_2} {S : Type u_3} [NormedRing R] [IsUltrametricDist R] [NormedRing S] [IsUltrametricDist S] {c : σ → ℝ} (φ : R →+* S) {C : ℝ} (hφ : ∀ (r : R), ‖φ r‖ ≤ C * ‖r‖) [∀ (i : σ), Fact (0 < c i)] : Continuous ⇑(restrictedMap φ hφ)

Bounded coefficient maps are continuous for the Gauss norm topologies.

theorem TauCeti.MvPowerSeries.exists_restrictedMap_eq_and_norm_coeff_le {σ : Type u_1} {R : Type u_2} {S : Type u_3} [NormedRing R] [IsUltrametricDist R] [NormedRing S] [IsUltrametricDist S] {c : σ → ℝ} (φ : R →+* S) {C : ℝ} (hφ : ∀ (r : R), ‖φ r‖ ≤ C * ‖r‖) {C' : ℝ} (hlift : ∀ (s : S), ∃ (r : R), φ r = s ∧ ‖r‖ ≤ C' * ‖s‖) (g : ↥(MvPowerSeries.IsRestricted.subring c)) : ∃ (f : ↥(MvPowerSeries.IsRestricted.subring c)), (restrictedMap φ hφ) f = g ∧ ∀ (t : σ →₀ ℕ), ‖(MvPowerSeries.coeff t) ↑f‖ ≤ C' * ‖(MvPowerSeries.coeff t) ↑g‖

A uniform bound for coefficient lifts gives a restricted lift with the same bound at each coefficient. This does not require positive radii or complete coefficient rings.

theorem TauCeti.MvPowerSeries.restrictedMap_surjective {σ : Type u_1} {R : Type u_2} {S : Type u_3} [NormedRing R] [IsUltrametricDist R] [NormedRing S] [IsUltrametricDist S] {c : σ → ℝ} (φ : R →+* S) {C : ℝ} (hφ : ∀ (r : R), ‖φ r‖ ≤ C * ‖r‖) {C' : ℝ} (hlift : ∀ (s : S), ∃ (r : R), φ r = s ∧ ‖r‖ ≤ C' * ‖s‖) : Function.Surjective ⇑(restrictedMap φ hφ)

Restricted series along a strict surjection. If every s ∈ S lifts along φ to some r with ‖r‖ ≤ C' ‖s‖, then every restricted series over S lifts coefficientwise to a restricted series over R, so R{X/c} → S{X/c} is surjective.

@[simp]

theorem TauCeti.MvPowerSeries.restrictedMap_algebraMap {σ : Type u_1} {R : Type u_2} {S : Type u_3} [NormedCommRing R] [IsUltrametricDist R] [NormedCommRing S] [IsUltrametricDist S] {c : σ → ℝ} (φ : R →+* S) {C : ℝ} (hφ : ∀ (r : R), ‖φ r‖ ≤ C * ‖r‖) (r : R) : (restrictedMap φ hφ) ((algebraMap R ↥(MvPowerSeries.IsRestricted.subring c)) r) = (algebraMap S ↥(MvPowerSeries.IsRestricted.subring c)) (φ r)

restrictedMap sends the constant r to the constant φ r.

@[simp]

theorem TauCeti.MvPowerSeries.restrictedMap_polynomialToRestricted {σ : Type u_1} {R : Type u_2} {S : Type u_3} [NormedCommRing R] [IsUltrametricDist R] [NormedCommRing S] [IsUltrametricDist S] {c : σ → ℝ} (φ : R →+* S) {C : ℝ} (hφ : ∀ (r : R), ‖φ r‖ ≤ C * ‖r‖) (p : MvPolynomial σ R) : (restrictedMap φ hφ) ((polynomialToRestricted c) p) = (polynomialToRestricted c) ((MvPolynomial.map φ) p)

restrictedMap sends a polynomial to its coefficientwise image under φ.

theorem TauCeti.MvPowerSeries.restrictedMap_renameAlgEquiv {σ : Type u_1} {R : Type u_2} {S : Type u_3} [NormedCommRing R] [IsUltrametricDist R] [NormedCommRing S] [IsUltrametricDist S] {c : σ → ℝ} (φ : R →+* S) {C : ℝ} (hφ : ∀ (r : R), ‖φ r‖ ≤ C * ‖r‖) {τ : Type u_4} (e : τ ≃ σ) (f : ↥(MvPowerSeries.IsRestricted.subring (c ∘ ⇑e))) : (restrictedMap φ hφ) ((MvPowerSeries.IsRestricted.renameAlgEquiv e c) f) = (MvPowerSeries.IsRestricted.renameAlgEquiv e c) ((restrictedMap φ hφ) f)

Bounded coefficient maps commute with renaming the variables along an equivalence.

theorem TauCeti.MvPowerSeries.coe_restrictedSumEquiv_restrictedMap {σ : Type u_1} {R : Type u_2} {S : Type u_3} [NormedCommRing R] [IsUltrametricDist R] [NormedCommRing S] [IsUltrametricDist S] {c : σ → ℝ} (φ : R →+* S) {C : ℝ} (hφ : ∀ (r : R), ‖φ r‖ ≤ C * ‖r‖) {τ : Type u_4} {d : τ → ℝ} [∀ (i : σ), Fact (0 < c i)] [∀ (j : τ), Fact (0 < d j)] (f : ↥(MvPowerSeries.IsRestricted.subring (Sum.elim c d))) : ↑(restrictedSumEquiv ((restrictedMap φ hφ) f)) = (MvPowerSeries.map (restrictedMap φ hφ)) ↑(restrictedSumEquiv f)

Iteration commutes with bounded coefficient maps: the iterated series of the coefficientwise image of f under φ : R →+* S is the image of the iterated series of f under the coefficientwise map R{Y/d} →+* S{Y/d} induced by φ.

theorem TauCeti.MvPowerSeries.isNoetherianRing_isRestricted_subring_of_surjective {σ : Type u_1} {R : Type u_3} {S : Type u_4} {c : σ → ℝ} [NormedRing R] [IsUltrametricDist R] [NormedRing S] [IsUltrametricDist S] (φ : R →+* S) {C C' : ℝ} (hφ : ∀ (r : R), ‖φ r‖ ≤ C * ‖r‖) (hlift : ∀ (s : S), ∃ (r : R), φ r = s ∧ ‖r‖ ≤ C' * ‖s‖) [IsNoetherianRing ↥(MvPowerSeries.IsRestricted.subring c)] : IsNoetherianRing ↥(MvPowerSeries.IsRestricted.subring c)

Noetherianity of restricted series passes along a strict surjection. If φ : R →+* S is bounded and every s ∈ S lifts to some r with ‖r‖ ≤ C' ‖s‖, then S{X/c} is noetherian whenever R{X/c} is.

theorem TauCeti.MvPowerSeries.isNoetherianRing_isRestricted_subring_of_surjective_of_sumElim {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {S : Type u_4} {c : σ → ℝ} [NormedCommRing R] [IsUltrametricDist R] [NormedRing S] [IsUltrametricDist S] [∀ (i : σ), Fact (0 < c i)] {d : τ → ℝ} [∀ (j : τ), Fact (0 < d j)] (ψ : ↥(MvPowerSeries.IsRestricted.subring d) →+* S) {C C' : ℝ} (hψ : ∀ (f : ↥(MvPowerSeries.IsRestricted.subring d)), ‖ψ f‖ ≤ C * ‖f‖) (hlift : ∀ (s : S), ∃ (f : ↥(MvPowerSeries.IsRestricted.subring d)), ψ f = s ∧ ‖f‖ ≤ C' * ‖s‖) [IsNoetherianRing ↥(MvPowerSeries.IsRestricted.subring (Sum.elim c d))] : IsNoetherianRing ↥(MvPowerSeries.IsRestricted.subring c)

Restricted series over a strict quotient of a ring of restricted series. Let ψ : R{Y/d} → S be a bounded ring homomorphism such that every s ∈ S lifts to some f with ‖f‖ ≤ C' ‖s‖. If the ring R{X/c, Y/d} of restricted series in both families of variables is noetherian, then so is S{X/c}: it is a quotient of R{Y/d}{X/c} ≅ R{X/c, Y/d}.