Documentation

TauCeti.AlgebraicGeometry.AdicSpace.Spa.HuberPair

Maps of adic spectra for Huber pairs #

This file bundles the generic pullback API from TauCeti.AlgebraicGeometry.AdicSpace.Spa.Comap for morphisms of Huber pairs and proves the quotient-pair form of Wedhorn, Adic Spaces, Proposition 7.38.

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. AINTLIB bundles its affinoid-ring data; this file instead delegates the topology and quotient-support arguments to the more general subring-level results and supplies only the Huber-pair interface.

source
def TauCeti.Huber.Pair.Hom.spaComap {A : Type u_1} {B : Type u_2} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsHuberRing B] {S : Pair A} {T : Pair B} (f : S.Hom T) :
↑(ValuationSpectrum.spa T.plus) → ↑(ValuationSpectrum.spa S.plus)

The contravariant continuous map on adic spectra induced by a morphism of Huber pairs: Spa(T) → Spa(S).

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.Huber.Pair.Hom.spaComap_val {A : Type u_1} {B : Type u_2} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsHuberRing B] {S : Pair A} {T : Pair B} (f : S.Hom T) (v : ↑(ValuationSpectrum.spa T.plus)) :
    ↑(f.spaComap v) = ValuationSpectrum.comap f.toRingHom ↑v

    The underlying valuation of f.spaComap v is the pullback of v along the underlying ring homomorphism of f.

    source
    theorem TauCeti.Huber.Pair.Hom.spaComap_def {A : Type u_1} {B : Type u_2} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsHuberRing B] {S : Pair A} {T : Pair B} (f : S.Hom T) :
    f.spaComap = ValuationSpectrum.spaComap f.toRingHom ⋯ S.plus T.plus ⋯

    f.spaComap is the subring-level pullback of the underlying ring homomorphism of f. This is the bridge to the unbundled API of TauCeti.AlgebraicGeometry.AdicSpace.Spa.Comap, whose definition is not exposed outside this module.

    source
    theorem TauCeti.Huber.Pair.Hom.continuous_spaComap {A : Type u_1} {B : Type u_2} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsHuberRing B] {S : Pair A} {T : Pair B} (f : S.Hom T) :
    Continuous f.spaComap

    f.spaComap is continuous.

    source
    @[simp]
    theorem TauCeti.Huber.Pair.Hom.spaComap_id {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] (S : Pair A) :
    (id S).spaComap = _root_.id

    spaComap for the identity morphism is the identity map on Spa(S).

    source
    @[simp]
    theorem TauCeti.Huber.Pair.Hom.spaComap_comp {A : Type u_1} {B : Type u_2} {C : Type u_3} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsHuberRing B] [CommRing C] [TopologicalSpace C] [IsTopologicalRing C] [IsHuberRing C] {S : Pair A} {T : Pair B} {U : Pair C} (g : T.Hom U) (f : S.Hom T) :
    (g.comp f).spaComap = f.spaComap ∘ g.spaComap

    spaComap is contravariantly functorial for composition of morphisms of Huber pairs: (g ∘ f).spaComap = f.spaComap ∘ g.spaComap.

    source
    theorem TauCeti.Huber.Pair.Hom.spaComap_preimage_rationalSubset {A : Type u_1} {B : Type u_2} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsHuberRing B] {S : Pair A} {T : Pair B} (f : S.Hom T) (T' : Finset A) (s : A) :
    f.spaComap ⁻¹' Subtype.val ⁻¹' ValuationSpectrum.rationalSubset S.plus T' s = Subtype.val ⁻¹' ValuationSpectrum.rationalSubset T.plus (Finset.image (⇑f.toRingHom) T') (f.toRingHom s)

    The preimage of a rational subset under the map induced by a morphism of Huber pairs is the rational subset obtained by mapping its defining functions.

    source
    theorem TauCeti.Huber.Pair.Hom.range_spaComap_quotientHom {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] (S : Pair A) (J : Ideal A) :
    Set.range (S.quotientHom J).spaComap = Subtype.val ⁻¹' {v : ValuationSpectrum A | J ≤ v.supp}

    The range of the quotient-pair map on adic spectra is the support locus containing J.

    source
    theorem TauCeti.Huber.Pair.Hom.isClosedEmbedding_spaComap_quotientHom {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] (S : Pair A) (J : Ideal A) :
    Topology.IsClosedEmbedding (S.quotientHom J).spaComap

    Wedhorn Proposition 7.38: the canonical quotient-pair morphism induces a closed embedding of adic spectra. Its image is identified by range_spaComap_quotientHom.