The cyclic representation of an automorphism of finite order

Let T be an additive commutative group, m > 0, and A : T ≃+ T an additive automorphism of order dividing m, that is A^[m] = id. Then the cyclic group C_m = Multiplicative (ZMod m) acts on T with its standard generator ofAdd 1 acting by A; this is the integral representation AddEquiv.cyclicRep A hA : Rep ℤ C_m. Its norm N = ∑ g, ρ g is the ordered sum of powers ∑ j < m, A^j (AddEquiv.cyclicRepresentation_norm_apply).

Its group cohomology is read off in TauCeti.RepresentationTheory.Homological.GroupCohomology.CyclicAutomorphism.

Main definitions

• AddEquiv.cyclicRepresentation A hA: the representation of C_m on T in which the generator acts by A.
• AddEquiv.cyclicRep A hA: the same representation, as an object of Rep ℤ C_m.
• AddMonoidHom.cyclicRepHom f hA hB hf: an additive map f with f ∘ A = B ∘ f, as a morphism of cyclic representations; it is compatible with composition (AddMonoidHom.cyclicRepHom_comp).
• AddEquiv.cyclicRepBinaryBicone hA hB: the cyclic representation of the product automorphism A × B of T × M, with the projections and inclusions of T × M, as a binary bicone of the cyclic representations of A and B; it is a biproduct (AddEquiv.cyclicRepBinaryBiconeIsBilimit).

Main results

• AddEquiv.cyclicRepresentation_ofAdd_apply: the element a of C_m acts by A^[a.val].
• AddEquiv.cyclicRepresentation_norm_apply, AddEquiv.cyclicRep_norm_apply: the norm is the ordered sum of powers of A.
• AddEquiv.mem_ker_cyclicRep_norm_iff, AddEquiv.mem_range_cyclicRep_norm_iff: the kernel and image of the norm, in terms of the ordered sum of powers of A.
• AddEquiv.mem_ker_cyclicRep_applyAsHom_sub_iff, AddEquiv.mem_range_cyclicRep_applyAsHom_sub_iff: the kernel of ρ(g) - 𝟙 for the generator g is the fixed points of A, and its image is that of 1 - A.
• AddEquiv.mem_ker_cyclicRep_refl_norm_iff, AddEquiv.mem_range_cyclicRep_refl_norm_iff: for the trivial action, given by the identity automorphism, the kernel of the norm is the m-torsion and its image is m T.
• AddMonoidHom.exists_apply_eq_sum_range_iterate, AddMonoidHom.sum_range_iterate_add_apply: for an exact sequence 0 → Λ → E → T with maps intertwining automorphisms of order dividing m, the norm of a lift of a norm-zero element of T is the image of a fixed point, and changing the lift by l adds the norm of l.

noncomputable def AddEquiv.cyclicRepresentation {T : Type u_1} [AddCommGroup T] {m : ℕ} [NeZero m] (A : T ≃+ T) (hA : (⇑A)^[m] = id) : Representation ℤ (Multiplicative (ZMod m)) T

The integral representation of the cyclic group C_m = Multiplicative (ZMod m) on T in which the generator ofAdd 1 acts by an additive automorphism A of order dividing m.

theorem AddEquiv.cyclicRepresentation_ofAdd_apply {T : Type u_1} [AddCommGroup T] {m : ℕ} [NeZero m] (A : T ≃+ T) (hA : (⇑A)^[m] = id) (a : ZMod m) (x : T) : ((A.cyclicRepresentation hA) (Multiplicative.ofAdd a)) x = (⇑A)^[a.val] x

The element a of C_m acts on T by the a.val-th iterate of A.

@[simp]

theorem AddEquiv.cyclicRepresentation_ofAdd_one_apply {T : Type u_1} [AddCommGroup T] {m : ℕ} [NeZero m] (A : T ≃+ T) (hA : (⇑A)^[m] = id) (x : T) : ((A.cyclicRepresentation hA) (Multiplicative.ofAdd 1)) x = A x

The generator ofAdd 1 of C_m acts on T by A.

