Base change of completed rational localisations along a ring homomorphism

Let φ : A → B be a continuous ring homomorphism of topological rings with pairs of definition P and P'. For a presentation p = (T, s) of A and a presentation q of B with denominator φ(s) whose numerators contain φ(T), the universal property of A⟨T/s⟩ (Wedhorn, Proposition and Definition 5.51) extends φ uniquely to a continuous ring homomorphism

A⟨T/s⟩ → B⟨q⟩

compatible with the structure maps. This file packages that homomorphism as a morphism Presentation.mapHom of CompleteSeparatedTopCommRingCat, together with the extensionality principle for morphisms out of A⟨p⟩ and the compatibility of the structure maps with the restriction and comparison morphisms between completed rational localisations.

When φ carries open ideals to open ideals and A⁺ into B⁺, the preimage of the rational subset R(T/s) of Spa(A, A⁺) under the induced map Spa(B, B⁺) → Spa(A, A⁺) is the rational subset R(φ(T)/φ(s)) of Spa(B, B⁺) (Wedhorn, Lemma 7.46(3)). PresentationIndex.map records this at the level of the indices of the presentation limits: an admissible presentation refining an open U of Spa(A, A⁺) induces an admissible presentation refining any open of Spa(B, B⁺) containing the preimage of U. These are the components from which morphisms between the structure presheaves of Spa(A, A⁺) and Spa(B, B⁺) are assembled, in TauCeti.AlgebraicGeometry.AdicSpace.Spa.StructurePresheaf.Transport for isomorphisms and completions and in TauCeti.AlgebraicGeometry.AdicSpace.Spa.StructurePresheaf.Comap for a general φ with sheafy target.

Main definitions

• TauCeti.Huber.PairOfDefinition.Presentation.toCompletionLocTopHom: the structure map A → A⟨p⟩ as a morphism of TopCommRingCat.
• TauCeti.Huber.PairOfDefinition.Presentation.mapHom: the base change A⟨p⟩ ⟶ B⟨q⟩ of φ.
• TauCeti.ValuationSpectrum.PresentationIndex.map: the index of Spa(B, B⁺) induced by an index of Spa(A, A⁺).

Main results

• TauCeti.Huber.PairOfDefinition.Presentation.hom_ext: morphisms out of A⟨p⟩ are determined by their composites with the structure map.
• TauCeti.Huber.PairOfDefinition.Presentation.toCompletionLocTopHom_comp_mapHom: the base change is compatible with the structure maps.
• TauCeti.ValuationSpectrum.spaBasicOpen_map_pres: the rational open presented by the induced index is the preimage of the rational open presented by the original index.
• TauCeti.ValuationSpectrum.presentationLimitπToPresentation_comp_eq: two projections of a presentation limit followed by morphisms agreeing on A agree.

References

• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Proposition and Definition 5.51, Lemma 7.46 and §8.1.

The structure map, and maps out of A⟨p⟩

noncomputable def TauCeti.Huber.PairOfDefinition.Presentation.toCompletionLocTopHom {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : PairOfDefinition A} (p : P.Presentation) : ↧A ⟶ p.completionLocObj.obj

The structure map A → A⟨p⟩, as a morphism of TopCommRingCat.

Equations

• p.toCompletionLocTopHom = CategoryTheory.CategoryStruct.comp ⟨P.toCompletionLoc p.num p.den (Localization.Away p.den) ⋯, ⋯⟩ (CategoryTheory.eqToHom ⋯)

theorem TauCeti.Huber.PairOfDefinition.Presentation.toCompletionLocTopHom_eq {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : PairOfDefinition A} (p : P.Presentation) : p.toCompletionLocTopHom = CategoryTheory.CategoryStruct.comp ⟨P.toCompletionLoc p.num p.den (Localization.Away p.den) ⋯, ⋯⟩ (CategoryTheory.eqToHom ⋯)

The defining equation of Presentation.toCompletionLocTopHom: the structure map toCompletionLoc, transported across completionLocObj_obj.

theorem TauCeti.Huber.PairOfDefinition.Presentation.hom_ext {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : PairOfDefinition A} (p : P.Presentation) {X : CompleteSeparatedTopCommRingCat} {f g : p.completionLocObj ⟶ X} (h : CategoryTheory.CategoryStruct.comp p.toCompletionLocTopHom f.hom = CategoryTheory.CategoryStruct.comp p.toCompletionLocTopHom g.hom) : f = g

