Coordinate-free transport along algebra equivalences

This file proves that intrinsic places, divisors, Riemann--Roch spaces, and genus are invariant under an equivalence of function fields over the constant field. No rational-function chart or function-field hypotheses are needed: the intrinsic definitions only use the two field structures and their algebras over the common constant field.

theorem MarkoffRiemannRoch.FunctionField.Place.valuation_surjective {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] (v : Place k K) : Function.Surjective ⇑v.valuation

The normalized valuation associated to an intrinsic place is surjective.

noncomputable def MarkoffRiemannRoch.FunctionField.Place.mapAlgEquiv {k : Type u_1} {K : Type u_2} {L : Type u_3} [Field k] [Field K] [Field L] [Algebra k K] [Algebra k L] (e : K ≃ₐ[k] L) (v : Place k K) : Place k L

Transport an intrinsic place through an algebra equivalence.

Equations

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

@[simp]

theorem MarkoffRiemannRoch.FunctionField.Place.mapAlgEquiv_toValuationSubring {k : Type u_1} {K : Type u_2} {L : Type u_3} [Field k] [Field K] [Field L] [Algebra k K] [Algebra k L] (e : K ≃ₐ[k] L) (v : Place k K) : (mapAlgEquiv e v).toValuationSubring = v.toValuationSubring.comap e.symm.toRingEquiv.toRingHom

The valuation subring of a transported place is the corresponding pullback.

noncomputable def MarkoffRiemannRoch.FunctionField.Place.algEquiv {k : Type u_1} {K : Type u_2} {L : Type u_3} [Field k] [Field K] [Field L] [Algebra k K] [Algebra k L] (e : K ≃ₐ[k] L) : Place k K ≃ Place k L

Intrinsic places are equivalent under an equivalence of their ambient fields.

Equations

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

theorem MarkoffRiemannRoch.FunctionField.Place.mapAlgEquiv_valuation_eq_comap {k : Type u_1} {K : Type u_2} {L : Type u_3} [Field k] [Field K] [Field L] [Algebra k K] [Algebra k L] (e : K ≃ₐ[k] L) (v : Place k K) : (mapAlgEquiv e v).valuation = Valuation.comap e.symm.toRingEquiv.toRingHom v.valuation

Transporting a place preserves its normalized valuation exactly.

@[simp]

theorem MarkoffRiemannRoch.FunctionField.Place.algEquiv_valuation_apply {k : Type u_1} {K : Type u_2} {L : Type u_3} [Field k] [Field K] [Field L] [Algebra k K] [Algebra k L] (e : K ≃ₐ[k] L) (v : Place k K) (x : K) : ((algEquiv e) v).valuation (e x) = v.valuation x

Evaluation of normalized valuations is preserved by transport.

noncomputable def MarkoffRiemannRoch.FunctionField.Place.valuationSubringAlgEquiv {k : Type u_1} {K : Type u_2} {L : Type u_3} [Field k] [Field K] [Field L] [Algebra k K] [Algebra k L] (e : K ≃ₐ[k] L) (v : Place k K) : ↥v.toValuationSubring ≃ₐ[k] ↥((algEquiv e) v).toValuationSubring

The valuation subrings at corresponding places are equivalent as constant-field algebras.

Equations

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

noncomputable def MarkoffRiemannRoch.FunctionField.Place.residueFieldAlgEquiv {k : Type u_1} {K : Type u_2} {L : Type u_3} [Field k] [Field K] [Field L] [Algebra k K] [Algebra k L] (e : K ≃ₐ[k] L) (v : Place k K) : v.residueField ≃ₐ[k] ((algEquiv e) v).residueField

Residue fields at corresponding places are equivalent over the constant field.

Equations

• MarkoffRiemannRoch.FunctionField.Place.residueFieldAlgEquiv e v = IsLocalRing.ResidueField.mapAlgEquiv (MarkoffRiemannRoch.FunctionField.Place.valuationSubringAlgEquiv e v)

@[simp]

