Specializing Laurent modules at a unit

Let R be a commutative ring and ε a unit of R. Evaluation at q = ε is the R-algebra map TauCeti.laurentEval ε : R[q,q⁻¹] → R. For a module N over R[q,q⁻¹], the specialization of N at ε is the quotient

N_ε = N ⧸ I_ε N, where I_ε = ker (laurentEval ε).

This is the base change R ⊗_{R[q,q⁻¹]} N along evaluation: evaluation is surjective, so R[q,q⁻¹] ⧸ I_ε ≃ R (Ideal.quotientKerAlgEquivOfSurjective), and (R[q,q⁻¹] ⧸ I_ε) ⊗ N ≃ N ⧸ I_ε N is TensorProduct.quotTensorEquivQuotSMul. The quotient presentation is used because it needs no auxiliary algebra structure of R over R[q,q⁻¹]. On N_ε every Laurent scalar acts through its value at ε; in particular q acts as ε. The universal property says that R-linear maps out of N_ε are the R-linear maps out of N turning multiplication by q into multiplication by ε.

Main definitions

• TauCeti.LaurentSpecialization ε N: the specialization of an R[q,q⁻¹]-module at q = ε.
• TauCeti.LaurentSpecialization.mk: the specialization map N → N_ε.
• TauCeti.LaurentSpecialization.lift: the universal property for R-linear maps.
• TauCeti.LaurentSpecialization.map: specialize a Laurent-linear map.
• TauCeti.LaurentSpecialization.basis: specialize a Laurent-module basis coefficientwise, as the base-change basis IsBaseChange.basis.

Main results

• TauCeti.LaurentSpecialization.mk_smul: a Laurent scalar acts on N_ε by its value at ε.
• TauCeti.LaurentSpecialization.lift_mk and TauCeti.LaurentSpecialization.hom_ext: the universal property.
• TauCeti.LaurentSpecialization.isBaseChange: the specialization is the base change along evaluation at ε, for any algebra structure on R given by that evaluation.

@[reducible, inline]

abbrev TauCeti.LaurentSpecialization {R : Type u_1} [CommRing R] (ε : Rˣ) (N : Type u_2) [AddCommGroup N] [Module (LaurentPolynomial R) N] : Type u_2

The specialization of an R[q,q⁻¹]-module at q = ε: the quotient of N by the kernel of evaluation at ε acting on N. It is the base change of N along TauCeti.laurentEval ε : R[q,q⁻¹] → R, and q acts on it as ε.

Equations

• TauCeti.LaurentSpecialization ε N = (N ⧸ RingHom.ker (TauCeti.laurentEval ε) • ⊤)

noncomputable def TauCeti.LaurentSpecialization.mk {R : Type u_1} [CommRing R] (ε : Rˣ) {N : Type u_2} [AddCommGroup N] [Module (LaurentPolynomial R) N] : N →ₗ[LaurentPolynomial R] LaurentSpecialization ε N

The specialization map N → N_ε.

Equations

• TauCeti.LaurentSpecialization.mk ε = (RingHom.ker (TauCeti.laurentEval ε) • ⊤).mkQ

theorem TauCeti.LaurentSpecialization.mk_apply {R : Type u_1} [CommRing R] (ε : Rˣ) {N : Type u_2} [AddCommGroup N] [Module (LaurentPolynomial R) N] (x : N) : (mk ε) x = Submodule.Quotient.mk x

The specialization of an element is its quotient class.

theorem TauCeti.LaurentSpecialization.mk_surjective {R : Type u_1} [CommRing R] (ε : Rˣ) {N : Type u_2} [AddCommGroup N] [Module (LaurentPolynomial R) N] : Function.Surjective ⇑(mk ε)

Every element of the specialization is specialized from N.

@[simp]

theorem TauCeti.LaurentSpecialization.mk_smul {R : Type u_1} [CommRing R] (ε : Rˣ) {N : Type u_2} [AddCommGroup N] [Module (LaurentPolynomial R) N] [Module R N] [IsScalarTower R (LaurentPolynomial R) N] (p : LaurentPolynomial R) (x : N) : p • (mk ε) x = (laurentEval ε) p • (mk ε) x

A Laurent scalar acts on the specialization at ε by its value at ε. In particular q acts as ε.