Morphisms out of A⟨p⟩ are determined by their composites with the structure map.

theorem TauCeti.Huber.PairOfDefinition.Presentation.toCompletionLocTopHom_comp_restrictionHom {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : PairOfDefinition A} {p q : P.Presentation} (h : p ≤ q) : CategoryTheory.CategoryStruct.comp p.toCompletionLocTopHom (restrictionHom h).hom = q.toCompletionLocTopHom

Restriction morphisms commute with the structure maps.

theorem TauCeti.Huber.PairOfDefinition.Presentation.toCompletionLocTopHom_comp_restrictionHom_assoc {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : PairOfDefinition A} {p q : P.Presentation} (h : p ≤ q) {Z : TopCommRingCat} (h✝ : q.completionLocObj.obj ⟶ Z) : CategoryTheory.CategoryStruct.comp p.toCompletionLocTopHom (CategoryTheory.CategoryStruct.comp (restrictionHom h).hom h✝) = CategoryTheory.CategoryStruct.comp q.toCompletionLocTopHom h✝

Restriction morphisms commute with the structure maps.

theorem TauCeti.Huber.PairOfDefinition.Presentation.toCompletionLocTopHom_comp_eqToHom_hom {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : PairOfDefinition A} {p q : P.Presentation} (e : p = q) : CategoryTheory.CategoryStruct.comp p.toCompletionLocTopHom (CategoryTheory.eqToHom ⋯).hom = q.toCompletionLocTopHom

The structure map is compatible with the transport along an equality of presentations.

theorem TauCeti.Huber.PairOfDefinition.Presentation.toCompletionLocTopHom_comp_eqToHom_hom_assoc {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : PairOfDefinition A} {p q : P.Presentation} (e : p = q) {Z : TopCommRingCat} (h : q.completionLocObj.obj ⟶ Z) : CategoryTheory.CategoryStruct.comp p.toCompletionLocTopHom (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯).hom h) = CategoryTheory.CategoryStruct.comp q.toCompletionLocTopHom h

The structure map is compatible with the transport along an equality of presentations.

noncomputable def TauCeti.Huber.PairOfDefinition.Presentation.mapHom {A B : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] {P : PairOfDefinition A} {P' : PairOfDefinition B} (φ : A →+* B) (hφ : Continuous ⇑φ) (p : P.Presentation) (q : P'.Presentation) (hden : q.den = φ p.den) (hnum : ∀ t ∈ p.num, φ t ∈ q.num) : p.completionLocObj ⟶ q.completionLocObj

The morphism A⟨p⟩ ⟶ B⟨q⟩ of existsUnique_continuous_ringHom_comp_eq.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.Huber.PairOfDefinition.Presentation.toCompletionLocTopHom_comp_mapHom {A B : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] {P : PairOfDefinition A} {P' : PairOfDefinition B} (φ : A →+* B) (hφ : Continuous ⇑φ) (p : P.Presentation) (q : P'.Presentation) (hden : q.den = φ p.den) (hnum : ∀ t ∈ p.num, φ t ∈ q.num) : CategoryTheory.CategoryStruct.comp p.toCompletionLocTopHom (mapHom φ hφ p q hden hnum).hom = CategoryTheory.CategoryStruct.comp ⟨φ, hφ⟩ q.toCompletionLocTopHom

Presentation.mapHom carries the structure map of p to that of q after φ.

theorem TauCeti.Huber.PairOfDefinition.Presentation.toCompletionLocTopHom_comp_mapHom_assoc {A B : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] {P : PairOfDefinition A} {P' : PairOfDefinition B} (φ : A →+* B) (hφ : Continuous ⇑φ) (p : P.Presentation) (q : P'.Presentation) (hden : q.den = φ p.den) (hnum : ∀ t ∈ p.num, φ t ∈ q.num) {Z : TopCommRingCat} (h : q.completionLocObj.obj ⟶ Z) : CategoryTheory.CategoryStruct.comp p.toCompletionLocTopHom (CategoryTheory.CategoryStruct.comp (mapHom φ hφ p q hden hnum).hom h) = CategoryTheory.CategoryStruct.comp ⟨φ, hφ⟩ (CategoryTheory.CategoryStruct.comp q.toCompletionLocTopHom h)

Presentation.mapHom carries the structure map of p to that of q after φ.

Transporting presentations

