The tensor topology of Huber rings along adic homomorphisms #
Let A → B and A → C be adic homomorphisms of Huber rings. Choose a pair of definition
(A₀, I) of A and pairs of definition (B₀, I B₀) of B and (C₀, I C₀) of C with
A₀ → B₀ and A₀ → C₀ (a TauCeti.Huber.TensorDatum). In E = B ⊗[A] C let F be the subring
generated by the images of B₀ and C₀, that is the image of B₀ ⊗[A₀] C₀, and let J = I F.
The images in E of the powers Jⁿ are a basis of neighbourhoods of zero for a ring topology on
E, for which (F, J) is a pair of definition and both inclusions B → E and C → E are adic.
This topology does not depend on the chosen pairs of definition
(TauCeti.Huber.TensorDatum.topology_eq), and compatible pairs exist as soon as both structure
maps are adic. The result is the tensor topology TauCeti.Huber.tensorTopology A B C. Its
Hausdorff completion is Huber's completed tensor product B ⊗̂_A C, the affinoid form of the
fibre product of adic spaces.
Main definitions #
TauCeti.Huber.TensorDatum A B C: compatible pairs of definition ofA,BandC.TauCeti.Huber.TensorDatum.ringOfDefinition,TauCeti.Huber.TensorDatum.idealOfDefinition: the subringFofB ⊗[A] Cand its idealJ = I F.TauCeti.Huber.TensorDatum.topology: the topology onB ⊗[A] Cwhose neighbourhoods of zero are the images of the powers ofJ.TauCeti.Huber.TensorDatum.pairOfDefinition:(F, J)as a pair of definition.TauCeti.Huber.tensorTopology A B C: the tensor topology, for adic structure maps.
Main results #
TauCeti.Huber.TensorDatum.isTopologicalRing,TauCeti.Huber.TensorDatum.isHuberRing: the topology of a datum makesB ⊗[A] Ca Huber ring.TauCeti.Huber.TensorDatum.isAdicHom_includeLeft,TauCeti.Huber.TensorDatum.isAdicHom_includeRight: the two inclusions are adic.TauCeti.Huber.TensorDatum.topology_eq: the topology does not depend on the datum.TauCeti.Huber.hasBasis_tensorTopology: every datum gives a neighbourhood basis of zero for the tensor topology.
References #
- R. Huber, A generalization of formal schemes and rigid analytic varieties, Math. Z. 217 (1994), §3, proof of Lemma 3.9(i).
- R. Huber, Étale cohomology of rigid analytic varieties and adic spaces, Aspects of Mathematics E30 (1996), §1.2, proof of Proposition 1.2.2(1).
- S. Morel, Adic spaces, §II.3.2, Proposition II.3.2.1.
Pairs of definition of A, B and C compatible with the structure maps A → B and
A → C: the ring of definition of A maps into those of B and C, and the ideal of
definition of A generates theirs. Such data define the tensor topology on B ⊗[A] C; they
make both structure maps adic, and they exist when both structure maps are adic
(TauCeti.Huber.TensorDatum.nonempty).
- base : PairOfDefinition A
The pair of definition
(A₀, I)ofA. - left : PairOfDefinition B
The pair of definition
(B₀, I B₀)ofB. - right : PairOfDefinition C
The pair of definition
(C₀, I C₀)ofC. - algebraMap_mem_left (a : A) : a ∈ self.base.ringOfDefinition → (algebraMap A B) a ∈ self.left.ringOfDefinition
The ring of definition of
Amaps into that ofB. - algebraMap_mem_right (a : A) : a ∈ self.base.ringOfDefinition → (algebraMap A C) a ∈ self.right.ringOfDefinition
The ring of definition of
Amaps into that ofC. - map_idealOfDefinition_left : Ideal.map ((algebraMap A B).restrict self.base.ringOfDefinition self.left.ringOfDefinition ⋯) self.base.idealOfDefinition = self.left.idealOfDefinition
The ideal of definition of
Bis generated by the image of that ofA. - map_idealOfDefinition_right : Ideal.map ((algebraMap A C).restrict self.base.ringOfDefinition self.right.ringOfDefinition ⋯) self.base.idealOfDefinition = self.right.idealOfDefinition
The ideal of definition of
Cis generated by the image of that ofA.
Instances For
The structure map A → B of a tensor datum is adic.
The structure map A → C of a tensor datum is adic.
The ring and the ideal of definition #
The ring of definition F of B ⊗[A] C: the subring generated by the images of the rings
of definition of B and C.
Instances For
F is the supremum of the images of B₀ and C₀.
F contains the image of B₀.
F contains the image of C₀.
F contains the image of B₀ ⊗[A₀] C₀.
F is the smallest subring containing the image of B₀ ⊗[A₀] C₀.
The ring of definition of a tensor datum is additively generated by the pure tensors of elements of the two rings of definition.
F contains the image of A₀.
The homomorphism A₀ → F induced by the structure map A → B ⊗[A] C.
Instances For
A₀ → F is the restriction of the structure map.
The ideal of definition J = I F of F, generated by the image of the ideal of definition
of A.
Instances For
Unfolding lemma for TauCeti.Huber.TensorDatum.idealOfDefinition.
J is finitely generated, since the ideal of definition of A is.
Induction on Jᵏ: a property of elements of F that holds at zero, is closed under
addition and under multiplication by elements of F, and holds on the image of Iᵏ, holds on
Jᵏ.
The neighbourhoods of zero #
The image in B ⊗[A] C of the power Jⁿ of the ideal of definition.
Instances For
Membership in the image of Jⁿ.
The image of Iⁿ lies in the image of Jⁿ.
The zeroth neighbourhood is F itself.
The images of the powers of J are nested.
Pulling the image of Jⁿ back to F gives Jⁿ.
Every element of B ⊗[A] C multiplies a power of J into F. This is the
left-multiplication condition making the images of the powers of J a RingSubgroupsBasis.
The topology of a tensor datum #
The topology on B ⊗[A] C whose neighbourhoods of zero are the images of the powers of the
ideal of definition J. When A, B and C are topological rings it does not depend on the
datum (TauCeti.Huber.TensorDatum.topology_eq).
Instances For
The images of the powers of J are a basis of neighbourhoods of zero.
The topology of a tensor datum is a ring topology.
The image of each power of J is open.
F is open.
The subspace topology on F is the J-adic topology.
(F, J) is a pair of definition of B ⊗[A] C for the topology of the datum.
Instances For
The ring of definition of pairOfDefinition is F.
The neighbourhoods of zero of pairOfDefinition are the images of the powers of J.
Membership in the ideal of definition of pairOfDefinition is membership in J.
The topology of a tensor datum makes B ⊗[A] C a Huber ring.
The inclusion B → B ⊗[A] C is adic for the topology of a tensor datum: it carries B₀
into F, and I B₀ to the ideal J = I F.
The inclusion C → B ⊗[A] C is adic for the topology of a tensor datum: it carries C₀
into F, and I C₀ to the ideal J = I F.
Independence of the datum #
The tensor topology does not depend on the choice of compatible pairs of definition.
Compatible pairs of definition exist when both structure maps are adic.
The tensor topology #
The tensor topology on B ⊗[A] C, for adic structure maps A → B and A → C: for any
compatible pairs of definition (A₀, I), (B₀, I B₀) and (C₀, I C₀), its neighbourhoods of
zero are generated by the images of Iⁿ F, where F is the image of B₀ ⊗[A₀] C₀
(TauCeti.Huber.hasBasis_tensorTopology). It is not an instance, since B ⊗[A] C may carry
other topologies.
Instances For
The tensor topology is the topology of any tensor datum.
For any tensor datum, the images of the powers of its ideal of definition are a basis of neighbourhoods of zero for the tensor topology.
The tensor topology is a ring topology.
The tensor topology makes B ⊗[A] C a Huber ring.
The inclusion B → B ⊗[A] C is adic for the tensor topology.
The inclusion C → B ⊗[A] C is adic for the tensor topology.