theorem AddEquiv.cyclicRepresentation_ofAdd_one_pow_apply {T : Type u_1} [AddCommGroup T] {m : ℕ} [NeZero m] (A : T ≃+ T) (hA : (⇑A)^[m] = id) (d : ℕ) (x : T) : ((A.cyclicRepresentation hA) (Multiplicative.ofAdd 1 ^ d)) x = (⇑A)^[d] x

A power of the selected generator acts by the corresponding iterate, without reducing its exponent modulo the period.

theorem AddEquiv.cyclicRepresentation_norm_apply {T : Type u_1} [AddCommGroup T] {m : ℕ} [NeZero m] (A : T ≃+ T) (hA : (⇑A)^[m] = id) (x : T) : (A.cyclicRepresentation hA).norm x = ∑ j ∈ Finset.range m, (⇑A)^[j] x

The norm of the cyclic representation of A is the ordered sum of the powers A^0, …, A^(m-1).

@[reducible, inline]

noncomputable abbrev AddEquiv.cyclicRep {T : Type u_1} [AddCommGroup T] {m : ℕ} [NeZero m] (A : T ≃+ T) (hA : (⇑A)^[m] = id) : Rep ℤ (Multiplicative (ZMod m))

The cyclic representation of A as an object of Rep ℤ C_m.

theorem AddEquiv.cyclicRep_norm_apply {T : Type u_1} [AddCommGroup T] {m : ℕ} [NeZero m] (A : T ≃+ T) (hA : (⇑A)^[m] = id) (x : T) : (Rep.Hom.hom (A.cyclicRep hA).norm.asHom).toLinearMap x = ∑ j ∈ Finset.range m, (⇑A)^[j] x

The norm of the bundled cyclic representation of A is the ordered sum of its powers.

theorem AddEquiv.mem_ker_cyclicRep_norm_iff {T : Type u_1} [AddCommGroup T] {m : ℕ} [NeZero m] (A : T ≃+ T) (hA : (⇑A)^[m] = id) (x : T) : x ∈ (Rep.Hom.hom (A.cyclicRep hA).norm.asHom).ker ↔ ∑ j ∈ Finset.range m, (⇑A)^[j] x = 0

An element of T lies in the kernel of the norm of the cyclic representation of A exactly when the ordered sum of its images under the powers of A vanishes.

theorem AddEquiv.mem_range_cyclicRep_norm_iff {T : Type u_1} [AddCommGroup T] {m : ℕ} [NeZero m] (A : T ≃+ T) (hA : (⇑A)^[m] = id) (x : T) : x ∈ (Rep.Hom.hom (A.cyclicRep hA).norm.asHom).range ↔ ∃ (y : T), ∑ j ∈ Finset.range m, (⇑A)^[j] y = x

An element of T lies in the image of the norm of the cyclic representation of A exactly when it is the ordered sum of the images of some y under the powers of A.

theorem AddEquiv.cyclicRep_applyAsHom_sub_apply {T : Type u_1} [AddCommGroup T] {m : ℕ} [NeZero m] (A : T ≃+ T) (hA : (⇑A)^[m] = id) (y : T) : (Rep.Hom.hom ((A.cyclicRep hA).applyAsHom (Multiplicative.ofAdd 1) - CategoryTheory.CategoryStruct.id (A.cyclicRep hA))).toLinearMap y = A y - y

The map ρ(g) - 𝟙 of the periodic resolution, for the generator g = ofAdd 1, sends y to A y - y.

theorem AddEquiv.mem_ker_cyclicRep_applyAsHom_sub_iff {T : Type u_1} [AddCommGroup T] {m : ℕ} [NeZero m] (A : T ≃+ T) (hA : (⇑A)^[m] = id) (x : T) : x ∈ (Rep.Hom.hom ((A.cyclicRep hA).applyAsHom (Multiplicative.ofAdd 1) - CategoryTheory.CategoryStruct.id (A.cyclicRep hA))).ker ↔ A x = x

An element of T lies in the kernel of ρ(g) - 𝟙, for the generator g = ofAdd 1, exactly when it is fixed by A.

