Documentation

TauCeti.RingTheory.Huber.LocalizationTopology.Pair

Completed rational localisation as a Huber pair #

Bundle the completed coordinate ring A⟨T/s⟩ and its ring of integral elements A_U⁺ into a Huber pair, together with the structure morphism from (A, A⁺). The plus ring is the closure of the image of the integral closure of A⁺[T/s] in A[1/s], as constructed in TauCeti.RingTheory.Huber.LocalizationTopology.Plus.

This construction applies to arbitrary Huber rings, including non-Tate rings. It lets statements about coordinate rings retain the plus-ring data used by the adic spectrum.

References #

source
noncomputable def TauCeti.Huber.PairOfDefinition.completedPlusPair {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) (Aplus : Subring A) (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → IsPowerBounded a) (hP : P.ringOfDefinition ≤ Aplus) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower (↑T) s S) :
Pair (UniformSpace.Completion S)

The completed rational localisation pair (A⟨T/s⟩, A_U⁺) built from a power-bounded subring A⁺ containing P.ringOfDefinition.

Instances For
    source
    @[simp]
    theorem TauCeti.Huber.PairOfDefinition.completedPlusPair_plus {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) (Aplus : Subring A) (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → IsPowerBounded a) (hP : P.ringOfDefinition ≤ Aplus) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower (↑T) s S) :
    (P.completedPlusPair Aplus hAplus hP T s S hden).plus = P.completedPlusSubring Aplus T s S hden

    The plus ring of completedPlusPair is completedPlusSubring.

    source
    theorem TauCeti.Huber.PairOfDefinition.completionLocalization_ringOfDefinition_le_completedPlusPair {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) (Aplus : Subring A) (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → IsPowerBounded a) (hP : P.ringOfDefinition ≤ Aplus) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower (↑T) s S) :
    (P.completionLocalization (↑T) s S hden).ringOfDefinition ≤ (P.completedPlusPair Aplus hAplus hP T s S hden).plus

    The ring of definition of completionLocalization is contained in the plus ring of completedPlusPair.

    source
    noncomputable def TauCeti.Huber.PairOfDefinition.rationalLocalizationPair {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] (P : PairOfDefinition A) (U : Pair A) (hP : P.ringOfDefinition ≤ U.plus) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower (↑T) s S) :
    Pair (UniformSpace.Completion S)

    The completed rational localisation pair (A⟨T/s⟩, A_U⁺), with plus ring the closure of the image of the integral closure of A⁺[T/s] in A[1/s].

    Instances For
      source
      @[simp]
      theorem TauCeti.Huber.PairOfDefinition.rationalLocalizationPair_plus {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] (P : PairOfDefinition A) (U : Pair A) (hP : P.ringOfDefinition ≤ U.plus) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower (↑T) s S) :
      (P.rationalLocalizationPair U hP T s S hden).plus = P.completedPlusSubring U.plus T s S hden

      The plus ring of the rational localisation pair is completedPlusSubring.

      source
      theorem TauCeti.Huber.PairOfDefinition.completionLocalization_ringOfDefinition_le_rationalLocalizationPair {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] (P : PairOfDefinition A) (U : Pair A) (hP : P.ringOfDefinition ≤ U.plus) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower (↑T) s S) :
      (P.completionLocalization (↑T) s S hden).ringOfDefinition ≤ (P.rationalLocalizationPair U hP T s S hden).plus

      The ring of definition of completionLocalization is contained in the plus ring of rationalLocalizationPair.

      source
      noncomputable def TauCeti.Huber.PairOfDefinition.toCompletionLocHom {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] (P : PairOfDefinition A) (U : Pair A) (hP : P.ringOfDefinition ≤ U.plus) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower (↑T) s S) :
      U.Hom (P.rationalLocalizationPair U hP T s S hden)

      The structure map to a completed rational localisation as a morphism of Huber pairs.

      Instances For
        source
        @[simp]
        theorem TauCeti.Huber.PairOfDefinition.toRingHom_toCompletionLocHom {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] (P : PairOfDefinition A) (U : Pair A) (hP : P.ringOfDefinition ≤ U.plus) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower (↑T) s S) :
        (P.toCompletionLocHom U hP T s S hden).toRingHom = P.toCompletionLoc (↑T) s S hden

        The pair structure map has toCompletionLoc as its underlying ring homomorphism.