The Huber pair of a finite algebra

Let (A, A⁺) be a Huber pair and B a commutative A-algebra, finite as an A-module and carrying its natural topology (IsModuleTopology A B), so that B is a Huber ring (TauCeti.Huber.IsHuberRing.of_isModuleTopology). The integral closure B⁺ of the image of A⁺ in B is a ring of integral elements, which makes (B, B⁺) a Huber pair and A → B a morphism of Huber pairs. Every A-algebra map from B to a Huber pair under (A, A⁺) is a morphism of Huber pairs, so (B, B⁺) is the pair that finite étale geometry attaches to a finite étale algebra. The plus ring is the integral closure of the image of A⁺, which need not equal B°: already for B = A they differ when A⁺ ≠ A°.

No completeness, separatedness, noetherian or étaleness hypothesis is needed for the construction and its universal property; completeness of B over a complete base is TauCeti.completeSpace_moduleTopology, and separatedness over a Hausdorff base for projective B is TauCeti.t2Space_moduleTopology_of_projective.

Main definitions

• TauCeti.Huber.Pair.finiteAlgebra: the Huber pair (B, B⁺), with B⁺ the integral closure of the image of A⁺.
• TauCeti.Huber.Pair.finiteAlgebra.algebraHom: the morphism (A, A⁺) → (B, B⁺).
• TauCeti.Huber.Pair.finiteAlgebra.lift: an A-algebra map B → D into a Huber pair (D, D⁺) under (A, A⁺), as a morphism of Huber pairs.
• TauCeti.Huber.Pair.Hom.IsFiniteEtale: a morphism of Huber pairs (A, A⁺) → (B, B⁺) is finite étale if A → B is finite étale, B carries its natural A-module topology, and B⁺ is the integral closure of the image of A⁺.

Main results

• TauCeti.Huber.Pair.finiteAlgebra_self: the Huber pair of A itself is (A, A⁺).
• TauCeti.Huber.Pair.finiteAlgebra.homEquiv: morphisms of Huber pairs (B, B⁺) → (D, D⁺) under (A, A⁺) are exactly the A-algebra maps B → D.
• TauCeti.Huber.Pair.finiteAlgebra.isFiniteEtale_algebraHom: for finite étale B, the structure morphism (A, A⁺) → (B, B⁺) is finite étale.
• TauCeti.Huber.Pair.Hom.IsFiniteEtale.exists_hom: every ring map out of the target of a finite étale morphism of Huber pairs that is compatible with morphisms of Huber pairs out of the source is itself a morphism of Huber pairs.

References

• R. Huber, Étale cohomology of rigid analytic varieties and adic spaces, Aspects of Mathematics E30 (1996), §1.4, (1.4.2).
• K. S. Kedlaya and R. Liu, Relative p-adic Hodge theory: foundations, Astérisque 371 (2015), §2.4, Remark 2.4.2, and §8.2, Definition 8.2.16.
• P. Scholze, Perfectoid spaces, Publ. Math. IHÉS 116 (2012), §7, Definition 7.1(i).

noncomputable def TauCeti.Huber.Pair.finiteAlgebra {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] (S : Pair A) (B : Type u_2) [CommRing B] [Algebra A B] [Module.Finite A B] [TopologicalSpace B] [IsModuleTopology A B] [IsTopologicalRing B] [IsHuberRing B] : Pair B

The Huber pair of a finite algebra. For a Huber pair (A, A⁺) and a finite A-algebra B with its natural topology, (B, B⁺) with B⁺ the integral closure of the image of A⁺.

@[simp]

theorem TauCeti.Huber.Pair.finiteAlgebra_plus {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] (S : Pair A) (B : Type u_2) [CommRing B] [Algebra A B] [Module.Finite A B] [TopologicalSpace B] [IsModuleTopology A B] [IsTopologicalRing B] [IsHuberRing B] : (S.finiteAlgebra B).plus = (integralClosure (↥(Subring.map (algebraMap A B) S.plus)) B).toSubring

The plus ring of finiteAlgebra S B is the integral closure of the image of A⁺.

theorem TauCeti.Huber.Pair.mem_finiteAlgebra_plus {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] (S : Pair A) (B : Type u_2) [CommRing B] [Algebra A B] [Module.Finite A B] [TopologicalSpace B] [IsModuleTopology A B] [IsTopologicalRing B] [IsHuberRing B] {b : B} : b ∈ (S.finiteAlgebra B).plus ↔ IsIntegral (↥(Subring.map (algebraMap A B) S.plus)) b

