The two-piece Laurent cover

Let A be a complete separated nonarchimedean ring and let f : A. The two Laurent pieces and their overlap have the presentations

A⟨X⟩/(f-X),   A⟨Y⟩/(1-fY),   A⟨X,Y⟩/(1-XY, f-X).

This file descends the exact Laurent row from TauCeti.RingTheory.Huber.WeightedRestrictedSeries.Laurent.Basic to these presentations. The difference of the two restriction maps is surjective, and its kernel consists exactly of pairs of equal constants. This is the algebraic exactness assertion for the two-piece Laurent cover in Wedhorn's Lemma 8.33.

The proof uses the decomposition of every restricted Laurent series as a series in X plus Y times a series in Y. Multiplying that decomposition by f-X expresses an arbitrary element of the overlap relation ideal as the image of the two piece relation ideals.

References

• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Lemma 8.33, p. 84.

Provenance

AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0) at commit 37bbdaeb9, projects/AdicSpaces/Adic spaces/LaurentCoverExact.lean, treats the same cover. Its complete exactness theorem is for the discrete case; its general section stops before constructing the difference map. The quotient descent below instead uses Tau Ceti's exact Laurent row and its restricted-series decomposition.

noncomputable def TauCeti.Huber.laurentCoverLeIdeal (A : Type u_1) [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] (f : A) : Ideal ↥(weightedRestrictedSubring (fun (x : Fin 1) => {1}) ⋯)

The relation ideal (f-X) defining the Laurent piece {|f| ≤ 1}.

Equations

• TauCeti.Huber.laurentCoverLeIdeal A f = Ideal.span {(TauCeti.Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) f - TauCeti.Huber.weightedX (fun (x : Fin 1) => {1}) ⋯ 0}

theorem TauCeti.Huber.laurentCoverLeIdeal_def (A : Type u_1) [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] (f : A) : laurentCoverLeIdeal A f = Ideal.span {(weightedC (fun (x : Fin 1) => {1}) ⋯) f - weightedX (fun (x : Fin 1) => {1}) ⋯ 0}

The defining presentation of laurentCoverLeIdeal.

theorem TauCeti.Huber.mem_laurentCoverLeIdeal_iff (A : Type u_1) [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] (f : A) {a : ↥(weightedRestrictedSubring (fun (x : Fin 1) => {1}) ⋯)} : a ∈ laurentCoverLeIdeal A f ↔ ∃ (b : ↥(weightedRestrictedSubring (fun (x : Fin 1) => {1}) ⋯)), b * ((weightedC (fun (x : Fin 1) => {1}) ⋯) f - weightedX (fun (x : Fin 1) => {1}) ⋯ 0) = a

Membership in the principal relation ideal defining the piece {|f| ≤ 1}.

noncomputable def TauCeti.Huber.laurentCoverGeIdeal (A : Type u_1) [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] (f : A) : Ideal ↥(weightedRestrictedSubring (fun (x : Fin 1) => {1}) ⋯)

The relation ideal (1-fY) defining the Laurent piece {|f| ≥ 1}.

Equations

• TauCeti.Huber.laurentCoverGeIdeal A f = Ideal.span {1 - (TauCeti.Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) f * TauCeti.Huber.weightedX (fun (x : Fin 1) => {1}) ⋯ 0}

theorem TauCeti.Huber.laurentCoverGeIdeal_def (A : Type u_1) [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] (f : A) : laurentCoverGeIdeal A f = Ideal.span {1 - (weightedC (fun (x : Fin 1) => {1}) ⋯) f * weightedX (fun (x : Fin 1) => {1}) ⋯ 0}

The defining presentation of laurentCoverGeIdeal.

theorem TauCeti.Huber.mem_laurentCoverGeIdeal_iff (A : Type u_1) [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] (f : A) {a : ↥(weightedRestrictedSubring (fun (x : Fin 1) => {1}) ⋯)} : a ∈ laurentCoverGeIdeal A f ↔ ∃ (b : ↥(weightedRestrictedSubring (fun (x : Fin 1) => {1}) ⋯)), b * (1 - (weightedC (fun (x : Fin 1) => {1}) ⋯) f * weightedX (fun (x : Fin 1) => {1}) ⋯ 0) = a

Membership in the principal relation ideal defining the piece {|f| ≥ 1}.

