The conorm of a divisor along an extension of function fields

Let F' / k' be a finite extension of the algebraic function field F / k. Every place P' of F' / k' restricts to a place P'.restrict k F of F / k, and a place of F / k has only finitely many places above it. The conorm

Con(P) = ∑_{P' ∣ P} e(P' ∣ P) · P'

therefore extends by additivity to a homomorphism Con : Divisor k F →+ Divisor k' F' of divisor groups. Equivalently — and this is the definition used here, because it makes the coefficient formula definitional — the coefficient of Con D at P' is e(P' ∣ P) · D(P) for the place P = P'.restrict k F below P'.

The conorm carries the divisor of a function z to the divisor of its image in F', because on F the order function at P' is e(P' ∣ P) times the order function at P. Hence it descends to a homomorphism of divisor class groups.

The degree identity [k' : k] · deg (Con D) = [F' : F] · deg D is proved here from the fundamental identity ∑_{P' ∣ P} e(P' ∣ P) f(P' ∣ P) = [F' : F]. It therefore holds without a separability hypothesis when F / k is an algebraic function field; a second form assumes separability of F' / F and does not require the function-field hypothesis. The identity is stated cross-multiplied, since the divisibility [k' : k] ∣ [F' : F] that turns it into deg (Con D) = n(F'/F) · deg D needs F and k' to be linearly disjoint over k; under that hypothesis the divided form is degree_conorm, with n(F'/F) the geometric degree of the extension.

Main definitions

