Weil differentials over intrinsic places

Weil differentials are defined here as linear functionals on the intrinsic adele space that vanish on A(D) plus the diagonal for some intrinsic divisor. The equivalence weilDifferentialEquivChart transports the existing chart proofs without exposing chart-indexed carriers in the public statements.

structure FunctionField.WeilDifferential (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] : Type (max u_1 u_2)

A Weil differential is a functional on intrinsic adeles that vanishes on A(D) plus the diagonal for some intrinsic divisor D.

• toFun : ↥(AdeleSpace k K) →ₗ[k] k

  The underlying linear functional on intrinsic adeles.

• vanishes_on : ∃ (D : Divisor k K), ∀ a ∈ adeleFilt k K D + diagonalSubmodule k K, self.toFun a = 0

  A filtration piece plus the diagonal on which the functional vanishes.

def FunctionField.WeilDifferential.IsNonzero {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (omega : WeilDifferential k K) : Prop

A Weil differential is nonzero when its underlying functional is nonzero.

Equations

• omega.IsNonzero = (omega.toFun ≠ 0)

def FunctionField.WeilDifferential.differentialSpace {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D : Divisor k K) : Submodule k (↥(AdeleSpace k K) →ₗ[k] k)

The space of functionals vanishing on A(D) plus the diagonal.

Equations

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

noncomputable def FunctionField.WeilDifferential.adeleDualEquivChart {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] : (↥(AdeleSpace k K) →ₗ[k] k) ≃ₗ[k] ↥(Chart.AdeleSpace k K) →ₗ[k] k

The dual-space equivalence induced by reindexing intrinsic adeles to chart adeles.

Equations

• FunctionField.WeilDifferential.adeleDualEquivChart = (FunctionField.adeleEquivChart k K).symm.dualMap

@[simp]

theorem FunctionField.WeilDifferential.adeleDualEquivChart_apply {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (phi : ↥(AdeleSpace k K) →ₗ[k] k) (a : ↥(Chart.AdeleSpace k K)) : (adeleDualEquivChart phi) a = phi ((adeleEquivChart k K).symm a)

@[simp]

theorem FunctionField.WeilDifferential.adeleDualEquivChart_symm_apply {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (phi : ↥(Chart.AdeleSpace k K) →ₗ[k] k) (a : ↥(AdeleSpace k K)) : (adeleDualEquivChart.symm phi) a = phi ((adeleEquivChart k K) a)

noncomputable def FunctionField.WeilDifferential.toChart {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (omega : WeilDifferential k K) : Chart.WeilDifferential k K

Reindex an intrinsic Weil differential as a chart Weil differential.

Equations

• omega.toChart = { toFun := FunctionField.WeilDifferential.adeleDualEquivChart omega.toFun, vanishes_on := ⋯ }

noncomputable def FunctionField.WeilDifferential.ofChart {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (omega : Chart.WeilDifferential k K) : WeilDifferential k K

Reindex a chart Weil differential as an intrinsic Weil differential.

Equations

• FunctionField.WeilDifferential.ofChart omega = { toFun := FunctionField.WeilDifferential.adeleDualEquivChart.symm omega.toFun, vanishes_on := ⋯ }

theorem FunctionField.WeilDifferential.ext {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] {omega eta : WeilDifferential k K} (h : omega.toFun = eta.toFun) : omega = eta

theorem FunctionField.WeilDifferential.ext_iff {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] {omega eta : WeilDifferential k K} : omega = eta ↔ omega.toFun = eta.toFun

@[instance_reducible]

instance FunctionField.WeilDifferential.instZero {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] : Zero (WeilDifferential k K)

Equations

• FunctionField.WeilDifferential.instZero = { zero := { toFun := 0, vanishes_on := ⋯ } }

@[instance_reducible]

instance FunctionField.WeilDifferential.instAdd {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] : Add (WeilDifferential k K)

Equations

• FunctionField.WeilDifferential.instAdd = { add := fun (omega eta : FunctionField.WeilDifferential k K) => { toFun := omega.toFun + eta.toFun, vanishes_on := ⋯ } }

@[instance_reducible]

instance FunctionField.WeilDifferential.instNeg {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] : Neg (WeilDifferential k K)

Equations

• FunctionField.WeilDifferential.instNeg = { neg := fun (omega : FunctionField.WeilDifferential k K) => { toFun := -omega.toFun, vanishes_on := ⋯ } }

@[instance_reducible]

instance FunctionField.WeilDifferential.instAddCommGroup {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] : AddCommGroup (WeilDifferential k K)

Equations

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

noncomputable def FunctionField.WeilDifferential.weilDifferentialAddEquivChart {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] : WeilDifferential k K ≃+ Chart.WeilDifferential k K

Intrinsic and chart Weil differentials are equivalent as additive groups.

Equations

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

@[instance_reducible]

noncomputable instance FunctionField.WeilDifferential.instSMul {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] : SMul K (WeilDifferential k K)

Equations

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

@[simp]

theorem FunctionField.WeilDifferential.weilDifferentialAddEquivChart_smul {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (x : K) (omega : WeilDifferential k K) : weilDifferentialAddEquivChart (x • omega) = x • weilDifferentialAddEquivChart omega

@[instance_reducible]

noncomputable instance FunctionField.WeilDifferential.instModule {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] : Module K (WeilDifferential k K)

Equations

• FunctionField.WeilDifferential.instModule = Function.Injective.module K FunctionField.WeilDifferential.weilDifferentialAddEquivChart.toAddMonoidHom ⋯ ⋯

noncomputable def FunctionField.WeilDifferential.weilDifferentialEquivChart {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] : WeilDifferential k K ≃ₗ[K] Chart.WeilDifferential k K

Intrinsic and chart Weil differentials are linearly equivalent over the function field.

Equations

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

noncomputable def FunctionField.WeilDifferential.differentialSpaceEquivChart {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D : Divisor k K) : ↥(differentialSpace D) ≃ₗ[k] ↥(Chart.WeilDifferential.differentialSpace ((divisorEquivChart k K).symm D))

The intrinsic space Omega(D) is linearly equivalent to its chart presentation.

Equations

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

theorem FunctionField.WeilDifferential.finrank_differentialSpace_eq_chart {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D : Divisor k K) : Module.finrank k ↥(differentialSpace D) = Module.finrank k ↥(Chart.WeilDifferential.differentialSpace ((divisorEquivChart k K).symm D))

The intrinsic and chart differential spaces have the same dimension.

theorem FunctionField.WeilDifferential.finrank_weilDifferential_eq_one {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] : Module.finrank K (WeilDifferential k K) = 1

The intrinsic space of Weil differentials is one-dimensional over K.

theorem FunctionField.WeilDifferential.isNonzero_toChart {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (omega : WeilDifferential k K) : omega.IsNonzero ↔ omega.toChart.IsNonzero

Non-vanishing is preserved by the intrinsic-to-chart equivalence.

noncomputable def FunctionField.WeilDifferential.divOmega {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] (omega : WeilDifferential k K) (homega : omega.IsNonzero) : Divisor k K

The divisor of a nonzero intrinsic Weil differential.

Equations

• omega.divOmega homega = (FunctionField.divisorEquivChart k K) (omega.toChart.divOmega ⋯)

theorem FunctionField.WeilDifferential.divOmega_smul {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] (x : Kˣ) (omega : WeilDifferential k K) (homega : omega.IsNonzero) (hxomega : (↑x • omega).IsNonzero) : (↑x • omega).divOmega hxomega = omega.divOmega homega + (principalDivisor k K) (Additive.ofMul x)

Multiplying a differential adds the corresponding intrinsic principal divisor.

def FunctionField.IsCanonical (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] (W : Divisor k K) : Prop

A divisor is canonical when it is the divisor of a nonzero intrinsic Weil differential.

Equations

• FunctionField.IsCanonical k K W = ∃ (omega : FunctionField.WeilDifferential k K) (homega : omega.IsNonzero), omega.divOmega homega = W

theorem FunctionField.isCanonical_iff_chart (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] (W : Divisor k K) : IsCanonical k K W ↔ Chart.IsCanonical k K ((divisorEquivChart k K).symm W)

Intrinsic and chart definitions of canonical divisors agree.