Spv (A, I) is a spectral space

Wedhorn, Adic Spaces (arXiv:1910.05934v1), Lemma 7.5(1).

Wedhorn gives Spv (A, I) the subspace topology of Spv A (§7.1, after (7.1.1)) and proves it spectral with the sets

Spv (A, I)(T/s) = { v ∈ Spv (A, I) | v(t) ≤ v(s) ≠ 0 for all t ∈ T },   I ⊆ √(T · A)

as a generating family. (Wedhorn states them as a basis of quasi-compact opens, and that is what is proved: they generate the topology, which is what the patch criterion consumes; each is quasi-compact; and the family is stable under intersection — Wedhorn's step (i) — which upgrades generation to isTopologicalBasis_rationalFamily.) No second topology on the subtype is introduced here: the Subtype instance is that topology, which is the content of instTopologicalSpace_spvOfIdeal_eq_generateFrom.

The proof is Wedhorn's, via the patch criterion TauCeti.spectralSpace_of_isClopen_generateFrom (his Proposition 3.31). The compact witness topology it consumes is the one coinduced along the retraction r_I : Spv A → Spv (A, I) from the patch topology of Spv A. That choice is what makes the proof short: continuity of r_I holds by construction, and compactness is then the image of the compact (Spv A)_cons under a surjection. Wedhorn's step (iii) is still needed, but only as restrictToIdealCodRestrict_preimage, which turns clopen-ness of Spv(A)(T/s) in the patch of Spv A into clopen-ness of Spv(A,I)(T/s) in the witness topology.

Wedhorn's step (i) — stability of the family under intersection — is not needed for spectrality: the subspace topology is induced of a generateFrom, so induced_generateFrom_eq reduces the basis condition to single subbasic opens, and the patch criterion absorbs finite intersections itself. It is needed for the basis claim, and later for the spectral-map half of Lemma 7.5(2), so it is proved here all the same: basicOpenFinset_inter supplies the identity in Spv A, IsAdmissible.mul keeps the product pair admissible, and inter_mem_rationalFamily closes the family.

Note that Spv (A, I) is not pro-constructible in Spv A in general, so TauCeti.IsProConstructible.spectralSpace cannot be used: that would give a spectral inclusion (TauCeti.IsProConstructible.isSpectralMap_subtypeVal), which Wedhorn's Remark 7.6 denies.

Main definitions

• TauCeti.ValuationSpectrum.basicOpenFinset : Wedhorn's Spv(A)(T/s) for finite T.
• TauCeti.ValuationSpectrum.IsAdmissible : his condition I ⊆ √(T · A) on a numerator set.
• TauCeti.ValuationSpectrum.rationalFamily : Wedhorn's family R, which generates the topology of Spv (A, I). (Two things used in the proof are deliberately private: the compact witness topology coinduced along r_I, a device for the patch criterion rather than API, and the two branch lemmas of step (ii), whose statements are specific to the case split. exists_isAdmissible_basicOpenFinset below is the public neighbourhood interface that merges them.)

Main results

• TauCeti.ValuationSpectrum.spectralSpace_spvOfIdeal : Lemma 7.5(1).
• TauCeti.ValuationSpectrum.instTopologicalSpace_spvOfIdeal_eq_generateFrom : step (ii), that R generates the subspace topology.
• TauCeti.ValuationSpectrum.isTopologicalBasis_rationalFamily : step (i), that R is moreover a basis — it is closed under intersection, through IsAdmissible.mul and inter_mem_rationalFamily.
• TauCeti.ValuationSpectrum.restrictToIdealCodRestrict_preimage : step (iii), r_I⁻¹(Spv(A,I)(T/s)) = Spv(A)(T/s).
• TauCeti.ValuationSpectrum.isCompact_of_mem_rationalFamily : the members of R are quasi-compact, the other half of what Lemma 7.5(1) asserts about them.
• TauCeti.ValuationSpectrum.continuous_restrictToIdealCodRestrict : Lemma 7.5(2), the continuity half — steps (ii) and (iii) give it at once.
• TauCeti.ValuationSpectrum.isSpectralMap_restrictToIdealCodRestrict : Lemma 7.5(2), the spectral-map half, closing out Lemma 7.5: spectrality is tested on the basis R, whose preimages step (iii) computes and isCompact_basicOpenFinset bounds.
• TauCeti.ValuationSpectrum.isProConstructible_val_preimage_setOfPred_forall_vle_one : the sub-unit locus of a set of ring elements is pro-constructible in Spv (A, I) — the form Wedhorn's Theorem 7.35 consumes, proved from the rational family since the inclusion into Spv A is not spectral.

References

• T. Wedhorn, Adic Spaces, arXiv:1910.05934v1, Lemma 7.5 and Proposition 3.31.

Provenance

The corresponding development in AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0), project projects/AdicSpaces/, file Adic spaces/SpvAITopology.lean, was consulted rather than copied, and this file departs from it in two ways. Two revisions are cited below, each for what was checked against it: branch dev/adic-spaces at 37bbdaeb9ad9e3bc9f0d660feadc2779e455a91c, the revision the spectrality material here was written against, and 2baa76f742bdb4fb8ee323fabba41203bd390e08, the revision re-checked when Lemma 7.5(2) was added.