An element of B lies in the plus ring of finiteAlgebra S B iff it is integral over the image of A⁺.

noncomputable def TauCeti.Huber.Pair.finiteAlgebra.algebraHom {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] (S : Pair A) (B : Type u_2) [CommRing B] [Algebra A B] [Module.Finite A B] [TopologicalSpace B] [IsModuleTopology A B] [IsTopologicalRing B] [IsHuberRing B] : S.Hom (S.finiteAlgebra B)

The structure morphism (A, A⁺) → (B, B⁺) of the Huber pair of a finite algebra.

@[simp]

theorem TauCeti.Huber.Pair.finiteAlgebra.algebraHom_toRingHom {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] (S : Pair A) (B : Type u_2) [CommRing B] [Algebra A B] [Module.Finite A B] [TopologicalSpace B] [IsModuleTopology A B] [IsTopologicalRing B] [IsHuberRing B] : (algebraHom S B).toRingHom = algebraMap A B

The underlying map of the structure morphism is algebraMap A B.

@[simp]

theorem TauCeti.Huber.Pair.finiteAlgebra_self {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] (S : Pair A) : S.finiteAlgebra A = S

The Huber pair of A itself is (A, A⁺): A⁺ is integrally closed in A.

noncomputable def TauCeti.Huber.Pair.finiteAlgebra.lift {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] {S : Pair A} {B : Type u_2} [CommRing B] [Algebra A B] [Module.Finite A B] [TopologicalSpace B] [IsModuleTopology A B] [IsTopologicalRing B] [IsHuberRing B] {D : Type u_3} [CommRing D] [TopologicalSpace D] [IsTopologicalRing D] [IsHuberRing D] [Algebra A D] {V : Pair D} (χ : S.Hom V) (hχ : χ.toRingHom = algebraMap A D) (f : B →ₐ[A] D) : (S.finiteAlgebra B).Hom V

The universal property of the Huber pair of a finite algebra. If χ : (A, A⁺) → (D, D⁺) is a morphism of Huber pairs with underlying map algebraMap A D, every A-algebra map B → D is a morphism of Huber pairs (B, B⁺) → (D, D⁺). It is continuous because B carries the natural topology, and it carries B⁺ into D⁺ because D⁺ is integrally closed in D.

@[simp]

theorem TauCeti.Huber.Pair.finiteAlgebra.lift_toRingHom {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] {S : Pair A} {B : Type u_2} [CommRing B] [Algebra A B] [Module.Finite A B] [TopologicalSpace B] [IsModuleTopology A B] [IsTopologicalRing B] [IsHuberRing B] {D : Type u_3} [CommRing D] [TopologicalSpace D] [IsTopologicalRing D] [IsHuberRing D] [Algebra A D] {V : Pair D} (χ : S.Hom V) (hχ : χ.toRingHom = algebraMap A D) (f : B →ₐ[A] D) : (lift χ hχ f).toRingHom = f.toRingHom

The underlying map of finiteAlgebra.lift χ hχ f is f.

@[simp]

theorem TauCeti.Huber.Pair.finiteAlgebra.lift_comp_algebraHom {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] {S : Pair A} {B : Type u_2} [CommRing B] [Algebra A B] [Module.Finite A B] [TopologicalSpace B] [IsModuleTopology A B] [IsTopologicalRing B] [IsHuberRing B] {D : Type u_3} [CommRing D] [TopologicalSpace D] [IsTopologicalRing D] [IsHuberRing D] [Algebra A D] {V : Pair D} (χ : S.Hom V) (hχ : χ.toRingHom = algebraMap A D) (f : B →ₐ[A] D) : (lift χ hχ f).comp (algebraHom S B) = χ

finiteAlgebra.lift χ hχ f is a morphism under (A, A⁺).

