Affine automorphisms of an additive commutative group

Let T be an additive commutative group, A : T ≃+ T an additive automorphism of T, and t : T. The affine automorphism of T with linear part A and translation part t is the map x ↦ A x + t. It is a bijection of the underlying type, written AddEquiv.affineEquiv A t, but an additive homomorphism only when t = 0. Its basic algebra (composition, inverse, and the fact that it determines its linear and translation parts) holds over any additive group. Conjugating it by the translation by b changes the translation part t to t + (b - A b) (AddEquiv.conj_addRight_affineEquiv).

Iterating the affine automorphism accumulates its translations: the k-th iterate is the k-th iterate of the linear part followed by the partial norm AddEquiv.partialNorm A k t = ∑ i < k, A^i t, that is

(affineEquiv A t)^k x = A^k x + partialNorm A k t

(AddEquiv.affineEquiv_iterate_apply). The partial norm is indexed by an arbitrary exponent k. For a linear part of period dividing m, its value at k = m is the norm of the cyclic representation of A (AddEquiv.cyclicRepresentation_norm_eq_partialNorm).

The iterate formula turns the period of the affine automorphism into a linear condition on its translation. If the linear part has period dividing m, then the affine automorphism has m-th power the identity exactly when the translation is killed by the m-th partial norm, and its order then divides m (AddEquiv.affineEquiv_pow_eq_one_iff_of_iterate_eq_id, AddEquiv.orderOf_affineEquiv_dvd_iff); without a hypothesis on the linear part the criterion is AddEquiv.affineEquiv_iterate_eq_id_iff. The iterates then depend only on the exponent modulo m: the affine automorphism has m-th power the identity, so it is the generator of an action of ZMod m on T by its iterates (AddEquiv.affineAddAction), and the residue 1 acts by the affine automorphism itself (AddEquiv.affineAddAction_one_vadd). The affine automorphism has exact order m exactly when, in addition, every smaller positive iterate differs from the identity (AddEquiv.orderOf_affineEquiv_eq_iff), which for an affine automorphism means that each of those iterates has a nontrivial linear part or a nonzero partial norm.

A point x is fixed by the k-th iterate exactly when x - A^k x is the k-th partial norm, so the k-th iterate has a fixed point exactly when that partial norm lies in the image of 1 - A^k (AddEquiv.exists_affineEquiv_iterate_apply_eq_self_iff). Consequently the action of ZMod m is faithful exactly when the affine automorphism has exact order m (AddEquiv.faithfulVAdd_affineAddAction_iff), and it is free, that is IsCancelVAdd, exactly when for every 0 < k < m the k-th partial norm does not lie in the image of 1 - A^k (AddEquiv.isCancelVAdd_affineAddAction_iff). For composite m every such k must be checked; for prime m the generator suffices (AddEquiv.isCancelVAdd_affineAddAction_iff_of_prime). Up to conjugation by translations, the translation parts of norm zero are classified by degree-one group cohomology, as shown in TauCeti.RepresentationTheory.Homological.GroupCohomology.CyclicAutomorphism.

Main definitions

• AddEquiv.affineEquiv A t: the affine equivalence x ↦ A x + t of T, with linear part A and translation part t.
• AddEquiv.partialNorm A k t: the partial norm ∑ i < k, A^i t of the translation part, that is the translation accumulated by k iterates.
• AddEquiv.cyclicNormHom A k: the partial norm bundled as an additive endomorphism.
• AddEquiv.oneSubPow A k: the difference endomorphism 1 - A^k.
• AddEquiv.affineAddAction: the action of ZMod m on T by the iterates of an affine equivalence whose m-th power is the identity.

Main results

