Inverting one component of a unit #

An idempotent e of a commutative ring R splits it as R ≅ e R × (1 - e) R, and so splits each unit u into its e-component e u and its (1 - e)-component (1 - e) u. Inverting the first component and keeping the second is the automorphism

u ↦ e u⁻¹ + (1 - e) u

of the unit group Rˣ, written here without reference to the product decomposition: since e² = e and e (1 - e) = 0, products of elements of the form e x + (1 - e) y are computed componentwise.

The automorphism is an involution. At e = 0 it is the identity and at e = 1 it is inversion. For the idempotent of ZMod N attached to an exact divisor Q of N it is the automorphism of (ZMod N)ˣ inverting the residue modulo Q and fixing the residue modulo N / Q, through which the Atkin–Lehner operator W_Q shifts the nebentypus of a modular form.

Main definitions #

IsIdempotentElem.unitsInvPart: the automorphism u ↦ e u⁻¹ + (1 - e) u of Rˣ.

Main results #

IsIdempotentElem.mul_unitsInvPart, IsIdempotentElem.one_sub_mul_unitsInvPart: its two components are e u⁻¹ and (1 - e) u.
IsIdempotentElem.unitsInvPart_symm: it is an involution.
IsIdempotentElem.unitsInvPart_zero, IsIdempotentElem.unitsInvPart_one: at e = 0 and e = 1 it is the identity and inversion.

source

def IsIdempotentElem.unitsInvPart {R : Type u_1} [CommRing R] {e : R} (he : IsIdempotentElem e) :

Rˣ ≃* Rˣ

Inverting the e-component of a unit: for an idempotent e of a commutative ring R, the automorphism u ↦ e u⁻¹ + (1 - e) u of Rˣ. Under R ≅ e R × (1 - e) R it inverts the first component and fixes the second. It is its own inverse (unitsInvPart_symm).

Equations