The ring of two-sided restricted series A⟨X, X⁻¹⟩ #
TauCeti.Huber.twoSidedRestrictedSubmodule A A is the A-module of coefficient families
underlying Wedhorn's A⟨X, X⁻¹⟩ (Example 6.39). This module equips it with the convolution
product (fg)ₙ = ∑_{i + j = n} aᵢ bⱼ, making it a ring, and a commutative A-algebra when A is
commutative, in which the Laurent variable X = twoSidedMonomial 1 1 is a unit.
Main definitions #
TauCeti.Huber.twoSidedRestrictedSubmodule.instMulandTauCeti.Huber.twoSidedRestrictedSubmodule.instOne: the product and the unit.TauCeti.Huber.twoSidedRestrictedSubmodule.instRing,TauCeti.Huber.twoSidedRestrictedSubmodule.instCommRingandTauCeti.Huber.twoSidedRestrictedSubmodule.instAlgebra: the ring structure ofA⟨X, X⁻¹⟩, and its commutativeA-algebra structure whenAis commutative.TauCeti.Huber.twoSidedMonomial: the monomiala Xⁿ.
Main results #
TauCeti.Huber.twoSidedMonomial_mul_twoSidedMonomial: monomials multiply by adding degrees,(a Xᵐ)(b Xⁿ) = ab X^{m+n}.TauCeti.Huber.isUnit_twoSidedMonomial: a monomial with a unit coefficient is a unit.TauCeti.Huber.twoSidedRestrictedMul_apply: the bilinear mapTauCeti.Huber.twoSidedRestrictedMulis the ring multiplication.
Implementation notes #
The product is not the pointwise product of ℤ → A, so A⟨X, X⁻¹⟩ is not a subring of ℤ → A;
the multiplication is installed directly on the submodule's coercion to a type.
The unit and the monomials, with their additive and scalar laws, need only continuous addition
and scalar multiplication. The product and the monomial rule need a nonarchimedean ring
topology; each coefficient of a product is a tsum, which is 0 if the sum diverges. The ring
axioms assume A complete and T0, so that these sums converge; this is Wedhorn's convention, his
"complete" including Hausdorff (Definition 5.31).
References #
- T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Example 6.39.
The unit of A⟨X, X⁻¹⟩: the constant series 1 = 1 · X⁰.
The coefficient family of the unit is supported at degree 0 with value 1.
The monomial a Xⁿ of A⟨X, X⁻¹⟩: the family supported at degree n with value a.
The Laurent variable X is twoSidedMonomial 1 1.
Equations
- TauCeti.Huber.twoSidedMonomial n a = ⟨Pi.single n a, ⋯⟩
Instances For
The coefficient family of the monomial a Xⁿ is Pi.single n a.
The degree-0 monomial with coefficient 1 is the unit: 1 · X⁰ = 1.
The monomial with coefficient 0 is 0.
The monomial a Xⁿ is additive in its coefficient.
Scaling a monomial scales its coefficient: a • b Xⁿ = (ab) Xⁿ.
The monomial a Xⁿ commutes with negating its coefficient.
The product on A⟨X, X⁻¹⟩: the coefficient convolution (fg)ₙ = ∑_{i + j = n} aᵢ bⱼ.
Equations
- TauCeti.Huber.twoSidedRestrictedSubmodule.instMul = { mul := fun (f g : ↥(TauCeti.Huber.twoSidedRestrictedSubmodule A A)) => ⟨DiscreteConvolution.addRingConvolution ↑f ↑g, ⋯⟩ }
The coefficient family of a product is the convolution of the coefficient families.
Monomials multiply by adding degrees: (a Xᵐ)(b Xⁿ) = ab X^{m+n}.
A⟨X, X⁻¹⟩ is a ring (Wedhorn, Example 6.39): the additive group of the submodule, with
the convolution product instMul and the unit instOne.
Equations
- One or more equations did not get rendered due to their size.
A monomial with a unit coefficient is a unit of A⟨X, X⁻¹⟩: the inverse of a Xⁿ is
b X⁻ⁿ for the inverse b of a. In particular the Laurent variable twoSidedMonomial 1 1 is a
unit (Wedhorn, Example 6.39).
The bilinear convolution twoSidedRestrictedMul is the multiplication of A⟨X, X⁻¹⟩.
A⟨X, X⁻¹⟩ is commutative when A is (Wedhorn, Example 6.39).
Equations
- TauCeti.Huber.twoSidedRestrictedSubmodule.instCommRing = { toRing := TauCeti.Huber.twoSidedRestrictedSubmodule.instRing, mul_comm := ⋯ }
A⟨X, X⁻¹⟩ is an A-algebra (Wedhorn, Example 6.39), with the coefficientwise scalar
action it carries as a submodule of ℤ → A.
The structure map sends a to the constant series a = a · X⁰.
The degree-0 monomial a X⁰ is the constant series a, the image of a under the structure
map.