• AddEquiv.affineEquiv_inj, AddEquiv.affineEquiv_mul_affineEquiv, AddEquiv.affineEquiv_inv: the affine equivalence determines its linear and translation parts, and affine equivalences are closed under composition and inversion.
• AddEquiv.conj_addRight_affineEquiv: conjugation by the translation by b changes the translation part t to t + (b - A b).
• AddEquiv.affineEquiv_iterate_apply: the k-th iterate of the affine equivalence is the k-th iterate of its linear part plus the k-th partial norm of its translation part.
• AddEquiv.partialNorm_def: the partial norm as its defining finite sum.
• AddEquiv.partialNorm_add, AddEquiv.partialNorm_neg, AddEquiv.partialNorm_sub, AddEquiv.partialNorm_zero_right, AddEquiv.partialNorm_add_exponent: the partial norm is additive in its translation argument, vanishes on the zero translation part, and splits over the exponent.
• AddEquiv.partialNorm_refl: for the identity linear part, the partial norm of k iterates is k • t.
• AddEquiv.oneSubPow_comp_cyclicNormHom, AddEquiv.cyclicNormHom_comp_oneSubPow: for a linear part of period dividing m, both composites of the norm and 1 - A vanish.
• AddEquiv.cyclicNormHom_two: the norm for two iterates is 1 + A, including with 2-torsion.
• AddEquiv.cyclicRepresentation_norm_eq_partialNorm: the norm of the cyclic representation of A is the partial norm of order m.
• AddEquiv.affineEquiv_iterate_eq_id_iff, AddEquiv.affineEquiv_pow_eq_one_iff: the affine equivalence has m-th power the identity exactly when its linear part has m-th iterate the identity and the m-th partial norm of its translation part vanishes.
• AddEquiv.affineEquiv_pow_eq_one_iff_of_iterate_eq_id, AddEquiv.orderOf_affineEquiv_dvd_iff: under a linear part of period dividing m, the same criterion needs only the partial norm, and then the order of the affine equivalence divides m.
• AddEquiv.orderOf_affineEquiv_eq_iff: the affine equivalence has exact order m exactly when its m-th power is the identity and no smaller positive power is.
• AddEquiv.affineAddAction_vadd, AddEquiv.affineAddAction_one_vadd: the residue k of ZMod m acts by the k-th iterate of the affine equivalence, and the residue 1 by the affine equivalence itself.
• AddEquiv.affineEquiv_iterate_apply_eq_self_iff, AddEquiv.exists_affineEquiv_iterate_apply_eq_self_iff: x is fixed by the k-th iterate exactly when x - A^k x is the k-th partial norm, so the k-th iterate has a fixed point exactly when that partial norm lies in the image of 1 - A^k.
• AddEquiv.faithfulVAdd_affineAddAction_iff: the action of ZMod m is faithful exactly when the affine equivalence has exact order m.
• AddEquiv.isCancelVAdd_affineAddAction_iff, AddEquiv.isCancelVAdd_affineAddAction_iff_of_prime: the action of ZMod m is free exactly when no partial norm of order 0 < k < m lies in the image of 1 - A^k; for prime m, exactly when t does not lie in the image of 1 - A.

References

• W. P. Barth, K. Hulek, C. A. M. Peters, A. Van de Ven, Compact Complex Surfaces, second edition, Springer (2004), Chapter V, section Logarithmic transformations, for the cyclic quotients of tori by affine automorphisms.

The affine equivalence

def AddEquiv.affineEquiv {T : Type u_1} [AddGroup T] (A : T ≃+ T) (t : T) : T ≃ T

The affine equivalence of an additive group with linear part A and translation part t, sending x to A x + t.

Its inverse sends y to A⁻¹ (y - t). It is an additive homomorphism only when t = 0. When T is moreover an additive commutative group, hence a ℤ-module, it is, as an affine self-map of T, the affine equivalence with linear part A.toIntLinearEquiv and base points 0 and t (so 0 ↦ t), which Mathlib provides as AffineEquiv.ofLinearEquiv, and it is the element of the group AffineEquiv with those data. It is recorded here as a permutation of T, because the iterates, the order and the action of ZMod m below are those of the underlying permutation.

@[simp]

theorem AddEquiv.affineEquiv_apply {T : Type u_1} [AddGroup T] (A : T ≃+ T) (t x : T) : (A.affineEquiv t) x = A x + t

The affine equivalence sends x to A x + t.

@[simp]

theorem AddEquiv.affineEquiv_symm_apply {T : Type u_1} [AddGroup T] (A : T ≃+ T) (t y : T) : (A.affineEquiv t).symm y = A.symm (y - t)

The inverse of the affine equivalence sends y to A⁻¹ (y - t).

@[simp]

