Documentation

TauCeti.AlgebraicGeometry.AdicSpace.Spa.Comap

Pullbacks and quotient embeddings of sub-unit valuation loci #

Wedhorn, Adic Spaces (arXiv:1910.05934v1), Definition 7.23, Remark 7.30, and Proposition 7.38.

This file constructs the contravariant continuous map on sub-unit valuation loci induced by a continuous ring homomorphism preserving the chosen subrings:

spaComap φ : spa Bplus → spa Aplus

No Huber-ring hypotheses are needed. The bundled version for morphisms of Huber pairs is in TauCeti.AlgebraicGeometry.AdicSpace.Spa.HuberPair.

Main definitions #

Main results #

References #

Provenance #

AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0), branch dev/adic-spaces at commit 37bbdaeb9ad9e3bc9f0d660feadc2779e455a91c, files AffinoidRings.lean and AdicSpectrum.lean, was consulted rather than copied for the induced map and quotient embedding. It bundles the plus ring into its affinoid ring and phrases those results at that level. Here the plus subrings are explicit, the generic results require no Huber hypotheses, and the bundled Huber-pair interface is provided separately. The rational-subset criteria are direct proofs; AINTLIB was not consulted for them.

source
theorem TauCeti.ValuationSpectrum.comap_mem_spa {A : Type u_1} {B : Type u_2} [CommRing A] [TopologicalSpace A] [CommRing B] [TopologicalSpace B] {φ : A →+* B} (hφ : Continuous ⇑φ) {Aplus : Subring A} {Bplus : Subring B} (hplus : ∀ a ∈ Aplus, φ a ∈ Bplus) {v : ValuationSpectrum B} (hv : v ∈ spa Bplus) :
comap φ v ∈ spa Aplus

A continuous ring homomorphism mapping A⁺ into B⁺ pulls points of spa (B, B⁺) back to points of spa (A, A⁺).

source
theorem TauCeti.ValuationSpectrum.mem_spa_map_iff {A : Type u_1} {B : Type u_2} [CommRing A] [TopologicalSpace A] [CommRing B] [TopologicalSpace B] {φ : A →+* B} (hφ : Continuous ⇑φ) (Aplus : Subring A) {w : ValuationSpectrum B} (hw : w.IsContinuous) :
w ∈ spa (Subring.map φ Aplus) ↔ comap φ w ∈ spa Aplus

A continuous point of Spv B lies in spa (φ(A⁺)) exactly when its pullback along a continuous ring homomorphism φ : A →+* B lies in spa A⁺.

source
def TauCeti.ValuationSpectrum.spaComap {A : Type u_1} {B : Type u_2} [CommRing A] [TopologicalSpace A] [CommRing B] [TopologicalSpace B] (φ : A →+* B) (hφ : Continuous ⇑φ) (Aplus : Subring A) (Bplus : Subring B) (hplus : ∀ a ∈ Aplus, φ a ∈ Bplus) (v : ↑(spa Bplus)) :
↑(spa Aplus)