noncomputable def TauCeti.Huber.laurentCoverOverlapIdeal (A : Type u_1) [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] (f : A) : Ideal (↥(weightedRestrictedSubring (fun (x : Fin 2) => {1}) ⋯) ⧸ laurentIdeal A)

The relation ideal (f-X) in A⟨X, X⁻¹⟩; quotienting by it defines the overlap of the two Laurent pieces.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.Huber.laurentCoverOverlapIdeal_def (A : Type u_1) [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] (f : A) : laurentCoverOverlapIdeal A f = Ideal.span {(algebraMap A (↥(weightedRestrictedSubring (fun (x : Fin 2) => {1}) ⋯) ⧸ laurentIdeal A)) f - (Ideal.Quotient.mk (laurentIdeal A)) (weightedX (fun (x : Fin 2) => {1}) ⋯ 0)}

The defining presentation of laurentCoverOverlapIdeal.

theorem TauCeti.Huber.mem_laurentCoverOverlapIdeal_iff (A : Type u_1) [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] (f : A) {a : ↥(weightedRestrictedSubring (fun (x : Fin 2) => {1}) ⋯) ⧸ laurentIdeal A} : a ∈ laurentCoverOverlapIdeal A f ↔ ∃ (b : ↥(weightedRestrictedSubring (fun (x : Fin 2) => {1}) ⋯) ⧸ laurentIdeal A), b * ((algebraMap A (↥(weightedRestrictedSubring (fun (x : Fin 2) => {1}) ⋯) ⧸ laurentIdeal A)) f - (Ideal.Quotient.mk (laurentIdeal A)) (weightedX (fun (x : Fin 2) => {1}) ⋯ 0)) = a

Membership in the principal relation ideal defining the overlap.

@[reducible, inline]

noncomputable abbrev TauCeti.Huber.laurentCoverLe (A : Type u_1) [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] (f : A) : Type u_1

The coordinate ring of the Laurent piece {|f| ≤ 1}.

Equations

• TauCeti.Huber.laurentCoverLe A f = (↥(TauCeti.Huber.weightedRestrictedSubring (fun (x : Fin 1) => {1}) ⋯) ⧸ TauCeti.Huber.laurentCoverLeIdeal A f)

@[reducible, inline]

noncomputable abbrev TauCeti.Huber.laurentCoverGe (A : Type u_1) [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] (f : A) : Type u_1

The coordinate ring of the Laurent piece {|f| ≥ 1}.

Equations

• TauCeti.Huber.laurentCoverGe A f = (↥(TauCeti.Huber.weightedRestrictedSubring (fun (x : Fin 1) => {1}) ⋯) ⧸ TauCeti.Huber.laurentCoverGeIdeal A f)

@[reducible, inline]

noncomputable abbrev TauCeti.Huber.laurentCoverOverlap (A : Type u_1) [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] (f : A) : Type u_1

The coordinate ring of the overlap {|f| = 1} of the two Laurent pieces.

Equations

• TauCeti.Huber.laurentCoverOverlap A f = ((↥(TauCeti.Huber.weightedRestrictedSubring (fun (x : Fin 2) => {1}) ⋯) ⧸ TauCeti.Huber.laurentIdeal A) ⧸ TauCeti.Huber.laurentCoverOverlapIdeal A f)

@[simp]

theorem TauCeti.Huber.mk_weightedC_eq_mk_weightedX_in_laurentCoverOverlap (A : Type u_1) [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] (f : A) : (Ideal.Quotient.mk (laurentCoverOverlapIdeal A f)) ((Ideal.Quotient.mk (laurentIdeal A)) ((weightedC (fun (x : Fin 2) => {1}) ⋯) f)) = (Ideal.Quotient.mk (laurentCoverOverlapIdeal A f)) ((Ideal.Quotient.mk (laurentIdeal A)) (weightedX (fun (x : Fin 2) => {1}) ⋯ 0))

In the overlap ring the class of X is the image of f.

noncomputable def TauCeti.Huber.laurentCoverLeToOverlap (A : Type u_1) [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] (f : A) : laurentCoverLe A f →ₐ[A] laurentCoverOverlap A f

The restriction from the piece {|f| ≤ 1} to the overlap.

Equations