theorem AddEquiv.affineEquiv_inj {T : Type u_1} [AddGroup T] {A B : T ≃+ T} {t s : T} : A.affineEquiv t = B.affineEquiv s ↔ A = B ∧ t = s

An affine equivalence determines its linear part and its translation part.

@[simp]

theorem AddEquiv.affineEquiv_zero {T : Type u_1} [AddGroup T] (A : T ≃+ T) : A.affineEquiv 0 = A.toEquiv

The affine equivalence with zero translation part is the linear part.

@[simp]

theorem AddEquiv.refl_affineEquiv {T : Type u_1} [AddGroup T] (t : T) : (refl T).affineEquiv t = Equiv.addRight t

The affine equivalence with trivial linear part is a translation.

@[simp]

theorem AddEquiv.affineEquiv_mul_affineEquiv {T : Type u_1} [AddGroup T] (A B : T ≃+ T) (t s : T) : A.affineEquiv t * B.affineEquiv s = (B.trans A).affineEquiv (A s + t)

The composite of two affine equivalences is affine: its linear part is the composite of the linear parts.

@[simp]

theorem AddEquiv.affineEquiv_inv {T : Type u_1} [AddGroup T] (A : T ≃+ T) (t : T) : (A.affineEquiv t)⁻¹ = A.symm.affineEquiv (-A.symm t)

The inverse of an affine equivalence is affine, with linear part A⁻¹.

theorem AddEquiv.conj_addRight_affineEquiv {T : Type u_1} [AddCommGroup T] (A : T ≃+ T) (t b : T) : (MulAut.conj (Equiv.addRight b)) (A.affineEquiv t) = A.affineEquiv (t + (b - A b))

Conjugation by a translation. Conjugating x ↦ A x + t by the translation by b gives the affine equivalence with the same linear part and translation part t + (b - A b).

The partial norm of a translation part

def AddEquiv.partialNorm {T : Type u_1} [AddCommGroup T] (A : T ≃+ T) (k : ℕ) (t : T) : T

The partial norm ∑ i < k, A^i t of the translation part t: the translation accumulated by the first k iterates of the affine equivalence with linear part A and translation part t.

theorem AddEquiv.partialNorm_def {T : Type u_1} [AddCommGroup T] (A : T ≃+ T) (k : ℕ) (t : T) : A.partialNorm k t = ∑ i ∈ Finset.range k, (⇑A)^[i] t

The partial norm is the defining finite sum ∑ i < k, A^i t.

@[simp]

theorem AddEquiv.partialNorm_zero {T : Type u_1} [AddCommGroup T] (A : T ≃+ T) (t : T) : A.partialNorm 0 t = 0

The partial norm of zero iterates is zero.

@[simp]

theorem AddEquiv.partialNorm_one {T : Type u_1} [AddCommGroup T] (A : T ≃+ T) (t : T) : A.partialNorm 1 t = t

The partial norm of one iterate is the translation part itself.

@[simp]

theorem AddEquiv.partialNorm_add {T : Type u_1} [AddCommGroup T] (A : T ≃+ T) (k : ℕ) (u v : T) : A.partialNorm k (u + v) = A.partialNorm k u + A.partialNorm k v

The partial norm is additive in its translation argument.

@[simp]

theorem AddEquiv.partialNorm_neg {T : Type u_1} [AddCommGroup T] (A : T ≃+ T) (k : ℕ) (u : T) : A.partialNorm k (-u) = -A.partialNorm k u

The partial norm is additive in its translation argument, in negative form.

@[simp]

theorem AddEquiv.partialNorm_sub {T : Type u_1} [AddCommGroup T] (A : T ≃+ T) (k : ℕ) (u v : T) : A.partialNorm k (u - v) = A.partialNorm k u - A.partialNorm k v

The partial norm is additive in its translation argument, in difference form.

@[simp]

theorem AddEquiv.partialNorm_zero_right {T : Type u_1} [AddCommGroup T] (A : T ≃+ T) (k : ℕ) : A.partialNorm k 0 = 0

The partial norm vanishes on the zero translation part.

@[simp]

theorem AddEquiv.partialNorm_refl {T : Type u_1} [AddCommGroup T] (k : ℕ) (t : T) : (refl T).partialNorm k t = k • t

