Hahn series with coefficients on monomial lines

Given units B g of a K-algebra R, indexed by an ordered group Γ and multiplying like monomials up to scalars, the Hahn series over R whose g-th coefficient lies on the line K ∙ B g form a subring. Every nonzero element of this subring has a unit leading coefficient, and a noncommutative geometric series argument inverts it inside the subring, so the subring is a division ring. No commutativity of R is assumed; HahnGeometric adapts Mathlib's HahnSeries.SummableFamily.powers, which requires a commutative coefficient ring.

Main definitions

• QuantumSeries.line: the coefficient line K ∙ B g.
• QuantumSeries.coefficientRing: the subring of Hahn series with coefficients on these lines.
• HahnGeometric.geometricPowers: the summable family of powers of a series of positive order.
• QuantumSeries.divisionRing: the division ring structure on coefficientRing.

Main results

• HahnGeometric.one_sub_self_mul_hsum_geometricPowers: (1 - x) * ∑ xⁿ = 1.
• HahnGeometric.normalized_right_inverse: a right inverse of a series with unit leading coefficient.
• QuantumSeries.coefficientRing_isUnit_or_eq_zero: every element of coefficientRing is a unit or zero.

References

• Adapted from OpenAI's formalization [OAI26a] at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a (file lean/OAI/Computability/RationalHitting/QuantumSeries.lean), via the complexitylib port [Sch26d] at revision add0aca8ee0d71e68969f2cb45cf91554a50f787.
• The geometric series construction HahnGeometric adapts Mathlib's HahnSeries.SummableFamily.powers (Mathlib/RingTheory/HahnSeries/Summable.lean, Copyright (c) 2021 Aaron Anderson, Apache 2.0) from commutative to arbitrary coefficient rings.

def Cslib.Circuits.Rational.QuantumSeries.line {Γ : Type u_1} {K : Type u_2} {R : Type u_3} [Field K] [Ring R] [Algebra K R] (B : Γ → Rˣ) (g : Γ) : Submodule K R

Each exponent has the one-dimensional coefficient line of its ordered quantum monomial. Lexicographic leading terms do not require a domain matrix coefficient ring.

theorem Cslib.Circuits.Rational.QuantumSeries.line_mul {Γ : Type u_1} {K : Type u_2} {R : Type u_3} [AddCommGroup Γ] [Field K] [Ring R] [Algebra K R] (B : Γ → Rˣ) (hB : ∀ (g h : Γ), ∃ (c : K), ↑(B g) * ↑(B h) = c • ↑(B (g + h))) {g h : Γ} {x y : R} (hx : x ∈ line B g) (hy : y ∈ line B h) : x * y ∈ line B (g + h)

theorem Cslib.Circuits.Rational.QuantumSeries.line_isUnit {Γ : Type u_1} {K : Type u_2} {R : Type u_3} [Field K] [Ring R] [Algebra K R] (B : Γ → Rˣ) {g : Γ} {x : R} (hx : x ∈ line B g) (hne : x ≠ 0) : IsUnit x

def Cslib.Circuits.Rational.QuantumSeries.coefficientRing {Γ : Type u_1} {K : Type u_2} {R : Type u_3} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Field K] [Ring R] [Algebra K R] (B : Γ → Rˣ) (h0 : B 0 = 1) (hB : ∀ (g h : Γ), ∃ (c : K), ↑(B g) * ↑(B h) = c • ↑(B (g + h))) : Subring (HahnSeries Γ R)

The Hahn-series subring with each coefficient on its prescribed monomial line.

theorem Cslib.Circuits.Rational.QuantumSeries.coefficientRing_noZeroDivisors {Γ : Type u_1} {K : Type u_2} {R : Type u_3} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Field K] [Ring R] [Algebra K R] [Nontrivial R] (B : Γ → Rˣ) (h0 : B 0 = 1) (hB : ∀ (g h : Γ), ∃ (c : K), ↑(B g) * ↑(B h) = c • ↑(B (g + h))) : NoZeroDivisors ↥(coefficientRing B h0 hB)

Geometric series of Hahn series over a noncommutative ring

