Documentation

TauCeti.AlgebraicGeometry.AdicSpace.Spa.RationalSubset.Laurent.Basic

Laurent covers of the adic spectrum #

The covering geometry of Wedhorn, Adic Spaces (arXiv:1910.05934v1), Lemma 8.34(ii) and (iii).

For a family f₁, …, f_r of elements of A, the Laurent cover of Spa (A, A⁺) generated by the family consists of the pieces

X(f₁^{ε₁}, …, f_r^{ε_r}) = {v | v(fᵢ) ≤ 1 if εᵢ = 1,  v(fᵢ) ≥ 1 if εᵢ = -1},

one for each choice of signs. Here the signs are recorded by the set J of indices with εᵢ = -1, and the piece is laurentPiece Aplus f J. The pieces are rational subsets (val_preimage_laurentPiece_mem_spaRationalFamily), and they cover Spa (A, A⁺), each point lying in the piece of its own signs (mem_laurentPiece_setOf_vle).

Wedhorn's Lemma 8.34 reduces Čech acyclicity of an arbitrary finite rational cover to Laurent covers, and the reduction rests on two refinement statements about the standard rational cover (R(T/t))_{t ∈ T} of a finite set T generating the unit ideal. This file proves both, at the level of subsets of Spa (A, A⁺).

What part (ii) calls units are units of the coordinate ring 𝒪_X(V). Here they appear only in pointwise form, as elements vanishing at no point of V; their invertibility in 𝒪_X(V) is not proved here. Nor is the algebraic half of Lemma 8.34, Čech acyclicity of Laurent covers and its transfer along refinements. The two-piece Laurent cover {|f| ≤ 1}, {|f| ≥ 1}, with its coordinate rings, is treated in TauCeti.AlgebraicGeometry.AdicSpace.Spa.Localization.LaurentCover.Basic.

Main definitions #

Main results #

References #

AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0), branch dev/adic-spaces at commit 37bbdaeb9ad9e3bc9f0d660feadc2779e455a91c, file projects/AdicSpaces/Adic spaces/WedhornCechAcyclicity.lean, states parts (ii) and (iii) for its bundled rational covering data, with the Laurent cover built as an iterated list of two-piece splits (laurentProdLeaves) and Corollary 7.32 for a finite family (cor_7_32_dominating_unit) carrying strong-noetherian and completeness hypotheses. Here the pieces are indexed by sign sets, and the dominating unit uses only the Tate property.

Laurent covers #

source
def TauCeti.ValuationSpectrum.laurentPiece {A : Type u_1} [CommRing A] [TopologicalSpace A] {ι : Type u_2} (Aplus : Subring A) (f : ι → A) (J : Set ι) :
Set (ValuationSpectrum A)

A piece of the Laurent cover generated by the family f: the points of Spa (A, A⁺) with v(fᵢ) ≥ 1 for i ∈ J and v(fᵢ) ≤ 1 for i ∉ J. This is Wedhorn's X(f₁^{ε₁}, …, f_r^{ε_r}) with J the set of indices of sign εᵢ = -1.

As with rationalSubset, nothing is assumed of A, A⁺ or the family; the pieces are rational subsets when the family is finite and A is a Huber ring (val_preimage_laurentPiece_mem_spaRationalFamily).