The contravariant map on sub-unit valuation loci induced by a continuous ring homomorphism φ : A →+* B carrying Aplus into Bplus.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.ValuationSpectrum.spaComap_val {A : Type u_1} {B : Type u_2} [CommRing A] [TopologicalSpace A] [CommRing B] [TopologicalSpace B] (φ : A →+* B) (hφ : Continuous ⇑φ) (Aplus : Subring A) (Bplus : Subring B) (hplus : ∀ a ∈ Aplus, φ a ∈ Bplus) (v : ↑(spa Bplus)) :
    ↑(spaComap φ hφ Aplus Bplus hplus v) = comap φ ↑v
    source
    theorem TauCeti.ValuationSpectrum.continuous_spaComap {A : Type u_1} {B : Type u_2} [CommRing A] [TopologicalSpace A] [CommRing B] [TopologicalSpace B] (φ : A →+* B) (hφ : Continuous ⇑φ) (Aplus : Subring A) (Bplus : Subring B) (hplus : ∀ a ∈ Aplus, φ a ∈ Bplus) :
    Continuous (spaComap φ hφ Aplus Bplus hplus)

    spaComap is continuous for the subspace topologies.

    source
    @[simp]
    theorem TauCeti.ValuationSpectrum.spaComap_id {A : Type u_4} [CommRing A] [TopologicalSpace A] (Aplus : Subring A) :
    spaComap (RingHom.id A) ⋯ Aplus Aplus ⋯ = id

    spaComap of the identity homomorphism is the identity map on spa Aplus.

    source
    @[simp]
    theorem TauCeti.ValuationSpectrum.spaComap_comp {A : Type u_1} {B : Type u_2} {C : Type u_3} [CommRing A] [TopologicalSpace A] [CommRing B] [TopologicalSpace B] [CommRing C] [TopologicalSpace C] {φ : A →+* B} (hφ : Continuous ⇑φ) {ψ : B →+* C} (hψ : Continuous ⇑ψ) (Aplus : Subring A) (Bplus : Subring B) (Cplus : Subring C) (hφ_plus : ∀ a ∈ Aplus, φ a ∈ Bplus) (hψ_plus : ∀ b ∈ Bplus, ψ b ∈ Cplus) :
    spaComap (ψ.comp φ) ⋯ Aplus Cplus ⋯ = spaComap φ hφ Aplus Bplus hφ_plus ∘ spaComap ψ hψ Bplus Cplus hψ_plus

    spaComap is contravariantly functorial: spaComap (ψ ∘ φ) = spaComap φ ∘ spaComap ψ.

    source
    theorem TauCeti.ValuationSpectrum.comap_preimage_rationalSubset_inter_spa {A : Type u_1} {B : Type u_2} [CommRing A] [TopologicalSpace A] [CommRing B] [TopologicalSpace B] (φ : A →+* B) (hφ : Continuous ⇑φ) {Aplus : Subring A} {Bplus : Subring B} (hplus : ∀ a ∈ Aplus, φ a ∈ Bplus) (T : Finset A) (s : A) :
    comap φ ⁻¹' rationalSubset Aplus T s ∩ spa Bplus = rationalSubset Bplus (Finset.image (⇑φ) T) (φ s)

    Preimage of a rational subset under comap φ, after intersecting with spa Bplus: (comap φ) ⁻¹' R(T/s) ∩ spa Bplus = R(φ(T)/φ(s)).

    source
    theorem TauCeti.ValuationSpectrum.comap_mem_rationalSubset {A : Type u_1} {B : Type u_2} [CommRing A] [TopologicalSpace A] [CommRing B] [TopologicalSpace B] {φ : A →+* B} (hφ : Continuous ⇑φ) {Aplus : Subring A} {Bplus : Subring B} (hplus : ∀ a ∈ Aplus, φ a ∈ Bplus) (T : Finset A) (s : A) {c : B} (hc : φ s * c = 1) (hT : ∀ t ∈ T, φ t * c ∈ Bplus) {v : ValuationSpectrum B} (hv : v ∈ spa Bplus) :
    comap φ v ∈ rationalSubset Aplus T s

    A point of Spa (B, B⁺) pulls back into R(T/s) if φ inverts s and makes the fractions t/s sub-unit. No Huber hypothesis is needed, and T is arbitrary.

    source
    theorem TauCeti.ValuationSpectrum.rationalSubset_image_eq_spa {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [TopologicalSpace B] (φ : A →+* B) (Bplus : Subring B) (T : Finset A) (s : A) {c : B} (hc : φ s * c = 1) (hT : ∀ t ∈ T, φ t * c ∈ Bplus) :
    rationalSubset Bplus (Finset.image (⇑φ) T) (φ s) = spa Bplus

    If φ inverts s and makes every fraction φ(t) / φ(s) sub-unit, the rational subset presented by the images of T and s is the whole target adic spectrum.

    source
    theorem TauCeti.ValuationSpectrum.spaComap_preimage_rationalSubset {A : Type u_1} {B : Type u_2} [CommRing A] [TopologicalSpace A] [CommRing B] [TopologicalSpace B] (φ : A →+* B) (hφ : Continuous ⇑φ) (Aplus : Subring A) (Bplus : Subring B) (hplus : ∀ a ∈ Aplus, φ a ∈ Bplus) (T : Finset A) (s : A) :
    spaComap φ hφ Aplus Bplus hplus ⁻¹' Subtype.val ⁻¹' rationalSubset Aplus T s = Subtype.val ⁻¹' rationalSubset Bplus (Finset.image (⇑φ) T) (φ s)

    The preimage of R(T/s) under spaComap φ is R(φ(T)/φ(s)).

    source
    @[reducible, inline]
    noncomputable abbrev TauCeti.ValuationSpectrum.spaComapTopHom {A B : Type v} [CommRing A] [TopologicalSpace A] [CommRing B] [TopologicalSpace B] {Aplus : Subring A} {Bplus : Subring B} (φ : A →+* B) (hφ : Continuous ⇑φ) (hplus : ∀ a ∈ Aplus, φ a ∈ Bplus) :
    ↧↑(spa Bplus) ⟶ ↧↑(spa Aplus)

    The map of adic spectra Spa(B, B⁺) → Spa(A, A⁺) induced by φ, as a morphism of TopCat.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.ValuationSpectrum.map_spaComapTopHom_obj_spaBasicOpen {A B : Type v} [CommRing A] [TopologicalSpace A] [CommRing B] [TopologicalSpace B] {Aplus : Subring A} {Bplus : Subring B} (φ : A →+* B) (hφ : Continuous ⇑φ) (hplus : ∀ a ∈ Aplus, φ a ∈ Bplus) (T : Finset A) (s : A) :
      (TopologicalSpace.Opens.map (spaComapTopHom φ hφ hplus)).obj (spaBasicOpen Aplus T s) = spaBasicOpen Bplus (Finset.image (⇑φ) T) (φ s)

      The preimage of a basic open is a basic open: the preimage of R(T/s) under the induced map of adic spectra is R(φ(T)/φ(s)). This is spaComap_preimage_rationalSubset for Opens.

      source
      theorem TauCeti.ValuationSpectrum.isEmbedding_spaComap {A : Type u_1} {B : Type u_2} [CommRing A] [TopologicalSpace A] [CommRing B] [TopologicalSpace B] (φ : A →+* B) (hφ : Continuous ⇑φ) (Aplus : Subring A) (Bplus : Subring B) (hplus : ∀ a ∈ Aplus, φ a ∈ Bplus) (hemb : Topology.IsEmbedding (comap φ)) :
      Topology.IsEmbedding (spaComap φ hφ Aplus Bplus hplus)

      If pullback along φ embeds valuation spectra, then its restriction to compatible sub-unit loci is also an embedding.

      source
      @[simp]
      theorem TauCeti.ValuationSpectrum.isOpen_supp_comap_quotientMk_iff {A : Type u_1} [CommRing A] [TopologicalSpace A] (J : Ideal A) (v : ValuationSpectrum (A ⧸ J)) :
      IsOpen ↑(comap (Ideal.Quotient.mk J) v).supp ↔ IsOpen ↑v.supp

      Pullback along a quotient map preserves and reflects whether the support of a valuation is open.

      source
      theorem TauCeti.ValuationSpectrum.isEmbedding_spaComap_quotientMk {A : Type u_1} [CommRing A] [TopologicalSpace A] (J : Ideal A) (Aplus : Subring A) :
      Topology.IsEmbedding (spaComap (Ideal.Quotient.mk J) ⋯ Aplus (Subring.map (Ideal.Quotient.mk J) Aplus) ⋯)

      The map on sub-unit valuation loci for a quotient homomorphism and the image plus ring is a topological embedding.

      source
      theorem TauCeti.ValuationSpectrum.range_spaComap_quotientMk {A : Type u_1} [CommRing A] [TopologicalSpace A] (J : Ideal A) (Aplus : Subring A) :
      Set.range (spaComap (Ideal.Quotient.mk J) ⋯ Aplus (Subring.map (Ideal.Quotient.mk J) Aplus) ⋯) = Subtype.val ⁻¹' {v : ValuationSpectrum A | J ≤ v.supp}

      The range of the quotient map with the image plus ring is the points whose support contains J.

      source
      theorem TauCeti.ValuationSpectrum.isClosed_support_locus {A : Type u_1} [CommRing A] [TopologicalSpace A] (Aplus : Subring A) (J : Ideal A) :
      IsClosed (Subtype.val ⁻¹' {v : ValuationSpectrum A | J ≤ v.supp})

      The locus in a sub-unit valuation space where the support contains J is closed.

      source
      theorem TauCeti.ValuationSpectrum.isClosedEmbedding_spaComap_quotientMk {A : Type u_1} [CommRing A] [TopologicalSpace A] (J : Ideal A) (Aplus : Subring A) :
      Topology.IsClosedEmbedding (spaComap (Ideal.Quotient.mk J) ⋯ Aplus (Subring.map (Ideal.Quotient.mk J) Aplus) ⋯)

      The quotient homomorphism with the image plus ring induces a closed embedding of sub-unit valuation loci.