theorem AddEquiv.mem_range_cyclicRep_applyAsHom_sub_iff {T : Type u_1} [AddCommGroup T] {m : ℕ} [NeZero m] (A : T ≃+ T) (hA : (⇑A)^[m] = id) (x : T) : x ∈ (Rep.Hom.hom ((A.cyclicRep hA).applyAsHom (Multiplicative.ofAdd 1) - CategoryTheory.CategoryStruct.id (A.cyclicRep hA))).range ↔ ∃ (b : T), b - A b = x

An element of T lies in the image of ρ(g) - 𝟙, for the generator g = ofAdd 1, exactly when it has the form b - A b: the images of A - 1 and 1 - A agree.

The trivial action

theorem AddEquiv.iterate_refl {T : Type u_1} [AddCommGroup T] (n : ℕ) : (⇑(refl T))^[n] = id

The identity automorphism has order dividing every n. Its cyclic representation is the trivial action of C_n on T.

theorem AddEquiv.mem_ker_cyclicRep_refl_norm_iff {T : Type u_1} [AddCommGroup T] {m : ℕ} [NeZero m] (x : T) : x ∈ (Rep.Hom.hom ((refl T).cyclicRep ⋯).norm.asHom).ker ↔ x ∈ Submodule.torsionBy ℤ T ↑m

For the trivial action, the kernel of the norm is the m-torsion.

theorem AddEquiv.mem_range_cyclicRep_refl_norm_iff {T : Type u_1} [AddCommGroup T] {m : ℕ} [NeZero m] (x : T) : x ∈ (Rep.Hom.hom ((refl T).cyclicRep ⋯).norm.asHom).range ↔ ∃ (y : T), m • y = x

For the trivial action, the image of the norm is m T.

theorem AddEquiv.mem_ker_cyclicRep_refl_applyAsHom_sub {T : Type u_1} [AddCommGroup T] {m : ℕ} [NeZero m] (x : T) : x ∈ (Rep.Hom.hom (((refl T).cyclicRep ⋯).applyAsHom (Multiplicative.ofAdd 1) - CategoryTheory.CategoryStruct.id ((refl T).cyclicRep ⋯))).ker

For the trivial action, every element is fixed by the generator.

theorem AddEquiv.mem_range_cyclicRep_refl_applyAsHom_sub_iff {T : Type u_1} [AddCommGroup T] {m : ℕ} [NeZero m] (x : T) : x ∈ (Rep.Hom.hom (((refl T).cyclicRep ⋯).applyAsHom (Multiplicative.ofAdd 1) - CategoryTheory.CategoryStruct.id ((refl T).cyclicRep ⋯))).range ↔ x = 0

For the trivial action, the image of ρ(g) - 𝟙, for the generator g, is zero.

noncomputable def AddMonoidHom.cyclicRepHom {T M : Type u} [AddCommGroup T] [AddCommGroup M] {m : ℕ} [NeZero m] {A : T ≃+ T} {B : M ≃+ M} (f : T →+ M) (hA : (⇑A)^[m] = _root_.id) (hB : (⇑B)^[m] = _root_.id) (hf : ∀ (x : T), f (A x) = B (f x)) : A.cyclicRep hA ⟶ B.cyclicRep hB

An additive map f : T →+ M with f ∘ A = B ∘ f is a morphism from the cyclic representation of A to that of B.

@[simp]

theorem AddMonoidHom.coe_cyclicRepHom_hom {T M : Type u} [AddCommGroup T] [AddCommGroup M] {m : ℕ} [NeZero m] {A : T ≃+ T} {B : M ≃+ M} (f : T →+ M) (hA : (⇑A)^[m] = _root_.id) (hB : (⇑B)^[m] = _root_.id) (hf : ∀ (x : T), f (A x) = B (f x)) : ⇑(Rep.Hom.hom (f.cyclicRepHom hA hB hf)) = ⇑f

The morphism of cyclic representations defined by f is f on underlying groups. The coercion is stated on the intertwining maps of the underlying representations, rather than of the Rep objects, which is the form simp meets in applications.