Equations
Instances For
    source
    theorem TauCeti.ValuationSpectrum.laurentPiece_def {A : Type u_1} [CommRing A] [TopologicalSpace A] {ι : Type u_2} (Aplus : Subring A) (f : ι → A) (J : Set ι) :
    laurentPiece Aplus f J = spa Aplus ∩ {v : ValuationSpectrum A | ∀ (i : ι), (i ∈ J → 1 ≤ᵥ f i) ∧ (i ∉ J → f i ≤ᵥ 1)}

    The set-level characterization of a Laurent piece.

    source
    @[simp]
    theorem TauCeti.ValuationSpectrum.mem_laurentPiece_iff {A : Type u_1} [CommRing A] [TopologicalSpace A] {ι : Type u_2} (Aplus : Subring A) (f : ι → A) (J : Set ι) (v : ValuationSpectrum A) :
    v ∈ laurentPiece Aplus f J ↔ v ∈ spa Aplus ∧ ∀ (i : ι), (i ∈ J → 1 ≤ᵥ f i) ∧ (i ∉ J → f i ≤ᵥ 1)

    Membership in a piece of a Laurent cover.

    source
    theorem TauCeti.ValuationSpectrum.laurentPiece_subset_spa {A : Type u_1} [CommRing A] [TopologicalSpace A] {ι : Type u_2} (Aplus : Subring A) (f : ι → A) (J : Set ι) :
    laurentPiece Aplus f J ⊆ spa Aplus

    Every piece of a Laurent cover is contained in the adic spectrum.

    source
    theorem TauCeti.ValuationSpectrum.mem_laurentPiece_setOf_vle {A : Type u_1} [CommRing A] [TopologicalSpace A] {ι : Type u_2} {Aplus : Subring A} {v : ValuationSpectrum A} (hv : v ∈ spa Aplus) (f : ι → A) :
    v ∈ laurentPiece Aplus f {i : ι | 1 ≤ᵥ f i}

    A point lies in the piece of its own signs: the one whose sign set consists of the indices i with v(fᵢ) ≥ 1.

    source
    theorem TauCeti.ValuationSpectrum.spa_eq_iUnion_laurentPiece {A : Type u_1} [CommRing A] [TopologicalSpace A] {ι : Type u_2} (Aplus : Subring A) (f : ι → A) :
    spa Aplus = ⋃ (J : Set ι), laurentPiece Aplus f J

    The pieces of a Laurent cover cover the adic spectrum.

    source
    theorem TauCeti.ValuationSpectrum.val_preimage_laurentPiece_eq_iInter {A : Type u_1} [CommRing A] [TopologicalSpace A] {ι : Type u_2} (Aplus : Subring A) (f : ι → A) (J : Set ι) :
    Subtype.val ⁻¹' laurentPiece Aplus f J = ⋂ (i : ι), Subtype.val ⁻¹' if i ∈ J then rationalSubset Aplus {1} (f i) else rationalSubset Aplus {f i, 1} 1

    A piece of a Laurent cover is an intersection of rational subsets: of R({1}/fᵢ) for i ∈ J and of R({fᵢ, 1}/1) for i ∉ J. The numerator 1 makes both numerator ideals the unit ideal, and costs nothing: v(1) ≤ v(1) always, and v(1) ≤ v(fᵢ) already forces v(fᵢ) ≠ 0.

    source
    theorem TauCeti.ValuationSpectrum.val_preimage_laurentPiece_mem_spaRationalFamily {A : Type u_1} [CommRing A] [TopologicalSpace A] {ι : Type u_2} [IsTopologicalRing A] [Huber.IsHuberRing A] [Finite ι] (Aplus : Subring A) (f : ι → A) (J : Set ι) :
    Subtype.val ⁻¹' laurentPiece Aplus f J ∈ spaRationalFamily Aplus

    The pieces of a Laurent cover generated by a finite family are rational subsets of the adic spectrum of a Huber ring.

    Part (ii): restricting a standard cover to a Laurent cover #

    source
    theorem TauCeti.ValuationSpectrum.not_vle_zero_of_mem_laurentPiece_inv_mul {A : Type u_1} [CommRing A] [TopologicalSpace A] {Aplus : Subring A} {T : Finset A} (ϖ : Aˣ) {J : Set ↥T} {t : ↥T} (ht : t ∈ J) {v : ValuationSpectrum A} (hv : v ∈ laurentPiece Aplus (fun (t : ↥T) => ↑ϖ⁻¹ * ↑t) J) :
    ¬↑t ≤ᵥ 0

    The generators of the ≥ side vanish nowhere on the piece (Wedhorn Lemma 8.34(ii)). On a piece V of the Laurent cover generated by the elements ϖ⁻¹ t, t ∈ T, every t of sign ≥ satisfies v(t) ≥ v(ϖ) ≠ 0. These are the elements that generate the restricted cover (R(T/t) ∩ V)_{t ∈ T} (mem_rationalSubset_iff_of_mem_laurentPiece_inv_mul), and this is the pointwise form of Wedhorn's assertion that they are units of 𝒪_X(V).

    source
    theorem TauCeti.ValuationSpectrum.rationalSubset_inter_laurentPiece_inv_mul_eq_empty {A : Type u_1} [CommRing A] [TopologicalSpace A] {Aplus : Subring A} {T : Finset A} {ϖ : Aˣ} (hϖ : ∀ v ∈ spa Aplus, ∃ t ∈ T, ↑ϖ <ᵥ t) {J : Set ↥T} {t : ↥T} (ht : t ∉ J) :
    rationalSubset Aplus T ↑t ∩ laurentPiece Aplus (fun (t : ↥T) => ↑ϖ⁻¹ * ↑t) J = ∅

    Off the ≥ side, the restricted piece is empty (Wedhorn Lemma 8.34(ii)). Let ϖ be a unit strictly dominated at every point of Spa (A, A⁺) by an element of T, as exists_unit_forall_mem_spa_exists_vlt provides. On a piece V of the Laurent cover generated by the ϖ⁻¹ t, if t has sign ≤ then R(T/t) does not meet V: at a point of R(T/t) the value of t is the largest on T, hence above v(ϖ), whereas on V it is at most v(ϖ).

    source
    theorem TauCeti.ValuationSpectrum.mem_rationalSubset_iff_of_mem_laurentPiece_inv_mul {A : Type u_1} [CommRing A] [TopologicalSpace A] {Aplus : Subring A} {T : Finset A} (ϖ : Aˣ) {J : Set ↥T} {t : ↥T} (ht : t ∈ J) {v : ValuationSpectrum A} (hv : v ∈ laurentPiece Aplus (fun (t : ↥T) => ↑ϖ⁻¹ * ↑t) J) :
    v ∈ rationalSubset Aplus T ↑t ↔ ∀ t' ∈ J, ↑t' ≤ᵥ ↑t

    On the ≥ side, the restricted piece is cut out by the ≥ generators (Wedhorn Lemma 8.34(ii)). On a piece V of the Laurent cover generated by the ϖ⁻¹ t, for t of sign ≥, a point of V lies in R(T/t) exactly when t dominates every element of T of sign ≥: the elements of sign ≤ are at most v(ϖ) ≤ v(t) on V anyway, and t vanishes nowhere on V by not_vle_zero_of_mem_laurentPiece_inv_mul. So the restriction of the standard cover (R(T/t))_{t ∈ T} to V is the standard cover of V generated by the elements of sign ≥.

    Part (iii): refining a standard cover generated by units #

    source
    theorem TauCeti.ValuationSpectrum.exists_rationalSubset_superset_laurentPiece_mul_inverse {A : Type u_1} [CommRing A] [TopologicalSpace A] (Aplus : Subring A) {T : Finset A} (hT : T.Nonempty) (hu : ∀ t ∈ T, IsUnit t) (J : Set (↥T × ↥T)) :
    ∃ t ∈ T, laurentPiece Aplus (fun (p : ↥T × ↥T) => ↑p.1 * Ring.inverse ↑p.2) J ⊆ rationalSubset Aplus T t

    The Laurent cover of ratios refines a standard cover generated by units (Wedhorn Lemma 8.34(iii)). Let T be a nonempty finite set of units of A. Every piece of the Laurent cover generated by the ratios t t'⁻¹, (t, t') ∈ T × T, lies in R(T/t) for some t ∈ T; since the pieces cover Spa (A, A⁺) (spa_eq_iUnion_laurentPiece), this Laurent cover refines the standard rational cover (R(T/t))_{t ∈ T}.

    The resulting refinement of the standard rational cover is the unit-generated case of part (iii).