Adic Spaces — Lean blueprint

7. Rational subsets🔗

Definition7.1
uses 1
Used by 5
Reverse dependency previews
Preview
Theorem 7.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

For f_1, \dots, f_n, s \in A generating an open ideal, the rational subset R\!\left(\tfrac{f_1, \dots, f_n}{s}\right) = \{\, v \in \mathrm{Spa}(A, A^{+}) : v(f_i) \le v(s) \ne 0 \,\} is the basic open of \mathrm{Spa} cut out by \texttt{rationalOpen} (Definition 6.1); \texttt{IsRationalSubset} is the predicate on sets that arise this way. Following Wedhorn Definition 7.29.

Lean code for Definition7.1●2 definitions
  • defdefined in «Adic spaces»/AdicSpectrum.lean
    complete
    def ValuationSpectrum.rationalOpen.{u_1} {A : Type u_1} [CommRing A]
  [TopologicalSpace A] [ValuationSpectrum.PlusSubring A] (T : Finset A)
  (s : A) : Set (Spv A)
    def ValuationSpectrum.rationalOpen.{u_1}
  {A : Type u_1} [CommRing A]
  [TopologicalSpace A]
  [ValuationSpectrum.PlusSubring A]
  (T : Finset A) (s : A) : Set (Spv A)
    A rational subset `R(T/s)` of `Spa(A, A⁺)` (Definition 7.29).
  • defdefined in «Adic spaces»/RationalSubsets.lean
    complete
    def ValuationSpectrum.IsRationalSubset.{u_1} {A : Type u_1} [CommRing A]
  [TopologicalSpace A] [ValuationSpectrum.PlusSubring A]
  (U : Set (Spv A)) : Prop
    def ValuationSpectrum.IsRationalSubset.{u_1}
  {A : Type u_1} [CommRing A]
  [TopologicalSpace A]
  [ValuationSpectrum.PlusSubring A]
  (U : Set (Spv A)) : Prop
    A rational subset is one of the form `rationalOpen T s` (Definition 7.29).
Theorem7.2
uses 1used by 0✓L∃∀N

The intersection of two rational subsets is again rational (Definition 7.1): rational subsets form a basis of the topology of \mathrm{Spa}(A, A^{+}) closed under finite intersection. Following Wedhorn Remark 7.30(5).

Lean code for Theorem7.2●2 theorems
  • theoremdefined in «Adic spaces»/RationalSubsets.lean
    complete
    theorem ValuationSpectrum.IsRationalSubset.inter.{u_1} {A : Type u_1}
  [CommRing A] [TopologicalSpace A] [ValuationSpectrum.PlusSubring A]
  {U V : Set (Spv A)} (hU : ValuationSpectrum.IsRationalSubset U)
  (hV : ValuationSpectrum.IsRationalSubset V) :
  ValuationSpectrum.IsRationalSubset (U ∩ V)
    theorem ValuationSpectrum.IsRationalSubset.inter.{u_1}
  {A : Type u_1} [CommRing A]
  [TopologicalSpace A]
  [ValuationSpectrum.PlusSubring A]
  {U V : Set (Spv A)}
  (hU :
    ValuationSpectrum.IsRationalSubset U)
  (hV :
    ValuationSpectrum.IsRationalSubset
      V) :
  ValuationSpectrum.IsRationalSubset
    (U ∩ V)
    The intersection of two rational subsets is rational (Theorem 7.35(2)).
  • theoremdefined in «Adic spaces»/RationalSubsets.lean
    complete
    theorem ValuationSpectrum.rationalOpen_inter.{u_1} {A : Type u_1} [CommRing A]
  [TopologicalSpace A] [ValuationSpectrum.PlusSubring A] [DecidableEq A]
  (T₁ T₂ : Finset A) (s₁ s₂ : A) (hs₁ : s₁ ∈ T₁) (hs₂ : s₂ ∈ T₂) :
  ValuationSpectrum.rationalOpen T₁ s₁ ∩
      ValuationSpectrum.rationalOpen T₂ s₂ =
    ValuationSpectrum.rationalOpen (T₁ * T₂) (s₁ * s₂)
    theorem ValuationSpectrum.rationalOpen_inter.{u_1}
  {A : Type u_1} [CommRing A]
  [TopologicalSpace A]
  [ValuationSpectrum.PlusSubring A]
  [DecidableEq A] (T₁ T₂ : Finset A)
  (s₁ s₂ : A) (hs₁ : s₁ ∈ T₁)
  (hs₂ : s₂ ∈ T₂) :
  ValuationSpectrum.rationalOpen T₁ s₁ ∩
      ValuationSpectrum.rationalOpen T₂
        s₂ =
    ValuationSpectrum.rationalOpen
      (T₁ * T₂) (s₁ * s₂)
    `R(T₁/s₁) ∩ R(T₂/s₂) = R(T₁·T₂ / s₁·s₂)` (Remark 7.30(5)).
