The sieve of a finite Laurent cover

For a finite set T ⊆ A and an open W of Spa(A, A⁺), laurentSieve Aplus T W consists of the opens inside a piece of the Laurent cover of W generated by T. The membership, empty-cover, pullback, and insert lemmas describe this sieve independently of the sheaf condition. For unit generators, the Laurent sieve of all ratios refines the standard rational sieve (laurentSieve_mul_inverse_le_ofArrows_inf_spaBasicOpen).

References

• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Lemma 8.34(iii).
• S. Bosch, U. Güntzer, R. Remmert, Non-Archimedean Analysis, §8.2.2, Lemma 3.

The Laurent sieve

def TauCeti.ValuationSpectrum.laurentSieve {A : Type u_1} [CommRing A] [UniformSpace A] (Aplus : Subring A) (T : Finset A) (W : TopologicalSpace.Opens ↑(spa Aplus)) : CategoryTheory.Sieve W

The sieve of the Laurent cover of an open W ⊆ Spa(A, A⁺) generated by a finite set T: the opens V ≤ W on which every t ∈ T has a fixed sign, V ≤ {|t| ≤ 1} or V ≤ {|t| ≥ 1} (laurentCoverOpen Aplus t true and laurentCoverOpen Aplus t false). Equivalently, these are the opens V ≤ W contained in one of the pieces laurentPiece Aplus (↑) J, J ⊆ T, of the Laurent cover (laurentSieve_apply_iff_exists_laurentPiece).

Equations

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

@[simp]

theorem TauCeti.ValuationSpectrum.laurentSieve_apply {A : Type u_1} [CommRing A] [UniformSpace A] {Aplus : Subring A} {T : Finset A} {W V : TopologicalSpace.Opens ↑(spa Aplus)} (g : V ⟶ W) : (laurentSieve Aplus T W).arrows g ↔ ∀ t ∈ T, ∃ (b : Bool), V ≤ laurentCoverOpen Aplus t b

Membership in the Laurent sieve.

theorem TauCeti.ValuationSpectrum.laurentSieve_image_apply_iff_exists_laurentPiece {A : Type u_1} [CommRing A] [UniformSpace A] {Aplus : Subring A} [DecidableEq A] {ι : Type u_2} [Fintype ι] (f : ι → A) {W V : TopologicalSpace.Opens ↑(spa Aplus)} (g : V ⟶ W) : (laurentSieve Aplus (Finset.image f Finset.univ) W).arrows g ↔ ∃ (J : Set ι), ↑V ⊆ Subtype.val ⁻¹' laurentPiece Aplus f J

The Laurent sieve of a finite family consists of the opens inside a piece of its Laurent cover: for a family f : ι → A indexed by a finite type, an open V ≤ W lies in the Laurent sieve generated by the values of f exactly when it is contained in the piece laurentPiece Aplus f J for some set J ⊆ ι of indices of sign ≥ 1.

theorem TauCeti.ValuationSpectrum.laurentSieve_apply_iff_exists_laurentPiece {A : Type u_1} [CommRing A] [UniformSpace A] {Aplus : Subring A} {T : Finset A} {W V : TopologicalSpace.Opens ↑(spa Aplus)} (g : V ⟶ W) : (laurentSieve Aplus T W).arrows g ↔ ∃ (J : Set ↥T), ↑V ⊆ Subtype.val ⁻¹' laurentPiece Aplus Subtype.val J

The Laurent sieve consists of the opens inside a piece of the Laurent cover: an open V ≤ W lies in laurentSieve Aplus T W exactly when it is contained in the piece laurentPiece Aplus (↑) J for some set J ⊆ T of generators of sign ≥ 1.

@[simp]

theorem TauCeti.ValuationSpectrum.laurentSieve_empty {A : Type u_1} [CommRing A] [UniformSpace A] {Aplus : Subring A} (W : TopologicalSpace.Opens ↑(spa Aplus)) : laurentSieve Aplus ∅ W = ⊤

The Laurent cover generated by the empty set is the trivial cover.

@[simp]

theorem TauCeti.ValuationSpectrum.laurentSieve_pullback {A : Type u_1} [CommRing A] [UniformSpace A] {Aplus : Subring A} (T : Finset A) {W V : TopologicalSpace.Opens ↑(spa Aplus)} (g : V ⟶ W) : CategoryTheory.Sieve.pullback g (laurentSieve Aplus T W) = laurentSieve Aplus T V

The Laurent sieve of W restricts to the Laurent sieve of any V ≤ W.

theorem TauCeti.ValuationSpectrum.laurentSieve_insert_of_le {A : Type u_1} [CommRing A] [UniformSpace A] {Aplus : Subring A} [DecidableEq A] {T : Finset A} {a : A} {V : TopologicalSpace.Opens ↑(spa Aplus)} {b : Bool} (h : V ≤ laurentCoverOpen Aplus a b) : laurentSieve Aplus (insert a T) V = laurentSieve Aplus T V

On an open where a has a fixed sign, adding a to the generators does not change the Laurent sieve.

theorem TauCeti.ValuationSpectrum.laurentSieve_mul_inverse_le_ofArrows_inf_spaBasicOpen {A : Type u_1} [CommRing A] [UniformSpace A] [DecidableEq A] {Aplus : Subring A} {T : Finset A} (hT : T.Nonempty) (hu : ∀ t ∈ T, IsUnit t) (W : TopologicalSpace.Opens ↑(spa Aplus)) : laurentSieve Aplus (Finset.image (fun (p : ↥T × ↥T) => ↑p.1 * Ring.inverse ↑p.2) Finset.univ) W ≤ CategoryTheory.Sieve.ofArrows (fun (t : ↥T) => W ⊓ spaBasicOpen Aplus T ↑t) fun (x : ↥T) => CategoryTheory.homOfLE ⋯

The Laurent sieve generated by all ratios of a nonempty finite set of units refines the standard rational sieve on any open, as in Wedhorn's Lemma 8.34(iii).