This section adapts Mathlib's HahnSeries.SummableFamily.powers and its lemmas (Mathlib/RingTheory/HahnSeries/Summable.lean, by Aaron Anderson), whose coefficient ring must be commutative, to an arbitrary ring of coefficients.

theorem Cslib.Circuits.Rational.HahnGeometric.power_finite_co_support {Γ : Type u_1} {R : Type u_2} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] {x : HahnSeries Γ R} (hx : 0 < x.orderTop) (g : Γ) : {a : ℕ | ((fun (n : ℕ) => x ^ n) a).coeff g ≠ 0}.Finite

noncomputable def Cslib.Circuits.Rational.HahnGeometric.geometricPowers {Γ : Type u_1} {R : Type u_2} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] (x : HahnSeries Γ R) : HahnSeries.SummableFamily Γ R ℕ

The summable family of powers of a Hahn series x. If x does not have positive orderTop, this returns the junk value obtained by pretending x = 0.

@[simp]

theorem Cslib.Circuits.Rational.HahnGeometric.geometricPowers_toFun {Γ : Type u_1} {R : Type u_2} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] (x : HahnSeries Γ R) (n : ℕ) : (geometricPowers x) n = (if 0 < x.orderTop then x else 0) ^ n

theorem Cslib.Circuits.Rational.HahnGeometric.geometricPowers_of_orderTop_pos {Γ : Type u_1} {R : Type u_2} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] {x : HahnSeries Γ R} (hx : 0 < x.orderTop) (n : ℕ) : (geometricPowers x) n = x ^ n

theorem Cslib.Circuits.Rational.HahnGeometric.geometricPowers_of_not_orderTop_pos {Γ : Type u_1} {R : Type u_2} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] {x : HahnSeries Γ R} (hx : ¬0 < x.orderTop) : geometricPowers x = HahnSeries.SummableFamily.single 0 1

@[simp]

theorem Cslib.Circuits.Rational.HahnGeometric.geometricPowers_zero {Γ : Type u_1} {R : Type u_2} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] : geometricPowers 0 = HahnSeries.SummableFamily.single 0 1

@[simp]

theorem Cslib.Circuits.Rational.HahnGeometric.coe_geometricPowers {Γ : Type u_1} {R : Type u_2} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] {x : HahnSeries Γ R} (hx : 0 < x.orderTop) : ⇑(geometricPowers x) = HPow.hPow x

theorem Cslib.Circuits.Rational.HahnGeometric.embDomain_succ_smul_geometricPowers {Γ : Type u_1} {R : Type u_2} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] {x : HahnSeries Γ R} (hx : 0 < x.orderTop) : (x • geometricPowers x).embDomain { toFun := Nat.succ, inj' := Nat.succ_injective } = geometricPowers x - HahnSeries.SummableFamily.ofFinsupp (Finsupp.single 0 1)

theorem Cslib.Circuits.Rational.HahnGeometric.one_sub_self_mul_hsum_geometricPowers {Γ : Type u_1} {R : Type u_2} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] {x : HahnSeries Γ R} (hx : 0 < x.orderTop) : (1 - x) * (geometricPowers x).hsum = 1

theorem Cslib.Circuits.Rational.HahnGeometric.normalized_pos {Γ : Type u_1} {R : Type u_2} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] (x : HahnSeries Γ R) (u : Rˣ) (hu : x.leadingCoeff = ↑u) : 0 < (1 - (HahnSeries.single (-x.order)) ↑u⁻¹ * x).orderTop

A unit leading coefficient permits the usual normalization, without any commutativity assumption on the coefficient ring.

theorem Cslib.Circuits.Rational.HahnGeometric.normalized_right_inverse {Γ : Type u_1} {R : Type u_2} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] (x : HahnSeries Γ R) (u : Rˣ) (hu : x.leadingCoeff = ↑u) : x * ((geometricPowers (1 - (HahnSeries.single (-x.order)) ↑u⁻¹ * x)).hsum * (HahnSeries.single (-x.order)) ↑u⁻¹) = 1

