Huber pairs

A ring of integral elements of a Huber ring A is an open subring A⁺ which is integrally closed in A and consists of power-bounded elements, and a Huber pair (A, A⁺) is a Huber ring together with such a subring. Huber pairs are the affine objects of the theory: the adic spectrum of the next layer is built from one.

A Huber ring has many rings of integral elements, so A⁺ is carried as data rather than selected by a typeclass; this is the roadmap's standing convention that the plus ring is explicit.

Main definitions

• TauCeti.Huber.IsRingOfIntegralElements: A⁺ is open, integrally closed in A in the sense of Mathlib's IsIntegrallyClosedIn, and contained in A°.
• TauCeti.Huber.Pair: a Huber pair, that is, a choice of A⁺.
• TauCeti.Huber.Pair.Hom: a continuous ring homomorphism carrying A⁺ into B⁺.

Main results

• TauCeti.Huber.IsRingOfIntegralElements.mem_of_isTopologicallyNilpotent: A°° ⊆ A⁺ for every ring of integral elements.
• TauCeti.Huber.IsRingOfIntegralElements.map: an isomorphism of topological rings carries a ring of integral elements onto a ring of integral elements.
• TauCeti.Huber.Pair.powerBounded: A⁺ = A° is a ring of integral elements, the largest one.
• TauCeti.Huber.Pair.discrete: a discrete ring is a Huber pair with A⁺ = A, so the definitions above are not vacuous.
• TauCeti.Huber.Pair.Hom.id, TauCeti.Huber.Pair.Hom.comp: morphisms of Huber pairs compose, associatively and unitally (TauCeti.Huber.Pair.Hom.comp_assoc, TauCeti.Huber.Pair.Hom.id_comp, TauCeti.Huber.Pair.Hom.comp_id).
• TauCeti.Huber.Pair.isRingOfIntegralElements_integralClosure: the integral closure of an open subring contained in the power-bounded subring is a ring of integral elements.
• TauCeti.Huber.Pair.quotient: the quotient Huber pair, whose plus ring is the integral closure of the image of the original plus ring.
• TauCeti.Huber.Pair.Hom.quotientLift: the universal factorisation of a morphism annihilating the quotient ideal.

Provenance

The shape of these declarations follows the roadmap's own prototype in TauCetiRoadmap/AdicSpaces/Suggested.lean, which fixes the design choice that the plus ring is explicit data rather than a typeclass, and the selection of results follows AINTLIB's AffinoidRings.lean; neither's proofs were used. That AINTLIB file was also consulted for the quotient-pair construction and its universal property. Its quotient uses the same integral closure of the image plus ring; this file bundles the construction with the current Tau Ceti Huber-pair API.

References

• Wedhorn, Adic Spaces, Definition 7.14, Remark 7.15, and Definition 7.22.
• AINTLIB, branch dev/adic-spaces, projects/AdicSpaces/Adic spaces/AffinoidRings.lean.

structure TauCeti.Huber.IsRingOfIntegralElements {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] (Aplus : Subring A) : Prop

A subring A⁺ of a nonarchimedean ring is a ring of integral elements if it is open, integrally closed in A, and contained in the power-bounded subring A°.

• isOpen : IsOpen ↑Aplus

  A⁺ is open in A.

• isIntegrallyClosedIn : IsIntegrallyClosedIn (↥Aplus) A

  A⁺ is integrally closed in A.

• le_powerBoundedSubring : Aplus ≤ powerBoundedSubring A

  Every element of A⁺ is power-bounded.

