Repartitions of an algebraic function field

A repartition (Chevalley's name; Stichtenoth says adele) of an algebraic function field F / k is a family a : Place k F → F of elements of F itself — no completions are taken — that is integral at all but finitely many places. They form the repartition space

A_F = {a : Place k F → F | ∀ᶠ P in cofinite, v_P (a P) ≤ 1},

filtered by the subspaces

A_F(D) = {a : Place k F → F | ∀ P, v_P (a P) ≤ exp (D P)}

attached to the divisors D of F / k. This file constructs both, embeds F diagonally, and proves the basic calculus of the filtration: it is monotone and directed, it exhausts A_F, and it cuts the diagonal copy of F in exactly the Riemann–Roch space L(D).

It is Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., Definitions 1.5.2 and 1.5.3, together with the elementary lemmas that Section I.5 uses without numbering them, and the repartitions ι_P x supported at a single place from his Definition 1.7.1. The quotients A_F(E)/A_F(D) and A_F ⧸ (A_F(D) + F), the index of specialty, and Weil differentials are the work that consumes this file.

Main definitions

• TauCeti.repartitionSpace: the repartition space A_F (Definition 1.5.2), as a k-subspace of Place k F → F.
• TauCeti.adeleFiltration: the subspace A_F(D) attached to a divisor (Definition 1.5.3).
• TauCeti.diagonalRepartitions: the diagonal copy of F inside Place k F → F, the image of Pi.constAlgHom.
• TauCeti.submoduleOfAdeleFiltrationSupDiagonalRepartitions: the subspace (A_F(D) + F) ∩ A_F of A_F, whose cokernel computes the index of specialty.
• TauCeti.repartitionMul: multiplication of a repartition by a function, as a k-algebra map to the k-linear endomorphisms of A_F.
• TauCeti.singleRepartition: the repartition ι_P x carrying the entry x at a single place P, as a k-linear map F →ₗ[k] A_F.

Main results

• TauCeti.mem_repartitionSpace_iff_finite and TauCeti.mem_adeleFiltration_iff: the two membership conditions, cofinite integrality and the pointwise bound.
• TauCeti.adeleFiltration_le_repartitionSpace, TauCeti.adeleFiltration_mono and TauCeti.directed_adeleFiltration: the filtration lands in A_F, and is monotone and directed.
• TauCeti.adeleFiltration_sup: A_F(D ⊔ E) = A_F(D) + A_F(E), the place-by-place splitting.
• TauCeti.repartitionSpace_eq_iSup and TauCeti.coe_repartitionSpace_eq_iUnion: A_F = ⋃_D A_F(D), the exhaustion.
• TauCeti.diagonalRepartitions_le_repartitionSpace: the diagonal F ↪ A_F, which is where the finiteness of the zeros and poles of a function enters.
• TauCeti.diagonalRepartitions_inf_adeleFiltration: F ∩ A_F(D) = L(D), the lemma that ties the filtration to the Riemann–Roch spaces, and its relative form TauCeti.adeleFiltration_inf_sup_diagonalRepartitions: A_F(E) ∩ (A_F(D) + F) = A_F(D) + L(E) for D ≤ E.
• TauCeti.smul_mem_adeleFiltration_iff and TauCeti.smul_mem_adeleFiltration_sub_principal: multiplying by a function z translates the filtration by div z, exactly as it does for Riemann–Roch spaces.
• TauCeti.smul_mem_repartitionSpace and TauCeti.smul_mem_diagonalRepartitions: both A_F and the diagonal are stable under multiplication by a function.
• TauCeti.singleRepartition_mem_adeleFiltration_iff: the bound defining A_F(D) is a condition at the single place P on the repartitions supported there.

Implementation notes

Both membership conditions are stated multiplicatively, as v_P (a P) ≤ exp (D P), and never in the additive form ord_P (a P) ≥ -D P. The additive form is wrong as written: the junk value ord_P 0 = 0 would throw the zero entries out of A_F(D) at every place where D P < 0, so the additive carrier is not even closed under addition. With the multiplicative condition, v_P 0 = 0 ≤ exp (D P) holds at every place, so A_F(D) contains 0 definitionally. This is the same convention as TauCeti.riemannRochSpace, entrywise, which is what makes TauCeti.diagonalRepartitions_inf_adeleFiltration hold on the nose.

A_F is pinned as a Submodule k, because a Weil differential is by definition a k-linear form on it. Its multiplicative structure is not lost: TauCeti.one_mem_repartitionSpace and TauCeti.mul_mem_repartitionSpace record that it is a subring, and TauCeti.smul_mem_repartitionSpace records the F-scalar multiplication that the F-vector space structure on the Weil differentials is built from.

ι_P x is built from Finsupp.lsingle P, not from Pi.single or LinearMap.single: the latter two carry a DecidableEq argument, and no instance supplies a decidable equality of places, while Finsupp.single needs none. TauCeti.singleRepartition_self and TauCeti.singleRepartition_of_ne determine ι_P x entrywise, so nothing downstream has to mention Finsupp.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Section I.5 and Definition 1.7.1.

The repartition space

noncomputable def TauCeti.repartitionSpace (k : Type u_1) (F : Type u_2) [Field k] [Field F] [Algebra k F] : Submodule k (Place k F → F)

The repartition space A_F of F / k (Stichtenoth, Definition 1.5.2): the families a : Place k F → F whose entries lie in F itself — no completions — and are integral at all but finitely many places.

The integrality condition is the multiplicative v_P (a P) ≤ 1, which is junk-free at zero entries, and the "all but finitely many" is Filter.cofinite; the equivalent finite-exceptional- set form is TauCeti.mem_repartitionSpace_iff_finite.

Equations

• TauCeti.repartitionSpace k F = { carrier := {a : TauCeti.Place k F → F | ∀ᶠ (P : TauCeti.Place k F) in Filter.cofinite, P.valuation (a P) ≤ 1}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem TauCeti.mem_repartitionSpace_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {a : Place k F → F} : a ∈ repartitionSpace k F ↔ ∀ᶠ (P : Place k F) in Filter.cofinite, P.valuation (a P) ≤ 1

Membership in A_F, unfolded: the entries are integral at cofinitely many places.

theorem TauCeti.mem_repartitionSpace_iff_finite {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {a : Place k F → F} : a ∈ repartitionSpace k F ↔ {P : Place k F | ¬P.valuation (a P) ≤ 1}.Finite

Membership in A_F in terms of the finite exceptional set.

theorem TauCeti.mem_repartitionSpace_iff_integers {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {a : Place k F → F} : a ∈ repartitionSpace k F ↔ ∀ᶠ (P : Place k F) in Filter.cofinite, a P ∈ P.integers

Membership in A_F in terms of the valuation rings: the entries lie in the local ring at all but finitely many places.

theorem TauCeti.one_mem_repartitionSpace {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] : 1 ∈ repartitionSpace k F

The constant repartition 1 is a repartition.

theorem TauCeti.mul_mem_repartitionSpace {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {a b : Place k F → F} (ha : a ∈ repartitionSpace k F) (hb : b ∈ repartitionSpace k F) : a * b ∈ repartitionSpace k F

A_F is closed under multiplication: it is a subring of Place k F → F, not merely a k-subspace.

The filtration by divisors

noncomputable def TauCeti.adeleFiltration {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D : Divisor k F) : Submodule k (Place k F → F)

The subspace A_F(D) of the repartition space attached to a divisor D (Stichtenoth, Definition 1.5.3): the repartitions whose pole at each place P is bounded by D P.

The condition is the multiplicative v_P (a P) ≤ exp (D P) at every place, entrywise the condition defining TauCeti.riemannRochSpace. In particular 0 ∈ A_F(D) definitionally, for every D, which the additive form ord_P (a P) ≥ -D P would get wrong.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.mem_adeleFiltration_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D : Divisor k F} {a : Place k F → F} : a ∈ adeleFiltration D ↔ ∀ (P : Place k F), P.valuation (a P) ≤ WithZero.exp (AlgebraicGeometry.WeilDivisor.coeff D P)

Membership in A_F(D), unfolded: the poles of the entries are bounded by D.

theorem TauCeti.mem_adeleFiltration_iff_neg_le_ord {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D : Divisor k F} {a : Place k F → F} : a ∈ adeleFiltration D ↔ ∀ (P : Place k F), a P ≠ 0 → -AlgebraicGeometry.WeilDivisor.coeff D P ≤ P.ord (a P)

The additive form of the bound: at each place with a nonzero entry the order is at least -D P. The nonvanishing guard is not a hypothesis but part of the statement, because ord_P 0 = 0 is a junk value: a zero entry satisfies the multiplicative bound at every place, including those where D P < 0.

theorem TauCeti.mem_adeleFiltration_zero_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {a : Place k F → F} : a ∈ adeleFiltration 0 ↔ ∀ (P : Place k F), a P ∈ P.integers

A_F(0) consists of the everywhere integral repartitions.

theorem TauCeti.adeleFiltration_mono {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D E : Divisor k F} (h : D ≤ E) : adeleFiltration D ≤ adeleFiltration E

Enlarging the divisor enlarges the subspace.

@[simp]

theorem TauCeti.adeleFiltration_sup {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D E : Divisor k F) : adeleFiltration (D ⊔ E) = adeleFiltration D ⊔ adeleFiltration E

The filtration turns suprema of divisors into sums of subspaces: A_F(D ⊔ E) is the sum of A_F(D) and A_F(E).

theorem TauCeti.directed_adeleFiltration {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] : Directed (fun (x1 x2 : Submodule k (Place k F → F)) => x1 ≤ x2) adeleFiltration

The filtration is directed: any two of its members are contained in a third, namely the one attached to the pointwise maximum of the two divisors.

theorem TauCeti.adeleFiltration_le_repartitionSpace {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D : Divisor k F) : adeleFiltration D ≤ repartitionSpace k F

Every A_F(D) consists of repartitions: outside the support of D its defining bound reads v_P (a P) ≤ exp 0 = 1.

theorem TauCeti.exists_mem_adeleFiltration {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {a : Place k F → F} (ha : a ∈ repartitionSpace k F) : ∃ (D : Divisor k F), a ∈ adeleFiltration D

Every repartition is bounded by some divisor: the exceptional set is finite, and the pole orders max 0 (-ord_P (a P)) of the entries there are the coefficients of a divisor that works.

theorem TauCeti.repartitionSpace_eq_iSup {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] : ⨆ (D : Divisor k F), adeleFiltration D = repartitionSpace k F

The filtration exhausts the repartition space: A_F = ⨆_D A_F(D).

theorem TauCeti.coe_repartitionSpace_eq_iUnion {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] : ↑(repartitionSpace k F) = ⋃ (D : Divisor k F), ↑(adeleFiltration D)

The filtration exhausts the repartition space, as the literal union of sets: A_F = ⋃_D A_F(D). The union is directed by TauCeti.directed_adeleFiltration.

The diagonal copy of F

noncomputable def TauCeti.diagonalRepartitions (k : Type u_1) (F : Type u_2) [Field k] [Field F] [Algebra k F] : Submodule k (Place k F → F)

The diagonal copy of F inside Place k F → F: the constant families. Together with TauCeti.diagonalRepartitions_le_repartitionSpace this is the embedding F ↪ A_F of Stichtenoth, Definition 1.5.2.

Equations

• TauCeti.diagonalRepartitions k F = (Pi.constAlgHom k (TauCeti.Place k F) F).toLinearMap.range

theorem TauCeti.mem_diagonalRepartitions_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {a : Place k F → F} : a ∈ diagonalRepartitions k F ↔ ∃ (f : F), Function.const (Place k F) f = a

Membership in the diagonal: a repartition is diagonal exactly when it is constant.

theorem TauCeti.const_mem_diagonalRepartitions {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (f : F) : Function.const (Place k F) f ∈ diagonalRepartitions k F

The constant families are diagonal.

theorem TauCeti.const_mem_repartitionSpace {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (f : F) : Function.const (Place k F) f ∈ repartitionSpace k F

The diagonal embedding F ↪ A_F at the level of elements: a function of an algebraic function field is integral at all but finitely many places, because it has only finitely many poles (Stichtenoth, Corollary 1.3.4).

theorem TauCeti.diagonalRepartitions_le_repartitionSpace {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) : diagonalRepartitions k F ≤ repartitionSpace k F

The diagonal embedding F ↪ A_F: the constant families are repartitions.

theorem TauCeti.const_mem_adeleFiltration_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D : Divisor k F} {f : F} : Function.const (Place k F) f ∈ adeleFiltration D ↔ f ∈ riemannRochSpace D

A constant family lies in A_F(D) exactly when its value lies in L(D): the two conditions are literally the same, since A_F(D) is the entrywise L(D) condition.

theorem TauCeti.diagonalRepartitions_inf_adeleFiltration {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D : Divisor k F) : diagonalRepartitions k F ⊓ adeleFiltration D = Submodule.map (Pi.constAlgHom k (Place k F) F).toLinearMap (riemannRochSpace D)

F ∩ A_F(D) = L(D): the diagonal meets the D-th step of the filtration in exactly the Riemann–Roch space of D. This is the lemma that makes the repartition quotients compute the index of specialty.

theorem TauCeti.adeleFiltration_inf_sup_diagonalRepartitions {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D E : Divisor k F} (h : D ≤ E) : adeleFiltration E ⊓ (adeleFiltration D ⊔ diagonalRepartitions k F) = adeleFiltration D ⊔ Submodule.map (Pi.constAlgHom k (Place k F) F).toLinearMap (riemannRochSpace E)

The relative form of F ∩ A_F(D) = L(D) (Stichtenoth, in the proof of Theorem 1.5.4): for D ≤ E, a repartition bounded by E that differs from a constant by a repartition bounded by D differs from a constant of L(E), so that

A_F(E) ∩ (A_F(D) + F) = A_F(D) + L(E).

Given A_F(D) ≤ A_F(E) this is the modular law for the lattice of subspaces followed by TauCeti.diagonalRepartitions_inf_adeleFiltration.

theorem TauCeti.const_mem_adeleFiltration_inf_sup_diagonalRepartitions {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D : Divisor k F) {E : Divisor k F} {f : F} (hf : f ∈ riemannRochSpace E) : Function.const (Place k F) f ∈ adeleFiltration E ⊓ (adeleFiltration D ⊔ diagonalRepartitions k F)

The constant repartition of a function of L(E) is bounded by E, and is a constant, so it lies in A_F(E) ∩ (A_F(D) + F).

theorem TauCeti.mem_adeleFiltration_sup_diagonalRepartitions_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D : Divisor k F} {a : Place k F → F} : a ∈ adeleFiltration D ⊔ diagonalRepartitions k F ↔ ∃ (f : F), (fun (P : Place k F) => a P - f) ∈ adeleFiltration D

Membership in A_F(D) + F, the subspace whose cokernel in A_F computes the index of specialty: a repartition lies in it exactly when subtracting a single constant brings it into A_F(D).

theorem TauCeti.adeleFiltration_sup_diagonalRepartitions_le {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (D : Divisor k F) : adeleFiltration D ⊔ diagonalRepartitions k F ≤ repartitionSpace k F

A_F(D) + F is a subspace of the repartition space.

noncomputable def TauCeti.submoduleOfAdeleFiltrationSupDiagonalRepartitions {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D : Divisor k F) : Submodule k ↥(repartitionSpace k F)

The subspace (A_F(D) + F) ∩ A_F of the repartition space: the repartitions that differ from a constant by one whose poles are bounded by D. Its cokernel in A_F is the index of specialty of D, and a Weil differential bounded by D is a k-linear form killing it.

Equations

• TauCeti.submoduleOfAdeleFiltrationSupDiagonalRepartitions D = (TauCeti.adeleFiltration D ⊔ TauCeti.diagonalRepartitions k F).submoduleOf (TauCeti.repartitionSpace k F)

theorem TauCeti.submoduleOfAdeleFiltrationSupDiagonalRepartitions_eq_submoduleOf {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D : Divisor k F) : submoduleOfAdeleFiltrationSupDiagonalRepartitions D = (adeleFiltration D ⊔ diagonalRepartitions k F).submoduleOf (repartitionSpace k F)

(A_F(D) + F) ∩ A_F is A_F(D) + F cut down to A_F in the sense of Submodule.submoduleOf, so that combinator's API applies to it.

@[simp]

theorem TauCeti.mem_submoduleOfAdeleFiltrationSupDiagonalRepartitions_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D : Divisor k F} {a : ↥(repartitionSpace k F)} : a ∈ submoduleOfAdeleFiltrationSupDiagonalRepartitions D ↔ ↑a ∈ adeleFiltration D ⊔ diagonalRepartitions k F

Membership in (A_F(D) + F) ∩ A_F is membership in A_F(D) + F of the underlying family.

theorem TauCeti.submoduleOfAdeleFiltrationSupDiagonalRepartitions_mono {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D E : Divisor k F} (h : D ≤ E) : submoduleOfAdeleFiltrationSupDiagonalRepartitions D ≤ submoduleOfAdeleFiltrationSupDiagonalRepartitions E

Enlarging the divisor enlarges (A_F(D) + F) ∩ A_F.

Translating the filtration by a principal divisor

theorem TauCeti.smul_mem_adeleFiltration_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) (D : Divisor k F) (a : Place k F → F) : ↑z • a ∈ adeleFiltration D ↔ a ∈ adeleFiltration (D + Divisor.principal hF z)

Multiplying a repartition by a nonzero function z translates the filtration by div z: the entrywise valuations are all scaled by v_P z = exp (-ord_P z).

theorem TauCeti.smul_mem_adeleFiltration_sub_principal {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) {D : Divisor k F} {a : Place k F → F} (ha : a ∈ adeleFiltration D) : ↑z • a ∈ adeleFiltration (D - Divisor.principal hF z)

Multiplying by z carries A_F(D) into A_F(D - div z), the repartition analogue of TauCeti.mul_mem_riemannRochSpace_sub_principal.

theorem TauCeti.smul_mem_repartitionSpace {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (f : F) {a : Place k F → F} (ha : a ∈ repartitionSpace k F) : f • a ∈ repartitionSpace k F

The repartition space is stable under multiplication by a function: it is an F-subspace of Place k F → F, which is what the F-vector space structure on the Weil differentials is built from.

theorem TauCeti.smul_mem_diagonalRepartitions {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (f : F) {a : Place k F → F} (ha : a ∈ diagonalRepartitions k F) : f • a ∈ diagonalRepartitions k F

The diagonal copy of F is stable under multiplication by a function: a constant times a constant is a constant.

noncomputable def TauCeti.repartitionMul {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) : F →ₐ[k] Module.End k ↥(repartitionSpace k F)

Multiplication of repartitions by a function, as a k-algebra map to the k-linear endomorphisms of the repartition space. It lands in the repartition space because a function of an algebraic function field has only finitely many poles.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.coe_repartitionMul_apply {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (f : F) (a : ↥(repartitionSpace k F)) : ↑(((repartitionMul hF) f) a) = f • ↑a

Multiplying a repartition by f multiplies each of its entries by f.

Repartitions supported at a single place

noncomputable def TauCeti.singleRepartition {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) : F →ₗ[k] ↥(repartitionSpace k F)

The repartition ι_P x with the entry x at the place P and 0 at every other place (Stichtenoth, Definition 1.7.1), as a k-linear map F →ₗ[k] A_F.

It is Finsupp.single P x, read as a family indexed by all the places; a finitely supported family is integral outside its support, hence a repartition.

Equations

• TauCeti.singleRepartition P = LinearMap.codRestrict (TauCeti.repartitionSpace k F) (Finsupp.lcoeFun ∘ₗ Finsupp.lsingle P) ⋯

@[simp]

theorem TauCeti.singleRepartition_self {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (x : F) : ↑((singleRepartition P) x) P = x

The entry of ι_P x at P is x.

@[simp]

theorem TauCeti.singleRepartition_of_ne {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {P Q : Place k F} (h : Q ≠ P) (x : F) : ↑((singleRepartition P) x) Q = 0

The entries of ι_P x away from P vanish.

theorem TauCeti.singleRepartition_mem_adeleFiltration_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D : Divisor k F} {P : Place k F} {x : F} : ↑((singleRepartition P) x) ∈ adeleFiltration D ↔ P.valuation x ≤ WithZero.exp (AlgebraicGeometry.WeilDivisor.coeff D P)

ι_P x is bounded by D exactly when the pole of x at P is: at every other place its entry is 0, which every divisor bounds.

This is not @[simp]: TauCeti.mem_adeleFiltration_iff is, and it rewrites this left-hand side first, so tagging this one is a simp-normal-form violation that scripts/lint-env.sh rejects.

@[simp]

theorem TauCeti.repartitionMul_singleRepartition {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (f : F) (P : Place k F) (x : F) : ((repartitionMul hF) f) ((singleRepartition P) x) = (singleRepartition P) (f * x)

Multiplying ι_P x by a function multiplies its entry: f · ι_P x = ι_P (f x).