Documentation

TauCeti.RepresentationTheory.Cyclic.Restriction

Restricting cyclic representations of additive automorphisms #

A homomorphism χ : C_n → C_m sending the selected generator to its d-th power restricts the cyclic representation of A to one whose generator acts by A^d. An additive map intertwining A^d with B therefore gives a morphism from the restricted representation of A to the cyclic representation of B.

AddMonoidHom.cyclicRepResHom constructs this morphism from the generator equation, without requiring equivariance to be supplied separately for every group element. It permits the degree-one partial norms, degree-two classes, and connecting classes of cyclic representations to be compared under arbitrary homomorphisms of cyclic groups.

References #

source
noncomputable def AddMonoidHom.cyclicRepResHom {T M : Type u} [AddCommGroup T] [AddCommGroup M] {m n : ℕ} [NeZero m] [NeZero n] {A : T ≃+ T} {B : M ≃+ M} (f : T →+ M) (hA : (⇑A)^[m] = _root_.id) (hB : (⇑B)^[n] = _root_.id) (χ : Multiplicative (ZMod n) →* Multiplicative (ZMod m)) (d : ℕ) (hχ : χ (Multiplicative.ofAdd 1) = Multiplicative.ofAdd 1 ^ d) (hf : ∀ (x : T), f ((⇑A)^[d] x) = B (f x)) :
Rep.res χ (A.cyclicRep hA) ⟶ B.cyclicRep hB

An additive map intertwining A^d with B is equivariant from the restriction of the cyclic representation of A along χ to that of B, when χ sends the generator to its d-th power. Neither injectivity nor surjectivity of χ is required.

Instances For
    source
    @[simp]
    theorem AddMonoidHom.coe_cyclicRepResHom_hom {T M : Type u} [AddCommGroup T] [AddCommGroup M] {m n : ℕ} [NeZero m] [NeZero n] {A : T ≃+ T} {B : M ≃+ M} (f : T →+ M) (hA : (⇑A)^[m] = _root_.id) (hB : (⇑B)^[n] = _root_.id) (χ : Multiplicative (ZMod n) →* Multiplicative (ZMod m)) (d : ℕ) (hχ : χ (Multiplicative.ofAdd 1) = Multiplicative.ofAdd 1 ^ d) (hf : ∀ (x : T), f ((⇑A)^[d] x) = B (f x)) :
    ⇑(Rep.Hom.hom (f.cyclicRepResHom hA hB χ d hχ hf)) = ⇑f

    On underlying groups the morphism induced by f is f. The coercion is stated on intertwining maps, so simplification also recognizes evaluations with restricted instances.