structure BaseExtensionData (C : Type u_1) (F : Type u_2) (k : Type u_3) [Field k] [Field F] [Algebra k F] [RiemannRochData C F k] : Type (max (max (max (max u_1 u_3) (u_4 + 1)) (u_5 + 1)) (u_6 + 1))

Data packaging a base extension $k \hookrightarrow k'$ for a smooth projective curve $(C, F/k)$: a new curve $C'$ over a field $F'/k'$, together with a RiemannRochData structure on $(C', F', k')$ and explicit divisor base-extension and restriction maps.

• C' : Type u_4
• F' : Type u_5
• k' : Type u_6
• field_k' : Field self.k'
• field_F' : Field self.F'
• algebra_k_k' : Algebra k self.k'
• algebra_k'_F' : Algebra self.k' self.F'
• rrData' : RiemannRochData self.C' self.F' self.k'
• baseExtDiv : CurveDivisor C → CurveDivisor self.C'
• restrictDiv : CurveDivisor self.C' → CurveDivisor C

theorem BaseExtensionData.degree_baseExt_ax {C : Type u_1} {F : Type u_2} {k : Type u_3} [Field k] [Field F] [Algebra k F] [RiemannRochData C F k] (ext : BaseExtensionData C F k) (D : CurveDivisor C) : (CurveDivisor.degree ext.C') (ext.baseExtDiv D) = (CurveDivisor.degree C) D

Axiomatized: the divisor base-extension map preserves degree, $\deg_{C'}(\mathrm{baseExt}(D)) = \deg_C(D)$.

theorem BaseExtensionData.divisorDim_baseExt_ax {C : Type u_1} {F : Type u_2} {k : Type u_3} [Field k] [Field F] [Algebra k F] [RiemannRochData C F k] (ext : BaseExtensionData C F k) (D : CurveDivisor C) : RiemannRochSpace.divisorDim (ext.baseExtDiv D) = RiemannRochSpace.divisorDim D

Axiomatized: the divisor base-extension map preserves the Riemann–Roch dimension, $\dim L(\mathrm{baseExt}(D))_{F'/k'} = \dim L(D)_{F/k}$.

theorem BaseExtensionData.degree_restrict_ax {C : Type u_1} {F : Type u_2} {k : Type u_3} [Field k] [Field F] [Algebra k F] [RiemannRochData C F k] (ext : BaseExtensionData C F k) (D' : CurveDivisor ext.C') : (CurveDivisor.degree C) (ext.restrictDiv D') = (CurveDivisor.degree ext.C') D'

Axiomatized: the divisor restriction map preserves degree, $\deg_C(\mathrm{restrict}(D')) = \deg_{C'}(D')$.

theorem BaseExtensionData.divisorDim_restrict_ax {C : Type u_1} {F : Type u_2} {k : Type u_3} [Field k] [Field F] [Algebra k F] [RiemannRochData C F k] (ext : BaseExtensionData C F k) (D' : CurveDivisor ext.C') : RiemannRochSpace.divisorDim (ext.restrictDiv D') = RiemannRochSpace.divisorDim D'

Axiomatized: the divisor restriction map preserves the Riemann–Roch dimension.

theorem genus_preserved_under_base_extension {C : Type u_1} {F : Type u_2} {k : Type u_3} [Field k] [Field F] [Algebra k F] [RiemannRochData C F k] [PerfectField k] (ext : BaseExtensionData C F k) : RiemannRochSpace.genus = RiemannRochSpace.genus

Invariance of genus under base extension: for a perfect base field $k$, base-changing the curve $C$ to a curve $C'$ over $k'$ preserves the genus, $g_{C'/k'} = g_{C/k}$. The proof uses mutual upper bounds obtained from degree_baseExt_ax/divisorDim_baseExt_ax and degree_restrict_ax/divisorDim_restrict_ax.