noncomputable def TauCeti.LaurentSpecialization.lift {R : Type u_1} [CommRing R] (ε : Rˣ) {N : Type u_2} [AddCommGroup N] [Module (LaurentPolynomial R) N] [Module R N] [IsScalarTower R (LaurentPolynomial R) N] {A : Type u_3} [AddCommGroup A] [Module R A] (f : N →ₗ[R] A) (hf : ∀ (x : N), f (LaurentPolynomial.T 1 • x) = ↑ε • f x) : LaurentSpecialization ε N →ₗ[R] A

The universal property of the specialization at ε: an R-linear map out of N which turns multiplication by q into multiplication by ε factors through N_ε.

Equations

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

@[simp]

theorem TauCeti.LaurentSpecialization.lift_mk {R : Type u_1} [CommRing R] (ε : Rˣ) {N : Type u_2} [AddCommGroup N] [Module (LaurentPolynomial R) N] [Module R N] [IsScalarTower R (LaurentPolynomial R) N] {A : Type u_3} [AddCommGroup A] [Module R A] (f : N →ₗ[R] A) (hf : ∀ (x : N), f (LaurentPolynomial.T 1 • x) = ↑ε • f x) (x : N) : (lift ε f hf) ((mk ε) x) = f x

The map induced on the specialization agrees with the original map on specialized elements.

noncomputable def TauCeti.LaurentSpecialization.map {R : Type u_1} [CommRing R] (ε : Rˣ) {N : Type u_2} [AddCommGroup N] [Module (LaurentPolynomial R) N] [Module R N] [IsScalarTower R (LaurentPolynomial R) N] {M : Type u_4} [AddCommGroup M] [Module (LaurentPolynomial R) M] [Module R M] [IsScalarTower R (LaurentPolynomial R) M] (f : N →ₗ[LaurentPolynomial R] M) : LaurentSpecialization ε N →ₗ[R] LaurentSpecialization ε M

A Laurent-linear map induces an R-linear map between specializations at the same unit.

Equations

• TauCeti.LaurentSpecialization.map ε f = ↑R ((RingHom.ker (TauCeti.laurentEval ε) • ⊤).mapQ (RingHom.ker (TauCeti.laurentEval ε) • ⊤) f ⋯)

@[simp]

theorem TauCeti.LaurentSpecialization.map_mk {R : Type u_1} [CommRing R] (ε : Rˣ) {N : Type u_2} [AddCommGroup N] [Module (LaurentPolynomial R) N] [Module R N] [IsScalarTower R (LaurentPolynomial R) N] {M : Type u_4} [AddCommGroup M] [Module (LaurentPolynomial R) M] [Module R M] [IsScalarTower R (LaurentPolynomial R) M] (f : N →ₗ[LaurentPolynomial R] M) (x : N) : (map ε f) ((mk ε) x) = (mk ε) (f x)

Specializing a Laurent-linear map commutes with taking quotient classes.

theorem TauCeti.LaurentSpecialization.hom_ext {R : Type u_1} [CommRing R] (ε : Rˣ) {N : Type u_2} [AddCommGroup N] [Module (LaurentPolynomial R) N] [Module R N] [IsScalarTower R (LaurentPolynomial R) N] {A : Type u_3} [AddCommGroup A] [Module R A] {f g : LaurentSpecialization ε N →ₗ[R] A} (h : ∀ (x : N), f ((mk ε) x) = g ((mk ε) x)) : f = g

An R-linear map out of the specialization is determined by its values on specialized elements.

theorem TauCeti.LaurentSpecialization.hom_ext_iff {R : Type u_1} [CommRing R] {ε : Rˣ} {N : Type u_2} [AddCommGroup N] [Module (LaurentPolynomial R) N] [Module R N] [IsScalarTower R (LaurentPolynomial R) N] {A : Type u_3} [AddCommGroup A] [Module R A] {f g : LaurentSpecialization ε N →ₗ[R] A} : f = g ↔ ∀ (x : N), f ((mk ε) x) = g ((mk ε) x)

@[simp]

theorem TauCeti.LaurentSpecialization.map_id {R : Type u_1} [CommRing R] (ε : Rˣ) {N : Type u_2} [AddCommGroup N] [Module (LaurentPolynomial R) N] [Module R N] [IsScalarTower R (LaurentPolynomial R) N] : map ε LinearMap.id = LinearMap.id

Specializing the identity map gives the identity on the specialization.

