Restriction maps as morphisms of complete separated rings

LocalizationTopology.Restriction builds the restriction map A⟨T/s⟩ → A⟨T''/s''⟩ of a refinement as a continuous ring homomorphism, and LocalizationTopology.CompleteSeparated.Basic exhibits A⟨T/s⟩ as an object of CompleteSeparatedTopCommRingCat. This module joins the two: the restriction map becomes a morphism of that category, and the identity and composition laws of the ring homomorphisms become the identity and composition laws of the morphisms.

Main definitions

• TauCeti.Huber.PairOfDefinition.restrictionObjHom : the restriction map of a refinement, as a morphism completionLocObj … ⟶ completionLocObj ….

Main results

• TauCeti.Huber.PairOfDefinition.restrictionObjHom_congr : the morphism does not depend on the cofactor witnessing the refinement.
• TauCeti.Huber.PairOfDefinition.restrictionObjHom_self : a presentation refines itself and gives the identity morphism.
• TauCeti.Huber.PairOfDefinition.restrictionObjHom_comp_restrictionObjHom : refinements compose, and the morphism of the composite is the composite of the morphisms.

Why the cofactor drops out

restrictionRingHom is indexed by a cofactor r with s'' = s * r, and a refinement can be witnessed by more than one. restrictionObjHom_congr says the morphism is nonetheless a function of the two presentations alone: the underlying ring homomorphism is characterised by continuity and compatibility with the structure maps from A (eq_restrictionRingHom), and neither mentions r. That is what makes the assignment a diagram over a preorder of presentations — the refinement relation, with the cofactor existentially quantified — rather than over a category whose morphisms carry data, and so what lets 𝒪_X be formed as a limit.

References

• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), §8.1–§8.2, for the structure presheaf and its restriction maps.

The restriction morphism

noncomputable def TauCeti.Huber.PairOfDefinition.restrictionObjHom {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) (T : Finset A) (s : A) (S : Type u) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (T'' : Finset A) (s'' : A) (S'' : Type u) [CommRing S''] [Algebra A S''] [IsLocalization.Away s'' S''] (hden'' : P.HasDenominatorPower T'' s'' S'') (r : A) (hs'' : s'' = s * r) (hT : ∀ t ∈ T, t * r ∈ T'') : P.completionLocObj T s S hden ⟶ P.completionLocObj T'' s'' S'' hden''

The restriction map of a refinement, as a morphism of CompleteSeparatedTopCommRingCat. The cofactor r and the two refinement conditions determine the morphism but do not appear in its type; restrictionObjHom_congr shows they do not affect it either.

Equations

• P.restrictionObjHom T s S hden T'' s'' S'' hden'' r hs'' hT = P.completionLocObjHom T s S hden T'' s'' S'' hden'' (P.restrictionRingHom T s S hden T'' s'' S'' hden'' r hs'' hT) ⋯

theorem TauCeti.Huber.PairOfDefinition.restrictionObjHom_congr {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) (T : Finset A) (s : A) (S : Type u) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (T'' : Finset A) (s'' : A) (S'' : Type u) [CommRing S''] [Algebra A S''] [IsLocalization.Away s'' S''] (hden'' : P.HasDenominatorPower T'' s'' S'') (r₁ r₂ : A) (hs₁ : s'' = s * r₁) (hT₁ : ∀ t ∈ T, t * r₁ ∈ T'') (hs₂ : s'' = s * r₂) (hT₂ : ∀ t ∈ T, t * r₂ ∈ T'') : P.restrictionObjHom T s S hden T'' s'' S'' hden'' r₁ hs₁ hT₁ = P.restrictionObjHom T s S hden T'' s'' S'' hden'' r₂ hs₂ hT₂

The morphism does not depend on the cofactor. Two cofactors witnessing the same refinement give the same morphism, because the underlying ring homomorphism is determined by continuity and compatibility with the structure maps from A.

@[simp]

theorem TauCeti.Huber.PairOfDefinition.restrictionObjHom_self {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) (T : Finset A) (s : A) (S : Type u) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) : P.restrictionObjHom T s S hden T s S hden 1 ⋯ ⋯ = CategoryTheory.CategoryStruct.id (P.completionLocObj T s S hden)

The identity law. A presentation refines itself with cofactor 1, and the morphism that gives is the identity of completionLocObj.

@[simp]

theorem TauCeti.Huber.PairOfDefinition.restrictionObjHom_comp_restrictionObjHom {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) (T : Finset A) (s : A) (S : Type u) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (T'' : Finset A) (s'' : A) (S'' : Type u) [CommRing S''] [Algebra A S''] [IsLocalization.Away s'' S''] (hden'' : P.HasDenominatorPower T'' s'' S'') (r : A) (hs'' : s'' = s * r) (hT : ∀ t ∈ T, t * r ∈ T'') (T''' : Finset A) (s''' : A) (S''' : Type u) [CommRing S'''] [Algebra A S'''] [IsLocalization.Away s''' S'''] (hden''' : P.HasDenominatorPower T''' s''' S''') (r₂ : A) (hs''' : s''' = s'' * r₂) (hT₂ : ∀ t ∈ T'', t * r₂ ∈ T''') : CategoryTheory.CategoryStruct.comp (P.restrictionObjHom T s S hden T'' s'' S'' hden'' r hs'' hT) (P.restrictionObjHom T'' s'' S'' hden'' T''' s''' S''' hden''' r₂ hs''' hT₂) = P.restrictionObjHom T s S hden T''' s''' S''' hden''' (r * r₂) ⋯ ⋯

The composition law. A refinement with cofactor r followed by one with cofactor r₂ is a refinement with cofactor r * r₂, and its morphism is the composite. With restrictionObjHom_self this is the functoriality of the assignment.