• TauCeti.Huber.laurentCoverLeToOverlap A f = Ideal.Quotient.liftₐ (TauCeti.Huber.laurentCoverLeIdeal A f) (TauCeti.Huber.laurentCoverLeMap✝ A f) ⋯

noncomputable def TauCeti.Huber.laurentCoverGeToOverlap (A : Type u_1) [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] (f : A) : laurentCoverGe A f →ₐ[A] laurentCoverOverlap A f

The restriction from the piece {|f| ≥ 1} to the overlap.

Equations

• TauCeti.Huber.laurentCoverGeToOverlap A f = Ideal.Quotient.liftₐ (TauCeti.Huber.laurentCoverGeIdeal A f) (TauCeti.Huber.laurentCoverGeMap✝ A f) ⋯

@[simp]

theorem TauCeti.Huber.laurentCoverLeToOverlap_mk (A : Type u_1) [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] (f : A) (a : ↥(weightedRestrictedSubring (fun (x : Fin 1) => {1}) ⋯)) : (laurentCoverLeToOverlap A f) ((Ideal.Quotient.mk (laurentCoverLeIdeal A f)) a) = (Ideal.Quotient.mk (laurentCoverOverlapIdeal A f)) ((Ideal.Quotient.mk (laurentIdeal A)) ((weightedRename Fin.castSuccEmb ⋯ ⋯ ⋯) a))

The restriction from {|f| ≤ 1} sends a representative to the same series in the overlap.

@[simp]

theorem TauCeti.Huber.laurentCoverGeToOverlap_mk (A : Type u_1) [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] (f : A) (a : ↥(weightedRestrictedSubring (fun (x : Fin 1) => {1}) ⋯)) : (laurentCoverGeToOverlap A f) ((Ideal.Quotient.mk (laurentCoverGeIdeal A f)) a) = (Ideal.Quotient.mk (laurentCoverOverlapIdeal A f)) ((Ideal.Quotient.mk (laurentIdeal A)) ((weightedRename (Fin.succEmb 1) ⋯ ⋯ ⋯) a))

The restriction from {|f| ≥ 1} sends a representative to the same series in the overlap.

noncomputable def TauCeti.Huber.laurentCoverDiff (A : Type u_1) [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] (f : A) : laurentCoverLe A f × laurentCoverGe A f →ₗ[A] laurentCoverOverlap A f

The Čech differential for the two-piece Laurent cover: the difference of the two restrictions to the overlap.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.Huber.laurentCoverDiff_apply (A : Type u_1) [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] (f : A) (x : laurentCoverLe A f) (y : laurentCoverGe A f) : (laurentCoverDiff A f) (x, y) = (laurentCoverLeToOverlap A f) x - (laurentCoverGeToOverlap A f) y

The Čech differential sends a pair of sections to the difference of their restrictions.

theorem TauCeti.Huber.laurentCoverDiff_mk (A : Type u_1) [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] (f : A) (a b : ↥(weightedRestrictedSubring (fun (x : Fin 1) => {1}) ⋯)) : (laurentCoverDiff A f) ((Ideal.Quotient.mk (laurentCoverLeIdeal A f)) a, (Ideal.Quotient.mk (laurentCoverGeIdeal A f)) b) = (Ideal.Quotient.mk (laurentCoverOverlapIdeal A f)) ((laurentDiff A) (a, b))

On quotient representatives, the Čech differential is represented by laurentDiff A (a, b) in the overlap quotient.

theorem TauCeti.Huber.laurentCoverDiff_surjective (A : Type u_1) [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [NonarchimedeanRing A] [CompleteSpace A] [T0Space A] (f : A) : Function.Surjective ⇑(laurentCoverDiff A f)

The Čech differential of the two-piece Laurent cover is surjective.

theorem TauCeti.Huber.exact_algebraMap_laurentCoverDiff (A : Type u_1) [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [NonarchimedeanRing A] [CompleteSpace A] [T0Space A] (f : A) : Function.Exact ⇑(algebraMap A (laurentCoverLe A f × laurentCoverGe A f)) ⇑(laurentCoverDiff A f)

Wedhorn's Lemma 8.33, exactness in the middle. For the two Laurent pieces {|f| ≤ 1} and {|f| ≥ 1}, a pair of sections has equal restrictions to the overlap exactly when it is a pair of equal constants.