NYLL
Module

Divisor_evalFun_pullback_of_isPurelyInseparable.lean

Nyll.AlgebraicCurves.Divisors.Divisor_evalFun_pullback_of_isPurelyInseparable
7 declarations indexed from sourceView source ↗

Module documentation

Divisor eval Fun pullback of is Purely Inseparable

Imports6
Imported by2

Declarations

theorem

exists_algebraMap_eq_pow_finrank

L37 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_evalFun_pullback_of_isPurelyInseparable.Ws47.EVPI.exists_algebraMap_eq_pow_finrank
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_evalFun_pullback_of_isPurelyInseparable
open _root_.AlgebraicCurve
namespace Ws47
namespace EVPI
section PI
variable {F E : Type*} [Field F] [Field E] [Algebra F E] [FiniteDimensional F E]
  [IsPurelyInseparable F E]
Lean source · statement
theorem exists_algebraMap_eq_pow_finrank (x : E) : ∃ y : F, algebraMap F E y = x ^ Module.finrank F
  E
theorem

algebraMap_norm_eq_pow_finrank

L61 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_evalFun_pullback_of_isPurelyInseparable.Ws47.EVPI.algebraMap_norm_eq_pow_finrank
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_evalFun_pullback_of_isPurelyInseparable
open _root_.AlgebraicCurve
namespace Ws47
namespace EVPI
section PI
variable {F E : Type*} [Field F] [Field E] [Algebra F E] [FiniteDimensional F E]
  [IsPurelyInseparable F E]
Lean source · statement
theorem algebraMap_norm_eq_pow_finrank (x : E) :
    algebraMap F E (Algebra.norm F x) = x ^ Module.finrank F E
theorem

deg_eq_one_of_isRational

L78 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_evalFun_pullback_of_isPurelyInseparable.Ws47.EVPI.deg_eq_one_of_isRational
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_evalFun_pullback_of_isPurelyInseparable
open _root_.AlgebraicCurve
namespace Ws47
namespace EVPI
section Places
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F'] [Algebra F F']
  [IsScalarTower K F F'] [FiniteDimensional F F']
Lean source · statement
theorem deg_eq_one_of_isRational {L : Type*} [Field L] [Algebra K L] (v : Place K L) (hv :
  v.IsRational) : v.deg = 1
theorem

evalAt_restrict_eq

L84 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_evalFun_pullback_of_isPurelyInseparable.Ws47.EVPI.evalAt_restrict_eq
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_evalFun_pullback_of_isPurelyInseparable
open _root_.AlgebraicCurve
namespace Ws47
namespace EVPI
section Places
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F'] [Algebra F F']
  [IsScalarTower K F F'] [FiniteDimensional F F']
omit [FiniteDimensional F F'] in
Lean source · statement
theorem evalAt_restrict_eq [Algebra.IsIntegral F F'] (w : Place K F') (hv : (w.restrict
  F).IsRational) (hw : w.IsRational)
    {y : F} (hy : algebraMap F F' y ∈ w.toValuationSubring) :
    (w.restrict F).evalAt y = w.evalAt (algebraMap F F' y)
theorem

evalAt_pow

L96 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_evalFun_pullback_of_isPurelyInseparable.Ws47.EVPI.evalAt_pow
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_evalFun_pullback_of_isPurelyInseparable
open _root_.AlgebraicCurve
namespace Ws47
namespace EVPI
section Places
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F'] [Algebra F F']
  [IsScalarTower K F F'] [FiniteDimensional F F']
omit [Algebra F F'] [IsScalarTower K F F'] [FiniteDimensional F F'] in
Lean source · statement
theorem evalAt_pow (w : Place K F') (hw : w.IsRational) {f : F'} (hf : f ∈ w.toValuationSubring) (n
  : ℕ) :
    w.evalAt (f ^ n) = w.evalAt f ^ n
theorem

restrict_injective

L105 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_evalFun_pullback_of_isPurelyInseparable.Ws47.EVPI.restrict_injective
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_evalFun_pullback_of_isPurelyInseparable
open _root_.AlgebraicCurve
namespace Ws47
namespace EVPI
section Places
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F'] [Algebra F F']
  [IsScalarTower K F F'] [FiniteDimensional F F']
variable [IsPurelyInseparable F F']
Lean source · full declaration
theorem restrict_injective : Function.Injective fun w : Place K F' => w.restrict F := by
  intro w₁ w₂ h
  simp only at h
  have key : ∀ (w : Place K F') (x : F'), x ∈ w.toValuationSubring ↔
      ∃ y : F, algebraMap F F' y = x ^ Module.finrank F F' ∧ y ∈ (w.restrict F).toValuationSubring
        := by
    intro w x
    obtain ⟨y, hy⟩ := exists_algebraMap_eq_pow_finrank (F := F) x
    have hn : 0 < Module.finrank F F' := Module.finrank_pos
    constructor
    · intro hx
      exact ⟨y, hy, show algebraMap F F' y ∈ w.toValuationSubring from hy ▸ pow_mem hx _⟩
    · rintro ⟨y', hy', hmem⟩
      have hxn : x ^ Module.finrank F F' ∈ w.toValuationSubring := hy' ▸ (show algebraMap F F' y' ∈
        w.toValuationSubring from hmem)
      rcases eq_or_ne x 0 with rfl | hx0
      · exact zero_mem _
      · rw [w.mem_iff_ord_nonneg hx0]
        have h2 := (w.mem_iff_ord_nonneg (pow_ne_zero _ hx0)).mp hxn
        rw [← zpow_natCast, w.ord_zpow] at h2
        exact nonneg_of_mul_nonneg_right
          (a := (Module.finrank F F' : ℤ)) (b := w.ord x) h2 (by exact_mod_cast hn)
  ext x
  rw [key w₁ x, key w₂ x, h]
theorem

evalFun_pullback_of_isPurelyInseparable

L135 ↗
AlgebraicCurve.Divisor.evalFun_pullback_of_isPurelyInseparable
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_evalFun_pullback_of_isPurelyInseparable
open _root_.AlgebraicCurve
open Ws47.EVPI in
Lean source · statement
theorem _root_.AlgebraicCurve.Divisor.evalFun_pullback_of_isPurelyInseparable {K F F' : Type*}
  [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [IsPurelyInseparable F F'] [HasPrincipalDivisors K F']
  [FundamentalIdentity K F F'] {f : F'} (hf : f ≠ 0) (E : Divisor K F) (hrat : ∀ v ∈ E.support,
  Place.IsRational v) (hratw : ∀ v ∈ E.support, ∀ w ∈ v.fiber F', Place.IsRational w) (hord : ∀ v ∈
  E.support, ∀ w ∈ v.fiber F', w.ord f = 0) : Divisor.evalFun f (Divisor.pullback F' E) =
  Divisor.evalFun (Algebra.norm F f) E

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.