Proof for Theorem 7.2
uses 0

Given R(f_i/s) and R(g_j/t), their intersection is R(f_i g_j / st): a point v lies in both iff v(f_i) \le v(s) and v(g_j) \le v(t) with v(s), v(t) \ne 0, which by multiplicativity of v is exactly v(f_i g_j) \le v(st) \ne 0. The numerator family of the product still generates an open ideal, so the intersection is again a rational subset. Following Wedhorn Remark 7.30(5).

Theorem7.3
uses 1used by 0✓L∃∀N

Every rational subset is open in \mathrm{Spa}(A, A^{+}) (Definition 7.1): it is a finite intersection of basic opens \{v(f_i) \le v(s) \ne 0\}. Following Wedhorn Theorem 7.35(2).

Lean code for Theorem7.3●2 theorems
  • theoremdefined in «Adic spaces»/RationalSubsets.lean
    complete
    theorem ValuationSpectrum.IsRationalSubset.isOpen.{u_1} {A : Type u_1}
  [CommRing A] [TopologicalSpace A] [ValuationSpectrum.PlusSubring A]
  {U : Set (Spv A)} (hU : ValuationSpectrum.IsRationalSubset U) :
  IsOpen (Subtype.val ⁻¹' U)
    theorem ValuationSpectrum.IsRationalSubset.isOpen.{u_1}
  {A : Type u_1} [CommRing A]
  [TopologicalSpace A]
  [ValuationSpectrum.PlusSubring A]
  {U : Set (Spv A)}
  (hU :
    ValuationSpectrum.IsRationalSubset
      U) :
  IsOpen (Subtype.val ⁻¹' U)
    A rational subset is open in `Spa(A, A⁺)`.
  • theoremdefined in «Adic spaces»/RationalSubsets.lean
    complete
    theorem ValuationSpectrum.rationalOpen_isOpen.{u_1} {A : Type u_1} [CommRing A]
  [TopologicalSpace A] [ValuationSpectrum.PlusSubring A] (T : Finset A)
  (s : A) : IsOpen (Subtype.val ⁻¹' ValuationSpectrum.rationalOpen T s)
    theorem ValuationSpectrum.rationalOpen_isOpen.{u_1}
  {A : Type u_1} [CommRing A]
  [TopologicalSpace A]
  [ValuationSpectrum.PlusSubring A]
  (T : Finset A) (s : A) :
  IsOpen
    (Subtype.val ⁻¹'
      ValuationSpectrum.rationalOpen T s)
    Rational subsets are open in `Spa(A, A⁺)` (Theorem 7.35(2)).
Proof for Theorem 7.3
uses 0

A rational subset R(T/s) is the finite intersection \bigcap_i \{v : v(f_i) \le v(s) \ne 0\} of the subbasic opens of \mathrm{Spa}. Each factor is open by definition of the topology on the valuation spectrum, and a finite intersection of opens is open. Following Wedhorn Theorem 7.35(2).