Functoriality of Novikov rings

Let N : H →+ ℝ and N' : H' →+ ℝ be period homomorphisms and φ : H →+ H' a homomorphism of exponent groups rescaling periods by a positive constant, N' (φ h) = c * N h with c > 0. The pushforward TauCeti.NovikovSeries.map ρ φ hφ of TauCeti.RingTheory.NovikovSeries.Map sums the coefficients of a Novikov series along the fibres of φ after applying the coefficient map ρ.

When ρ is multiplicative, so is the pushforward: the coefficient of map (a * b) at h' and that of map a * map b are both the finite sum of ρ (a.coeff u) * ρ (b.coeff v) over the pairs of support exponents with φ u + φ v = h' (TauCeti.NovikovSeries.finite_setOf_map_add_eq). For a unital ring homomorphism ρ : R →+* S this gives the unital ring homomorphism P_(ρ,φ) : Nov(R, H, N) →+* Nov(S, H', N'), which sends the monomial r e^g to ρ r e^(φ g) (TauCeti.NovikovSeries.map_single). It satisfies the identity and composition laws, and for an algebra homomorphism ρ it is an algebra homomorphism. No finiteness of the kernel of φ and no injectivity of the period maps is needed.

The pushforward moves the period neighbourhood U_C into U'_(c * C), so it is continuous for the period topologies. Since c > 0, it preserves nonnegative and strictly positive supports, and it restricts to a ring homomorphism of the nonnegative subrings which maps the positive ideal into the positive ideal. Likewise, when φ has finite kernel, the restriction along φ moves U'_(c * C) into U_C and is continuous.

For a subgroup K ≤ H, with the restricted period map N.comp K.subtype, the pushforward along the inclusion makes Nov(R, H, N) an algebra over Nov(R, K, N|K); its algebra map keeps every coefficient at its exponent (TauCeti.NovikovSeries.coeff_algebraMap_addSubgroup_coe). The restriction of coefficients comap K.subtype to K satisfies the projection formula comap (b * a) = b * comap a for b in Nov(R, K, N|K) (TauCeti.NovikovSeries.comap_subtype_algebraMap_mul). Applied to the inclusion of a finite-index subgroup of exponents, these maps compare the Novikov rings of a finite abelian covering and of its base.

Main definitions

• TauCeti.NovikovSeries.mapRingHom: the pushforward P_(ρ,φ) along a ring homomorphism of coefficients, as a ring homomorphism.
• TauCeti.NovikovSeries.mapAlgHom: the pushforward along an algebra homomorphism of coefficients, as an algebra homomorphism.
• TauCeti.NovikovSeries.mapNonnegSubring: the restriction of mapRingHom to the nonnegative subrings.
• TauCeti.NovikovSeries.instAlgebraAddSubgroup: Nov(R, H, N) as an algebra over Nov(R, K, N|K) for a subgroup K ≤ H, along the pushforward of the inclusion of exponents.

Main results

