Doubling is invertible on a real vector space

For a real vector space N, multiplication by 2 is a bijection, so the doubling map is a unit of the endomorphism ring — and it remains one when N is regarded only as a ℤ-module, where 2 itself is not invertible. This file records that as an Invertible (2 : Module.End ℤ N) instance, together with the rewrite rule identifying its inverse with the real scalar (2 : ℝ)⁻¹.

Main definitions

• TauCeti.invertibleTwoModuleEndInt: for any semiring S acting on N in which 2 is invertible, doubling is invertible on the ℤ-endomorphisms of N.

Main results

• TauCeti.invOf_two_moduleEndInt_apply: the inverse of doubling is halving by the scalar, for whichever Invertible (2 : Module.End ℤ N) instance is in scope.
• TauCeti.instInvertibleTwoModuleEndInt: the instance for S = ℝ, so that doubling is invertible on any real vector space viewed as an endomorphism of its underlying ℤ-module.
• TauCeti.half_moduleEndInt_apply_eq_half_smul: that inverse acts as the scalar (2 : ℝ)⁻¹. This is the R = ℤ counterpart of Mathlib's QuadraticMap.half_moduleEnd_apply_eq_half_smul, whose Invertible (2 : R) hypothesis is unavailable for R = ℤ; here the halving scalar comes from the module structure instead of from the ring.

The consumer this exists for

Mathlib builds the bilinear map associated with a quadratic map by halving the polar form: QuadraticMap.associatedHom is ⅟(2 : Module.End R N) • QuadraticMap.polarBilin, with QuadraticMap.associated' the ℤ-linear specialisation. Halving needs Invertible (2 : Module.End R N), and Mathlib's docstring for associatedHom names exactly the case this file supplies:

Note that this makes the bijection available in more cases than the simpler condition Invertible (2 : R), e.g., when R = ℤ and N = ℝ.

Mathlib provides no instance reaching it: its only route is [Invertible (2 : R)] → Invertible (2 : Module.End R M), which for R = ℤ asks for Invertible (2 : ℤ) and fails. With the instance below, associated' and its API — associated_apply, associated_isSymm, associated_flip, associated_eq_self_apply — become usable on ℤ-quadratic maps with values in a real vector space.

Implementation notes

The construction is stated for a general scalar semiring S but is a def rather than an instance, because S appears nowhere in the conclusion Invertible (2 : Module.End ℤ N) and so could never be inferred by instance search. Instances are registered by applying it to the scalar rings that are wanted; ℝ is the one this repository needs.

@[instance_reducible]

noncomputable def TauCeti.invertibleTwoModuleEndInt {N : Type u_1} [AddCommGroup N] (S : Type u_2) [Semiring S] [Module S N] [Invertible 2] : Invertible 2

Doubling is invertible on the ℤ-endomorphisms of a module over a semiring in which 2 is invertible. The halving scalar comes from the module structure rather than from ℤ.

Equations

• TauCeti.invertibleTwoModuleEndInt S = (Invertible.map MonoidHom.smulOneHom 2).copy 2 ⋯

theorem TauCeti.invOf_two_moduleEndInt_apply {N : Type u_1} [AddCommGroup N] (S : Type u_2) [Semiring S] [Module S N] [Invertible 2] [Invertible 2] (x : N) : ⅟2 x = ⅟2 • x

The inverse of doubling is halving by the scalar, for whichever Invertible (2 : Module.End ℤ N) instance is in scope.

@[instance_reducible]

noncomputable instance TauCeti.instInvertibleTwoModuleEndInt {N : Type u_1} [AddCommGroup N] [Module ℝ N] : Invertible 2

Doubling is invertible on a real vector space, as an endomorphism of its ℤ-module structure.

Equations

• TauCeti.instInvertibleTwoModuleEndInt = TauCeti.invertibleTwoModuleEndInt ℝ

@[simp]

theorem TauCeti.half_moduleEndInt_apply_eq_half_smul {N : Type u_1} [AddCommGroup N] [Module ℝ N] (x : N) : ⅟2 x = 2⁻¹ • x

The inverse of doubling acts as the real scalar (2 : ℝ)⁻¹.