Huber rings of noetherian type

A Huber ring is of noetherian type when it either has a noetherian ring of definition or is a strongly noetherian Tate ring. This is the pair of hypotheses in Huber's sheafiness theorem.

The two alternatives are genuinely needed. In particular, an arbitrary discrete ring need not be noetherian, but it has its prime subring as a noetherian ring of definition and is therefore of noetherian type. The results here provide the basic introduction and elimination API for this class.

References

• R. Huber, A generalization of formal schemes and rigid analytic varieties, Theorem 2.2.
• T. Wedhorn, Adic Spaces, Remark 6.37.

class TauCeti.Huber.IsNoetherianType (A : Type u_1) [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] : Prop

A Huber ring is of noetherian type if it has a noetherian ring of definition, or if it is a strongly noetherian Tate ring.

• out : (∃ (P : PairOfDefinition A), IsNoetherianRing ↥P.ringOfDefinition) ∨ IsTateRing A ∧ IsStronglyNoetherian A

  The disjunction defining a Huber ring of noetherian type.

theorem TauCeti.Huber.isNoetherianType_iff (A : Type u_1) [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] : IsNoetherianType A ↔ (∃ (P : PairOfDefinition A), IsNoetherianRing ↥P.ringOfDefinition) ∨ IsTateRing A ∧ IsStronglyNoetherian A

theorem TauCeti.Huber.IsNoetherianType.of_pairOfDefinition {A : Type u_2} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] (P : PairOfDefinition A) (hP : IsNoetherianRing ↥P.ringOfDefinition) : IsNoetherianType A

A noetherian ring of definition makes a Huber ring of noetherian type.

theorem TauCeti.Huber.IsNoetherianType.elim {A : Type u_2} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] {P : Prop} (hA : IsNoetherianType A) (hrod : ∀ (Q : PairOfDefinition A), IsNoetherianRing ↥Q.ringOfDefinition → P) (htate : IsTateRing A → IsStronglyNoetherian A → P) : P

Eliminate noetherian type by treating its noetherian-ring-of-definition and strongly noetherian Tate alternatives.

instance TauCeti.Huber.IsNoetherianType.of_isStronglyNoetherian {A : Type u_2} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsTateRing A] [IsStronglyNoetherian A] : IsNoetherianType A

A strongly noetherian Tate ring is of noetherian type.

instance TauCeti.Huber.IsNoetherianType.of_discreteTopology {A : Type u_2} [CommRing A] [TopologicalSpace A] [DiscreteTopology A] : IsNoetherianType A

Every discrete commutative ring is of noetherian type, even when the ring itself is not noetherian: its prime subring is a noetherian ring of definition.