• TauCeti.NovikovSeries.map_mul: the pushforward along a multiplicative coefficient map is multiplicative, and TauCeti.NovikovSeries.map_one: along a ring homomorphism it preserves 1.
• TauCeti.NovikovSeries.mapRingHom_id and TauCeti.NovikovSeries.mapRingHom_comp: the identity and composition laws.
• TauCeti.NovikovSeries.map_mem_periodFiltration: the pushforward sends U_C into U'_(c * C).
• TauCeti.NovikovSeries.continuous_map and TauCeti.NovikovSeries.continuous_mapRingHom: the pushforward is continuous for the period topologies.
• TauCeti.NovikovSeries.continuous_mapNonnegSubring and TauCeti.NovikovSeries.mapNonnegSubring_injective: the pushforward on the nonnegative subrings is continuous, and injective along injective coefficient and exponent maps.
• TauCeti.NovikovSeries.mapNonnegSubring_algebraMap, TauCeti.NovikovSeries.mapNonnegSubring_comp_algebraMap and TauCeti.NovikovSeries.mapNonnegSubring_smul: the pushforward on the nonnegative subrings is compatible with constants and semilinear over the coefficient map.
• TauCeti.NovikovSeries.comap_mem_periodFiltration and TauCeti.NovikovSeries.continuous_comap: the restriction sends U'_(c * C) into U_C, and is continuous for the period topologies.
• TauCeti.NovikovSeries.mapNonnegSubring_mem_posIdeal: the pushforward maps the positive ideal into the positive ideal.
• TauCeti.NovikovSeries.map_unitsOneSubSingle: the pushforward sends the unit 1 - r e^g to the unit 1 - ρ r e^(φ g).
• TauCeti.NovikovSeries.comap_subtype_algebraMap_mul: the projection formula for restriction of coefficients to a subgroup K.

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.map_mul {R : Type u_1} {S : Type u_2} {H : Type u_4} {H' : Type u_5} [AddZeroClass H] [AddZeroClass H'] {N : H →+ ℝ} {N' : H' →+ ℝ} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] {F : Type u_7} [FunLike F R S] [NonUnitalRingHomClass F R S] (ρ : F) (φ : H →+ H') (hφ : ∃ c > 0, ∀ (h : H), N' (φ h) = c * N h) (a b : NovikovSeries R H N) : (map (↑ρ) φ hφ) (a * b) = (map (↑ρ) φ hφ) a * (map (↑ρ) φ hφ) b

The pushforward along a multiplicative coefficient map is multiplicative.