First, AINTLIB equips Spv (A, I) with a separate topology, SpvAI.topology, described there as strictly finer than the subspace topology. That reading of Remark 7.6 is not Wedhorn's: Remark 7.6 says the inclusion is not a spectral map, whereas Wedhorn's step (ii) proves R to be a basis of the subspace topology itself. AINTLIB proves only the trivial half, SpvAI.topology_le_induced; the converse is instTopologicalSpace_spvOfIdeal_eq_generateFrom here, and the two topologies therefore agree.

Second, AINTLIB's route to compactness and quasi-soberness goes through SpvAI.retraction_continuous. At 2baa76f742bdb4fb8ee323fabba41203bd390e08 that theorem carries a proof, but it rests on Spv.restrictIdeal_preimage_basicOpen_isOpen — openness of r_I⁻¹(Spv(A)(f/s)) for an arbitrary pair (f, s) — which is a sorry there, as is SpvAI.retraction_preimage_rationalSubset. Taking the witness topology coinduced along the retraction removes the need for continuity in the proof of 7.5(1), and quasi-soberness then comes from the patch criterion rather than from a transfer along the retraction. Continuity is proved below all the same, as Lemma 7.5(2) in its own right, and by a route that needs only the admissible preimages already computed for 7.5(1) — never the general-(f, s) statement.

The two branches of step (ii) below follow AINTLIB's SpvAI.exists_rationalSubset_microbial and SpvAI.exists_rationalSubset_cofinality, which are proved there; they are restated against characteristicSubgroup … = ⊤ and CofinalValue rather than IsMicrobial, and the cofinal branch takes one exponent per generator instead of a uniform one.

Admissible numerator sets

def TauCeti.ValuationSpectrum.IsAdmissible {A : Type u_1} [CommRing A] (I : Ideal A) (T : Finset A) (u : A) : Prop

Wedhorn's condition I ⊆ √(T · A) on a numerator set, in the form that also absorbs the denominator — harmless because Spv(A,I)(T/s) = Spv(A,I)((T ∪ {s})/s), and it is what step (iii) actually uses.

Equations

• TauCeti.ValuationSpectrum.IsAdmissible I T u = (I ≤ (Ideal.span (insert u ↑T)).radical)

@[simp]

theorem TauCeti.ValuationSpectrum.isAdmissible_iff {A : Type u_1} [CommRing A] {I : Ideal A} {T : Finset A} {u : A} : IsAdmissible I T u ↔ I ≤ (Ideal.span (insert u ↑T)).radical

Admissibility, unfolded: I lies in the radical of the span of the numerators together with the denominator.

theorem TauCeti.ValuationSpectrum.isAdmissible_of_one_mem {A : Type u_1} [CommRing A] {I : Ideal A} {T : Finset A} {u : A} (h : 1 ∈ T) : IsAdmissible I T u

A numerator set containing 1 is admissible for every ideal. The span is then already everything, so its radical is ⊤ and the containment defining admissibility is vacuous — for any I and any denominator u. This is what discharges admissibility in the Γ_v = cΓ_v branch of 7.5(ii), where Wedhorn's witness Spv(A,I)((g₁d, …, gₙd, 1)/g₀d) carries 1 among its numerators; the cofinal branch instead needs isAdmissible_of_forall_exists_pow_mem.

theorem TauCeti.ValuationSpectrum.isAdmissible_of_forall_exists_pow_mem {A : Type u_1} [CommRing A] {I : Ideal A} {S T : Finset A} {u : A} (hI : I ≤ (Ideal.span ↑S).radical) (h : ∀ σ ∈ S, ∃ (k : ℕ), σ ^ k ∈ T) : IsAdmissible I T u

If I sits inside the radical of a span whose every generator has a power in T, then T is admissible for I. Only that containment is needed — no auxiliary ideal, and no equality of spans or radicals.

theorem TauCeti.ValuationSpectrum.IsAdmissible.mul {A : Type u_1} [CommRing A] {I : Ideal A} {T₁ T₂ : Finset A} {u₁ u₂ : A} (h₁ : IsAdmissible I T₁ u₁) (h₂ : IsAdmissible I T₂ u₂) : IsAdmissible I (insert u₁ T₁ * insert u₂ T₂) (u₁ * u₂)

Admissibility is stable under the product of pairs. The numerator sets multiply pointwise, each augmented by its own denominator — the same shape basicOpenFinset_inter produces — and the product pair is admissible for the same I: the radical of the span of a product of sets is the meet of the radicals.