@[simp]

theorem TauCeti.LaurentSpecialization.map_comp {R : Type u_1} [CommRing R] (ε : Rˣ) {N : Type u_2} [AddCommGroup N] [Module (LaurentPolynomial R) N] [Module R N] [IsScalarTower R (LaurentPolynomial R) N] {M : Type u_4} [AddCommGroup M] [Module (LaurentPolynomial R) M] [Module R M] [IsScalarTower R (LaurentPolynomial R) M] {P : Type u_5} [AddCommGroup P] [Module (LaurentPolynomial R) P] [Module R P] [IsScalarTower R (LaurentPolynomial R) P] (g : M →ₗ[LaurentPolynomial R] P) (f : N →ₗ[LaurentPolynomial R] M) : map ε (g ∘ₗ f) = map ε g ∘ₗ map ε f

Specialization preserves composition of Laurent-linear maps.

theorem TauCeti.LaurentSpecialization.isScalarTower {R : Type u_1} [CommRing R] (ε : Rˣ) {N : Type u_2} [AddCommGroup N] [Module (LaurentPolynomial R) N] [Module R N] [IsScalarTower R (LaurentPolynomial R) N] [Algebra (LaurentPolynomial R) R] (h : ∀ (p : LaurentPolynomial R), (algebraMap (LaurentPolynomial R) R) p = (laurentEval ε) p) : IsScalarTower (LaurentPolynomial R) R (LaurentSpecialization ε N)

Under an R[q,q⁻¹]-algebra structure on R given by evaluation at ε, Laurent scalars and coefficients act compatibly on the specialization at ε.

theorem TauCeti.LaurentSpecialization.isBaseChange {R : Type u_1} [CommRing R] (ε : Rˣ) {N : Type u_2} [AddCommGroup N] [Module (LaurentPolynomial R) N] [Module R N] [IsScalarTower R (LaurentPolynomial R) N] [Algebra (LaurentPolynomial R) R] (h : ∀ (p : LaurentPolynomial R), (algebraMap (LaurentPolynomial R) R) p = (laurentEval ε) p) [IsScalarTower (LaurentPolynomial R) R (LaurentSpecialization ε N)] : IsBaseChange R (mk ε)

The specialization at ε is the base change along evaluation at ε. This is stated for any R[q,q⁻¹]-algebra structure on R whose algebra map is TauCeti.laurentEval ε, since that structure depends on ε and so is not an instance.

noncomputable def TauCeti.LaurentSpecialization.basis {R : Type u_1} [CommRing R] (ε : Rˣ) {N : Type u_2} [AddCommGroup N] [Module (LaurentPolynomial R) N] [Module R N] [IsScalarTower R (LaurentPolynomial R) N] {ι : Type u_6} (b : Module.Basis ι (LaurentPolynomial R) N) : Module.Basis ι R (LaurentSpecialization ε N)

A Laurent-module basis specializes to a basis over the coefficient ring. It is the base-change basis IsBaseChange.basis along evaluation at ε: its vectors are the classes of the original basis vectors, and its coordinates are obtained by evaluating Laurent coordinates at ε.

Equations

• TauCeti.LaurentSpecialization.basis ε b = IsBaseChange.basis b ⋯

@[simp]

theorem TauCeti.LaurentSpecialization.basis_apply {R : Type u_1} [CommRing R] (ε : Rˣ) {N : Type u_2} [AddCommGroup N] [Module (LaurentPolynomial R) N] [Module R N] [IsScalarTower R (LaurentPolynomial R) N] {ι : Type u_6} (b : Module.Basis ι (LaurentPolynomial R) N) (i : ι) : (basis ε b) i = (mk ε) (b i)

Specializing a basis specializes each basis vector.

@[simp]

theorem TauCeti.LaurentSpecialization.basis_repr_mk_apply {R : Type u_1} [CommRing R] (ε : Rˣ) {N : Type u_2} [AddCommGroup N] [Module (LaurentPolynomial R) N] [Module R N] [IsScalarTower R (LaurentPolynomial R) N] {ι : Type u_6} (b : Module.Basis ι (LaurentPolynomial R) N) (x : N) (i : ι) : ((basis ε b).repr ((mk ε) x)) i = (laurentEval ε) ((b.repr x) i)

Coordinates in the specialized basis are evaluated Laurent coordinates.