Module

SemilinearEvaluation.lean

Nyll.AlgebraicCurves.Places.SemilinearEvaluation

5 declarations indexed from sourceView source ↗

Module documentation

Semilinear compatibility of residue and divisor evaluation

Imports3

Imported by2

theorem

mem_smul_toValuationSubring_iff

L32 ↗

AlgebraicCurve.SemilinearAut.mem_smul_toValuationSubring_iff

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace AlgebraicCurve.SemilinearAut
open IsLocalRing
open scoped Pointwise
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (g : SemilinearAut K F) (v : Place K F)

Lean source · statement

theorem mem_smul_toValuationSubring_iff (f : F) :
    g • f ∈ (g • v).toValuationSubring ↔ f ∈ v.toValuationSubring

theorem

isRational_smul

L43 ↗

AlgebraicCurve.SemilinearAut.isRational_smul

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace AlgebraicCurve.SemilinearAut
open IsLocalRing
open scoped Pointwise
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (g : SemilinearAut K F) (v : Place K F)

Lean source · statement

theorem isRational_smul (hv : v.IsRational) : (g • v).IsRational

theorem

residue_smul

L49 ↗

AlgebraicCurve.SemilinearAut.residue_smul

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace AlgebraicCurve.SemilinearAut
open IsLocalRing
open scoped Pointwise
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (g : SemilinearAut K F) (v : Place K F)

Lean source · statement

theorem residue_smul {f : F} (hf : f ∈ v.toValuationSubring) :
    residue (g • v).toValuationSubring
        (⟨g • f, (mem_smul_toValuationSubring_iff g v f).mpr hf⟩ :
          (g • v).toValuationSubring)
      = smulResidueRingEquiv g v (residue v.toValuationSubring ⟨f, hf⟩)

theorem

evalAt_smul

L60 ↗

AlgebraicCurve.SemilinearAut.evalAt_smul

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace AlgebraicCurve.SemilinearAut
open IsLocalRing
open scoped Pointwise
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (g : SemilinearAut K F) (v : Place K F)

Lean source · statement

theorem evalAt_smul (hv : v.IsRational) {f : F} (hf : f ∈ v.toValuationSubring) :
    (g • v).evalAt (g • f) = baseAut g (v.evalAt f)

theorem

evalFun_smul

L70 ↗

AlgebraicCurve.SemilinearAut.evalFun_smul

Documentation

Rational divisor evaluation commutes with the actual semilinear action.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace AlgebraicCurve.SemilinearAut
open IsLocalRing
open scoped Pointwise
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (g : SemilinearAut K F) (v : Place K F)

Lean source · statement

theorem evalFun_smul {f : F} (D : Divisor K F)
    (hrat : ∀ v ∈ D.support, Place.IsRational v)
    (hmem : ∀ v ∈ D.support, f ∈ v.toValuationSubring) :
    Divisor.evalFun (g • f) (g • D) = baseAut g (Divisor.evalFun f D)

Module documentation

Semilinear compatibility of residue and divisor evaluation

Declarations

mem_smul_toValuationSubring_iff

isRational_smul

residue_smul

evalAt_smul

evalFun_smul