Evaluating a Laurent polynomial at a unit of a not necessarily commutative algebra

Mathlib's LaurentPolynomial.eval₂ substitutes a unit of a commutative semiring into a Laurent polynomial. The Laurent coefficient ring of graded K-theory has to act on abelian groups, so it has to be substituted into endomorphism rings, which are not commutative. This file supplies that evaluation.

For a unit u of an R-algebra A, TauCeti.laurentEval u : R[T;T⁻¹] →ₐ[R] A is the algebra map sending T to u and T⁻¹ to u⁻¹. It is the algebra map attached by AddMonoidAlgebra.lift to the monoid homomorphism n ↦ uⁿ out of Multiplicative ℤ, so it exists for an arbitrary semiring A and is the unique algebra map with the prescribed value at T. Consequently TauCeti.laurentEvalEquiv identifies the units of A with the R-algebra maps out of R[T;T⁻¹]: the Laurent polynomial ring is the free R-algebra on one invertible generator.

The module-theoretic use is TauCeti.laurentTAut: multiplication by T -- written q in the graded K-theory literature -- is an automorphism of the underlying additive monoid. This only requires a distributive action of the Laurent polynomial monoid, so it applies in particular to every R[T;T⁻¹]-module. That automorphism is what a shift-compatible invariant is compared against.

Main definitions

• TauCeti.laurentEval: evaluation of a Laurent polynomial at a unit of an R-algebra.
• TauCeti.laurentEvalEquiv: the units of A are the R-algebra maps R[T;T⁻¹] →ₐ[R] A.
• TauCeti.laurentTAut: the action of T as an additive automorphism under a DistribMulAction (LaurentPolynomial R) N; Laurent modules are a specialization.

Main results

• TauCeti.laurentEval_unique: an algebra map out of R[T;T⁻¹] is determined by its value at T.
• TauCeti.laurentEval_eq_eval₂: over a commutative target, this evaluation is Mathlib's LaurentPolynomial.eval₂.
• TauCeti.eval₂_C_injective_of_val_eq_T: the substitution T ↦ Tᵏ is injective for k ≠ 0.
• TauCeti.eval₂_C_inv_pow_injective: in particular T ↦ T⁻ᵏ is injective for k ≠ 0.
• TauCeti.laurentPolynomialC_smul: a constant Laurent polynomial acts by integer scalar multiplication.
• TauCeti.map_smul_eq_laurentEval_smul: a linear map turning T into a unit turns every Laurent scalar into its value at that unit.

noncomputable def TauCeti.laurentEval {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] (u : Aˣ) : LaurentPolynomial R →ₐ[R] A

Evaluation of a Laurent polynomial at a unit u of an R-algebra A: the R-algebra map R[T;T⁻¹] →ₐ[R] A sending T to u, hence T⁻¹ to u⁻¹.

Unlike LaurentPolynomial.eval₂ this does not ask A to be commutative, because the intended targets are endomorphism rings. The construction is the universal property of the group algebra R[ℤ]: an integer power of a unit is a monoid homomorphism out of Multiplicative ℤ.

Equations

• TauCeti.laurentEval u = (AddMonoidAlgebra.lift R A ℤ) ((Units.coeHom A).comp ((zpowersHom Aˣ) u))

@[simp]

theorem TauCeti.laurentEval_T {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] (u : Aˣ) (n : ℤ) : (laurentEval u) (LaurentPolynomial.T n) = ↑(u ^ n)

@[simp]

theorem TauCeti.laurentEval_C {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] (u : Aˣ) (r : R) : (laurentEval u) (LaurentPolynomial.C r) = (algebraMap R A) r

theorem TauCeti.laurentEval_T_one {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] (u : Aˣ) : (laurentEval u) (LaurentPolynomial.T 1) = ↑u

The generator T evaluates to the chosen unit.

theorem TauCeti.laurentEval_unique {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] (u : Aˣ) (f : LaurentPolynomial R →ₐ[R] A) (hf : f (LaurentPolynomial.T 1) = ↑u) : f = laurentEval u

An R-algebra map out of R[T;T⁻¹] is determined by its value at T.

noncomputable def TauCeti.laurentEvalEquiv {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] : Aˣ ≃ (LaurentPolynomial R →ₐ[R] A)

The Laurent polynomial ring is the free R-algebra on one invertible generator: its R-algebra maps to A are exactly the units of A, through evaluation at T.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.laurentEvalEquiv_apply {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] (u : Aˣ) : laurentEvalEquiv u = laurentEval u

@[simp]

theorem TauCeti.laurentEvalEquiv_symm_apply {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] (f : LaurentPolynomial R →ₐ[R] A) : ↑(laurentEvalEquiv.symm f) = f (LaurentPolynomial.T 1)

@[simp]

theorem TauCeti.comp_laurentEval {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] {B : Type u_3} [Semiring B] [Algebra R B] (g : A →ₐ[R] B) (u : Aˣ) : g.comp (laurentEval u) = laurentEval ((Units.map ↑g) u)

