Documentation

TauCeti.AlgebraicGeometry.AdicSpace.Spa.SeparationQuotient

The analytic locus and the separated quotient #

For a topological ring A, every continuous valuation kills the closure of zero. Consequently, pullback along

A → A / closure (0)

identifies the adic spectrum of the quotient (with the image plus ring) with the adic spectrum of A. This identification preserves analytic points: a support ideal in the quotient is open if and only if its inverse image in A is open.

This is the passage-to-the-separation-quotient part of Wedhorn Proposition 7.49(2). It also proves that if the separation quotient is discrete, then the analytic locus is empty.

Main results #

References #

source
@[simp]
theorem TauCeti.ValuationSpectrum.spaComap_preimage_spaAnalytic_quotientMk {A : Type u_1} [CommRing A] [TopologicalSpace A] (J : Ideal A) (Aplus : Subring A) :
spaComap (Ideal.Quotient.mk J) ⋯ Aplus (Subring.map (Ideal.Quotient.mk J) Aplus) ⋯ ⁻¹' Subtype.val ⁻¹' spaAnalytic Aplus = Subtype.val ⁻¹' spaAnalytic (Subring.map (Ideal.Quotient.mk J) Aplus)

Under pullback from an ideal quotient, the preimage of the analytic locus is the analytic locus of the quotient.

source
@[reducible, inline]
abbrev TauCeti.ValuationSpectrum.separationQuotientRing {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] :
Type u_1

The ring quotient by the closure of zero. It is homeomorphic to Mathlib's SeparationQuotient A.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev TauCeti.ValuationSpectrum.separationQuotientPlus {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (Aplus : Subring A) :
    Subring separationQuotientRing

    The image of a plus ring in the quotient by the closure of zero.

    Equations
    Instances For
      source
      noncomputable def TauCeti.ValuationSpectrum.spaSeparationQuotientHomeomorph {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (Aplus : Subring A) :
      ↑(spa (separationQuotientPlus Aplus)) ≃ₜ ↑(spa Aplus)

      Wedhorn Proposition 7.49(2), separated-quotient invariance. Pullback along the quotient by the closure of zero is a homeomorphism on adic spectra. The plus ring on the quotient is the image of Aplus.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.ValuationSpectrum.spaSeparationQuotientHomeomorph_apply {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (Aplus : Subring A) (v : ↑(spa (separationQuotientPlus Aplus))) :
        (spaSeparationQuotientHomeomorph Aplus) v = spaComap (Ideal.Quotient.mk ⊥.closure) ⋯ Aplus (separationQuotientPlus Aplus) ⋯ v

        The separated-quotient homeomorphism is pullback along the quotient map.

        source
        @[simp]
        theorem TauCeti.ValuationSpectrum.spaSeparationQuotientHomeomorph_symm_apply_val {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (Aplus : Subring A) (v : ↑(spa Aplus)) :
        ↑((spaSeparationQuotientHomeomorph Aplus).symm v) = quotientLift ⊥.closure ⋯

        The inverse separated-quotient homeomorphism is the canonical lift through the quotient.

        source
        @[simp]
        theorem TauCeti.ValuationSpectrum.spaSeparationQuotientHomeomorph_preimage_spaAnalytic {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (Aplus : Subring A) :
        ⇑(spaSeparationQuotientHomeomorph Aplus) ⁻¹' Subtype.val ⁻¹' spaAnalytic Aplus = Subtype.val ⁻¹' spaAnalytic (separationQuotientPlus Aplus)

        Wedhorn Proposition 7.49(2)(iii), locus form. The homeomorphism induced by passage to the separated quotient identifies the analytic loci.

        source
        theorem TauCeti.ValuationSpectrum.spaAnalytic_eq_empty_iff_separationQuotient {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (Aplus : Subring A) :
        spaAnalytic Aplus = ∅ ↔ spaAnalytic (separationQuotientPlus Aplus) = ∅

        Emptiness of the analytic locus is invariant under passage to the separated quotient.

        source
        theorem TauCeti.ValuationSpectrum.spaAnalytic_eq_empty_of_discrete_separationQuotient {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (Aplus : Subring A) (hdisc : DiscreteTopology (SeparationQuotient A)) :
        spaAnalytic Aplus = ∅

        The easy implication of Wedhorn Proposition 7.49(2): if the separated quotient of a topological ring is discrete, then its analytic locus is empty. No condition on the plus ring is needed for this implication.