theorem AddMonoidHom.cyclicRepHom_comp {T M : Type u} [AddCommGroup T] [AddCommGroup M] {m : ℕ} [NeZero m] {A : T ≃+ T} {B : M ≃+ M} (f : T →+ M) (hA : (⇑A)^[m] = _root_.id) (hB : (⇑B)^[m] = _root_.id) (hf : ∀ (x : T), f (A x) = B (f x)) {N : Type u} [AddCommGroup N] {C : N ≃+ N} (g : M →+ N) (hC : (⇑C)^[m] = _root_.id) (hg : ∀ (x : M), g (B x) = C (g x)) : (g.comp f).cyclicRepHom hA hC ⋯ = CategoryTheory.CategoryStruct.comp (f.cyclicRepHom hA hB hf) (g.cyclicRepHom hB hC hg)

The morphism of cyclic representations defined by a composite g ∘ f is the composite of the morphisms defined by f and g.

Products

noncomputable def AddEquiv.cyclicRepBinaryBicone {T M : Type u} [AddCommGroup T] [AddCommGroup M] {m : ℕ} {A : T ≃+ T} {B : M ≃+ M} (hA : (⇑A)^[m] = id) (hB : (⇑B)^[m] = id) [NeZero m] : CategoryTheory.Limits.BinaryBicone (A.cyclicRep hA) (B.cyclicRep hB)

The cyclic representation of the product automorphism A × B of T × M, with the morphisms of cyclic representations defined by the projections T × M → T, T × M → M and the inclusions T → T × M, M → T × M, is a binary bicone of the cyclic representations of A and B. It is a biproduct (AddEquiv.cyclicRepBinaryBiconeIsBilimit). Its body is exposed, so that its cone point is the cyclic representation of A × B and its structure maps are the morphisms defined by the projections and inclusions by definition, as the cohomology of the cyclic representation of A × B is read through this bicone.

noncomputable def AddEquiv.cyclicRepBinaryBiconeIsBilimit {T M : Type u} [AddCommGroup T] [AddCommGroup M] {m : ℕ} {A : T ≃+ T} {B : M ≃+ M} (hA : (⇑A)^[m] = id) (hB : (⇑B)^[m] = id) [NeZero m] : (cyclicRepBinaryBicone hA hB).IsBilimit

The cyclic representation of A × B is the biproduct of the cyclic representations of A and B, with the projections and inclusions of T × M as structure maps.

Norms along an equivariant exact sequence

theorem AddMonoidHom.sum_range_iterate_add_apply {Λ : Type u_1} {E : Type u_2} [AddCommGroup Λ] [AddCommGroup E] {m : ℕ} {AΛ : Λ ≃+ Λ} {AE : E ≃+ E} (i : Λ →+ E) (hi : ∀ (x : Λ), i (AΛ x) = AE (i x)) (s : E) (l : Λ) : ∑ j ∈ Finset.range m, (⇑AE)^[j] (s + i l) = ∑ j ∈ Finset.range m, (⇑AE)^[j] s + i (∑ j ∈ Finset.range m, (⇑AΛ)^[j] l)

Changing the lift s by the image of l : Λ changes the norm ∑ j < m, AE^j s by the image of the norm ∑ j < m, AΛ^j l.

theorem AddMonoidHom.exists_apply_eq_sum_range_iterate {Λ : Type u_1} {E : Type u_2} {T : Type u_3} [AddCommGroup Λ] [AddCommGroup E] [AddCommGroup T] {m : ℕ} {AΛ : Λ ≃+ Λ} {AE : E ≃+ E} {AT : T ≃+ T} (i : Λ →+ E) (p : E →+ T) [NeZero m] (hE : (⇑AE)^[m] = _root_.id) (hi : ∀ (x : Λ), i (AΛ x) = AE (i x)) (hp : ∀ (x : E), p (AE x) = AT (p x)) (hinj : Function.Injective ⇑i) (hexact : Function.Exact ⇑i ⇑p) {s : E} (hs : ∑ j ∈ Finset.range m, (⇑AT)^[j] (p s) = 0) : ∃ (v : Λ), AΛ v = v ∧ i v = ∑ j ∈ Finset.range m, (⇑AE)^[j] s

The norm ∑ j < m, AE^j s of a lift s of a norm-zero element of T is the image of a fixed point of AΛ.