noncomputable def TauCeti.NovikovSeries.mapRingHom {R : Type u_1} {S : Type u_2} {H : Type u_4} {H' : Type u_5} [AddMonoid H] [AddMonoid H'] {N : H →+ ℝ} {N' : H' →+ ℝ} [Semiring R] [Semiring 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 P_(ρ,φ) of Novikov series along a ring homomorphism ρ of coefficients and an exponent homomorphism φ rescaling periods by a positive constant, as a ring homomorphism: the coefficient at h' is the sum of the images under ρ of the coefficients at the exponents h with φ h = h'.

@[simp]

theorem TauCeti.NovikovSeries.mapRingHom_apply {R : Type u_1} {S : Type u_2} {H : Type u_4} {H' : Type u_5} [AddMonoid H] [AddMonoid H'] {N : H →+ ℝ} {N' : H' →+ ℝ} [Semiring R] [Semiring S] (ρ : R →+* S) (φ : H →+ H') (hφ : ∃ c > 0, ∀ (h : H), N' (φ h) = c * N h) (a : NovikovSeries R H N) : (mapRingHom ρ φ hφ) a = (map (↑ρ) φ hφ) a

@[simp]

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

The pushforward along a ring homomorphism of coefficients preserves 1.

@[simp]

theorem TauCeti.NovikovSeries.mapRingHom_id {R : Type u_1} {H : Type u_4} [AddMonoid H] {N : H →+ ℝ} [Semiring R] : mapRingHom (RingHom.id R) (AddMonoidHom.id H) ⋯ = RingHom.id (NovikovSeries R H N)

The pushforward ring homomorphism along the identity coefficient and exponent maps is the identity.

theorem TauCeti.NovikovSeries.mapRingHom_comp {R : Type u_1} {S : Type u_2} {T : Type u_3} {H : Type u_4} {H' : Type u_5} {H'' : Type u_6} [AddMonoid H] [AddMonoid H'] [AddMonoid H''] {N : H →+ ℝ} {N' : H' →+ ℝ} {N'' : H'' →+ ℝ} [Semiring R] [Semiring S] [Semiring 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) : (mapRingHom ρ' φ' hφ').comp (mapRingHom ρ φ hφ) = mapRingHom (ρ'.comp ρ) (φ'.comp φ) ⋯

The composite of pushforward ring homomorphisms is the pushforward ring homomorphism along the composite coefficient and exponent maps.

noncomputable def TauCeti.NovikovSeries.mapAlgHom {R : Type u_1} {S : Type u_2} {H : Type u_4} {H' : Type u_5} [AddMonoid H] [AddMonoid H'] {N : H →+ ℝ} {N' : H' →+ ℝ} {A : Type u_7} [CommSemiring A] [Semiring R] [Semiring S] [Algebra A R] [Algebra A S] (ρ : R →ₐ[A] S) (φ : H →+ H') (hφ : ∃ c > 0, ∀ (h : H), N' (φ h) = c * N h) : NovikovSeries R H N →ₐ[A] NovikovSeries S H' N'

The pushforward of Novikov series along an A-algebra homomorphism ρ of coefficients and an exponent homomorphism φ rescaling periods by a positive constant, as an A-algebra homomorphism. For ρ = AlgHom.id A R this is the pushforward of A-algebras of Novikov series with fixed coefficient ring.

@[simp]

theorem TauCeti.NovikovSeries.mapAlgHom_apply {R : Type u_1} {S : Type u_2} {H : Type u_4} {H' : Type u_5} [AddMonoid H] [AddMonoid H'] {N : H →+ ℝ} {N' : H' →+ ℝ} {A : Type u_7} [CommSemiring A] [Semiring R] [Semiring S] [Algebra A R] [Algebra A S] (ρ : R →ₐ[A] S) (φ : H →+ H') (hφ : ∃ c > 0, ∀ (h : H), N' (φ h) = c * N h) (a : NovikovSeries R H N) : (mapAlgHom ρ φ hφ) a = (map (↑↑ρ) φ hφ) a

theorem TauCeti.NovikovSeries.map_mem_periodFiltration {R : Type u_1} {S : Type u_2} {H : Type u_4} {H' : Type u_5} [AddZeroClass H] [AddZeroClass H'] {N : H →+ ℝ} {N' : H' →+ ℝ} [AddGroup R] [AddCommGroup 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 : a ∈ periodFiltration R N C) : (map ρ φ hφ) a ∈ periodFiltration S N' (c * C)

If φ rescales periods by c ≥ 0, the pushforward sends the period neighbourhood U_C into U'_(c * C).

theorem TauCeti.NovikovSeries.continuous_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' →+ ℝ} [AddCommGroup R] [AddCommGroup S] (ρ : R →+ S) (φ : H →+ H') (hφ : ∃ c > 0, ∀ (h : H), N' (φ h) = c * N h) : Continuous ⇑(map ρ φ hφ)

The pushforward of Novikov series is continuous for the period topologies.

theorem TauCeti.NovikovSeries.comap_mem_periodFiltration {R : Type u_1} {H : Type u_4} {H' : Type u_5} [AddGroup H] [AddZeroClass H'] {N : H →+ ℝ} {N' : H' →+ ℝ} [AddGroup R] (φ : 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 : b ∈ periodFiltration R N' (c * C)) : (comap φ hφ hker) b ∈ periodFiltration R N C

If φ rescales periods by c > 0, the restriction sends the period neighbourhood U'_(c * C) into U_C.

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

The restriction of Novikov series is continuous for the period topologies.

theorem TauCeti.NovikovSeries.map_mem_nonnegSubring {R : Type u_1} {S : Type u_2} {H : Type u_4} {H' : Type u_5} [AddMonoid H] [AddMonoid H'] {N : H →+ ℝ} {N' : H' →+ ℝ} [Ring R] [Ring S] (ρ : R →+ S) (φ : H →+ H') (hφ : ∃ c > 0, ∀ (h : H), N' (φ h) = c * N h) {a : NovikovSeries R H N} (ha : a ∈ nonnegSubring R N) : (map ρ φ hφ) a ∈ nonnegSubring S N'

The pushforward sends series supported in nonnegative periods to series supported in nonnegative periods, for any additive coefficient map.

theorem TauCeti.NovikovSeries.continuous_mapRingHom {R : Type u_1} {S : Type u_2} {H : Type u_4} {H' : Type u_5} [AddMonoid H] [AddMonoid H'] {N : H →+ ℝ} {N' : H' →+ ℝ} [Ring R] [Ring S] (ρ : R →+* S) (φ : H →+ H') (hφ : ∃ c > 0, ∀ (h : H), N' (φ h) = c * N h) : Continuous ⇑(mapRingHom ρ φ hφ)

The pushforward ring homomorphism is continuous for the period topologies.

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

The restriction of the pushforward ring homomorphism to the nonnegative subrings.

@[simp]

theorem TauCeti.NovikovSeries.coe_mapNonnegSubring {R : Type u_1} {S : Type u_2} {H : Type u_4} {H' : Type u_5} [AddMonoid H] [AddMonoid H'] {N : H →+ ℝ} {N' : H' →+ ℝ} [Ring R] [Ring S] (ρ : R →+* S) (φ : H →+ H') (hφ : ∃ c > 0, ∀ (h : H), N' (φ h) = c * N h) (a : ↥(nonnegSubring R N)) : ↑((mapNonnegSubring ρ φ hφ) a) = (map (↑ρ) φ hφ) ↑a

theorem TauCeti.NovikovSeries.continuous_mapNonnegSubring {R : Type u_1} {S : Type u_2} {H : Type u_4} {H' : Type u_5} [AddMonoid H] [AddMonoid H'] {N : H →+ ℝ} {N' : H' →+ ℝ} [Ring R] [Ring S] (ρ : R →+* S) (φ : H →+ H') (hφ : ∃ c > 0, ∀ (h : H), N' (φ h) = c * N h) : Continuous ⇑(mapNonnegSubring ρ φ hφ)

The pushforward on the nonnegative subrings is continuous for the period topologies.

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

The pushforward on the nonnegative subrings along injective coefficient and exponent maps is injective.

theorem TauCeti.NovikovSeries.mapNonnegSubring_mem_posIdeal {R : Type u_1} {S : Type u_2} {H : Type u_4} {H' : Type u_5} [AddMonoid H] [AddMonoid H'] {N : H →+ ℝ} {N' : H' →+ ℝ} [Ring R] [Ring S] (ρ : R →+* S) (φ : H →+ H') (hφ : ∃ c > 0, ∀ (h : H), N' (φ h) = c * N h) {a : ↥(nonnegSubring R N)} (ha : a ∈ posIdeal R N) : (mapNonnegSubring ρ φ hφ) a ∈ posIdeal S N'

The pushforward maps the ideal of series supported in strictly positive periods into the corresponding ideal.

@[simp]

theorem TauCeti.NovikovSeries.map_unitsOneSubSingle {R : Type u_1} {S : Type u_2} {H : Type u_4} {H' : Type u_5} [AddMonoid H] [AddMonoid H'] {N : H →+ ℝ} {N' : H' →+ ℝ} [Ring R] [Ring S] (ρ : R →+* S) (φ : H →+ H') (hφ : ∃ c > 0, ∀ (h : H), N' (φ h) = c * N h) {g : H} (hg : 0 < N g) (hg' : 0 < N' (φ g)) (r : R) : (Units.map ↑(mapNonnegSubring ρ φ hφ)) (unitsOneSubSingle hg r) = unitsOneSubSingle hg' (ρ r)

The pushforward sends the unit 1 - r e^g of the nonnegative subring to the unit 1 - ρ r e^(φ g).

@[simp]

theorem TauCeti.NovikovSeries.mapNonnegSubring_algebraMap {R : Type u_1} {S : Type u_2} {H : Type u_4} {H' : Type u_5} [AddMonoid H] [AddMonoid H'] {N : H →+ ℝ} {N' : H' →+ ℝ} [CommRing R] [CommRing S] (ρ : R →+* S) (φ : H →+ H') (hφ : ∃ c > 0, ∀ (h : H), N' (φ h) = c * N h) (r : R) : (mapNonnegSubring ρ φ hφ) ((algebraMap R ↥(nonnegSubring R N)) r) = (algebraMap S ↥(nonnegSubring S N')) (ρ r)

The pushforward on the nonnegative subrings sends the constant r to the constant ρ r.

theorem TauCeti.NovikovSeries.mapNonnegSubring_comp_algebraMap {R : Type u_1} {S : Type u_2} {H : Type u_4} {H' : Type u_5} [AddMonoid H] [AddMonoid H'] {N : H →+ ℝ} {N' : H' →+ ℝ} [CommRing R] [CommRing S] (ρ : R →+* S) (φ : H →+ H') (hφ : ∃ c > 0, ∀ (h : H), N' (φ h) = c * N h) : (mapNonnegSubring ρ φ hφ).comp (algebraMap R ↥(nonnegSubring R N)) = (algebraMap S ↥(nonnegSubring S N')).comp ρ

The pushforward on the nonnegative subrings commutes with the constant embeddings.

@[simp]

theorem TauCeti.NovikovSeries.mapNonnegSubring_smul {R : Type u_1} {S : Type u_2} {H : Type u_4} {H' : Type u_5} [AddMonoid H] [AddMonoid H'] {N : H →+ ℝ} {N' : H' →+ ℝ} [CommRing R] [CommRing S] (ρ : R →+* S) (φ : H →+ H') (hφ : ∃ c > 0, ∀ (h : H), N' (φ h) = c * N h) (r : R) (a : ↥(nonnegSubring R N)) : (mapNonnegSubring ρ φ hφ) (r • a) = ρ r • (mapNonnegSubring ρ φ hφ) a

The pushforward on the nonnegative subrings is semilinear over ρ.

theorem TauCeti.NovikovSeries.exists_period_rescale_subtype {H : Type u_4} [AddCommGroup H] {N : H →+ ℝ} (K : AddSubgroup H) : ∃ c > 0, ∀ (k : ↥K), N (K.subtype k) = c * (N.comp K.subtype) k

The inclusion of a subgroup preserves periods, for the restricted period map.

@[instance_reducible]

noncomputable instance TauCeti.NovikovSeries.instAlgebraAddSubgroup {R : Type u_1} {H : Type u_4} [AddCommGroup H] {N : H →+ ℝ} (K : AddSubgroup H) [CommSemiring R] : Algebra (NovikovSeries R (↥K) (N.comp K.subtype)) (NovikovSeries R H N)

Novikov series on H form an algebra over Novikov series on a subgroup K, with the restricted period map, along the pushforward of the inclusion K → H.

theorem TauCeti.NovikovSeries.algebraMap_addSubgroup_eq_mapRingHom {R : Type u_1} {H : Type u_4} [AddCommGroup H] {N : H →+ ℝ} (K : AddSubgroup H) [CommSemiring R] : algebraMap (NovikovSeries R (↥K) (N.comp K.subtype)) (NovikovSeries R H N) = mapRingHom (RingHom.id R) K.subtype ⋯

The algebra map from Novikov series on K is the pushforward along the inclusion.

@[simp]

theorem TauCeti.NovikovSeries.coeff_algebraMap_addSubgroup_coe {R : Type u_1} {H : Type u_4} [AddCommGroup H] {N : H →+ ℝ} {K : AddSubgroup H} [CommSemiring R] (b : NovikovSeries R (↥K) (N.comp K.subtype)) (k : ↥K) : ((algebraMap (NovikovSeries R (↥K) (N.comp K.subtype)) (NovikovSeries R H N)) b).coeff ↑k = b.coeff k

The algebra map from Novikov series on K keeps every coefficient at its exponent.

@[simp]

theorem TauCeti.NovikovSeries.coeff_algebraMap_addSubgroup_of_notMem {R : Type u_1} {H : Type u_4} [AddCommGroup H] {N : H →+ ℝ} {K : AddSubgroup H} [CommSemiring R] (b : NovikovSeries R (↥K) (N.comp K.subtype)) {h : H} (hh : h ∉ K) : ((algebraMap (NovikovSeries R (↥K) (N.comp K.subtype)) (NovikovSeries R H N)) b).coeff h = 0

The algebra map from Novikov series on K has zero coefficients outside K.

theorem TauCeti.NovikovSeries.algebraMap_comap_subtype_of_support_subset {R : Type u_1} {H : Type u_4} [AddCommGroup H] {N : H →+ ℝ} {K : AddSubgroup H} [CommSemiring R] (a : NovikovSeries R H N) (ha : a.support ⊆ ↑K) : (algebraMap (NovikovSeries R (↥K) (N.comp K.subtype)) (NovikovSeries R H N)) ((comap K.subtype ⋯ ⋯) a) = a

Restricting to a subgroup and then including recovers a series supported on that subgroup.

@[simp]

theorem TauCeti.NovikovSeries.mem_range_algebraMap_addSubgroup_iff {R : Type u_1} {H : Type u_4} [AddCommGroup H] {N : H →+ ℝ} {K : AddSubgroup H} [CommSemiring R] (a : NovikovSeries R H N) : a ∈ Set.range ⇑(algebraMap (NovikovSeries R (↥K) (N.comp K.subtype)) (NovikovSeries R H N)) ↔ a.support ⊆ ↑K

A series comes from the subgroup Novikov ring exactly when its support lies in the subgroup.

@[simp]

theorem TauCeti.NovikovSeries.algebraMap_addSubgroup_single {R : Type u_1} {H : Type u_4} [AddCommGroup H] {N : H →+ ℝ} {K : AddSubgroup H} [CommSemiring R] (k : ↥K) (r : R) : (algebraMap (NovikovSeries R (↥K) (N.comp K.subtype)) (NovikovSeries R H N)) (single k r) = single (↑k) r

The algebra map from Novikov series on K sends the monomial r e^k to r e^k.

instance TauCeti.NovikovSeries.instIsScalarTowerAddSubgroup {R : Type u_1} {H : Type u_4} [AddCommGroup H] {N : H →+ ℝ} (K : AddSubgroup H) [CommSemiring R] : IsScalarTower R (NovikovSeries R (↥K) (N.comp K.subtype)) (NovikovSeries R H N)

The coefficient scalars act on Novikov series on H through Novikov series on K.

@[simp]

theorem TauCeti.NovikovSeries.comap_subtype_algebraMap {R : Type u_1} {H : Type u_4} [AddCommGroup H] {N : H →+ ℝ} {K : AddSubgroup H} [CommSemiring R] (hφ : ∃ c > 0, ∀ (k : ↥K), N (K.subtype k) = c * (N.comp K.subtype) k) (hker : (↑K.subtype.ker).Finite) (b : NovikovSeries R (↥K) (N.comp K.subtype)) : (comap K.subtype hφ hker) ((algebraMap (NovikovSeries R (↥K) (N.comp K.subtype)) (NovikovSeries R H N)) b) = b

Restricting the image of a Novikov series on K back to K recovers the series.

theorem TauCeti.NovikovSeries.algebraMap_addSubgroup_injective {R : Type u_1} {H : Type u_4} [AddCommGroup H] {N : H →+ ℝ} {K : AddSubgroup H} [CommSemiring R] : Function.Injective ⇑(algebraMap (NovikovSeries R (↥K) (N.comp K.subtype)) (NovikovSeries R H N))

The algebra map induced by inclusion of a subgroup of exponents is injective.

theorem TauCeti.NovikovSeries.comap_subtype_algebraMap_mul {R : Type u_1} {H : Type u_4} [AddCommGroup H] {N : H →+ ℝ} {K : AddSubgroup H} [CommSemiring R] (hφ : ∃ c > 0, ∀ (k : ↥K), N (K.subtype k) = c * (N.comp K.subtype) k) (hker : (↑K.subtype.ker).Finite) (b : NovikovSeries R (↥K) (N.comp K.subtype)) (a : NovikovSeries R H N) : (comap K.subtype hφ hker) ((algebraMap (NovikovSeries R (↥K) (N.comp K.subtype)) (NovikovSeries R H N)) b * a) = b * (comap K.subtype hφ hker) a

The projection formula: restriction of coefficients to K is linear over Novikov series on K.