For the identity linear part, the partial norm of k iterates is k • t: the affine equivalence is the translation by t.

theorem AddEquiv.map_partialNorm {T : Type u_1} [AddCommGroup T] (A : T ≃+ T) (k : ℕ) (t : T) : A (A.partialNorm k t) = A.partialNorm k (A t)

Shifting the linear part through the partial norm: A (N_{A,k} t) = N_{A,k} (A t).

theorem AddEquiv.partialNorm_add_exponent {T : Type u_1} [AddCommGroup T] (A : T ≃+ T) (k l : ℕ) (t : T) : A.partialNorm (k + l) t = A.partialNorm k t + (⇑A)^[k] (A.partialNorm l t)

Splitting the exponent of a partial norm: the partial norm of k + l iterates is the partial norm of k iterates plus the k-th iterate of the linear part applied to the partial norm of l iterates, N_{A,k+l} t = N_{A,k} t + A^k (N_{A,l} t).

theorem AddEquiv.partialNorm_succ {T : Type u_1} [AddCommGroup T] (A : T ≃+ T) (k : ℕ) (t : T) : A.partialNorm (k + 1) t = t + A (A.partialNorm k t)

The partial norm satisfies the recurrence N_{A,k+1} t = t + A (N_{A,k} t): a further iterate appends one more translate of the linear part.

def AddEquiv.cyclicNormHom {T : Type u_1} [AddCommGroup T] (A : T ≃+ T) (k : ℕ) : T →+ T

The partial cyclic norm as an additive endomorphism, with no periodicity assumption.

@[simp]

theorem AddEquiv.cyclicNormHom_apply {T : Type u_1} [AddCommGroup T] (A : T ≃+ T) (k : ℕ) (x : T) : (A.cyclicNormHom k) x = A.partialNorm k x

Evaluating the bundled partial norm gives the translation accumulated by an affine iterate.

@[simp]

theorem AddEquiv.cyclicNormHom_zero {T : Type u_1} [AddCommGroup T] (A : T ≃+ T) : A.cyclicNormHom 0 = 0

The empty partial norm is the zero endomorphism.

@[simp]

theorem AddEquiv.cyclicNormHom_one {T : Type u_1} [AddCommGroup T] (A : T ≃+ T) : A.cyclicNormHom 1 = AddMonoidHom.id T

The partial norm for one iterate is the identity endomorphism.

def AddEquiv.oneSubPow {T : Type u_1} [AddCommGroup T] (A : T ≃+ T) (k : ℕ) : T →+ T

The difference from the k-th power of an additive automorphism.

@[simp]

theorem AddEquiv.oneSubPow_apply {T : Type u_1} [AddCommGroup T] (A : T ≃+ T) (k : ℕ) (x : T) : (A.oneSubPow k) x = x - (⇑A)^[k] x

The difference endomorphism sends x to x - A^k x.

@[simp]

theorem AddEquiv.oneSubPow_zero {T : Type u_1} [AddCommGroup T] (A : T ≃+ T) : A.oneSubPow 0 = 0

The difference from the zeroth power vanishes.

@[simp]

theorem AddEquiv.cyclicNormHom_two {T : Type u_1} [AddCommGroup T] (A : T ≃+ T) : A.cyclicNormHom 2 = AddMonoidHom.id T + A.toAddMonoidHom

The norm for two iterates is 1 + A, also in the presence of 2-torsion.

@[simp]

theorem AddEquiv.oneSubPow_one {T : Type u_1} [AddCommGroup T] (A : T ≃+ T) : A.oneSubPow 1 = AddMonoidHom.id T - A.toAddMonoidHom

The difference for one iterate is 1 - A.

theorem AddEquiv.oneSubPow_comp_cyclicNormHom {T : Type u_1} [AddCommGroup T] (A : T ≃+ T) {m : ℕ} (hA : (⇑A)^[m] = id) : (A.oneSubPow 1).comp (A.cyclicNormHom m) = 0

For a periodic automorphism, 1 - A annihilates the cyclic norm.

theorem AddEquiv.cyclicNormHom_comp_oneSubPow {T : Type u_1} [AddCommGroup T] (A : T ≃+ T) {m : ℕ} (hA : (⇑A)^[m] = id) : (A.cyclicNormHom m).comp (A.oneSubPow 1) = 0

