Documentation

TauCeti.LinearAlgebra.SesquilinearForm.LaurentSpecialization

Specializing q-sesquilinear forms at a unit #

Let R be a commutative ring. For a unit ε of R and a module N over R[q,q⁻¹], the specialization N_ε = TauCeti.LaurentSpecialization ε N is the base change of N along evaluation at q = ε; on it q acts as ε.

A sesquilinear form b : N₁ × N₂ → R[q,q⁻¹], antilinear in its first argument for the involution q ↦ q⁻¹ (LaurentPolynomial.invert) and linear in its second, specializes to an R-bilinear form on N₁_ε₁ × N₂_ε₂ with values laurentEval ε₂ (b x y) whenever ε₁⁻¹ = ε₂: evaluating invert p at ε₂ is evaluating p at ε₂⁻¹. Taking ε₁ = ε₂ = ε needs ε⁻¹ = ε; over R = ℤ this is automatic, the two units being q = 1 and q = -1. This is how the q-Euler form of a graded category specializes.

Specialization does not preserve nondegeneracy: over a nontrivial coefficient ring, the Laurent matrix with rows (1, q) and (q, 1) has determinant 1 - q², which is a non-zero-divisor, while its value at any ε with ε⁻¹ = ε has determinant zero.

Main definitions #

Main results #

References #

source
noncomputable def LinearMap.laurentSpecialize {R : Type u_1} [CommRing R] {ε₁ ε₂ : Rˣ} {N₁ : Type u_2} {N₂ : Type u_3} [AddCommGroup N₁] [Module (LaurentPolynomial R) N₁] [Module R N₁] [IsScalarTower R (LaurentPolynomial R) N₁] [AddCommGroup N₂] [Module (LaurentPolynomial R) N₂] [Module R N₂] [IsScalarTower R (LaurentPolynomial R) N₂] (b : N₁ →ₛₗ[LaurentPolynomial.invert.toRingEquiv.toRingHom] N₂ →ₗ[LaurentPolynomial R] LaurentPolynomial R) (hε : ε₁⁻¹ = ε₂) :
TauCeti.LaurentSpecialization ε₁ N₁ →ₗ[R] TauCeti.LaurentSpecialization ε₂ N₂ →ₗ[R] R

The specialization of a q-sesquilinear form, at q = ε₁ in the first argument and at q = ε₂ in the second, for units with ε₁⁻¹ = ε₂. The form b is antilinear in its first argument for q ↦ q⁻¹ and linear in its second; its specialization is the R-bilinear form on the specialized modules whose values are the values of b evaluated at ε₂. Taking ε₁ = ε₂ = ε specializes both arguments at a unit with ε⁻¹ = ε; over ℤ this holds for both units, q = 1 and q = -1.

Equations
Instances For
    source
    @[simp]
    theorem LinearMap.laurentSpecialize_mk_mk {R : Type u_1} [CommRing R] {ε₁ ε₂ : Rˣ} {N₁ : Type u_2} {N₂ : Type u_3} [AddCommGroup N₁] [Module (LaurentPolynomial R) N₁] [Module R N₁] [IsScalarTower R (LaurentPolynomial R) N₁] [AddCommGroup N₂] [Module (LaurentPolynomial R) N₂] [Module R N₂] [IsScalarTower R (LaurentPolynomial R) N₂] (b : N₁ →ₛₗ[LaurentPolynomial.invert.toRingEquiv.toRingHom] N₂ →ₗ[LaurentPolynomial R] LaurentPolynomial R) (hε : ε₁⁻¹ = ε₂) (x : N₁) (y : N₂) :
    ((b.laurentSpecialize hε) ((TauCeti.LaurentSpecialization.mk ε₁) x)) ((TauCeti.LaurentSpecialization.mk ε₂) y) = (TauCeti.laurentEval ε₂) ((b x) y)

    The specialized form is the evaluated form: on specialized elements its value is the value of the Laurent form evaluated at ε₂.

    source
    theorem TauCeti.exists_nondegenerate_and_not_nondegenerate_map_laurentEval (R : Type u_1) [CommRing R] [Nontrivial R] :
    ∃ (M : Matrix (Fin 2) (Fin 2) (LaurentPolynomial R)), M.Nondegenerate ∧ ∀ (ε : Rˣ), ε⁻¹ = ε → ¬(M.map ⇑(laurentEval ε)).Nondegenerate

    Specialization need not preserve nondegeneracy. Over a nontrivial commutative ring R, some two-by-two Laurent-polynomial matrix is nondegenerate while its value at every unit ε with ε⁻¹ = ε is degenerate; over ℤ these are both specializations q = 1 and q = -1. The witness has rows (1, q) and (q, 1), with determinant 1 - q², a non-zero-divisor.