theorem MarkoffRiemannRoch.FunctionField.Place.degree_algEquiv {k : Type u_1} {K : Type u_2} {L : Type u_3} [Field k] [Field K] [Field L] [Algebra k K] [Algebra k L] (e : K ≃ₐ[k] L) (v : Place k K) : ((algEquiv e) v).degree = v.degree

Place degree is preserved under an equivalence of ambient fields.

noncomputable def MarkoffRiemannRoch.FunctionField.divisorAlgEquiv {k : Type u_1} {K : Type u_2} {L : Type u_3} [Field k] [Field K] [Field L] [Algebra k K] [Algebra k L] (e : K ≃ₐ[k] L) : Divisor k K ≃+ Divisor k L

Reindex intrinsic divisors through an equivalence of their ambient fields.

Equations

• MarkoffRiemannRoch.FunctionField.divisorAlgEquiv e = Finsupp.domCongr (MarkoffRiemannRoch.FunctionField.Place.algEquiv e)

@[simp]

theorem MarkoffRiemannRoch.FunctionField.Divisor.deg_algEquiv {k : Type u_1} {K : Type u_2} {L : Type u_3} [Field k] [Field K] [Field L] [Algebra k K] [Algebra k L] (e : K ≃ₐ[k] L) (D : Divisor k K) : deg k L ((divisorAlgEquiv e) D) = deg k K D

Intrinsic divisor degree is preserved by ambient-field equivalence.

theorem MarkoffRiemannRoch.FunctionField.memRRspace_algEquiv_iff {k : Type u_1} {K : Type u_2} {L : Type u_3} [Field k] [Field K] [Field L] [Algebra k K] [Algebra k L] (e : K ≃ₐ[k] L) (D : Divisor k K) (x : K) : memRRspace k L ((divisorAlgEquiv e) D) (e x) ↔ memRRspace k K D x

Riemann--Roch membership is preserved by ambient-field equivalence.

theorem MarkoffRiemannRoch.FunctionField.RRspace_map_algEquiv {k : Type u_1} {K : Type u_2} {L : Type u_3} [Field k] [Field K] [Field L] [Algebra k K] [Algebra k L] (e : K ≃ₐ[k] L) (D : Divisor k K) : Submodule.map (↑↑e) (RRspace k K D) = RRspace k L ((divisorAlgEquiv e) D)

The image of an intrinsic Riemann--Roch space is the transported space.

noncomputable def MarkoffRiemannRoch.FunctionField.RRspaceAlgEquiv {k : Type u_1} {K : Type u_2} {L : Type u_3} [Field k] [Field K] [Field L] [Algebra k K] [Algebra k L] (e : K ≃ₐ[k] L) (D : Divisor k K) : ↥(RRspace k K D) ≃ₗ[k] ↥(RRspace k L ((divisorAlgEquiv e) D))

Corresponding intrinsic Riemann--Roch spaces are linearly equivalent.

Equations

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

@[simp]

theorem MarkoffRiemannRoch.FunctionField.ell_algEquiv {k : Type u_1} {K : Type u_2} {L : Type u_3} [Field k] [Field K] [Field L] [Algebra k K] [Algebra k L] (e : K ≃ₐ[k] L) (D : Divisor k K) : ell k L ((divisorAlgEquiv e) D) = ell k K D

Riemann--Roch dimension is invariant under ambient-field equivalence.

@[simp]

theorem MarkoffRiemannRoch.FunctionField.defect_algEquiv {k : Type u_1} {K : Type u_2} {L : Type u_3} [Field k] [Field K] [Field L] [Algebra k K] [Algebra k L] (e : K ≃ₐ[k] L) (D : Divisor k K) : defect k L ((divisorAlgEquiv e) D) = defect k K D

Divisor defect is invariant under ambient-field equivalence.

theorem MarkoffRiemannRoch.FunctionField.genus_eq_of_algEquiv {k : Type u_1} {K : Type u_2} {L : Type u_3} [Field k] [Field K] [Field L] [Algebra k K] [Algebra k L] (e : K ≃ₐ[k] L) : genus k K = genus k L

Intrinsic function-field genus is invariant under an equivalence over the constant field.