A⟨X⟩_T is a Huber ring #
For a Huber ring A with pair of definition (A₀, I), the ring A⟨X₁,…,Xₖ⟩_T of weighted
restricted power series is again a Huber ring, with pair of definition
(A₀⟨X⟩_T, I⟨X⟩_T), Iⁿ⟨X⟩_T = {f; coeff ν f ∈ Tν · Iⁿ for every ν}.
The content is the identification of the neighbourhood subgroups with the powers of one finitely generated ideal:
(I⟨X⟩_T) ^ n = Iⁿ⟨X⟩_T.
The inclusion ⊆ is coefficientwise multiplication. The reverse inclusion is where finite
generation of I is used, and it is not a formal consequence of it: a series whose coefficients
all lie in Iⁿ⁺¹ must be written as a combination of finitely many generators with cofactors that
are themselves restricted series, so the cofactors have to tend to zero. They are obtained by
decomposing each coefficient not at the uniform level n + 1 but at the level n + 1 + m ν that
the coefficient actually attains, cut off at the degree of ν so that the level is attained;
a private level-selection lemma packages that choice.
A pseudouniformiser of A stays one in A⟨X⟩_T as a constant series, so the Tate property is
inherited too. Since completion preserves both properties
(TauCeti.Huber.IsHuberRing.completion, TauCeti.Huber.IsTateRing.completion), the completed
algebra A⟨X₁,…,Xₖ⟩ — the separated completion of the trivial-weight A⟨X⟩_T — is
a Huber ring, Tate whenever A is; its completeness and separatedness are those of any separated
completion and need no argument here.
Main definitions #
TauCeti.Huber.PairOfDefinition.weightedRingOfDefinition:A₀⟨X⟩_T, the ring of definition, with its structure mapTauCeti.Huber.PairOfDefinition.weightedRingOfDefinitionCfromA₀.TauCeti.Huber.PairOfDefinition.weightedIdeal:Iⁿ⟨X⟩_T, as an ideal ofA₀⟨X⟩_T. The ideal of definition is the casen = 1.TauCeti.Huber.PairOfDefinition.weighted: the pair of definition ofA⟨X⟩_T.
Main results #
TauCeti.Huber.PairOfDefinition.exists_sum_weightedRingOfDefinitionC_mul: the decomposition of a series over generators ofI, with restricted cofactors.TauCeti.Huber.PairOfDefinition.weightedIdeal_one_pow:(I⟨X⟩_T) ^ n = Iⁿ⟨X⟩_T, from which both the finite generation of the ideal of definition (TauCeti.Huber.PairOfDefinition.fg_weightedIdeal_one) and its adicity (TauCeti.Huber.PairOfDefinition.isAdic_weightedIdeal_one) follow.TauCeti.Huber.isHuberRing_weightedRestrictedSubringandTauCeti.Huber.isTateRing_weightedRestrictedSubring: the two instances. The completed algebraA⟨X₁,…,Xₖ⟩at the trivial weight inherits both from them by synthesis, with no separate result: see theexamples at the end of the file.
Provenance #
The coefficient decomposition reuses TauCeti.Huber.exists_sum_eq_of_mem_span_mul, proved for
Wedhorn Remark 6.8 — the Huber structure on the completion  — and serves the same purpose here:
it bounds, uniformly in the level, the number of generators a decomposition needs.
References #
- T. Wedhorn, Adic Spaces, Remark and Definition 5.48 for
A⟨X⟩_T, Example 5.54 for the trivial weight, and Proposition and Definition 6.1 for pairs of definition.
The coefficient decomposition #
One weighted coefficient, decomposed. The same decomposition through the weight: an
element of Tν · Iⁿ⁺¹ is a combination of the generators with cofactors in Tν · Iⁿ.
The weight is carried by the cofactors, which is what keeps the decomposition inside the
neighbourhood subgroup indexed by the same ν.
The pair of definition of A⟨X⟩_T #
A₀⟨X⟩_T, the ring of definition of A⟨X⟩_T: the series all of whose coefficients meet
the A₀ bound.
Its carrier is the neighbourhood subgroup TauCeti.Huber.weightedNhd of A₀, which is what makes
it open; that it is a subring is coefficientwise multiplicativity of A₀.
Equations
- P.weightedRingOfDefinition hT = { carrier := ↑(TauCeti.Huber.weightedNhd T hT P.ringOfDefinition.toAddSubgroup), mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
Instances For
Membership in A₀⟨X⟩_T is the A₀ bound on every coefficient.
The constant series A₀ → A₀⟨X⟩_T, the structure map of the ring of definition.
Equations
- P.weightedRingOfDefinitionC hT = ((TauCeti.Huber.weightedC T hT).comp P.ringOfDefinition.subtype).codRestrict (P.weightedRingOfDefinition hT) ⋯
Instances For
Iⁿ⟨X⟩_T, an ideal of A₀⟨X⟩_T: the series all of whose coefficients meet the Iⁿ
bound. The ideal of definition of A⟨X⟩_T is the case n = 1; the general n is named because
the point of the file is that these are its powers
(TauCeti.Huber.PairOfDefinition.weightedIdeal_one_pow).
Equations
- P.weightedIdeal hT n = { carrier := {f : ↥(P.weightedRingOfDefinition hT) | ↑f ∈ TauCeti.Huber.weightedNhd T hT (P.idealImage n)}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
Instances For
Membership in Iⁿ⟨X⟩_T is the Iⁿ bound on every coefficient.
A constant series with value in Iⁿ lies in Iⁿ⟨X⟩_T.
At n = 0 the bound is the A₀ bound, so I⁰⟨X⟩_T is all of A₀⟨X⟩_T.
The bounds are nested: Iⁿ⟨X⟩_T ⊆ Iᵐ⟨X⟩_T for m ≤ n.
The bounds multiply: Iᵃ⟨X⟩_T · Iᵇ⟨X⟩_T ⊆ Iᵃ⁺ᵇ⟨X⟩_T. This is one half of
TauCeti.Huber.PairOfDefinition.weightedIdeal_one_pow, and needs no finiteness.
The decomposition of a series. A series all of whose coefficients meet the Iⁿ⁺¹ bound is
a combination, with cofactors in Iⁿ⟨X⟩_T, of the constant series attached to a finite generating
set G of I.
This is the mathematical content of the file. The cofactors are restricted series because each
coefficient is decomposed at the level it attains; decomposing every coefficient at the uniform
level n + 1 would leave the cofactors with no reason to tend to zero.
The reverse inclusion of TauCeti.Huber.PairOfDefinition.weightedIdeal_one_pow, read off the
decomposition TauCeti.Huber.PairOfDefinition.exists_sum_weightedRingOfDefinitionC_mul.
The neighbourhood subgroups are the powers of one ideal: (I⟨X⟩_T) ^ n = Iⁿ⟨X⟩_T.
Both inclusions go by induction on n, the step being
TauCeti.Huber.PairOfDefinition.weightedIdeal_mul_le one way and
TauCeti.Huber.PairOfDefinition.weightedIdeal_succ_le_mul the other.
The ideal of definition is finitely generated: I⟨X⟩_T is generated by the constant series
attached to a finite generating set of I.
The generators lie in the ideal, and the reverse containment is the decomposition of a series at
n = 0, where the cofactors are unconstrained.
The Huber and Tate structures #
A₀⟨X⟩_T is open in A⟨X⟩_T.
Each Iⁿ⟨X⟩_T is open in A₀⟨X⟩_T.
The subspace topology on A₀⟨X⟩_T is the I⟨X⟩_T-adic topology.
The powers of I⟨X⟩_T are the neighbourhood subgroups by
TauCeti.Huber.PairOfDefinition.weightedIdeal_one_pow, and those are cofinal among the
neighbourhoods of zero because the Iⁿ are cofinal in A.
The pair of definition of A⟨X⟩_T: (A₀⟨X⟩_T, I⟨X⟩_T).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Membership in the ideal of definition of the pair (A₀⟨X⟩_T, I⟨X⟩_T) is membership in
I⟨X⟩_T.
Stated as a membership characterisation rather than an equation because the type of
idealOfDefinition depends on ringOfDefinition, exactly as
TauCeti.Huber.PairOfDefinition.mem_completion_idealOfDefinition is.
A⟨X⟩_T is a Huber ring when A is: a pair of definition of A gives one of A⟨X⟩_T, by
TauCeti.Huber.PairOfDefinition.weighted.
A⟨X⟩_T is a Tate ring when A is: a pseudouniformiser of A is one of A⟨X⟩_T as a
constant series, a unit there and topologically nilpotent by continuity of weightedC.