Adic homomorphisms of Huber rings

An adic homomorphism admits compatible pairs of definition for which the target ideal of definition is generated by the source ideal. This condition implies continuity and is stronger than continuity: it also preserves open ideals. Conversely these two intrinsic conditions characterize adic homomorphisms. They make composition and cancellation independent of the chosen pairs of definition, and they show that an adic homomorphism is adic for every pair of definition of its source (TauCeti.Huber.IsAdicHom.exists_pairOfDefinition_map_eq).

The definition follows Wedhorn, Adic Spaces, Definition 6.23; the intrinsic criterion and composition properties are the content of §6.5.

class TauCeti.Huber.IsAdicHom {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [TopologicalSpace A] [TopologicalSpace B] (f : A →+* B) : Prop

A ring homomorphism is adic if it carries some pair of definition to a pair of definition, with the target ideal generated by the image of the source ideal.

• exists_pairOfDefinition : ∃ (P : PairOfDefinition A) (Q : PairOfDefinition B) (h : ∀ a ∈ P.ringOfDefinition, f a ∈ Q.ringOfDefinition), Ideal.map (f.restrict P.ringOfDefinition Q.ringOfDefinition h) P.idealOfDefinition = Q.idealOfDefinition

  Compatible pairs whose ideals of definition are related by extension.

theorem TauCeti.Huber.isAdicHom_iff {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [TopologicalSpace A] [TopologicalSpace B] {f : A →+* B} : IsAdicHom f ↔ ∃ (P : PairOfDefinition A) (Q : PairOfDefinition B) (h : ∀ a ∈ P.ringOfDefinition, f a ∈ Q.ringOfDefinition), Ideal.map (f.restrict P.ringOfDefinition Q.ringOfDefinition h) P.idealOfDefinition = Q.idealOfDefinition

Characteristic introduction and elimination criterion for adic homomorphisms.

theorem TauCeti.Huber.IsAdicHom.continuous {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [TopologicalSpace A] [TopologicalSpace B] [IsTopologicalRing A] [IsTopologicalRing B] {f : A →+* B} (hf : IsAdicHom f) : Continuous ⇑f

An adic homomorphism is continuous.

theorem TauCeti.Huber.IsAdicHom.id {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] : IsAdicHom (RingHom.id A)

The identity homomorphism of a Huber ring is adic.

theorem TauCeti.Huber.IsAdicHom.isOpen_map {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [TopologicalSpace A] [TopologicalSpace B] [IsTopologicalRing B] {f : A →+* B} (hf : IsAdicHom f) {I : Ideal A} (hI : IsOpen ↑I) : IsOpen ↑(Ideal.map f I)

Adic homomorphisms carry open ideals to open ideals.

theorem TauCeti.Huber.IsAdicHom.isBounded_image {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [TopologicalSpace A] [TopologicalSpace B] [IsTopologicalRing A] [IsTopologicalRing B] {f : A →+* B} (hf : IsAdicHom f) {S : Set A} (hS : IsBounded S) : IsBounded (⇑f '' S)

Adic homomorphisms carry bounded sets to bounded sets.

theorem TauCeti.Huber.IsAdicHom.isPowerBounded_map {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [TopologicalSpace A] [TopologicalSpace B] [IsTopologicalRing A] [IsTopologicalRing B] {f : A →+* B} (hf : IsAdicHom f) {a : A} (ha : IsPowerBounded a) : IsPowerBounded (f a)

Adic homomorphisms carry power-bounded elements to power-bounded elements.

theorem TauCeti.Huber.IsAdicHom.of_continuous_isOpen_map {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [TopologicalSpace A] [TopologicalSpace B] [IsTopologicalRing A] [IsTopologicalRing B] {f : A →+* B} [IsHuberRing A] [IsHuberRing B] (hf : Continuous ⇑f) (hopen : ∀ (I : Ideal A), IsOpen ↑I → IsOpen ↑(Ideal.map f I)) : IsAdicHom f

Continuity and preservation of open ideals imply adicness.

theorem TauCeti.Huber.IsAdicHom.exists_pairOfDefinition_map_eq {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [TopologicalSpace A] [TopologicalSpace B] [IsTopologicalRing A] [IsTopologicalRing B] {f : A →+* B} (hf : IsAdicHom f) (P : PairOfDefinition A) : ∃ (Q : PairOfDefinition B) (h : ∀ a ∈ P.ringOfDefinition, f a ∈ Q.ringOfDefinition), Ideal.map (f.restrict P.ringOfDefinition Q.ringOfDefinition h) P.idealOfDefinition = Q.idealOfDefinition

An adic homomorphism is adic for every pair of definition of its source: for any pair of definition (A₀, I) of A there is a pair of definition (B₀, J) of B with f(A₀) ⊆ B₀ and J generated by f(I).

theorem TauCeti.Huber.IsAdicHom.of_isOpenQuotientMap {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [TopologicalSpace A] [TopologicalSpace B] [IsTopologicalRing A] {f : A →+* B} [IsHuberRing A] (hf : IsOpenQuotientMap ⇑f) : IsAdicHom f

An open quotient homomorphism from a Huber ring is adic.

theorem TauCeti.Huber.IsAdicHom.iff_continuous_isOpen_map {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [TopologicalSpace A] [TopologicalSpace B] [IsTopologicalRing A] [IsTopologicalRing B] {f : A →+* B} [IsHuberRing A] [IsHuberRing B] : IsAdicHom f ↔ Continuous ⇑f ∧ ∀ (I : Ideal A), IsOpen ↑I → IsOpen ↑(Ideal.map f I)

Intrinsic criterion: an adic homomorphism is precisely a continuous homomorphism preserving open ideals.

theorem TauCeti.Huber.IsAdicHom.comp {A : Type u_1} {B : Type u_2} {C : Type u_3} [CommRing A] [CommRing B] [CommRing C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] [IsTopologicalRing A] [IsTopologicalRing B] [IsTopologicalRing C] {f : A →+* B} {g : B →+* C} (hg : IsAdicHom g) (hf : IsAdicHom f) : IsAdicHom (g.comp f)

The composite of adic homomorphisms is adic.

theorem TauCeti.Huber.IsAdicHom.of_comp {A : Type u_1} {B : Type u_2} {C : Type u_3} [CommRing A] [CommRing B] [CommRing C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] [IsTopologicalRing B] [IsTopologicalRing C] {f : A →+* B} {g : B →+* C} [IsHuberRing B] (h : IsAdicHom (g.comp f)) (hf : Continuous ⇑f) (hg : Continuous ⇑g) : IsAdicHom g

If a composite is adic and both factors are continuous, then its final factor is adic.

theorem TauCeti.Huber.IsAdicHom.of_isTateRing {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [TopologicalSpace A] [TopologicalSpace B] [IsTopologicalRing A] [IsTopologicalRing B] {f : A →+* B} [IsHuberRing B] [IsTateRing A] (hf : Continuous ⇑f) : IsAdicHom f

Every continuous homomorphism from a Tate ring to a Huber ring is adic.

theorem TauCeti.Huber.IsAdicHom.of_discrete_iff {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [TopologicalSpace A] [TopologicalSpace B] [IsTopologicalRing B] {f : A →+* B} [DiscreteTopology A] : IsAdicHom f ↔ DiscreteTopology B

A homomorphism from a discrete Huber ring is adic exactly when its target is discrete.

theorem TauCeti.Huber.IsAdicHom.of_radical_eq {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [TopologicalSpace A] [TopologicalSpace B] {f : A →+* B} (P : PairOfDefinition A) (Q : PairOfDefinition B) (h : ∀ a ∈ P.ringOfDefinition, f a ∈ Q.ringOfDefinition) (hrad : (Ideal.map (f.restrict P.ringOfDefinition Q.ringOfDefinition h) P.idealOfDefinition).radical = Q.idealOfDefinition.radical) : IsAdicHom f

The radical criterion for compatible pairs of definition. Equality of radicals permits replacing the target ideal by the ideal generated by the source ideal.