Finite algebras over a Huber ring

Let A be a Huber ring and B a commutative A-algebra that is finite as an A-module, with its natural topology (IsModuleTopology A B). Then B is a topological ring (IsModuleTopology.isTopologicalRing), and this file shows that it is again a Huber ring, and a Tate ring when A is. No completeness, noetherian, flatness or separatedness hypothesis is needed. This is how a finite étale algebra over a complete Tate ring becomes a Tate ring, the first step in making it a Huber pair over (A, A⁺).

Fix a pair of definition (A₀, I) of A and a finitely generated A₀-submodule M₀ ⊆ B containing 1 and spanning B over A. The submodules Iⁿ • M₀ are a neighbourhood basis of 0 (TauCeti.Huber.PairOfDefinition.hasBasis_nhds_zero_idealOfDefinition_pow_smul). The multiplier ring B₀ = {b ∈ B | b M₀ ⊆ M₀} is a subring of B (AddSubgroup.multiplierRing). Since M₀ * M₀ is finitely generated, a power Iʲ carries it into M₀ (TauCeti.Huber.PairOfDefinition.exists_pow_smul_le), so Iʲ • M₀ ⊆ B₀ (Submodule.smul_subset_multiplierRing) and B₀ is open. With the extension J of I to B₀, one gets I^(n + j) • M₀ ⊆ Jⁿ ⊆ Iⁿ • M₀ (Submodule.smul_subset_coe_map_pow, Submodule.coe_map_pow_subset), the second inclusion because 1 ∈ M₀ and B₀ M₀ ⊆ M₀. So the topology of B₀ is the J-adic one and (B₀, J) is a pair of definition of B. When A is Tate, the image of a pseudouniformiser of A is one of B.

Main results

• TauCeti.Huber.PairOfDefinition.exists_pairOfDefinition_isIntegral: every pair of definition (A₀, I) of A gives a pair of definition of B whose ring of definition contains the image of A₀ and is integral over A₀.
• TauCeti.Huber.IsHuberRing.of_isModuleTopology: a finite algebra over a Huber ring, with its natural topology, is a Huber ring.
• TauCeti.Huber.IsTateRing.of_isModuleTopology: a finite algebra over a Tate ring, with its natural topology, is a Tate ring.
• TauCeti.Huber.IsPowerBounded.algebraMap_of_isModuleTopology: the structure map A → B preserves power-boundedness.
• TauCeti.Huber.isOpen_integralClosure_map_algebraMap: the integral closure in B of the image of an open subring of A is open.

References

• R. Huber, A generalization of formal schemes and rigid analytic varieties, Math. Z. 217 (1994), §2, before Lemma 2.3.
• K. S. Kedlaya and R. Liu, Relative p-adic Hodge theory: foundations, Astérisque 371 (2015), §2.2, Lemma 2.2.12, and §2.4, Remark 2.4.2.

The pair of definition

theorem TauCeti.Huber.PairOfDefinition.exists_pairOfDefinition_isIntegral {A : Type u_1} [CommRing A] [TopologicalSpace A] {B : Type u_2} [CommRing B] [Algebra A B] [IsTopologicalRing A] [TopologicalSpace B] [IsModuleTopology A B] [Module.Finite A B] (P : PairOfDefinition A) : ∃ (Q : PairOfDefinition B), (∀ a ∈ P.ringOfDefinition, (algebraMap A B) a ∈ Q.ringOfDefinition) ∧ ∀ b ∈ Q.ringOfDefinition, IsIntegral (↥P.ringOfDefinition) b

Pairs of definition of a finite algebra. For every pair of definition (A₀, I) of A, a finite A-algebra B with its natural topology has a pair of definition (B₀, J) whose ring of definition contains the image of A₀ and is integral over A₀. It is the multiplier ring of a finitely generated spanning lattice containing 1, with the extension of I to it.

theorem TauCeti.Huber.IsHuberRing.of_isModuleTopology {A : Type u_1} [CommRing A] [TopologicalSpace A] {B : Type u_2} [CommRing B] [Algebra A B] [IsTopologicalRing A] [TopologicalSpace B] [IsModuleTopology A B] [Module.Finite A B] [IsHuberRing A] : IsHuberRing B

A finite algebra over a Huber ring is a Huber ring. If B is a commutative A-algebra, finite as an A-module and carrying its natural topology, then B is a Huber ring.

theorem TauCeti.Huber.IsTateRing.of_isModuleTopology {A : Type u_1} [CommRing A] [TopologicalSpace A] {B : Type u_2} [CommRing B] [Algebra A B] [IsTopologicalRing A] [TopologicalSpace B] [IsModuleTopology A B] [Module.Finite A B] [IsTateRing A] : IsTateRing B

A finite algebra over a Tate ring is a Tate ring. If B is a commutative A-algebra, finite as an A-module and carrying its natural topology, then B is a Tate ring; the image of a pseudouniformiser of A is a pseudouniformiser of B.

Power-bounded and integral elements

theorem TauCeti.Huber.IsPowerBounded.algebraMap_of_isModuleTopology {A : Type u_1} [CommRing A] [TopologicalSpace A] {B : Type u_2} [CommRing B] [Algebra A B] [IsTopologicalRing A] [TopologicalSpace B] [IsModuleTopology A B] [Module.Finite A B] [IsHuberRing A] {a : A} (ha : IsPowerBounded a) : IsPowerBounded ((algebraMap A B) a)

The structure map of a finite algebra preserves power-boundedness. A power-bounded a lies in a ring of definition A₀ of A, and algebraMap A B carries A₀ into a ring of definition of B.

theorem TauCeti.Huber.isOpen_integralClosure_map_algebraMap {A : Type u_1} [CommRing A] [TopologicalSpace A] {B : Type u_2} [CommRing B] [Algebra A B] [IsTopologicalRing A] [TopologicalSpace B] [IsModuleTopology A B] [Module.Finite A B] [IsHuberRing A] {C : Subring A} (hC : IsOpen ↑C) : IsOpen ↑(integralClosure (↥(Subring.map (algebraMap A B) C)) B).toSubring

The integral closure of the image of an open subring is open. If C is an open subring of a Huber ring A, the integral closure of its image in a finite A-algebra B with its natural topology is open: it contains a ring of definition of B that is integral over a ring of definition A₀ ⊆ C of A.