noncomputable def TauCeti.Huber.Pair.finiteAlgebra.homEquiv {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] {S : Pair A} {B : Type u_2} [CommRing B] [Algebra A B] [Module.Finite A B] [TopologicalSpace B] [IsModuleTopology A B] [IsTopologicalRing B] [IsHuberRing B] {D : Type u_3} [CommRing D] [TopologicalSpace D] [IsTopologicalRing D] [IsHuberRing D] [Algebra A D] {V : Pair D} (χ : S.Hom V) (hχ : χ.toRingHom = algebraMap A D) : { ψ : (S.finiteAlgebra B).Hom V // ψ.comp (algebraHom S B) = χ } ≃ (B →ₐ[A] D)

Morphisms out of the Huber pair of a finite algebra. Morphisms of Huber pairs (B, B⁺) → (D, D⁺) under (A, A⁺) are exactly the A-algebra maps B → D.

@[simp]

theorem TauCeti.Huber.Pair.finiteAlgebra.homEquiv_apply {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] {S : Pair A} {B : Type u_2} [CommRing B] [Algebra A B] [Module.Finite A B] [TopologicalSpace B] [IsModuleTopology A B] [IsTopologicalRing B] [IsHuberRing B] {D : Type u_3} [CommRing D] [TopologicalSpace D] [IsTopologicalRing D] [IsHuberRing D] [Algebra A D] {V : Pair D} (χ : S.Hom V) (hχ : χ.toRingHom = algebraMap A D) (ψ : { ψ : (S.finiteAlgebra B).Hom V // ψ.comp (algebraHom S B) = χ }) (b : B) : ((homEquiv χ hχ) ψ) b = (↑ψ).toRingHom b

finiteAlgebra.homEquiv sends a morphism of Huber pairs to its underlying map.

@[simp]

theorem TauCeti.Huber.Pair.finiteAlgebra.homEquiv_symm_apply {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] {S : Pair A} {B : Type u_2} [CommRing B] [Algebra A B] [Module.Finite A B] [TopologicalSpace B] [IsModuleTopology A B] [IsTopologicalRing B] [IsHuberRing B] {D : Type u_3} [CommRing D] [TopologicalSpace D] [IsTopologicalRing D] [IsHuberRing D] [Algebra A D] {V : Pair D} (χ : S.Hom V) (hχ : χ.toRingHom = algebraMap A D) (f : B →ₐ[A] D) : ↑((homEquiv χ hχ).symm f) = lift χ hχ f

The inverse of finiteAlgebra.homEquiv is finiteAlgebra.lift.

Finite étale morphisms of Huber pairs

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

A morphism φ : (A, A⁺) → (B, B⁺) of Huber pairs is finite étale if φ makes B a finite étale A-algebra, B carries the natural topology of a finite A-module, and B⁺ is the integral closure of φ(A⁺) in B (Kedlaya–Liu, Definition 8.2.16). The plus ring is part of the condition: the integral closure of φ(A⁺) can be smaller than B°.

• finite : φ.toRingHom.Finite

  B is a finite A-module.

• etale : φ.toRingHom.Etale

  B is an étale A-algebra.

• isModuleTopology : IsModuleTopology A B

  B carries the natural topology of an A-module.

• plus_eq : T.plus = (integralClosure (↥(Subring.map φ.toRingHom S.plus)) B).toSubring

  B⁺ is the integral closure of φ(A⁺) in B.

theorem TauCeti.Huber.Pair.finiteAlgebra.isFiniteEtale_algebraHom {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] (S : Pair A) (B : Type u_3) [CommRing B] [Algebra A B] [Module.Finite A B] [Algebra.Etale A B] [TopologicalSpace B] [IsModuleTopology A B] [IsTopologicalRing B] [IsHuberRing B] : (algebraHom S B).IsFiniteEtale

For a finite étale algebra, the structure morphism of its Huber pair is finite étale.

theorem TauCeti.Huber.Pair.Hom.IsFiniteEtale.exists_hom {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] {B : Type u_2} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsHuberRing B] {S : Pair A} {T : Pair B} {φ : S.Hom T} (hφ : φ.IsFiniteEtale) {D : Type u_3} [CommRing D] [TopologicalSpace D] [IsTopologicalRing D] [IsHuberRing D] {V : Pair D} (χ : S.Hom V) (ψ : B →+* D) (hψ : ψ.comp φ.toRingHom = χ.toRingHom) : ∃ (ψ' : T.Hom V), ψ'.toRingHom = ψ

Universal property of a finite étale morphism of Huber pairs. If φ : (A, A⁺) → (B, B⁺) is finite étale and χ : (A, A⁺) → (D, D⁺) is a morphism of Huber pairs, every ring map ψ : B → D with ψ ∘ φ = χ is a morphism of Huber pairs (B, B⁺) → (D, D⁺).