theorem TauCeti.Huber.IsRingOfIntegralElements.isPowerBounded_of_mem {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {Aplus : Subring A} (h : IsRingOfIntegralElements Aplus) ⦃a : A⦄ (ha : a ∈ Aplus) : IsPowerBounded a

Every element of a ring of integral elements is power-bounded: the field IsRingOfIntegralElements.le_powerBoundedSubring read elementwise.

theorem TauCeti.Huber.mem_of_isTopologicallyNilpotent_of_isIntegrallyClosedIn {A : Type u_1} [CommRing A] [TopologicalSpace A] {Aplus : Subring A} (hopen : IsOpen ↑Aplus) [IsIntegrallyClosedIn (↥Aplus) A] {a : A} (ha : IsTopologicallyNilpotent a) : a ∈ Aplus

Wedhorn: an open integrally closed subring contains every topologically nilpotent element.

Neither power-boundedness nor a nonarchimedean topology plays any part, so this is stated for an arbitrary open subring integrally closed in A, not just for a ring of integral elements.

theorem TauCeti.Huber.IsRingOfIntegralElements.mem_of_isTopologicallyNilpotent {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {Aplus : Subring A} (h : IsRingOfIntegralElements Aplus) {a : A} (ha : IsTopologicallyNilpotent a) : a ∈ Aplus

A°° ⊆ A⁺ for every ring of integral elements.

theorem TauCeti.Huber.IsRingOfIntegralElements.map {A : Type u_1} [CommRing A] [TopologicalSpace A] {B : Type u_2} [CommRing B] [TopologicalSpace B] [NonarchimedeanRing A] [NonarchimedeanRing B] {Aplus : Subring A} (h : IsRingOfIntegralElements Aplus) (e : A ≃+* B) (he : Continuous ⇑e) (he' : Continuous ⇑e.symm) : IsRingOfIntegralElements (Subring.map (↑e) Aplus)

An isomorphism of topological rings carries a ring of integral elements onto a ring of integral elements.

structure TauCeti.Huber.Pair (A : Type u_1) [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] : Type u_1

A Huber pair (A, A⁺): a Huber ring together with a ring of integral elements. Only the noncanonical subring A⁺ is stored; the Huber structure on A is a parameter.

• plus : Subring A

  The ring of integral elements A⁺.

• isRingOfIntegralElements : IsRingOfIntegralElements self.plus

  A⁺ really is a ring of integral elements.

theorem TauCeti.Huber.Pair.ext {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] {S T : Pair A} (h : S.plus = T.plus) : S = T

Two Huber pairs on the same Huber ring agree as soon as their rings of integral elements do: A⁺ is the only data a Huber pair carries.

theorem TauCeti.Huber.Pair.ext_iff {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] {S T : Pair A} : S = T ↔ S.plus = T.plus

structure TauCeti.Huber.Pair.Hom {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {B : Type u_2} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsHuberRing A] [IsHuberRing B] (S : Pair A) (T : Pair B) : Type (max u_1 u_2)

A morphism of Huber pairs is a continuous ring homomorphism carrying A⁺ into B⁺.

• toRingHom : A →+* B

  The underlying ring homomorphism.

• continuous_toRingHom : Continuous ⇑self.toRingHom

  The underlying ring homomorphism is continuous.

• map_mem_plus (a : A) : a ∈ S.plus → self.toRingHom a ∈ T.plus

  The underlying ring homomorphism carries A⁺ into B⁺.

def TauCeti.Huber.Pair.Hom.id {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] (S : Pair A) : S.Hom S

The identity morphism of a Huber pair.

Equations

• TauCeti.Huber.Pair.Hom.id S = { toRingHom := RingHom.id A, continuous_toRingHom := ⋯, map_mem_plus := ⋯ }

def TauCeti.Huber.Pair.Hom.comp {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {B : Type u_2} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] {C : Type u_3} [CommRing C] [TopologicalSpace C] [IsTopologicalRing C] [IsHuberRing A] [IsHuberRing B] [IsHuberRing C] {S : Pair A} {T : Pair B} {U : Pair C} (g : T.Hom U) (f : S.Hom T) : S.Hom U

Morphisms of Huber pairs compose.

Equations

• g.comp f = { toRingHom := g.toRingHom.comp f.toRingHom, continuous_toRingHom := ⋯, map_mem_plus := ⋯ }

@[simp]

theorem TauCeti.Huber.Pair.Hom.toRingHom_id {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] (S : Pair A) : (id S).toRingHom = RingHom.id A

@[simp]

theorem TauCeti.Huber.Pair.Hom.toRingHom_comp {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {B : Type u_2} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] {C : Type u_3} [CommRing C] [TopologicalSpace C] [IsTopologicalRing C] [IsHuberRing A] [IsHuberRing B] [IsHuberRing C] {S : Pair A} {T : Pair B} {U : Pair C} (g : T.Hom U) (f : S.Hom T) : (g.comp f).toRingHom = g.toRingHom.comp f.toRingHom

theorem TauCeti.Huber.Pair.Hom.ext {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {B : Type u_2} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsHuberRing A] [IsHuberRing B] {S : Pair A} {T : Pair B} {f g : S.Hom T} (h : f.toRingHom = g.toRingHom) : f = g

theorem TauCeti.Huber.Pair.Hom.ext_iff {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {B : Type u_2} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsHuberRing A] [IsHuberRing B] {S : Pair A} {T : Pair B} {f g : S.Hom T} : f = g ↔ f.toRingHom = g.toRingHom

theorem TauCeti.Huber.Pair.Hom.comp_assoc {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {B : Type u_2} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] {C : Type u_3} [CommRing C] [TopologicalSpace C] [IsTopologicalRing C] [IsHuberRing A] [IsHuberRing B] [IsHuberRing C] {D : Type u_4} [CommRing D] [TopologicalSpace D] [IsTopologicalRing D] [IsHuberRing D] {S : Pair A} {T : Pair B} {U : Pair C} {V : Pair D} (h : U.Hom V) (g : T.Hom U) (f : S.Hom T) : (h.comp g).comp f = h.comp (g.comp f)

Composition of morphisms of Huber pairs is associative.

@[simp]

theorem TauCeti.Huber.Pair.Hom.id_comp {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {B : Type u_2} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsHuberRing A] [IsHuberRing B] {S : Pair A} {T : Pair B} (f : S.Hom T) : (id T).comp f = f

The identity morphism is a left unit for composition of morphisms of Huber pairs.

@[simp]

theorem TauCeti.Huber.Pair.Hom.comp_id {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {B : Type u_2} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsHuberRing A] [IsHuberRing B] {S : Pair A} {T : Pair B} (f : S.Hom T) : f.comp (id S) = f

The identity morphism is a right unit for composition of morphisms of Huber pairs.

def TauCeti.Huber.Pair.discrete (A : Type u_1) [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] [DiscreteTopology A] : Pair A

A discrete ring is a Huber pair with A⁺ = A: every element is power-bounded, the whole ring is open, and ⊤ is trivially integrally closed. This is the witness that the definitions above are satisfiable.

Equations

• TauCeti.Huber.Pair.discrete A = { plus := ⊤, isRingOfIntegralElements := ⋯ }

@[simp]

theorem TauCeti.Huber.Pair.discrete_plus {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] [DiscreteTopology A] : (discrete A).plus = ⊤

The ring of integral elements of the discrete Huber pair is the whole ring.

def TauCeti.Huber.Pair.powerBounded (A : Type u_1) [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] : Pair A

The Huber pair with A⁺ = A°. This is a ring of integral elements because A° is open (TauCeti.Huber.isOpen_powerBoundedSubring) and integrally closed in A (TauCeti.Huber.isPowerBounded_of_isIntegral, Wedhorn Proposition 5.30(4)). Since every ring of integral elements is contained in A°, this is the largest one.

Equations

• TauCeti.Huber.Pair.powerBounded A = { plus := TauCeti.Huber.powerBoundedSubring A, isRingOfIntegralElements := ⋯ }

@[simp]

theorem TauCeti.Huber.Pair.powerBounded_plus {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] : (powerBounded A).plus = powerBoundedSubring A

The ring of integral elements of the largest Huber pair is A°.

theorem TauCeti.Huber.Pair.isRingOfIntegralElements_integralClosure {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {R : Subring A} (hopen : IsOpen ↑R) (hpb : R ≤ powerBoundedSubring A) : IsRingOfIntegralElements (integralClosure (↥R) A).toSubring

The integral closure of an open subring contained in powerBoundedSubring is a ring of integral elements.

noncomputable def TauCeti.Huber.Pair.quotient {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] (S : Pair A) (J : Ideal A) : Pair (A ⧸ J)

The quotient of a Huber pair by J (Wedhorn Definition 7.22). Its plus ring is the integral closure of the image of the original plus ring in the quotient.

Equations

• S.quotient J = { plus := (integralClosure (↥(Subring.map (Ideal.Quotient.mk J) S.plus)) (A ⧸ J)).toSubring, isRingOfIntegralElements := ⋯ }

@[simp]

theorem TauCeti.Huber.Pair.quotient_plus {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] (S : Pair A) (J : Ideal A) : (S.quotient J).plus = (integralClosure (↥(Subring.map (Ideal.Quotient.mk J) S.plus)) (A ⧸ J)).toSubring

The plus ring of the quotient pair is the integral closure of the image plus ring.

noncomputable def TauCeti.Huber.Pair.quotientHom {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] (S : Pair A) (J : Ideal A) : S.Hom (S.quotient J)

The canonical morphism from a Huber pair to its quotient by J.

Equations

• S.quotientHom J = { toRingHom := Ideal.Quotient.mk J, continuous_toRingHom := ⋯, map_mem_plus := ⋯ }

@[simp]

theorem TauCeti.Huber.Pair.Hom.toRingHom_quotientHom {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] (S : Pair A) (J : Ideal A) : (S.quotientHom J).toRingHom = Ideal.Quotient.mk J

The underlying map of the canonical quotient-pair morphism is the quotient map.

noncomputable def TauCeti.Huber.Pair.Hom.quotientLift {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {B : Type u_2} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsHuberRing A] [IsHuberRing B] {S : Pair A} {T : Pair B} (J : Ideal A) (f : S.Hom T) (hJ : J ≤ RingHom.ker f.toRingHom) : (S.quotient J).Hom T

A morphism of Huber pairs annihilating J factors through the quotient pair.

Equations

• TauCeti.Huber.Pair.Hom.quotientLift J f hJ = { toRingHom := Ideal.Quotient.lift J f.toRingHom ⋯, continuous_toRingHom := ⋯, map_mem_plus := ⋯ }

@[simp]

theorem TauCeti.Huber.Pair.Hom.toRingHom_quotientLift {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {B : Type u_2} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsHuberRing A] [IsHuberRing B] {S : Pair A} {T : Pair B} (J : Ideal A) (f : S.Hom T) (hJ : J ≤ RingHom.ker f.toRingHom) : (quotientLift J f hJ).toRingHom = Ideal.Quotient.lift J f.toRingHom ⋯

The underlying ring homomorphism of the quotient factorisation is Ideal.Quotient.lift.

@[simp]

theorem TauCeti.Huber.Pair.Hom.quotientLift_comp_quotientHom {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {B : Type u_2} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsHuberRing A] [IsHuberRing B] {S : Pair A} {T : Pair B} (J : Ideal A) (f : S.Hom T) (hJ : J ≤ RingHom.ker f.toRingHom) : (quotientLift J f hJ).comp (S.quotientHom J) = f

The factorisation through the quotient pair recovers the original morphism.

theorem TauCeti.Huber.Pair.Hom.quotientLift_unique {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {B : Type u_2} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsHuberRing A] [IsHuberRing B] {S : Pair A} {T : Pair B} (J : Ideal A) (f : S.Hom T) (hJ : J ≤ RingHom.ker f.toRingHom) (g : (S.quotient J).Hom T) (hg : g.comp (S.quotientHom J) = f) : g = quotientLift J f hJ

The factorisation through a quotient Huber pair is unique.