Wedhorn 7.5(ii): the rational subsets are a basis

theorem TauCeti.ValuationSpectrum.exists_isAdmissible_basicOpenFinset {A : Type u_1} [CommRing A] {I : Ideal A} (hfg : ∃ (J : Ideal A), J.FG ∧ I.radical = J.radical) {v : ValuationSpectrum A} (hvI : v ∈ spvOfIdeal I hfg) {f s : A} (hv : v ∈ basicOpen f s) : ∃ (T : Finset A) (u : A), IsAdmissible I T u ∧ v ∈ basicOpenFinset T u ∧ basicOpenFinset T u ⊆ basicOpen f s

Wedhorn 7.5(ii). Around a point of Spv (A, I), every basic open of Spv A contains an admissible Spv(A)(T/u) containing the point. The case split is Lemma 7.4(iii), taken at a finite generating set of the finitely generated ideal supplied by hfg.

The basis R and the topology it generates

def TauCeti.ValuationSpectrum.rationalFamily {A : Type u_1} [CommRing A] (I : Ideal A) (hfg : ∃ (J : Ideal A), J.FG ∧ I.radical = J.radical) : Set (Set ↑(spvOfIdeal I hfg))

Wedhorn's family R for Spv (A, I): the traces of the admissible Spv(A)(T/u). It generates the subspace topology — see instTopologicalSpace_spvOfIdeal_eq_generateFrom.

Equations

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

@[simp]

theorem TauCeti.ValuationSpectrum.mem_rationalFamily_iff {A : Type u_1} [CommRing A] {I : Ideal A} {hfg : ∃ (J : Ideal A), J.FG ∧ I.radical = J.radical} {U : Set ↑(spvOfIdeal I hfg)} : U ∈ rationalFamily I hfg ↔ ∃ (T : Finset A) (u : A), IsAdmissible I T u ∧ U = Subtype.val ⁻¹' basicOpenFinset T u

Membership in the generating family: a set belongs exactly when it is the trace of some admissible Spv(A)(T/u).

theorem TauCeti.ValuationSpectrum.instTopologicalSpace_spvOfIdeal_eq_generateFrom {A : Type u_1} [CommRing A] (I : Ideal A) (hfg : ∃ (J : Ideal A), J.FG ∧ I.radical = J.radical) : inferInstance = TopologicalSpace.generateFrom (rationalFamily I hfg)

Wedhorn 7.5(1), step (ii): the subspace topology of Spv (A, I) is generated by the admissible rational subsets. One direction is that each of them is the trace of an open of Spv A; the other is step (ii), applied to the subbasis of Spv A.

theorem TauCeti.ValuationSpectrum.univ_mem_rationalFamily {A : Type u_1} [CommRing A] (I : Ideal A) (hfg : ∃ (J : Ideal A), J.FG ∧ I.radical = J.radical) : Set.univ ∈ rationalFamily I hfg

The whole space is a member of R: it is the trace of Spv(A)({1}/1), whose defining conditions hold at every point and whose numerator set contains 1 and is therefore admissible for every ideal.

Deliberately not @[simp]: family membership already has a simp normal form through mem_rationalFamily_iff, which rewrites this left-hand side first, so the tag would be dead weight — and simpNF rejects it.

theorem TauCeti.ValuationSpectrum.inter_mem_rationalFamily {A : Type u_1} [CommRing A] {I : Ideal A} {hfg : ∃ (J : Ideal A), J.FG ∧ I.radical = J.radical} {U V : Set ↑(spvOfIdeal I hfg)} (hU : U ∈ rationalFamily I hfg) (hV : V ∈ rationalFamily I hfg) : U ∩ V ∈ rationalFamily I hfg

Wedhorn's step (i) in the proof of Lemma 7.5, on Spv (A, I): the family R is stable under intersection. The traces intersect along the trace of the intersection, which basicOpenFinset_inter computes as another rational subset, and IsAdmissible.mul keeps its pair admissible.

theorem TauCeti.ValuationSpectrum.isTopologicalBasis_rationalFamily {A : Type u_1} [CommRing A] (I : Ideal A) (hfg : ∃ (J : Ideal A), J.FG ∧ I.radical = J.radical) : TopologicalSpace.IsTopologicalBasis (rationalFamily I hfg)

The basis half of Wedhorn Lemma 7.5(1): the family R is a topological basis of Spv (A, I), not merely a generating family. Generation is instTopologicalSpace_spvOfIdeal_eq_generateFrom; this upgrades it with the two closure properties a basis needs, univ_mem_rationalFamily and inter_mem_rationalFamily. Together with isCompact_of_mem_rationalFamily below, this is Wedhorn's full claim: a basis of quasi-compact opens.