Evaluation at a unit is natural in the target algebra.

@[simp]

theorem TauCeti.laurentEval_invert {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] (u : Aˣ) (p : LaurentPolynomial R) : (laurentEval u) (LaurentPolynomial.invert p) = (laurentEval u⁻¹) p

Evaluating after the involution T ↦ T⁻¹ is evaluating at the inverse unit.

theorem TauCeti.laurentEval_eq_eval₂ {R : Type u_1} [CommSemiring R] {S : Type u_3} [CommSemiring S] [Algebra R S] (u : Sˣ) (p : LaurentPolynomial R) : (laurentEval u) p = (LaurentPolynomial.eval₂ (algebraMap R S) u) p

Over a commutative target this is Mathlib's LaurentPolynomial.eval₂. The two constructions are separate only because LaurentPolynomial.eval₂ is built by localization and so needs a commutative codomain.

theorem TauCeti.eval₂_C_injective_of_val_eq_T {R : Type u_1} [CommSemiring R] {u : (LaurentPolynomial R)ˣ} {k : ℤ} (hu : ↑u = LaurentPolynomial.T k) (hk : k ≠ 0) : Function.Injective ⇑(LaurentPolynomial.eval₂ LaurentPolynomial.C u)

Substituting a nonzero power of T is injective. Evaluating a Laurent polynomial at a unit of R[T;T⁻¹] whose value is T k substitutes Tᵏ for T; for k ≠ 0 this sends distinct monomials to distinct monomials, so it loses no information.

theorem TauCeti.val_isUnit_T_unit_inv_pow {R : Type u_3} [Semiring R] (n : ℤ) (k : ℕ) : ↑(⋯.unit⁻¹ ^ k) = LaurentPolynomial.T (-(n * ↑k))

The k-th power of the inverse of the unit T n is the monomial T (-(n * k)).

theorem TauCeti.eval₂_C_inv_pow_injective {R : Type u_1} [CommSemiring R] {k : ℕ} (hk : k ≠ 0) : Function.Injective ⇑(LaurentPolynomial.eval₂ LaurentPolynomial.C (⋯.unit⁻¹ ^ k))

Substituting T⁻ᵏ for T is injective for k ≠ 0: a Laurent polynomial is determined by its evaluation at the k-th power of the inverse of the generator.

theorem TauCeti.map_smul_eq_laurentEval_smul {R : Type u_1} [CommSemiring R] {N : Type u_2} [AddCommMonoid N] [Module (LaurentPolynomial R) N] [Module R N] [IsScalarTower R (LaurentPolynomial R) N] {A : Type u_3} [AddCommMonoid A] [Module R A] {S : Type u_4} [Semiring S] [Algebra R S] [Module S A] [IsScalarTower R S A] (ε : Sˣ) (f : N →ₗ[R] A) (hf : ∀ (x : N), f (LaurentPolynomial.T 1 • x) = ↑ε • f x) (p : LaurentPolynomial R) (x : N) : f (p • x) = (laurentEval ε) p • f x

Scalar compatibility with the specialization at ε. An R-linear map turning multiplication by q into multiplication by a unit ε of an R-algebra S turns every Laurent scalar into its value at ε. The target algebra need not be commutative.

noncomputable def TauCeti.laurentTAut (R : Type u_1) [Semiring R] (N : Type u_2) [AddMonoid N] [DistribMulAction (LaurentPolynomial R) N] : AddAut N

Action of the variable, as an automorphism of an additive monoid with a distributive R[T;T⁻¹]-action. In the graded K-theory notation the variable is q, so this is the operator x ↦ q • x against which a shift-compatible invariant is compared.

Equations

• TauCeti.laurentTAut R N = DistribMulAction.toAddEquiv N (unitOfInvertible (LaurentPolynomial.T 1))

@[simp]

theorem TauCeti.laurentTAut_apply (R : Type u_1) [Semiring R] (N : Type u_2) [AddMonoid N] [DistribMulAction (LaurentPolynomial R) N] (x : N) : (laurentTAut R N) x = LaurentPolynomial.T 1 • x

@[simp]

theorem TauCeti.laurentTAut_symm_apply (R : Type u_1) [Semiring R] (N : Type u_2) [AddMonoid N] [DistribMulAction (LaurentPolynomial R) N] (x : N) : (AddEquiv.symm (laurentTAut R N)) x = LaurentPolynomial.T (-1) • x

theorem TauCeti.laurentPolynomialC_smul {N : Type u_1} [AddCommGroup N] [Module (LaurentPolynomial ℤ) N] (a : ℤ) (x : N) : LaurentPolynomial.C a • x = a • x

A constant Laurent polynomial acts by the integer scalar multiplication of the underlying abelian group of a ℤ[T;T⁻¹]-module.

Not @[simp]: LaurentPolynomial.C a is not in simp-normal form, because eq_intCast rewrites the ring homomorphism C : ℤ →+* ℤ[T;T⁻¹] to the integer cast; the normal form of the statement is Mathlib's own Int.cast_smul_eq_zsmul.