Multiplicative properties of Hahn series #
If Γ
is ordered and R
has zero, then HahnSeries Γ R
consists of formal series over Γ
with
coefficients in R
, whose supports are partially well-ordered. This module introduces
multiplication and scalar multiplication on Hahn series. If Γ
is an ordered cancellative
commutative additive monoid and R
is a semiring, then we get a semiring structure on
HahnSeries Γ R
. If Γ
has an ordered vector-addition on Γ'
and R
has a scalar multiplication
on V
, we define HahnModule Γ' R V
as a type alias for HahnSeries Γ' V
that admits a scalar
multiplication from HahnSeries Γ R
. The scalar action of R
on HahnSeries Γ R
is compatible
with the action of HahnSeries Γ R
on HahnModule Γ' R V
.
Main Definitions #
HahnModule
is a type alias forHahnSeries
, which we use for defining scalar multiplication ofHahnSeries Γ R
onHahnModule Γ' R V
for anR
-moduleV
, whereΓ'
admits an ordered cancellative vector addition operation fromΓ
. The type alias allows us to avoid a potential instance diamond.HahnModule.of
is the isomorphism fromHahnSeries Γ V
toHahnModule Γ R V
.HahnSeries.C
is theconstant term
ring homomorphismR →+* HahnSeries Γ R
.HahnSeries.embDomainRingHom
is the ring homomorphismHahnSeries Γ R →+* HahnSeries Γ' R
induced by an order embeddingΓ ↪o Γ'
.
Main results #
- If
R
is a (commutative) (semi-)ring, then so isHahnSeries Γ R
. - If
V
is anR
-module, thenHahnModule Γ' R V
is aHahnSeries Γ R
-module.
TODO #
The following may be useful for composing vertex operators, but they seem to take time.
- rightTensorMap:
HahnModule Γ' R U ⊗[R] V →ₗ[R] HahnModule Γ' R (U ⊗[R] V)
- leftTensorMap:
U ⊗[R] HahnModule Γ' R V →ₗ[R] HahnModule Γ' R (U ⊗[R] V)
References #
Equations
- HahnSeries.instOne = { one := (HahnSeries.single 0) 1 }
Alias of HahnSeries.coeff_one
.
We introduce a type alias for HahnSeries
in order to work with scalar multiplication by
series. If we wrote a SMul (HahnSeries Γ R) (HahnSeries Γ V)
instance, then when
V = HahnSeries Γ R
, we would have two different actions of HahnSeries Γ R
on HahnSeries Γ V
.
See Mathlib.Algebra.Polynomial.Module
for more discussion on this problem.
Equations
- HahnModule Γ R V = HahnSeries Γ V
Instances For
The casting function to the type synonym.
Equations
- HahnModule.of R = Equiv.refl (HahnSeries Γ V)
Instances For
Recursion principle to reduce a result about the synonym to the original type.
Equations
- HahnModule.rec h x = h ((HahnModule.of R).symm x)
Instances For
Equations
Equations
- HahnModule.instBaseSMul = inferInstanceAs (SMul R (HahnSeries Γ V))
Equations
- One or more equations did not get rendered due to their size.
Alias of HahnModule.coeff_smul
.
Equations
Equations
- HahnModule.instSMulZeroClass = { toSMul := HahnModule.instSMul, smul_zero := ⋯ }
Alias of HahnModule.coeff_smul_right
.
Alias of HahnModule.coeff_smul_left
.
Equations
- HahnModule.instDistribSMul = { toSMulZeroClass := HahnModule.instSMulZeroClass, smul_add := ⋯ }
Alias of HahnModule.coeff_single_smul_vadd
.
Alias of HahnModule.coeff_single_zero_smul
.
Alias of HahnModule.coeff_smul_order_add_order
.
Equations
- HahnSeries.instMul = { mul := fun (x y : HahnSeries Γ R) => (HahnModule.of R).symm (x • (HahnModule.of R) y) }
Alias of HahnSeries.coeff_mul
.
Alias of HahnSeries.coeff_mul_left'
.
Alias of HahnSeries.coeff_mul_right'
.
Equations
- HahnSeries.instDistrib = { toMul := inferInstanceAs (Mul (HahnSeries Γ R)), toAdd := inferInstanceAs (Add (HahnSeries Γ R)), left_distrib := ⋯, right_distrib := ⋯ }
Alias of HahnSeries.coeff_single_mul_add
.
Alias of HahnSeries.coeff_mul_single_add
.
Alias of HahnSeries.coeff_mul_single_zero
.
Alias of HahnSeries.coeff_single_zero_mul
.
Alias of HahnSeries.coeff_mul_order_add_order
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- HahnSeries.instNonUnitalSemiring = { toNonUnitalNonAssocSemiring := inferInstanceAs (NonUnitalNonAssocSemiring (HahnSeries Γ R)), mul_assoc := ⋯ }
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- HahnSeries.instNonUnitalCommSemiring = { toNonUnitalSemiring := inferInstance, mul_comm := ⋯ }
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- HahnSeries.instNonUnitalRing = { toNonUnitalNonAssocRing := inferInstanceAs (NonUnitalNonAssocRing (HahnSeries Γ R)), mul_assoc := ⋯ }
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- HahnModule.instBaseModule = inferInstanceAs (Module R (HahnSeries Γ' V))
Equations
- HahnModule.instModule = { toSMul := SMulZeroClass.toSMul, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }
C a
is the constant Hahn Series a
. C
is provided as a ring homomorphism.
Equations
- HahnSeries.C = { toFun := ⇑(HahnSeries.single 0), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
Instances For
Extending the domain of Hahn series is a ring homomorphism.
Equations
- HahnSeries.embDomainRingHom f hfi hf = { toFun := HahnSeries.embDomain { toFun := ⇑f, inj' := hfi, map_rel_iff' := ⋯ }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
Instances For
Equations
- HahnSeries.instAlgebra = { toSMul := HahnSeries.instSMul, algebraMap := HahnSeries.C.comp (algebraMap R A), commutes' := ⋯, smul_def' := ⋯ }
Extending the domain of Hahn series is an algebra homomorphism.
Equations
- HahnSeries.embDomainAlgHom f hfi hf = { toRingHom := HahnSeries.embDomainRingHom f hfi hf, commutes' := ⋯ }