theorem Cslib.Circuits.Rational.QuantumSeries.line_inv_unit {Γ : Type u_1} {K : Type u_2} {R : Type u_3} [AddCommGroup Γ] [Field K] [Ring R] [Algebra K R] [Nontrivial R] (B : Γ → Rˣ) (h0 : B 0 = 1) (hB : ∀ (g h : Γ), ∃ (c : K), ↑(B g) * ↑(B h) = c • ↑(B (g + h))) {g : Γ} (u : Rˣ) (hu : ↑u ∈ line B g) : ↑u⁻¹ ∈ line B (-g)

theorem Cslib.Circuits.Rational.QuantumSeries.single_mem {Γ : Type u_1} {K : Type u_2} {R : Type u_3} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Field K] [Ring R] [Algebra K R] (B : Γ → Rˣ) (h0 : B 0 = 1) (hB : ∀ (g h : Γ), ∃ (c : K), ↑(B g) * ↑(B h) = c • ↑(B (g + h))) {g : Γ} {r : R} (hr : r ∈ line B g) : (HahnSeries.single g) r ∈ coefficientRing B h0 hB

theorem Cslib.Circuits.Rational.QuantumSeries.hsum_mem {Γ : Type u_1} {K : Type u_2} {R : Type u_3} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Field K] [Ring R] [Algebra K R] (B : Γ → Rˣ) (h0 : B 0 = 1) (hB : ∀ (g h : Γ), ∃ (c : K), ↑(B g) * ↑(B h) = c • ↑(B (g + h))) {α : Type u_4} (x : HahnSeries.SummableFamily Γ R α) (hx : ∀ (i : α), x i ∈ coefficientRing B h0 hB) : x.hsum ∈ coefficientRing B h0 hB

theorem Cslib.Circuits.Rational.QuantumSeries.inverse_candidate_mem {Γ : Type u_1} {K : Type u_2} {R : Type u_3} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Field K] [Ring R] [Algebra K R] [Nontrivial R] (B : Γ → Rˣ) (h0 : B 0 = 1) (hB : ∀ (g h : Γ), ∃ (c : K), ↑(B g) * ↑(B h) = c • ↑(B (g + h))) (x : HahnSeries Γ R) (hx : x ∈ coefficientRing B h0 hB) (u : Rˣ) (hu : x.leadingCoeff = ↑u) : (HahnGeometric.geometricPowers (1 - (HahnSeries.single (-x.order)) ↑u⁻¹ * x)).hsum * (HahnSeries.single (-x.order)) ↑u⁻¹ ∈ coefficientRing B h0 hB

theorem Cslib.Circuits.Rational.QuantumSeries.inverse_exists {Γ : Type u_1} {K : Type u_2} {R : Type u_3} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Field K] [Ring R] [Algebra K R] [Nontrivial R] (B : Γ → Rˣ) (h0 : B 0 = 1) (hB : ∀ (g h : Γ), ∃ (c : K), ↑(B g) * ↑(B h) = c • ↑(B (g + h))) (x : ↥(coefficientRing B h0 hB)) (hx : x ≠ 0) : ∃ (y : ↥(coefficientRing B h0 hB)), x * y = 1

theorem Cslib.Circuits.Rational.QuantumSeries.coefficientRing_isUnit_or_eq_zero {Γ : Type u_1} {K : Type u_2} {R : Type u_3} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Field K] [Ring R] [Algebra K R] [Nontrivial R] (B : Γ → Rˣ) (h0 : B 0 = 1) (hB : ∀ (g h : Γ), ∃ (c : K), ↑(B g) * ↑(B h) = c • ↑(B (g + h))) (x : ↥(coefficientRing B h0 hB)) : IsUnit x ∨ x = 0

@[reducible, inline]

noncomputable abbrev Cslib.Circuits.Rational.QuantumSeries.divisionRing {Γ : Type u_1} {K : Type u_2} {R : Type u_3} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Field K] [Ring R] [Algebra K R] [Nontrivial R] (B : Γ → Rˣ) (h0 : B 0 = 1) (hB : ∀ (g h : Γ), ∃ (c : K), ↑(B g) * ↑(B h) = c • ↑(B (g + h))) : DivisionRing ↥(coefficientRing B h0 hB)

An actual division ring containing all ordered quantum-monomial series; no finite-dimensional-domain or external division-algebra theorem is assumed.