For a periodic automorphism, the cyclic norm annihilates 1 - A.

theorem AddEquiv.cyclicRepresentation_norm_eq_partialNorm {T : Type u_1} [AddCommGroup T] {m : ℕ} [NeZero m] (A : T ≃+ T) (hA : (⇑A)^[m] = id) (x : T) : (A.cyclicRepresentation hA).norm x = A.partialNorm m x

The norm of the cyclic representation of a linear part A of period dividing m is the partial norm partialNorm A m of order m.

The iterate formula

theorem AddEquiv.affineEquiv_iterate_apply {T : Type u_1} [AddCommGroup T] (A : T ≃+ T) (t x : T) (k : ℕ) : (⇑(A.affineEquiv t))^[k] x = (⇑A)^[k] x + A.partialNorm k t

The k-th iterate of an affine equivalence is the k-th iterate of its linear part plus the k-th partial norm of its translation part.

The period criterion

theorem AddEquiv.affineEquiv_iterate_eq_id_iff {T : Type u_1} [AddCommGroup T] (A : T ≃+ T) (t : T) (m : ℕ) : (⇑(A.affineEquiv t))^[m] = id ↔ (⇑A)^[m] = id ∧ A.partialNorm m t = 0

An affine equivalence has m-th iterate the identity exactly when its linear part has m-th iterate the identity and the m-th partial norm of its translation part vanishes.

theorem AddEquiv.affineEquiv_pow_eq_one_iff {T : Type u_1} [AddCommGroup T] (A : T ≃+ T) (t : T) (m : ℕ) : A.affineEquiv t ^ m = 1 ↔ (⇑A)^[m] = id ∧ A.partialNorm m t = 0

An affine equivalence has m-th power the identity exactly when its linear part has m-th iterate the identity and the m-th partial norm of its translation part vanishes. This is AddEquiv.affineEquiv_iterate_eq_id_iff stated in the group of permutations of T.

theorem AddEquiv.affineEquiv_pow_eq_one_iff_of_iterate_eq_id {T : Type u_1} [AddCommGroup T] (A : T ≃+ T) (t : T) (m : ℕ) (hA : (⇑A)^[m] = id) : A.affineEquiv t ^ m = 1 ↔ A.partialNorm m t = 0

If the linear part has m-th iterate the identity, then the affine equivalence has m-th power the identity exactly when the m-th partial norm of its translation part vanishes: the order of the affine equivalence then divides m (AddEquiv.orderOf_affineEquiv_dvd_iff).

theorem AddEquiv.orderOf_affineEquiv_dvd_iff {T : Type u_1} [AddCommGroup T] (A : T ≃+ T) (t : T) (m : ℕ) (hA : (⇑A)^[m] = id) : orderOf (A.affineEquiv t) ∣ m ↔ A.partialNorm m t = 0

Under a linear part of period dividing m, the order of the affine equivalence divides m exactly when the m-th partial norm of its translation part vanishes.

theorem AddEquiv.orderOf_affineEquiv_eq_iff {T : Type u_1} [AddCommGroup T] (A : T ≃+ T) (t : T) (m : ℕ) (hm : 0 < m) (hA : (⇑A)^[m] = id) : orderOf (A.affineEquiv t) = m ↔ A.partialNorm m t = 0 ∧ ∀ (k : ℕ), 0 < k → k < m → (⇑A)^[k] ≠ id ∨ A.partialNorm k t ≠ 0

The exact order criterion: under a linear part of period dividing m, the affine equivalence has exact order m exactly when its m-th partial norm vanishes and no smaller positive iterate is the identity. For an affine equivalence the latter means that every iterate with 0 < k < m has a nontrivial linear part or a nonzero partial norm.

The action of ZMod m by iterates

@[instance_reducible]

noncomputable def AddEquiv.affineAddAction {T : Type u_1} [AddCommGroup T] {m : ℕ} [NeZero m] (A : T ≃+ T) (t : T) (hA : (⇑A)^[m] = id) (hN : A.partialNorm m t = 0) : AddAction (ZMod m) T

The action of ZMod m on T by the iterates of an affine equivalence whose m-th power is the identity: the residue k acts by the k-th iterate, which is well defined because the iterates are periodic with period m. AddEquiv.affineAddAction_vadd evaluates it.

