Pushforward and restriction of Novikov series

Let N : H →+ ℝ and N' : H' →+ ℝ be period homomorphisms and φ : H →+ H' a homomorphism of exponent groups that rescales periods by a positive constant: N' (φ h) = c * N h for some c > 0. For instance, the inclusion of a subgroup K ≤ H, with the restricted period map N.comp K.subtype, rescales periods by c = 1. For a finite cyclic covering, the exponent group of the cover is such a finite-index subgroup of the exponent group of the base.

Together with an additive map ρ : R →+ S of coefficients, φ pushes a Novikov series forward by summing coefficients along the fibres of φ:

(map ρ φ hφ a).coeff h' = ∑ᶠ h ∈ φ ⁻¹' {h'}, ρ (a.coeff h).

Since φ rescales periods, only finitely many nonzero coefficients of a lie in a fibre, and the result is again a Novikov series. No finiteness of the kernel of φ is needed. The pushforward is additive and satisfies the identity and composition laws, which include its naturality in the coefficient map. It extends the pushforward Finsupp.mapDomain φ ∘ Finsupp.mapRange ρ of the group ring, and sends series vanishing below the period cutoff C to series vanishing below c * C.

When φ has finite kernel, a Novikov series on H' also restricts along φ by precomposing its coefficients (TauCeti.NovikovSeries.comap), sending series vanishing below c * C to series vanishing below C. Restricting a pushforward along an injective φ gives back the series with ρ applied to its coefficients. Restriction keeps a monomial r e^(φ h) as r e^h when φ is injective, and kills a monomial whose exponent is not in the range of φ.

Main definitions

• TauCeti.NovikovSeries.map: the pushforward of Novikov series along a coefficient map and a period-rescaling exponent homomorphism.
• TauCeti.NovikovSeries.comap: the restriction of Novikov series along a period-rescaling exponent homomorphism with finite kernel.

Main results

• TauCeti.NovikovSeries.finite_support_inter_preimage_singleton: a fibre of a period-rescaling homomorphism meets the support of a Novikov series in a finite set.
• TauCeti.NovikovSeries.finite_setOf_map_add_eq: only finitely many pairs of support exponents of two Novikov series have images under a period-rescaling homomorphism adding up to a given exponent.
• TauCeti.NovikovSeries.exists_period_rescale_id and TauCeti.NovikovSeries.exists_period_rescale_comp: the identity rescales periods by 1, and composites rescale them by the product of the factors.
• TauCeti.NovikovSeries.period_rescale_neg: negating both a period-preserving exponent map and its target period rescales periods by 1.
• TauCeti.NovikovSeries.coeff_map_eq_sum: a coefficient of a pushforward as a sum over any finite set of exponents in the fibre containing the nonzero coefficients there.
• TauCeti.NovikovSeries.map_surjective: pushforward along surjective coefficient and exponent maps is surjective, even when the exponent map has infinite kernel.
• TauCeti.NovikovSeries.map_injective: pushforward along injective coefficient and exponent maps is injective.
• TauCeti.NovikovSeries.map_id and TauCeti.NovikovSeries.map_map: the identity and composition laws of the pushforward.
• TauCeti.NovikovSeries.map_ofFinsupp: the pushforward of a finitely supported series is the group-ring pushforward.
• TauCeti.NovikovSeries.map_single: the pushforward of the monomial r e^g is the monomial ρ r e^(φ g).
• TauCeti.NovikovSeries.coeff_map_eq_zero_of_lt and TauCeti.NovikovSeries.coeff_comap_eq_zero_of_lt: the pushforward moves the period cutoff C to c * C, and the restriction moves c * C back to C.
• TauCeti.NovikovSeries.comap_comap and TauCeti.NovikovSeries.comap_map_of_injective: the composition law of restriction, and restriction of a pushforward along an injective homomorphism.
• TauCeti.NovikovSeries.comap_single_of_injective and TauCeti.NovikovSeries.comap_single_of_notMem_range: restriction of monomials.

References

• M. Hutchings, Reidemeister torsion in generalized Morse theory, Forum Math. 14 (2002), Section 2.
• A. Pajitnov, Circle-valued Morse Theory, de Gruyter 2006, Chapter 3.

theorem TauCeti.NovikovSeries.period_rescale_neg {H : Type u_4} {H' : Type u_5} [AddZeroClass H] [AddCommGroup H'] {N : H →+ ℝ} {N' : H' →+ ℝ} {φ : H →+ H'} (hφ : ∀ (h : H), N' (φ h) = N h) (h : H) : (-N') ((-φ) h) = 1 * N h

Negating both the target period and a period-preserving exponent map rescales periods by 1.

theorem TauCeti.NovikovSeries.finite_support_inter_preimage_singleton {R : Type u_1} {H : Type u_4} {H' : Type u_5} [AddZeroClass H] [AddZeroClass H'] {N : H →+ ℝ} {N' : H' →+ ℝ} [Zero R] (a : NovikovSeries R H N) {φ : H →+ H'} (hφ : ∃ c > 0, ∀ (h : H), N' (φ h) = c * N h) (h' : H') : (a.support ∩ ⇑φ ⁻¹' {h'}).Finite

If φ rescales periods by a positive constant, only finitely many exponents in a fibre of φ carry a nonzero coefficient of a Novikov series.

theorem TauCeti.NovikovSeries.finite_setOf_map_add_eq {R : Type u_1} {S : Type u_2} {H : Type u_4} {H' : Type u_5} [AddZeroClass H] [AddZeroClass H'] {N : H →+ ℝ} {N' : H' →+ ℝ} [Zero R] [Zero S] (a : NovikovSeries R H N) (b : NovikovSeries S H N) {φ : H →+ H'} (hφ : ∃ c > 0, ∀ (h : H), N' (φ h) = c * N h) (h' : H') : {p : H × H | φ p.1 + φ p.2 = h' ∧ a.coeff p.1 ≠ 0 ∧ b.coeff p.2 ≠ 0}.Finite

If φ rescales periods by a positive constant, then for two Novikov series only finitely many pairs of support exponents have images under φ adding up to a given exponent.

theorem TauCeti.NovikovSeries.exists_period_rescale_id {H : Type u_4} [AddZeroClass H] {N : H →+ ℝ} : ∃ c > 0, ∀ (h : H), N ((AddMonoidHom.id H) h) = c * N h

The identity rescales periods by 1.

theorem TauCeti.NovikovSeries.exists_period_rescale_comp {H : Type u_4} {H' : Type u_5} {H'' : Type u_6} [AddZeroClass H] [AddZeroClass H'] [AddZeroClass H''] {N : H →+ ℝ} {N' : H' →+ ℝ} {N'' : H'' →+ ℝ} {φ : H →+ H'} {φ' : H' →+ H''} (hφ : ∃ c > 0, ∀ (h : H), N' (φ h) = c * N h) (hφ' : ∃ c > 0, ∀ (h : H'), N'' (φ' h) = c * N' h) : ∃ c > 0, ∀ (h : H), N'' ((φ'.comp φ) h) = c * N h

If φ rescales periods by c and φ' by c', then φ'.comp φ rescales them by c' * c.

theorem TauCeti.NovikovSeries.period_rescale_symm {H : Type u_4} {H' : Type u_5} [AddZeroClass H] [AddZeroClass H'] {N : H →+ ℝ} {N' : H' →+ ℝ} {e : H ≃+ H'} {c : ℝ} (hc : 0 < c) (hcN : ∀ (h : H), N' (e h) = c * N h) (h' : H') : N (e.symm h') = c⁻¹ * N' h'

If an additive equivalence rescales periods by a positive factor c, its inverse rescales them by c⁻¹.

theorem TauCeti.NovikovSeries.exists_period_rescale_symm {H : Type u_4} {H' : Type u_5} [AddZeroClass H] [AddZeroClass H'] {N : H →+ ℝ} {N' : H' →+ ℝ} {e : H ≃+ H'} (he : ∃ c > 0, ∀ (h : H), N' (e h) = c * N h) : ∃ c > 0, ∀ (h' : H'), N (e.symm h') = c * N' h'

The inverse of an additive equivalence that rescales periods positively also rescales periods positively.

theorem TauCeti.NovikovSeries.exists_period_rescale_trans {H : Type u_4} {H' : Type u_5} {H'' : Type u_6} [AddZeroClass H] [AddZeroClass H'] [AddZeroClass H''] {N : H →+ ℝ} {N' : H' →+ ℝ} {N'' : H'' →+ ℝ} {e : H ≃+ H'} {e' : H' ≃+ H''} (he : ∃ c > 0, ∀ (h : H), N' (e h) = c * N h) (he' : ∃ c > 0, ∀ (h : H'), N'' (e' h) = c * N' h) : ∃ c > 0, ∀ (h : H), N'' ((e.trans e') h) = c * N h

Successive additive equivalences rescaling periods positively have a composite that also rescales periods positively.

noncomputable def TauCeti.NovikovSeries.map {R : Type u_1} {S : Type u_2} {H : Type u_4} {H' : Type u_5} [AddZeroClass H] [AddZeroClass H'] {N : H →+ ℝ} {N' : H' →+ ℝ} [AddMonoid R] [AddCommMonoid S] (ρ : R →+ S) (φ : H →+ H') (hφ : ∃ c > 0, ∀ (h : H), N' (φ h) = c * N h) : NovikovSeries R H N →+ NovikovSeries S H' N'

The pushforward of a Novikov series along a coefficient map ρ and an exponent homomorphism φ rescaling periods by a positive constant: the coefficient at h' is the sum of the images under ρ of the coefficients at the exponents h with φ h = h'.

theorem TauCeti.NovikovSeries.coeff_map {R : Type u_1} {S : Type u_2} {H : Type u_4} {H' : Type u_5} [AddZeroClass H] [AddZeroClass H'] {N : H →+ ℝ} {N' : H' →+ ℝ} [AddMonoid R] [AddCommMonoid S] (ρ : R →+ S) (φ : H →+ H') (hφ : ∃ c > 0, ∀ (h : H), N' (φ h) = c * N h) (a : NovikovSeries R H N) (h' : H') : ((map ρ φ hφ) a).coeff h' = ∑ᶠ (h : H) (_ : h ∈ ⇑φ ⁻¹' {h'}), ρ (a.coeff h)

The coefficient of a pushforward at h' is the sum of the images under ρ of the coefficients at the exponents in the fibre of φ over h'.

theorem TauCeti.NovikovSeries.coeff_map_eq_sum {R : Type u_1} {S : Type u_2} {H : Type u_4} {H' : Type u_5} [AddZeroClass H] [AddZeroClass H'] {N : H →+ ℝ} {N' : H' →+ ℝ} [AddMonoid R] [AddCommMonoid S] (ρ : R →+ S) (φ : H →+ H') (hφ : ∃ c > 0, ∀ (h : H), N' (φ h) = c * N h) (a : NovikovSeries R H N) {h' : H'} (s : Finset H) (hs : a.support ∩ ⇑φ ⁻¹' {h'} ⊆ ↑s) (hsφ : ∀ h ∈ s, φ h = h') : ((map ρ φ hφ) a).coeff h' = ∑ h ∈ s, ρ (a.coeff h)

A coefficient of a pushforward is the sum over any finite set of exponents in the fibre containing the exponents of nonzero coefficient there.

theorem TauCeti.NovikovSeries.support_map_subset {R : Type u_1} {S : Type u_2} {H : Type u_4} {H' : Type u_5} [AddZeroClass H] [AddZeroClass H'] {N : H →+ ℝ} {N' : H' →+ ℝ} [AddMonoid R] [AddCommMonoid S] (ρ : R →+ S) (φ : H →+ H') (hφ : ∃ c > 0, ∀ (h : H), N' (φ h) = c * N h) (a : NovikovSeries R H N) : ((map ρ φ hφ) a).support ⊆ ⇑φ '' a.support

Every exponent of nonzero coefficient of a pushforward is the image of an exponent of nonzero coefficient.

theorem TauCeti.NovikovSeries.coeff_map_eq_zero_of_notMem_range {R : Type u_1} {S : Type u_2} {H : Type u_4} {H' : Type u_5} [AddZeroClass H] [AddZeroClass H'] {N : H →+ ℝ} {N' : H' →+ ℝ} [AddMonoid R] [AddCommMonoid S] (ρ : R →+ S) (φ : H →+ H') (hφ : ∃ c > 0, ∀ (h : H), N' (φ h) = c * N h) (a : NovikovSeries R H N) {h' : H'} (hh' : h' ∉ Set.range ⇑φ) : ((map ρ φ hφ) a).coeff h' = 0

A pushforward has zero coefficient outside the range of the exponent homomorphism.

theorem TauCeti.NovikovSeries.coeff_map_of_support_inter_subset_singleton {R : Type u_1} {S : Type u_2} {H : Type u_4} {H' : Type u_5} [AddZeroClass H] [AddZeroClass H'] {N : H →+ ℝ} {N' : H' →+ ℝ} [AddMonoid R] [AddCommMonoid S] (ρ : R →+ S) (φ : H →+ H') (hφ : ∃ c > 0, ∀ (h : H), N' (φ h) = c * N h) (a : NovikovSeries R H N) {h : H} (hs : a.support ∩ ⇑φ ⁻¹' {φ h} ⊆ {h}) : ((map ρ φ hφ) a).coeff (φ h) = ρ (a.coeff h)

If h is the only exponent of nonzero coefficient in its fibre, the pushforward moves the coefficient at h to φ h.

theorem TauCeti.NovikovSeries.map_surjective {R : Type u_1} {S : Type u_2} {H : Type u_4} {H' : Type u_5} [AddZeroClass H] [AddZeroClass H'] {N : H →+ ℝ} {N' : H' →+ ℝ} [AddMonoid R] [AddCommMonoid S] (ρ : R →+ S) (φ : H →+ H') (hφ : ∃ c > 0, ∀ (h : H), N' (φ h) = c * N h) (hρ : Function.Surjective ⇑ρ) (hφs : Function.Surjective ⇑φ) : Function.Surjective ⇑(map ρ φ hφ)

Pushforward along surjective coefficient and exponent maps is surjective. The exponent map may have infinite kernel and the period maps need not be injective or discrete.

@[simp]

theorem TauCeti.NovikovSeries.coeff_map_of_injective {R : Type u_1} {S : Type u_2} {H : Type u_4} {H' : Type u_5} [AddZeroClass H] [AddZeroClass H'] {N : H →+ ℝ} {N' : H' →+ ℝ} [AddMonoid R] [AddCommMonoid S] (ρ : R →+ S) (φ : H →+ H') (hφ : ∃ c > 0, ∀ (h : H), N' (φ h) = c * N h) (hinj : Function.Injective ⇑φ) (a : NovikovSeries R H N) (h : H) : ((map ρ φ hφ) a).coeff (φ h) = ρ (a.coeff h)

Along an injective exponent homomorphism, the pushforward moves each coefficient to the image exponent.

@[simp]

theorem TauCeti.NovikovSeries.coeff_map_id_right {R : Type u_1} {S : Type u_2} {H : Type u_4} [AddZeroClass H] {N : H →+ ℝ} [AddMonoid R] [AddCommMonoid S] (ρ : R →+ S) (a : NovikovSeries R H N) (h : H) : ((map ρ (AddMonoidHom.id H) ⋯) a).coeff h = ρ (a.coeff h)

The pushforward along the identity of exponents applies the coefficient map to each coefficient.

theorem TauCeti.NovikovSeries.map_injective {R : Type u_1} {S : Type u_2} {H : Type u_4} {H' : Type u_5} [AddZeroClass H] [AddZeroClass H'] {N : H →+ ℝ} {N' : H' →+ ℝ} [AddMonoid R] [AddCommMonoid S] (ρ : R →+ S) (φ : H →+ H') (hφ : ∃ c > 0, ∀ (h : H), N' (φ h) = c * N h) (hρ : Function.Injective ⇑ρ) (hinj : Function.Injective ⇑φ) : Function.Injective ⇑(map ρ φ hφ)

Pushforward along injective coefficient and exponent maps is injective.

theorem TauCeti.NovikovSeries.coeff_map_eq_zero_of_lt {R : Type u_1} {S : Type u_2} {H : Type u_4} {H' : Type u_5} [AddZeroClass H] [AddZeroClass H'] {N : H →+ ℝ} {N' : H' →+ ℝ} [AddMonoid R] [AddCommMonoid S] (ρ : R →+ S) (φ : H →+ H') (hφ : ∃ c > 0, ∀ (h : H), N' (φ h) = c * N h) {c C : ℝ} (hc : 0 ≤ c) (hcφ : ∀ (h : H), N' (φ h) = c * N h) {a : NovikovSeries R H N} (ha : ∀ (h : H), N h < C → a.coeff h = 0) {h' : H'} (hh' : N' h' < c * C) : ((map ρ φ hφ) a).coeff h' = 0

The pushforward sends a series vanishing below the period cutoff C to a series vanishing below c * C, where c is the period rescaling factor of φ.

@[simp]

theorem TauCeti.NovikovSeries.map_id {H : Type u_4} [AddZeroClass H] {N : H →+ ℝ} {M : Type u_7} [AddCommMonoid M] : map (AddMonoidHom.id M) (AddMonoidHom.id H) ⋯ = AddMonoidHom.id (NovikovSeries M H N)

Pushing forward along the identity coefficient map and the identity exponent homomorphism is the identity.

@[simp]

theorem TauCeti.NovikovSeries.map_map {R : Type u_1} {S : Type u_2} {T : Type u_3} {H : Type u_4} {H' : Type u_5} {H'' : Type u_6} [AddZeroClass H] [AddZeroClass H'] [AddZeroClass H''] {N : H →+ ℝ} {N' : H' →+ ℝ} {N'' : H'' →+ ℝ} [AddMonoid R] [AddCommMonoid S] [AddCommMonoid T] (ρ : R →+ S) (φ : H →+ H') (hφ : ∃ c > 0, ∀ (h : H), N' (φ h) = c * N h) (ρ' : S →+ T) (φ' : H' →+ H'') (hφ' : ∃ c > 0, ∀ (h : H'), N'' (φ' h) = c * N' h) (a : NovikovSeries R H N) : (map ρ' φ' hφ') ((map ρ φ hφ) a) = (map (ρ'.comp ρ) (φ'.comp φ) ⋯) a

The pushforward along composite coefficient and exponent maps is the composite of the pushforwards.

@[simp]

theorem TauCeti.NovikovSeries.map_ofFinsupp {R : Type u_1} {S : Type u_2} {H : Type u_4} {H' : Type u_5} [AddZeroClass H] [AddZeroClass H'] {N : H →+ ℝ} {N' : H' →+ ℝ} [AddMonoid R] [AddCommMonoid S] (ρ : R →+ S) (φ : H →+ H') (hφ : ∃ c > 0, ∀ (h : H), N' (φ h) = c * N h) (f : H →₀ R) : (map ρ φ hφ) (ofFinsupp f) = ofFinsupp (Finsupp.mapDomain (⇑φ) (Finsupp.mapRange ⇑ρ ⋯ f))

The pushforward of a finitely supported series is the pushforward of the group ring, along ρ on coefficients and along φ on exponents.

@[simp]

theorem TauCeti.NovikovSeries.map_single {R : Type u_1} {S : Type u_2} {H : Type u_4} {H' : Type u_5} [AddZeroClass H] [AddZeroClass H'] {N : H →+ ℝ} {N' : H' →+ ℝ} [AddMonoid R] [AddCommMonoid S] (ρ : R →+ S) (φ : H →+ H') (hφ : ∃ c > 0, ∀ (h : H), N' (φ h) = c * N h) (g : H) (r : R) : (map ρ φ hφ) (single g r) = single (φ g) (ρ r)

The pushforward of the monomial r e^g is the monomial ρ r e^(φ g).

def TauCeti.NovikovSeries.comap {R : Type u_1} {H : Type u_4} {H' : Type u_5} [AddGroup H] {N : H →+ ℝ} [AddMonoid R] [AddZeroClass H'] {N' : H' →+ ℝ} (φ : H →+ H') (hφ : ∃ c > 0, ∀ (h : H), N' (φ h) = c * N h) (hker : (↑φ.ker).Finite) : NovikovSeries R H' N' →+ NovikovSeries R H N

The restriction of a Novikov series along an exponent homomorphism φ with finite kernel rescaling periods by a positive constant: the coefficient at h is the coefficient at φ h.

@[simp]

theorem TauCeti.NovikovSeries.coeff_comap {R : Type u_1} {H : Type u_4} {H' : Type u_5} [AddGroup H] {N : H →+ ℝ} [AddMonoid R] [AddZeroClass H'] {N' : H' →+ ℝ} (φ : H →+ H') (hφ : ∃ c > 0, ∀ (h : H), N' (φ h) = c * N h) (hker : (↑φ.ker).Finite) (b : NovikovSeries R H' N') (h : H) : ((comap φ hφ hker) b).coeff h = b.coeff (φ h)

The coefficient of a restriction at h is the coefficient of the series at φ h.

@[simp]

theorem TauCeti.NovikovSeries.support_comap {R : Type u_1} {H : Type u_4} {H' : Type u_5} [AddGroup H] {N : H →+ ℝ} [AddMonoid R] [AddZeroClass H'] {N' : H' →+ ℝ} (φ : H →+ H') (hφ : ∃ c > 0, ∀ (h : H), N' (φ h) = c * N h) (hker : (↑φ.ker).Finite) (b : NovikovSeries R H' N') : ((comap φ hφ hker) b).support = ⇑φ ⁻¹' b.support

The exponents of nonzero coefficient of a restriction are the preimages of those of the series.

theorem TauCeti.NovikovSeries.coeff_comap_eq_zero_of_lt {R : Type u_1} {H : Type u_4} {H' : Type u_5} [AddGroup H] {N : H →+ ℝ} [AddMonoid R] [AddZeroClass H'] {N' : H' →+ ℝ} (φ : H →+ H') (hφ : ∃ c > 0, ∀ (h : H), N' (φ h) = c * N h) (hker : (↑φ.ker).Finite) {c C : ℝ} (hc : 0 < c) (hcφ : ∀ (h : H), N' (φ h) = c * N h) {b : NovikovSeries R H' N'} (hb : ∀ (h' : H'), N' h' < c * C → b.coeff h' = 0) {h : H} (hh : N h < C) : ((comap φ hφ hker) b).coeff h = 0

The restriction sends a series vanishing below the period cutoff c * C to a series vanishing below C, where c > 0 is the period rescaling factor of φ.

@[simp]

theorem TauCeti.NovikovSeries.comap_single_of_injective {R : Type u_1} {H : Type u_4} {H' : Type u_5} [AddGroup H] {N : H →+ ℝ} [AddMonoid R] [AddZeroClass H'] {N' : H' →+ ℝ} (φ : H →+ H') (hφ : ∃ c > 0, ∀ (h : H), N' (φ h) = c * N h) (hker : (↑φ.ker).Finite) (hinj : Function.Injective ⇑φ) (h : H) (r : R) : (comap φ hφ hker) (single (φ h) r) = single h r

Restricting the monomial r e^(φ h) along an injective φ gives the monomial r e^h.

@[simp]

theorem TauCeti.NovikovSeries.comap_single_of_notMem_range {R : Type u_1} {H : Type u_4} {H' : Type u_5} [AddGroup H] {N : H →+ ℝ} [AddMonoid R] [AddZeroClass H'] {N' : H' →+ ℝ} (φ : H →+ H') (hφ : ∃ c > 0, ∀ (h : H), N' (φ h) = c * N h) (hker : (↑φ.ker).Finite) {g : H'} (hg : g ∉ Set.range ⇑φ) (r : R) : (comap φ hφ hker) (single g r) = 0

Restricting a monomial whose exponent is not in the range of φ gives zero.

@[simp]

theorem TauCeti.NovikovSeries.comap_id {R : Type u_1} {H : Type u_4} [AddGroup H] {N : H →+ ℝ} [AddMonoid R] : comap (AddMonoidHom.id H) ⋯ ⋯ = AddMonoidHom.id (NovikovSeries R H N)

Restricting along the identity exponent homomorphism is the identity.

theorem TauCeti.NovikovSeries.comap_map_of_injective {R : Type u_1} {S : Type u_2} {H : Type u_4} {H' : Type u_5} [AddGroup H] {N : H →+ ℝ} [AddMonoid R] [AddZeroClass H'] {N' : H' →+ ℝ} (φ : H →+ H') (hφ : ∃ c > 0, ∀ (h : H), N' (φ h) = c * N h) (hker : (↑φ.ker).Finite) [AddCommMonoid S] (ρ : R →+ S) (hinj : Function.Injective ⇑φ) (a : NovikovSeries R H N) : (comap φ hφ hker) ((map ρ φ hφ) a) = (map ρ (AddMonoidHom.id H) ⋯) a

Restricting a pushforward along an injective exponent homomorphism gives back the series with the coefficient map applied to its coefficients.

@[simp]

theorem TauCeti.NovikovSeries.comap_comap {R : Type u_1} {H : Type u_4} {H' : Type u_5} {H'' : Type u_6} [AddGroup H] {N : H →+ ℝ} [AddMonoid R] [AddGroup H'] [AddZeroClass H''] {N' : H' →+ ℝ} {N'' : H'' →+ ℝ} (φ : H →+ H') (hφ : ∃ c > 0, ∀ (h : H), N' (φ h) = c * N h) (hker : (↑φ.ker).Finite) (φ' : H' →+ H'') (hφ' : ∃ c > 0, ∀ (h : H'), N'' (φ' h) = c * N' h) (hker' : (↑φ'.ker).Finite) (b : NovikovSeries R H'' N'') : (comap φ hφ hker) ((comap φ' hφ' hker') b) = (comap (φ'.comp φ) ⋯ ⋯) b

The restriction along a composite exponent homomorphism is the composite of the restrictions.