The compact witness topology

Wedhorn 7.5(iii)

theorem TauCeti.ValuationSpectrum.restrictToIdealCodRestrict_preimage {A : Type u_1} [CommRing A] (I : Ideal A) (hfg : ∃ (J : Ideal A), J.FG ∧ I.radical = J.radical) {T : Finset A} {u : A} (hadm : IsAdmissible I T u) : restrictToIdealCodRestrict I hfg ⁻¹' Subtype.val ⁻¹' basicOpenFinset T u = basicOpenFinset T u

Wedhorn 7.5(iii): r_I⁻¹(Spv(A,I)(T/u)) = Spv(A)(T/u) for admissible (T, u).

The inclusion ⊆ is Wedhorn's remark that a point of the preimage is a horizontal generization of its image, which here is the monotonicity restrictToIdeal_ne_zero_of_le. The inclusion ⊇ is his contradiction argument, restrictToIdeal_ne_zero_of_isAdmissible.

Wedhorn Lemma 7.5(1)

theorem TauCeti.ValuationSpectrum.spectralSpace_spvOfIdeal {A : Type u_1} [CommRing A] (I : Ideal A) (hfg : ∃ (J : Ideal A), J.FG ∧ I.radical = J.radical) : SpectralSpace ↑(spvOfIdeal I hfg)

Wedhorn, Lemma 7.5(1): Spv (A, I) is a spectral space.

The patch criterion is applied with the subspace topology as the generated one — the admissible rational subsets generate it by instTopologicalSpace_spvOfIdeal_eq_generateFrom — and with the coinduced patchTopologyOfIdeal as the compact witness, in which those subsets are clopen by step (iii). T0Space comes from Spv A through the subtype instance.

theorem TauCeti.ValuationSpectrum.isCompact_of_mem_rationalFamily {A : Type u_1} [CommRing A] (I : Ideal A) (hfg : ∃ (J : Ideal A), J.FG ∧ I.radical = J.radical) {V : Set ↑(spvOfIdeal I hfg)} (hV : V ∈ rationalFamily I hfg) : IsCompact V

Wedhorn Lemma 7.5(1), the quasi-compactness half. Every member of R is a quasi-compact open of Spv (A, I) — the property Wedhorn states alongside "basis", and the one that quasi-compactness in Spv A does not supply, since Spv (A, I) is not closed there.

Same witness topology as the spectrality proof, so the patch criterion's isCompact_of_isClopen_generateFrom applies directly.

Wedhorn Lemma 7.5(2)

theorem TauCeti.ValuationSpectrum.continuous_restrictToIdealCodRestrict {A : Type u_1} [CommRing A] (I : Ideal A) (hfg : ∃ (J : Ideal A), J.FG ∧ I.radical = J.radical) : Continuous (restrictToIdealCodRestrict I hfg)

Wedhorn Lemma 7.5(2), the continuity half: the retraction r_I : Spv A → Spv (A, I) is continuous.

The spectral-map half is isSpectralMap_restrictToIdealCodRestrict below.

theorem TauCeti.ValuationSpectrum.isSpectralMap_restrictToIdealCodRestrict {A : Type u_1} [CommRing A] (I : Ideal A) (hfg : ∃ (J : Ideal A), J.FG ∧ I.radical = J.radical) : IsSpectralMap (restrictToIdealCodRestrict I hfg)

Wedhorn Lemma 7.5(2), the spectral-map half: the retraction r_I : Spv A → Spv (A, I) is a spectral map. This closes out Lemma 7.5.

Spectrality is tested on the basis R (isSpectralMap_of_isTopologicalBasis with isTopologicalBasis_rationalFamily), where the preimage of a rational subset is computed by step (iii) and is quasi-compact in Spv A unconditionally.

The sub-unit locus is pro-constructible in Spv (A, I)

theorem TauCeti.ValuationSpectrum.isProConstructible_val_preimage_setOfPred_forall_vle_one {A : Type u_1} [CommRing A] (I : Ideal A) (hfg : ∃ (J : Ideal A), J.FG ∧ I.radical = J.radical) (S : Set A) : IsProConstructible (Subtype.val ⁻¹' {v : ValuationSpectrum A | ∀ a ∈ S, a ≤ᵥ 1})

The locus v ≤ 1 on a set of ring elements is pro-constructible in Spv (A, I). Its trace is the intersection over a ∈ S of the rational subsets Spv(A,I)({a,1}/1), each a quasi-compact open of the subspace by isCompact_of_mem_rationalFamily — carrying 1 among the numerators makes the pair admissible for any I (isAdmissible_of_one_mem).

This is the form Wedhorn's Theorem 7.35 consumes at S = A⁺. It does not follow from the corresponding Spv A statement by restriction — the inclusion Spv (A, I) → Spv A is not spectral — which is why it is proved here from the rational family instead.