Quotient mappings of Huber pairs

A quotient mapping of Huber pairs is an open surjection on the underlying topological rings, with target plus ring the integral closure of the image of the source plus ring. These are the quotient maps used in presentations of affinoid algebras topologically of finite type.

Pair.Hom.IsQuotientMapping records both conditions. Canonical quotient-pair maps are quotient mappings, and quotient mappings compose. The first isomorphism theorem identifies the target with the quotient pair by the kernel: IsQuotientMapping.quotientKerInverse is inverse to the canonical factorisation, as a continuous morphism preserving the plus rings in both directions. No completeness or separation hypothesis is needed for these statements. The inverse uses Mathlib's RingHom.quotientKerEquivOfSurjective and the topological refinement RingHom.isHomeomorph_kerLift; the new content is preservation of the quotient plus ring.

References

• T. Wedhorn, Adic Spaces, arXiv:1910.05934v1, Definitions 7.22 and 8.42.

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

A quotient mapping of Huber pairs is an open quotient map of underlying rings whose target plus ring is the integral closure of the image of the source plus ring.

• isOpenQuotientMap : IsOpenQuotientMap ⇑f.toRingHom

  The underlying ring map is continuous, open and surjective.

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

  The plus ring has the quotient-pair integral closure.

theorem TauCeti.Huber.Pair.Hom.IsQuotientMapping.mem_plus_iff {A : Type u_1} {B : Type u_2} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsHuberRing B] {S : Pair A} {T : Pair B} {f : S.Hom T} (hf : f.IsQuotientMapping) {b : B} : b ∈ T.plus ↔ IsIntegral (↥(Subring.map f.toRingHom S.plus)) b

Membership in the target plus ring is integrality over the image of the source plus ring.

theorem TauCeti.Huber.Pair.Hom.isQuotientMapping_iff_isOpenQuotientMap_and_isIntegral {A : Type u_1} {B : Type u_2} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsHuberRing B] {S : Pair A} {T : Pair B} (f : S.Hom T) : f.IsQuotientMapping ↔ IsOpenQuotientMap ⇑f.toRingHom ∧ ∀ b ∈ T.plus, IsIntegral (↥(Subring.map f.toRingHom S.plus)) b

A pair morphism that is an open quotient map is a quotient mapping if every target plus ring element is integral over the image plus ring. The other inclusion is automatic.

@[simp]

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

The identity of a Huber pair is a quotient mapping.

@[simp]

theorem TauCeti.Huber.Pair.Hom.isQuotientMapping_quotientHom {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] (S : Pair A) (J : Ideal A) : (S.quotientHom J).IsQuotientMapping

The canonical map to a quotient Huber pair is a quotient mapping, even when the ideal is not closed.

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

Quotient mappings of Huber pairs compose. In particular, successive quotient presentations have the same integral closure condition as their composite presentation.

noncomputable def TauCeti.Huber.Pair.Hom.IsQuotientMapping.quotientKerInverse {A : Type u_1} {B : Type u_2} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsHuberRing B] {S : Pair A} {T : Pair B} {f : S.Hom T} (hf : f.IsQuotientMapping) : T.Hom (S.quotient (RingHom.ker f.toRingHom))

For a quotient mapping, the inverse of the first-isomorphism-theorem ring equivalence is a continuous morphism of Huber pairs. The source of the inverse is the target pair, and its target is the canonical quotient pair by the kernel.

@[simp]

theorem TauCeti.Huber.Pair.Hom.IsQuotientMapping.toRingHom_quotientKerInverse {A : Type u_1} {B : Type u_2} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsHuberRing B] {S : Pair A} {T : Pair B} {f : S.Hom T} (hf : f.IsQuotientMapping) : hf.quotientKerInverse.toRingHom = (RingHom.quotientKerEquivOfSurjective ⋯).symm.toRingHom

The underlying ring homomorphism of the inverse is the inverse first-isomorphism-theorem ring equivalence.

@[simp]

theorem TauCeti.Huber.Pair.Hom.IsQuotientMapping.quotientKerInverse_comp_quotientLift {A : Type u_1} {B : Type u_2} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsHuberRing B] {S : Pair A} {T : Pair B} {f : S.Hom T} (hf : f.IsQuotientMapping) : hf.quotientKerInverse.comp (quotientLift (RingHom.ker f.toRingHom) f ⋯) = id (S.quotient (RingHom.ker f.toRingHom))

The factorisation through the kernel quotient followed by its inverse is the identity.

@[simp]

theorem TauCeti.Huber.Pair.Hom.IsQuotientMapping.quotientLift_comp_quotientKerInverse {A : Type u_1} {B : Type u_2} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsHuberRing B] {S : Pair A} {T : Pair B} {f : S.Hom T} (hf : f.IsQuotientMapping) : (quotientLift (RingHom.ker f.toRingHom) f ⋯).comp hf.quotientKerInverse = id T

The inverse followed by the factorisation through the kernel quotient is the identity.