noncomputable def TauCeti.ValuationSpectrum.PresentationIndex.map {A B : Type v} [CommRing A] [TopologicalSpace A] [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] {P : Huber.PairOfDefinition A} {P' : Huber.PairOfDefinition B} {Aplus : Subring A} {Bplus : Subring B} (φ : A →+* B) (hφ : Continuous ⇑φ) (hopen : ∀ ⦃J : Ideal A⦄, IsOpen ↑J → IsOpen ↑(Ideal.map φ J)) (hplus : ∀ a ∈ Aplus, φ a ∈ Bplus) {U : TopologicalSpace.Opens ↑(spa Aplus)} {V : TopologicalSpace.Opens ↑(spa Bplus)} (hUV : ∀ (w : ↑(spa Bplus)), spaComap φ hφ Aplus Bplus hplus w ∈ U → w ∈ V) (i : PresentationIndex Aplus U) : PresentationIndex Bplus V

The image under φ of an index of U, as an index of any V containing the preimage of U under the induced map of adic spectra: its presentation is (φ(T), φ(s)) for the presentation (T, s) of the index.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.ValuationSpectrum.PresentationIndex.map_pres_num {A B : Type v} [CommRing A] [TopologicalSpace A] [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] {P : Huber.PairOfDefinition A} {P' : Huber.PairOfDefinition B} {Aplus : Subring A} {Bplus : Subring B} (φ : A →+* B) (hφ : Continuous ⇑φ) (hopen : ∀ ⦃J : Ideal A⦄, IsOpen ↑J → IsOpen ↑(Ideal.map φ J)) (hplus : ∀ a ∈ Aplus, φ a ∈ Bplus) {U : TopologicalSpace.Opens ↑(spa Aplus)} {V : TopologicalSpace.Opens ↑(spa Bplus)} (hUV : ∀ (w : ↑(spa Bplus)), spaComap φ hφ Aplus Bplus hplus w ∈ U → w ∈ V) (i : PresentationIndex Aplus U) : (map φ hφ hopen hplus hUV i).pres.num = Finset.image (⇑φ) i.pres.num

The numerators of the induced index are the images of the numerators.

@[simp]

theorem TauCeti.ValuationSpectrum.PresentationIndex.map_pres_den {A B : Type v} [CommRing A] [TopologicalSpace A] [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] {P : Huber.PairOfDefinition A} {P' : Huber.PairOfDefinition B} {Aplus : Subring A} {Bplus : Subring B} (φ : A →+* B) (hφ : Continuous ⇑φ) (hopen : ∀ ⦃J : Ideal A⦄, IsOpen ↑J → IsOpen ↑(Ideal.map φ J)) (hplus : ∀ a ∈ Aplus, φ a ∈ Bplus) {U : TopologicalSpace.Opens ↑(spa Aplus)} {V : TopologicalSpace.Opens ↑(spa Bplus)} (hUV : ∀ (w : ↑(spa Bplus)), spaComap φ hφ Aplus Bplus hplus w ∈ U → w ∈ V) (i : PresentationIndex Aplus U) : (map φ hφ hopen hplus hUV i).pres.den = φ i.pres.den

The denominator of the induced index is the image of the denominator.

theorem TauCeti.ValuationSpectrum.PresentationIndex.spaBasicOpen_map_pres {A B : Type v} [CommRing A] [TopologicalSpace A] [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] {P : Huber.PairOfDefinition A} {P' : Huber.PairOfDefinition B} {Aplus : Subring A} {Bplus : Subring B} (φ : A →+* B) (hφ : Continuous ⇑φ) (hopen : ∀ ⦃J : Ideal A⦄, IsOpen ↑J → IsOpen ↑(Ideal.map φ J)) (hplus : ∀ a ∈ Aplus, φ a ∈ Bplus) {U : TopologicalSpace.Opens ↑(spa Aplus)} {V : TopologicalSpace.Opens ↑(spa Bplus)} (hUV : ∀ (w : ↑(spa Bplus)), spaComap φ hφ Aplus Bplus hplus w ∈ U → w ∈ V) (i : PresentationIndex Aplus U) : spaBasicOpen Bplus (map φ hφ hopen hplus hUV i).pres.num (map φ hφ hopen hplus hUV i).pres.den = (TopologicalSpace.Opens.map (spaComapTopHom φ hφ hplus)).obj (spaBasicOpen Aplus i.pres.num i.pres.den)

The induced index presents the preimage: the rational open R(φ(T)/φ(s)) presented by the induced index is the preimage of the rational open R(T/s) presented by the original index under the induced map of adic spectra.

theorem TauCeti.ValuationSpectrum.PresentationIndex.map_mono {A B : Type v} [CommRing A] [TopologicalSpace A] [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] {P : Huber.PairOfDefinition A} {P' : Huber.PairOfDefinition B} {Aplus : Subring A} {Bplus : Subring B} (φ : A →+* B) (hφ : Continuous ⇑φ) (hopen : ∀ ⦃J : Ideal A⦄, IsOpen ↑J → IsOpen ↑(Ideal.map φ J)) (hplus : ∀ a ∈ Aplus, φ a ∈ Bplus) {U : TopologicalSpace.Opens ↑(spa Aplus)} {V : TopologicalSpace.Opens ↑(spa Bplus)} (hUV : ∀ (w : ↑(spa Bplus)), spaComap φ hφ Aplus Bplus hplus w ∈ U → w ∈ V) {i j : PresentationIndex Aplus U} (h : i ≤ j) : map φ hφ hopen hplus hUV i ≤ map φ hφ hopen hplus hUV j

PresentationIndex.map preserves refinement.

The comparison maps of presentation limits

theorem TauCeti.ValuationSpectrum.presentationLimitπToPresentation_comp_eq {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} {W : TopologicalSpace.Opens ↑(spa Aplus)} {X : CompleteSeparatedTopCommRingCat} {k₁ k₂ : PresentationIndex Aplus W} (hk : k₁ ≤ k₂) {f₁ : k₁.pres.completionLocObj ⟶ X} {f₂ : k₂.pres.completionLocObj ⟶ X} (hf : CategoryTheory.CategoryStruct.comp k₁.pres.toCompletionLocTopHom f₁.hom = CategoryTheory.CategoryStruct.comp k₂.pres.toCompletionLocTopHom f₂.hom) : CategoryTheory.CategoryStruct.comp (presentationLimitπToPresentation Aplus W k₁) f₁ = CategoryTheory.CategoryStruct.comp (presentationLimitπToPresentation Aplus W k₂) f₂

Two projections of presentationLimit followed by maps agreeing on A agree, when the first index is refined by the second.

theorem TauCeti.ValuationSpectrum.toCompletionLocTopHom_comp_homOfRationalSubsetSubset {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) {p q : P.Presentation} (h : rationalSubset Aplus q.num q.den ⊆ rationalSubset Aplus p.num p.den) : CategoryTheory.CategoryStruct.comp p.toCompletionLocTopHom (homOfRationalSubsetSubset Aplus hAplus h).hom = q.toCompletionLocTopHom

The comparison morphism of a containment of rational subsets commutes with the structure maps.

theorem TauCeti.ValuationSpectrum.toCompletionLocTopHom_comp_homOfRationalSubsetSubset_assoc {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) {p q : P.Presentation} (h : rationalSubset Aplus q.num q.den ⊆ rationalSubset Aplus p.num p.den) {Z : TopCommRingCat} (h✝ : q.completionLocObj.obj ⟶ Z) : CategoryTheory.CategoryStruct.comp p.toCompletionLocTopHom (CategoryTheory.CategoryStruct.comp (homOfRationalSubsetSubset Aplus hAplus h).hom h✝) = CategoryTheory.CategoryStruct.comp q.toCompletionLocTopHom h✝

The comparison morphism of a containment of rational subsets commutes with the structure maps.

theorem TauCeti.ValuationSpectrum.presentationLimitπToPresentation_comp_eq_of_subset {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) {W : TopologicalSpace.Opens ↑(spa Aplus)} {X : CompleteSeparatedTopCommRingCat} {k₁ k₂ : PresentationIndex Aplus W} (hk : rationalSubset Aplus k₁.pres.num k₁.pres.den ⊆ rationalSubset Aplus k₂.pres.num k₂.pres.den) {f₁ : k₁.pres.completionLocObj ⟶ X} {f₂ : k₂.pres.completionLocObj ⟶ X} (hf : CategoryTheory.CategoryStruct.comp k₁.pres.toCompletionLocTopHom f₁.hom = CategoryTheory.CategoryStruct.comp k₂.pres.toCompletionLocTopHom f₂.hom) : CategoryTheory.CategoryStruct.comp (presentationLimitπToPresentation Aplus W k₁) f₁ = CategoryTheory.CategoryStruct.comp (presentationLimitπToPresentation Aplus W k₂) f₂

Two projections of presentationLimit followed by maps agreeing on A agree, when the rational subset of the first index lies in that of the second and A⁺ consists of power-bounded elements.