Comparing A⟨X₁,…,X_{k+m}⟩ with A⟨X₁,…,Xₖ⟩⟨Y₁,…,Y_m⟩ #
Splitting the variables of a completed restricted power-series algebra into a first block of k
and a second of m presents the algebra in k + m variables as an algebra in m variables over
the algebra in k. This file constructs the two comparison maps
A⟨X₁,…,X_{k+m}⟩ ⟶ A⟨X₁,…,Xₖ⟩⟨Y₁,…,Y_m⟩ and A⟨X₁,…,Xₖ⟩⟨Y₁,…,Y_m⟩ ⟶ A⟨X₁,…,X_{k+m}⟩
and proves them mutually inverse, so that A⟨X⟩⟨Y⟩ ≅ A⟨X,Y⟩.
The first carries Xᵢ to the i-th variable of the inner algebra read as a constant series of
the outer one when i < k, and to the corresponding variable of the outer algebra when i ≥ k.
The second carries the j-th variable of the outer algebra to X_{k+j}, and is a map over
A⟨X₁,…,Xₖ⟩ through the inclusion of the first block of variables.
Main definitions #
TauCeti.Huber.iterateVar: the generators ofA⟨X₁,…,Xₖ⟩⟨Y₁,…,Y_m⟩, indexed byFin (k + m)as those ofA⟨X₁,…,X_{k+m}⟩are.TauCeti.Huber.iterateStructureHom: the structure mapA → A⟨X₁,…,Xₖ⟩⟨Y₁,…,Y_m⟩, the composite of the two the iterated algebra is built from.TauCeti.Huber.iterateSplitHom: the comparison map that splits the variables.TauCeti.Huber.iterateFirstBlockHom: the inclusionA⟨X₁,…,Xₖ⟩ → A⟨X₁,…,X_{k+m}⟩of the first block, which the map below is taken over.TauCeti.Huber.iterateJoinHom: the comparison map that joins them.TauCeti.Huber.iterateRingEquiv: the isomorphism the two assemble into, withTauCeti.Huber.iterateAlgEquivitsA-algebra form.
Main results #
TauCeti.Huber.isPowerBounded_iterateVar: every generator of the iterated algebra is power-bounded in it, which is what Proposition 5.50 asks of the tuple.TauCeti.Huber.continuous_iterateSplitHomandTauCeti.Huber.continuous_iterateJoinHom, withTauCeti.Huber.continuous_iterateFirstBlockHom: all three are morphisms of topological rings.TauCeti.Huber.iterateSplitHom_coe_weightedC,…_coe_weightedXand theiriterateJoinHomanditerateFirstBlockHomcounterparts, withTauCeti.Huber.iterateVar_castAddandTauCeti.Huber.iterateVar_natAddfor the two blocks of generators: the values on the generators. The bodies of the definitions are not exported, so these are how a consumer computes with the maps.TauCeti.Huber.iterateJoinHom_comp_iterateSplitHomandTauCeti.Huber.iterateSplitHom_comp_iterateJoinHom: the two maps are mutually inverse, withTauCeti.Huber.iterateSplitHom_comp_iterateFirstBlockHomidentifying the composite of the splitting with the inclusion of the first block as the structure map of the iterate.TauCeti.Huber.continuous_iterateRingEquivand itssymm, with the_coeand_apply@[simp]lemmas: the isomorphism is one of topological rings, and it isiterateSplitHomwith inverseiterateJoinHom.TauCeti.Huber.iterateSplitHom_comp_algebraMap: the comparison carries the structure map ofA⟨X₁,…,X_{k+m}⟩to that of the iterate, which is what makes it a map ofA-algebras. The iterate carries noAlgebra Ainstance —Algebradoes not compose transitively — soiterateAlgEquivsupplies the one its structure map induces, andTauCeti.Huber.iterateAlgEquiv_toRingEquivwith its two_applyforms says that this changes nothing but the bundling.
References #
- T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Proposition 5.50, whose completed form both maps apply.
The generators of A⟨X₁,…,Xₖ⟩⟨Y₁,…,Y_m⟩, indexed as those of A⟨X₁,…,X_{k+m}⟩.
Equations
- One or more equations did not get rendered due to their size.
Instances For
On the first block the generator is the i-th variable of the inner algebra, read as a
constant series of the outer one.
On the second block the generator is the j-th variable of the outer algebra.
Each generator is power-bounded.
The structure map A → A⟨X₁,…,Xₖ⟩⟨Y₁,…,Y_m⟩, the composite of the two structure maps the
iterated algebra is built from.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The structure map of the iterated algebra is continuous.
The comparison map A⟨X₁,…,X_{k+m}⟩ → A⟨X₁,…,Xₖ⟩⟨Y₁,…,Y_m⟩.
Equations
Instances For
The comparison map is continuous.
The comparison map sends a constant to the corresponding constant.
The comparison map sends Xᵢ to the i-th generator of the iterated algebra: for i < k
the i-th variable of the inner algebra, read as a constant of the outer one, and for i ≥ k
the variable of the outer algebra.
Joining the variables #
The inclusion of the first block of variables, A⟨X₁,…,Xₖ⟩ → A⟨X₁,…,X_{k+m}⟩: the unique
continuous homomorphism over A carrying Xᵢ to Xᵢ.
Equations
Instances For
The inclusion of the first block of variables is continuous.
The comparison map A⟨X₁,…,Xₖ⟩⟨Y₁,…,Y_m⟩ → A⟨X₁,…,X_{k+m}⟩: the unique continuous
homomorphism over A⟨X₁,…,Xₖ⟩ — through the inclusion of the first block — carrying Y_j to
X_{k+j}.
Equations
Instances For
The join map is continuous.
The join map sends a constant series of the outer algebra to the image of its value under the inclusion of the first block.
The join map sends the j-th variable of the outer algebra to X_{k+j}.
The inclusion of the first block sends Xᵢ to Xᵢ.
The inclusion of the first block is a map of A-algebras.
The two maps are mutually inverse #
The structure map of the iterated algebra is the constant series of a constant series.
Joining after splitting is the identity on A⟨X₁,…,X_{k+m}⟩.
Splitting after including the first block is the structure map of the iterated algebra over
A⟨X₁,…,Xₖ⟩: the two agree on the constants and on the variables of A⟨X₁,…,Xₖ⟩.
Splitting after joining is the identity on A⟨X₁,…,Xₖ⟩⟨Y₁,…,Y_m⟩.
The iteration isomorphism A⟨X₁,…,X_{k+m}⟩ ≃+* A⟨X₁,…,Xₖ⟩⟨Y₁,…,Y_m⟩.
Equations
- TauCeti.Huber.iterateRingEquiv k m A = RingEquiv.ofRingHom (TauCeti.Huber.iterateSplitHom k m A) (TauCeti.Huber.iterateJoinHom k m A) ⋯ ⋯
Instances For
The iteration isomorphism is TauCeti.Huber.iterateSplitHom.
The pointwise form of TauCeti.Huber.iterateRingEquiv_coe.
The inverse of the iteration isomorphism is TauCeti.Huber.iterateJoinHom.
The pointwise form of TauCeti.Huber.iterateRingEquiv_symm_coe.
The iteration isomorphism is an isomorphism of topological rings.
Its inverse is continuous too.
As a map of A-algebras #
The comparison map carries the structure map of A⟨X₁,…,X_{k+m}⟩ to the structure map of
the iterated algebra, so it is a map of A-algebras.
The iteration isomorphism as an equivalence of A-algebras.
The algebra structure on the iterate is the one its structure map induces: Algebra does not
compose transitively, so A⟨X₁,…,Xₖ⟩⟨Y₁,…,Y_m⟩ carries no Algebra A instance of its own and the
statement supplies it.
Equations
Instances For
The algebra equivalence is the ring equivalence.
The pointwise form of TauCeti.Huber.iterateAlgEquiv_toRingEquiv.
The inverse of the algebra equivalence is the inverse of the ring equivalence.