• TauCeti.Divisor.conorm: the conorm homomorphism Con : Divisor k F →+ Divisor k' F' (Stichtenoth, Definition 3.1.8).
• TauCeti.Divisor.conormClassGroup: the induced homomorphism Cl(F) →+ Cl(F') of divisor class groups (Stichtenoth, Proposition 3.1.9).

Main results

• TauCeti.Divisor.coeff_conorm: the defining coefficient formula.
• TauCeti.Divisor.conorm_ofPoint: the conorm of a place is ∑_{P' ∣ P} e(P' ∣ P) · P', the form in which Stichtenoth defines it.
• TauCeti.Divisor.conorm_conorm: the conorm is transitive in a tower of extensions (Stichtenoth, Definition 3.1.8).
• TauCeti.Divisor.conorm_principal: the conorm of div z is the divisor of the image of z (Stichtenoth, Proposition 3.1.9).
• TauCeti.Divisor.conorm_zeros and TauCeti.Divisor.conorm_poles: the conorm of the zero and pole divisors of z are those of the image of z.
• TauCeti.Divisor.conorm_injective: the conorm is injective.
• TauCeti.Divisor.exists_le_conorm: every divisor of F' / k' is bounded above by a conorm.
• TauCeti.Divisor.finrank_mul_degree_conorm: the degree of a conorm, [k' : k] · deg (Con D) = [F' : F] · deg D for an algebraic function field, without a separability hypothesis (Stichtenoth, Corollary 3.1.14).
• TauCeti.Divisor.finrank_mul_degree_conorm_of_isSeparable: the same identity for an arbitrary lower field when F' / F is separable.
• TauCeti.Divisor.degree_conorm: the same identity divided through by [k' : k], for F and k' linearly disjoint over k: deg (Con D) = n(F'/F) · deg D (Stichtenoth, Corollary 3.6.4).
• TauCeti.Divisor.degree_conorm_of_finrank_eq_one: deg (Con D) = [F' : F] · deg D when the constant field does not grow, read straight off the cross-multiplied identity.

Implementation notes

The upper field F' / k' is an explicit argument of conorm, and the lower field F / k is implicit, because a divisor of F / k determines the latter but not the former. This is the opposite convention to TauCeti.Place.restrict, and for the same reason: there the argument determines the upper field and the lower one has to be supplied.

The conorm is built from its coefficients through Finsupp.ofSupportFinite rather than as the formal sum ∑_P D(P) · Con(P). The coefficient formula is then definitional and additivity is immediate, whereas the sum form needs the fibres to be disjoint before either can be read off; TauCeti.Divisor.conorm_ofPoint recovers the sum form at a single place.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Sections III.1 and III.6. The conorm and its cross-multiplied degree identity are III.1 (Definition 3.1.8, Proposition 3.1.9, Corollary 3.1.14); the quotient-valued degree identity deg (Con A) = [F' : F·k'] · deg A is Corollary 3.6.4.

noncomputable def TauCeti.Divisor.conorm {k : Type u} (k' : Type u') {F : Type v} (F' : Type v') [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] : Divisor k F →+ Divisor k' F'

The conorm of a divisor along a finite extension F' / k' of F / k (Stichtenoth, Definition 3.1.8): the divisor of F' / k' whose coefficient at a place P' is e(P' ∣ P) times the coefficient of D at the place P that P' lies over. On a single place it is the formal sum ∑_{P' ∣ P} e(P' ∣ P) · P'; see TauCeti.Divisor.conorm_ofPoint.

Equations

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

@[simp]

theorem TauCeti.Divisor.coeff_conorm {k : Type u} (k' : Type u') {F : Type v} (F' : Type v') [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] (D : Divisor k F) (P' : Place k' F') : AlgebraicGeometry.WeilDivisor.coeff ((conorm k' F') D) P' = ↑(Place.ramificationIdx F P') * AlgebraicGeometry.WeilDivisor.coeff D (Place.restrict k F P')

The defining coefficient formula of the conorm: the coefficient of Con D at a place P' of F' / k' is e(P' ∣ P) times the coefficient of D at the place P below it.

theorem TauCeti.Divisor.mem_support_conorm_iff {k : Type u} (k' : Type u') {F : Type v} (F' : Type v') [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] {D : Divisor k F} {P' : Place k' F'} : P' ∈ ((conorm k' F') D).support ↔ Place.restrict k F P' ∈ D.support

A place of F' / k' lies in the support of Con D exactly when the place below it lies in the support of D: the ramification indices are positive, so nothing cancels.

theorem TauCeti.Divisor.conorm_ofPoint {k : Type u} (k' : Type u') {F : Type v} (F' : Type v') [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] (P : Place k F) : (conorm k' F') (AlgebraicGeometry.WeilDivisor.ofPoint P) = AlgebraicGeometry.WeilDivisor.ofFinsetWithMultiplicity ⋯.toFinset (Place.ramificationIdx F)

The conorm of a place (Stichtenoth, Definition 3.1.8): Con P = ∑_{P' ∣ P} e(P' ∣ P) · P', the divisor supported on the finitely many places of F' / k' lying over P with the ramification indices as multiplicities. Its expansion as a sum of point divisors is TauCeti.AlgebraicGeometry.WeilDivisor.ofFinsetWithMultiplicity_eq_sum.

@[simp]

theorem TauCeti.Divisor.conorm_self {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D : Divisor k F) : (conorm k F) D = D

The conorm along the identity extension is the identity. Every place restricts to itself and the ramification index is 1, so no coefficient moves.

theorem TauCeti.Divisor.conorm_mono {k : Type u} (k' : Type u') {F : Type v} (F' : Type v') [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] : Monotone ⇑(conorm k' F')

The conorm is monotone: it multiplies coefficients by positive ramification indices.

theorem TauCeti.Divisor.isEffective_conorm {k : Type u} (k' : Type u') {F : Type v} (F' : Type v') [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] {D : Divisor k F} (hD : AlgebraicGeometry.WeilDivisor.IsEffective D) : AlgebraicGeometry.WeilDivisor.IsEffective ((conorm k' F') D)

The conorm of an effective divisor is effective.

theorem TauCeti.Divisor.exists_le_conorm {k : Type u} (k' : Type u') {F : Type v} (F' : Type v') [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] (D' : Divisor k' F') : ∃ (D : Divisor k F), D' ≤ (conorm k' F') D

Every divisor of F' / k' is bounded above by a conorm: for every divisor D' of F' / k' there is a divisor D of F / k with D' ≤ Con D. This transports estimates on the divisors of F / k to all divisors of F' / k'.

theorem TauCeti.Divisor.conorm_injective {k : Type u} (k' : Type u') {F : Type v} (F' : Type v') [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsIntegral k k'] (hF' : IsFunctionField k' F') : Function.Injective ⇑(conorm k' F')

The conorm is injective: every place of F / k is the restriction of a place of F' / k', and the ramification indices are nonzero.

The degree of a conorm

theorem TauCeti.Divisor.finrank_mul_degree_conorm_of_isSeparable {k : Type u} (k' : Type u') {F : Type v} (F' : Type v') [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsIntegral k k'] [Algebra.IsSeparable F F'] (D : Divisor k F) : ↑(Module.finrank k k') * degree ((conorm k' F') D) = ↑(Module.finrank F F') * degree D

The degree of a conorm for a separable extension, cross-multiplied (Stichtenoth, Corollary 3.1.14): [k' : k] · deg (Con D) = [F' : F] · deg D. Nothing here is divided, so no divisibility is presupposed; dividing through by [k' : k] needs TauCeti.finrank_dvd_finrank_of_finrank_constantCompositum_eq, and the divided identity is TauCeti.Divisor.degree_conorm_of_isSeparable.

This form requires no function-field hypothesis on F / k. For an algebraic function field the identity holds for every finite extension, without separability; that is TauCeti.Divisor.finrank_mul_degree_conorm.

theorem TauCeti.Divisor.finrank_mul_degree_conorm {k : Type u} (k' : Type u') {F : Type v} (F' : Type v') [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsIntegral k k'] (hF : IsFunctionField k F) (D : Divisor k F) : ↑(Module.finrank k k') * degree ((conorm k' F') D) = ↑(Module.finrank F F') * degree D

The degree of a conorm, cross-multiplied (Stichtenoth, Corollary 3.1.14): for an algebraic function field F / k and any finite extension F' / F, [k' : k] · deg (Con D) = [F' : F] · deg D. No separability or perfectness hypothesis is required.

Nothing here is divided, so no divisibility is presupposed; dividing through by [k' : k] needs TauCeti.finrank_dvd_finrank_of_finrank_constantCompositum_eq, and the divided identity is TauCeti.Divisor.degree_conorm. If F' / F is separable, the identity holds without assuming that F / k is a function field; see TauCeti.Divisor.finrank_mul_degree_conorm_of_isSeparable.

theorem TauCeti.Divisor.degree_conorm {k : Type u} (k' : Type u') {F : Type v} (F' : Type v') [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsIntegral k k'] (hF : IsFunctionField k F) (h : Module.finrank F ↥(constantCompositum F k' F') = Module.finrank k k') (D : Divisor k F) : degree ((conorm k' F') D) = ↑(geometricDegree F k' F') * degree D

The degree of a conorm, divided through: when adjoining the constant field k' to F costs exactly [k' : k] — the degree form of linear disjointness of F and k' over k — so that [k' : k] divides [F' : F] with quotient the geometric degree n(F'/F), the conorm multiplies degrees by n(F'/F).

This is Stichtenoth's Corollary 3.6.4. The cross-multiplied TauCeti.Divisor.finrank_mul_degree_conorm (Corollary 3.1.14) is the form that holds without linear disjointness, and this is that identity divided through by [k' : k]. No separability or perfectness hypothesis is required.

The hypothesis h is supplied by TauCeti.finrank_constantCompositum_eq_finrank_of_isSeparable whenever k' / k is finite separable and k is the exact constant field of F, and by TauCeti.finrank_constantCompositum_eq_finrank_of_linearDisjoint from Mathlib's IntermediateField.LinearDisjoint. Together with the section's [FiniteDimensional F F'] it forces [k' : k] to be finite and positive, which is what licenses the division; no separate finiteness assumption on k' / k is needed.

theorem TauCeti.Divisor.degree_conorm_of_isSeparable {k : Type u} (k' : Type u') {F : Type v} (F' : Type v') [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsIntegral k k'] [Algebra.IsSeparable F F'] (h : Module.finrank F ↥(constantCompositum F k' F') = Module.finrank k k') (D : Divisor k F) : degree ((conorm k' F') D) = ↑(geometricDegree F k' F') * degree D

The degree of a conorm for a separable extension, divided through: the version of TauCeti.Divisor.degree_conorm which requires no function-field hypothesis on F / k, but instead assumes that F' / F is separable.

@[simp]

theorem TauCeti.Divisor.degree_conorm_of_finrank_eq_one {k : Type u} (k' : Type u') {F : Type v} (F' : Type v') [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsIntegral k k'] (hF : IsFunctionField k F) (h : Module.finrank k k' = 1) (D : Divisor k F) : degree ((conorm k' F') D) = ↑(Module.finrank F F') * degree D

The conorm multiplies degrees by [F' : F] when the constant field does not grow, i.e. when [k' : k] = 1. No hypothesis on where the constants sit is needed: the cross-multiplied identity finrank_mul_degree_conorm already has [k' : k] as its left factor, so setting it to one reads the degree off directly. This is the shape a curve over its own base field presents, where k' = k is that base field.

@[simp]

theorem TauCeti.Divisor.degree_conorm_of_isSeparable_of_finrank_eq_one {k : Type u} (k' : Type u') {F : Type v} (F' : Type v') [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsIntegral k k'] [Algebra.IsSeparable F F'] (h : Module.finrank k k' = 1) (D : Divisor k F) : degree ((conorm k' F') D) = ↑(Module.finrank F F') * degree D

The conorm multiplies degrees by [F' : F] for a separable extension with unchanged constants, without requiring a function-field hypothesis on F / k.

Principal divisors and divisor classes

theorem TauCeti.Divisor.conorm_principal {k : Type u} (k' : Type u') {F : Type v} (F' : Type v') [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k' F') (z : Fˣ) : (conorm k' F') (principal hF z) = principal hF' ((Units.map ↑(algebraMap F F')) z)

The conorm of a principal divisor is principal (Stichtenoth, Proposition 3.1.9): the conorm of div z is the divisor of the image of z in F'.

@[simp]

theorem TauCeti.Divisor.conorm_zeros {k : Type u} (k' : Type u') {F : Type v} (F' : Type v') [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k' F') (z : Fˣ) : (conorm k' F') (zeros hF z) = zeros hF' ((Units.map ↑(algebraMap F F')) z)

The conorm of the zero divisor (z)₀ is the zero divisor of the image of z in F'.

@[simp]

theorem TauCeti.Divisor.conorm_poles {k : Type u} (k' : Type u') {F : Type v} (F' : Type v') [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k' F') (z : Fˣ) : (conorm k' F') (poles hF z) = poles hF' ((Units.map ↑(algebraMap F F')) z)

The conorm of the pole divisor (z)_∞ is the pole divisor of the image of z in F'.

theorem TauCeti.Divisor.conorm_mem_principalSubgroup {k : Type u} (k' : Type u') {F : Type v} (F' : Type v') [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k' F') {D : Divisor k F} (hD : D ∈ (Place.orderSystem hF).principalSubgroup) : (conorm k' F') D ∈ (Place.orderSystem hF').principalSubgroup

The conorm carries principal divisors to principal divisors.

theorem TauCeti.Divisor.linearlyEquivalent_conorm {k : Type u} (k' : Type u') {F : Type v} (F' : Type v') [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k' F') {A B : Divisor k F} (h : (Place.orderSystem hF).LinearlyEquivalent A B) : (Place.orderSystem hF').LinearlyEquivalent ((conorm k' F') A) ((conorm k' F') B)

The conorm respects linear equivalence (Stichtenoth, Proposition 3.1.9).

noncomputable def TauCeti.Divisor.conormClassGroup {k : Type u} (k' : Type u') {F : Type v} (F' : Type v') [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k' F') : (Place.orderSystem hF).ClassGroup →+ (Place.orderSystem hF').ClassGroup

The conorm on divisor classes (Stichtenoth, Proposition 3.1.9): the conorm descends to a homomorphism Cl(F) →+ Cl(F') of divisor class groups.

Equations

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

@[simp]

theorem TauCeti.Divisor.conormClassGroup_divisorClass {k : Type u} (k' : Type u') {F : Type v} (F' : Type v') [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k' F') (D : Divisor k F) : (conormClassGroup k' F' hF hF') ((Place.orderSystem hF).divisorClass D) = (Place.orderSystem hF').divisorClass ((conorm k' F') D)

@[simp]

theorem TauCeti.Divisor.conorm_conorm {k₀ : Type u₀} (k₁ : Type u₁) (k₂ : Type u₂) {F₀ : Type v₀} (F₁ : Type v₁) (F₂ : Type v₂) [Field k₀] [Field k₁] [Field k₂] [Field F₀] [Field F₁] [Field F₂] [Algebra k₀ k₁] [Algebra k₁ k₂] [Algebra k₀ k₂] [Algebra F₀ F₁] [Algebra F₁ F₂] [Algebra F₀ F₂] [IsScalarTower F₀ F₁ F₂] [Algebra k₀ F₀] [Algebra k₁ F₁] [Algebra k₂ F₂] [Algebra k₀ F₁] [Algebra k₁ F₂] [Algebra k₀ F₂] [IsScalarTower k₀ k₁ F₁] [IsScalarTower k₁ k₂ F₂] [IsScalarTower k₀ F₀ F₁] [IsScalarTower k₁ F₁ F₂] [IsScalarTower k₀ k₂ F₂] [IsScalarTower k₀ F₀ F₂] [FiniteDimensional F₀ F₁] [FiniteDimensional F₁ F₂] (D : Divisor k₀ F₀) : (conorm k₂ F₂) ((conorm k₁ F₁) D) = (conorm k₂ F₂) D

The conorm is transitive in a tower (Stichtenoth, Definition 3.1.8): the conorm from F₀ / k₀ to F₂ / k₂ factors through F₁ / k₁. This is the divisor form of the multiplicativity of the ramification indices in a tower.

The finiteness of F₂ / F₀, which the direct conorm needs, is supplied by FiniteDimensional.trans rather than assumed: FiniteDimensional.trans is not an instance, so it has to be installed by hand in the statement.