@[simp]

theorem AddEquiv.affineAddAction_vadd {T : Type u_1} [AddCommGroup T] {m : ℕ} [NeZero m] (A : T ≃+ T) (t : T) (hA : (⇑A)^[m] = id) (hN : A.partialNorm m t = 0) (k : ZMod m) (x : T) : k +ᵥ x = (⇑(A.affineEquiv t))^[k.val] x

The residue k of ZMod m acts on T by the k-th iterate of the affine equivalence.

theorem AddEquiv.affineAddAction_one_vadd {T : Type u_1} [AddCommGroup T] {m : ℕ} [NeZero m] (A : T ≃+ T) (t : T) (hA : (⇑A)^[m] = id) (hN : A.partialNorm m t = 0) (x : T) : 1 +ᵥ x = (A.affineEquiv t) x

The residue 1 of ZMod m acts by the affine equivalence itself: the action is generated by the affine equivalence.

Fixed points of the iterates

theorem AddEquiv.affineEquiv_iterate_apply_eq_self_iff {T : Type u_1} [AddCommGroup T] (A : T ≃+ T) (t x : T) (k : ℕ) : (⇑(A.affineEquiv t))^[k] x = x ↔ x - (⇑A)^[k] x = A.partialNorm k t

Fixed points of an iterate. A point x is fixed by the k-th iterate of x ↦ A x + t exactly when x - A^k x is the k-th partial norm of t.

theorem AddEquiv.exists_affineEquiv_iterate_apply_eq_self_iff {T : Type u_1} [AddCommGroup T] (A : T ≃+ T) (t : T) (k : ℕ) : (∃ (x : T), (⇑(A.affineEquiv t))^[k] x = x) ↔ ∃ (b : T), b - (⇑A)^[k] b = A.partialNorm k t

The fixed-point criterion. The k-th iterate of x ↦ A x + t has a fixed point exactly when the k-th partial norm of t lies in the image of 1 - A^k.

Faithfulness and freeness of the action of ZMod m

theorem AddEquiv.faithfulVAdd_affineAddAction_iff {T : Type u_1} [AddCommGroup T] {m : ℕ} [NeZero m] (A : T ≃+ T) (t : T) (hA : (⇑A)^[m] = id) (hN : A.partialNorm m t = 0) : FaithfulVAdd (ZMod m) T ↔ orderOf (A.affineEquiv t) = m

Faithfulness. The action of ZMod m by the iterates of x ↦ A x + t is faithful exactly when the affine equivalence has exact order m.

theorem AddEquiv.isCancelVAdd_affineAddAction_iff {T : Type u_1} [AddCommGroup T] {m : ℕ} [NeZero m] (A : T ≃+ T) (t : T) (hA : (⇑A)^[m] = id) (hN : A.partialNorm m t = 0) : IsCancelVAdd (ZMod m) T ↔ ∀ (k : ℕ), 0 < k → k < m → ∀ (b : T), b - (⇑A)^[k] b ≠ A.partialNorm k t

Freeness. The action of ZMod m by the iterates of x ↦ A x + t is free, that is IsCancelVAdd, or equivalently every point has trivial stabilizer, exactly when for every 0 < k < m the k-th partial norm of t does not lie in the image of 1 - A^k.

For composite m, checking the generator alone does not suffice: x ↦ x + 1 on ZMod 2 has no fixed point, but with m = 4 its square is the identity. For prime m the generator suffices (AddEquiv.isCancelVAdd_affineAddAction_iff_of_prime).

theorem AddEquiv.isCancelVAdd_affineAddAction_iff_of_prime {T : Type u_1} [AddCommGroup T] {m : ℕ} [NeZero m] (A : T ≃+ T) (t : T) (hA : (⇑A)^[m] = id) (hN : A.partialNorm m t = 0) (hm : Nat.Prime m) : IsCancelVAdd (ZMod m) T ↔ ∀ (b : T), b - A b ≠ t

Freeness in prime order. For m prime, the action of ZMod m by the iterates of x ↦ A x + t is free exactly when the affine equivalence has no fixed point, that is when t does not lie in the image of 1 - A: every nonzero residue generates ZMod m.