A⟨X, Y⟩ modulo 1 - XY

Let A be a nonarchimedean ring and write j₁, j₂ : A⟨Z⟩ → A⟨X, Y⟩ for the maps of restricted power series sending Z to X and to Y (TauCeti.Huber.weightedRename along Fin.castSuccEmb and Fin.succEmb 1). In the proof of Lemma 8.33 Wedhorn considers the row

0 → A → A⟨ζ⟩ × A⟨η⟩ → A⟨ζ, ζ⁻¹⟩ → 0,        λ(g, h) = g(ζ) - h(ζ⁻¹),

and in (8.2.1) writes the ring of the overlap as A⟨ζ, η⟩ ⧸ (f - ζ, 1 - ζη) = A⟨ζ, ζ⁻¹⟩ ⧸ (f - ζ). Read in A⟨ζ, ζ⁻¹⟩ = A⟨X, Y⟩ ⧸ (1 - XY), λ is induced by j₁ - j₂, and the two facts about the row that the proof uses become statements about A⟨X, Y⟩:

• A⟨ζ, ζ⁻¹⟩ = A⟨ζ⟩ + ζ⁻¹ A⟨ζ⁻¹⟩: every u ∈ A⟨X, Y⟩ is j₁ a + Y · j₂ b + (1 - XY) · w with a, b, w restricted, when A is complete and separated;
• im ι = ker λ: if j₁ a - j₂ b = (1 - XY) · w with w restricted, then a and b are the same constant, when A is separated.

In the second statement w ranges over A⟨X, Y⟩, not over all of A[[X, Y]], where 1 - XY is a unit.

The same decomposition, read on coefficients rather than in A⟨X, Y⟩, is TauCeti.Huber.twoSidedRestrictedSubmodule_eq_sup for two-sided restricted series.

Main results

• TauCeti.Huber.exists_eq_weightedRename_add_weightedX_mul_weightedRename_add_one_sub_mul: the decomposition, hence the surjectivity of λ.
• TauCeti.Huber.exists_eq_weightedC_of_weightedRename_sub_weightedRename_eq_one_sub_mul: the kernel of λ is the image of A.

References

• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), (8.2.1) and the proof of Lemma 8.33, p. 84.

Provenance

AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0) at commit 37bbdaeb9, projects/AdicSpaces/Adic spaces/LaurentCoverExact.lean, states both facts for its LaurentTateAlgebra A := TateAlgebra₂ A ⧸ (XY - 1): ker_lambdaMap_le_range_iotaHom (the kernel, with the diagonal-constancy argument used here) and lambdaMap_surjective (the decomposition by diagonal sums, in the variant j₁ a + j₂ b with b having zero constant term). The statements here are about A⟨X, Y⟩ itself rather than a quotient, over this repository's weightedRestrictedSubring, and the decomposition is stated in the variant j₁ a + X₁ · j₂ b + (1 - X₀X₁) w with no condition on the constant term of b.

Sums along a diagonal

Coefficients in two variables

The two statements for power series

The two statements in A⟨X, Y⟩

theorem TauCeti.Huber.exists_eq_weightedRename_add_weightedX_mul_weightedRename_add_one_sub_mul {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [NonarchimedeanRing A] [CompleteSpace A] [T0Space A] (u : ↥(weightedRestrictedSubring (fun (x : Fin 2) => {1}) ⋯)) : ∃ (a : ↥(weightedRestrictedSubring (fun (x : Fin 1) => {1}) ⋯)) (b : ↥(weightedRestrictedSubring (fun (x : Fin 1) => {1}) ⋯)) (w : ↥(weightedRestrictedSubring (fun (x : Fin 2) => {1}) ⋯)), u = (weightedRename Fin.castSuccEmb ⋯ ⋯ ⋯) a + weightedX (fun (x : Fin (1 + 1)) => {1}) ⋯ 1 * (weightedRename (Fin.succEmb 1) ⋯ ⋯ ⋯) b + (1 - weightedX (fun (x : Fin 2) => {1}) ⋯ 0 * weightedX (fun (x : Fin 2) => {1}) ⋯ 1) * w

Every element of A⟨X, Y⟩ is a(X) + Y · b(Y) modulo 1 - XY, with a, b ∈ A⟨Z⟩ and the multiple of 1 - XY restricted, when A is complete and separated. This is Wedhorn's A⟨ζ, ζ⁻¹⟩ = A⟨ζ⟩ + ζ⁻¹ A⟨ζ⁻¹⟩ in the proof of Lemma 8.33, the surjectivity of λ; its kernel is TauCeti.Huber.exists_eq_weightedC_of_weightedRename_sub_weightedRename_eq_one_sub_mul.

theorem TauCeti.Huber.exists_eq_weightedC_of_weightedRename_sub_weightedRename_eq_one_sub_mul {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] [T0Space A] {a b : ↥(weightedRestrictedSubring (fun (x : Fin 1) => {1}) ⋯)} {w : ↥(weightedRestrictedSubring (fun (x : Fin 2) => {1}) ⋯)} (h : (weightedRename Fin.castSuccEmb ⋯ ⋯ ⋯) a - (weightedRename (Fin.succEmb 1) ⋯ ⋯ ⋯) b = (1 - weightedX (fun (x : Fin 2) => {1}) ⋯ 0 * weightedX (fun (x : Fin 2) => {1}) ⋯ 1) * w) : ∃ (c : A), a = (weightedC (fun (x : Fin 1) => {1}) ⋯) c ∧ b = (weightedC (fun (x : Fin 1) => {1}) ⋯) c

A series in X and a series in Y that agree modulo 1 - XY in A⟨X, Y⟩ are the same constant: if a(X) - b(Y) = (1 - XY) · w with a, b ∈ A⟨Z⟩ and w ∈ A⟨X, Y⟩, then a = b = c for some c ∈ A, when A is separated. This is the inclusion ker λ ⊆ im ι in the proof of Wedhorn's Lemma 8.33; the other inclusion follows from TauCeti.Huber.weightedRename_weightedC.