Module

OrdDifferential_map_eq.lean

Nyll.AlgebraicCurves.Differentials.OrdDifferential_map_eq

84 declarations indexed from sourceView source ↗

Module documentation

Ord Differential map eq

Imports7

Imported by2

theorem

ord_nonneg_of_mem

L37 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.Place.ord_nonneg_of_mem

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

Lean source · statement

theorem ord_nonneg_of_mem {f : F} (hf : f ∈ v.toValuationSubring) : 0 ≤ v.ord f

theorem

mem_of_ord_nonneg

L51 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.Place.mem_of_ord_nonneg

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

Lean source · statement

theorem mem_of_ord_nonneg {f : F} (hf : f ≠ 0) (h : 0 ≤ v.ord f) :
    f ∈ v.toValuationSubring

theorem

mem_iff_ord_nonneg

L58 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.Place.mem_iff_ord_nonneg

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

Lean source · statement

theorem mem_iff_ord_nonneg {f : F} (hf : f ≠ 0) :
    f ∈ v.toValuationSubring ↔ 0 ≤ v.ord f

instance

instSumRamificationInertia_port

L69 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.instSumRamificationInertia_port

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg

Lean source · statement

instance instSumRamificationInertia_port {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'] [Algebra.IsSeparable F F']
    [HasPrincipalDivisors K F'] : SumRamificationInertia K F F'

def

CanonicalDifferentDegree

L87 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.CanonicalDifferentDegree

Documentation

The condition that the difference of canonical divisors has the specified degree.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K F']
variable (K F F') in

Lean source · statement

def CanonicalDifferentDegree (d : ℚ) : Prop

theorem

degree_canonicalDivisor_relation_of_canonicalDifferentDegree

L93 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.degree_canonicalDivisor_relation_of_canonicalDifferentDegree

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K F']
variable (K F F') in

Lean source · statement

theorem degree_canonicalDivisor_relation_of_canonicalDifferentDegree
    [FundamentalIdentity K F F']
    [HasCanonicalDivisor (K := K) (F := F)] [HasCanonicalDivisor (K := K) (F := F')]
    {d : ℚ} (h : CanonicalDifferentDegree K F F' d)
    {ω : Ω[F⁄K]} (hω : ω ≠ 0) {ω' : Ω[F'⁄K]} (hω' : ω' ≠ 0) :
    (Divisor.degree (canonicalDivisorOf (K := K) hω') : ℚ)
      = (Module.finrank F F' : ℚ)
          * (Divisor.degree (canonicalDivisorOf (K := K) hω) : ℚ) + d

theorem

canonicalDifferentDegree_of_degree_canonicalDivisor_relation

L106 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.canonicalDifferentDegree_of_degree_canonicalDivisor_relation

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K F']
variable (K F F') in

Lean source · statement

theorem canonicalDifferentDegree_of_degree_canonicalDivisor_relation
    [FundamentalIdentity K F F'] {d : ℚ}
    (h : ∀ [HasCanonicalDivisor (K := K) (F := F)] [HasCanonicalDivisor (K := K) (F := F')]
      {ω : Ω[F⁄K]} (_ : ω ≠ 0) {ω' : Ω[F'⁄K]} (_ : ω' ≠ 0),
        (Divisor.degree (canonicalDivisorOf (K := K) ‹ω' ≠ 0›) : ℚ)
          = (Module.finrank F F' : ℚ)
              * (Divisor.degree (canonicalDivisorOf (K := K) ‹ω ≠ 0›) : ℚ) + d) :
    CanonicalDifferentDegree K F F' d

theorem

canonicalDifferentDegree_iff_degreeRelation

L120 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.canonicalDifferentDegree_iff_degreeRelation

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K F']
variable (K F F') in

Lean source · statement

theorem canonicalDifferentDegree_iff_degreeRelation [FundamentalIdentity K F F'] {d : ℚ} :
    CanonicalDifferentDegree K F F' d
      ↔ ∀ [HasCanonicalDivisor (K := K) (F := F)] [HasCanonicalDivisor (K := K) (F := F')]
          {ω : Ω[F⁄K]} (_ : ω ≠ 0) {ω' : Ω[F'⁄K]} (_ : ω' ≠ 0),
            (Divisor.degree (canonicalDivisorOf (K := K) ‹ω' ≠ 0›) : ℚ)
              = (Module.finrank F F' : ℚ)
                  * (Divisor.degree (canonicalDivisorOf (K := K) ‹ω ≠ 0›) : ℚ) + d

theorem

canonicalDifferentDegree_unique

L131 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.canonicalDifferentDegree_unique

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K F']
variable (K F F') in

Lean source · statement

theorem canonicalDifferentDegree_unique {d d' : ℚ}
    [HasCanonicalDivisor (K := K) (F := F)] [HasCanonicalDivisor (K := K) (F := F')]
    {ω : Ω[F⁄K]} (hω : ω ≠ 0) {ω' : Ω[F'⁄K]} (hω' : ω' ≠ 0)
    (h : CanonicalDifferentDegree K F F' d) (h' : CanonicalDifferentDegree K F F' d') :
    d = d'

theorem

degree_eq_zero_of_isPrincipal'

L153 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.Divisor.degree_eq_zero_of_isPrincipal'

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace Divisor
open _root_.AlgebraicCurve.Divisor
open _root_.AlgebraicCurve.Divisor
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem degree_eq_zero_of_isPrincipal' [HasPrincipalDivisors K F] {D : Divisor K F}
    (hD : D.IsPrincipal) : Divisor.degree D = 0

def

HurwitzCanonicalDecomposition

L168 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.HurwitzCanonicalDecomposition

Documentation

The canonical-divisor difference agrees with the given divisor modulo a principal divisor.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K F']
variable (K F F') in

Lean source · statement

def HurwitzCanonicalDecomposition (𝔡 : Divisor K F') : Prop

theorem

canonicalDifferentDegree_of_hurwitzCanonicalDecomposition

L174 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.canonicalDifferentDegree_of_hurwitzCanonicalDecomposition

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K F']
variable (K F F') in

Lean source · statement

theorem canonicalDifferentDegree_of_hurwitzCanonicalDecomposition
    {𝔡 : Divisor K F'} (h : HurwitzCanonicalDecomposition K F F' 𝔡) :
    CanonicalDifferentDegree K F F' (Divisor.degree 𝔡 : ℚ)

theorem

canonicalDifferentDegree_of_hurwitz_of_degree_eq

L186 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.canonicalDifferentDegree_of_hurwitz_of_degree_eq

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K F']
variable (K F F') in

Lean source · statement

theorem canonicalDifferentDegree_of_hurwitz_of_degree_eq {𝔡 : Divisor K F'} {d : ℚ}
    (hH : HurwitzCanonicalDecomposition K F F' 𝔡) (hdeg : (Divisor.degree 𝔡 : ℚ) = d) :
    CanonicalDifferentDegree K F F' d

theorem

degree_eq_of_canonicalDifferentDegree_of_hurwitz

L191 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.degree_eq_of_canonicalDifferentDegree_of_hurwitz

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K F']
variable (K F F') in

Lean source · statement

theorem degree_eq_of_canonicalDifferentDegree_of_hurwitz
    [HasCanonicalDivisor (K := K) (F := F)] [HasCanonicalDivisor (K := K) (F := F')]
    {ω : Ω[F⁄K]} (hω : ω ≠ 0) {ω' : Ω[F'⁄K]} (hω' : ω' ≠ 0)
    {𝔡 : Divisor K F'} {d : ℚ}
    (hH : HurwitzCanonicalDecomposition K F F' 𝔡)
    (hCD : CanonicalDifferentDegree K F F' d) :
    (Divisor.degree 𝔡 : ℚ) = d

theorem

canonicalDifferentDegree_iff_degree_eq_of_hurwitz

L201 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.canonicalDifferentDegree_iff_degree_eq_of_hurwitz

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K F']
variable (K F F') in

Lean source · statement

theorem canonicalDifferentDegree_iff_degree_eq_of_hurwitz
    [HasCanonicalDivisor (K := K) (F := F)] [HasCanonicalDivisor (K := K) (F := F')]
    {ω : Ω[F⁄K]} (hω : ω ≠ 0) {ω' : Ω[F'⁄K]} (hω' : ω' ≠ 0)
    {𝔡 : Divisor K F'} (hH : HurwitzCanonicalDecomposition K F F' 𝔡) {d : ℚ} :
    CanonicalDifferentDegree K F F' d ↔ (Divisor.degree 𝔡 : ℚ) = d

theorem

degree_eq_of_hurwitzCanonicalDecomposition

L209 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.degree_eq_of_hurwitzCanonicalDecomposition

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K F']
variable (K F F') in

Lean source · statement

theorem degree_eq_of_hurwitzCanonicalDecomposition
    [HasCanonicalDivisor (K := K) (F := F)] [HasCanonicalDivisor (K := K) (F := F')]
    {ω : Ω[F⁄K]} (hω : ω ≠ 0) {ω' : Ω[F'⁄K]} (hω' : ω' ≠ 0)
    {𝔡₁ 𝔡₂ : Divisor K F'}
    (h₁ : HurwitzCanonicalDecomposition K F F' 𝔡₁)
    (h₂ : HurwitzCanonicalDecomposition K F F' 𝔡₂) :
    Divisor.degree 𝔡₁ = Divisor.degree 𝔡₂

theorem

degree_canonicalDivisor_relation_of_hurwitzCanonicalDecomposition

L221 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.degree_canonicalDivisor_relation_of_hurwitzCanonicalDecomposition

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K F']
variable (K F F') in

Lean source · statement

theorem degree_canonicalDivisor_relation_of_hurwitzCanonicalDecomposition
    [FundamentalIdentity K F F']
    [HasCanonicalDivisor (K := K) (F := F)] [HasCanonicalDivisor (K := K) (F := F')]
    {𝔡 : Divisor K F'} (h : HurwitzCanonicalDecomposition K F F' 𝔡)
    {ω : Ω[F⁄K]} (hω : ω ≠ 0) {ω' : Ω[F'⁄K]} (hω' : ω' ≠ 0) :
    (Divisor.degree (canonicalDivisorOf (K := K) hω') : ℚ)
      = (Module.finrank F F' : ℚ)
          * (Divisor.degree (canonicalDivisorOf (K := K) hω) : ℚ)
        + (Divisor.degree 𝔡 : ℚ)

def

tameDifferentDivisor

L247 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.tameDifferentDivisor

Documentation

The divisor with coefficients equal to the ramification indices minus one.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section TameDifferent
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F']
variable (K F) in

Lean source · statement

def tameDifferentDivisor (S : Finset (Place K F')) : Divisor K F'

theorem

tameDifferentDivisor_empty

L250 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.tameDifferentDivisor_empty

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section TameDifferent
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F']
variable (K F) in

Lean source · statement

theorem tameDifferentDivisor_empty :
    tameDifferentDivisor K F (∅ : Finset (Place K F')) = 0

theorem

degree_tameDifferentDivisor

L254 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.degree_tameDifferentDivisor

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section TameDifferent
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F']
variable (K F) in

Lean source · statement

theorem degree_tameDifferentDivisor (S : Finset (Place K F')) :
    Divisor.degree (tameDifferentDivisor K F S)
      = ∑ w ∈ S, ((w.ramificationIndex F : ℤ) - 1) * (w.deg : ℤ)

theorem

degree_tameDifferentDivisor_of_deg_eq_one

L261 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.degree_tameDifferentDivisor_of_deg_eq_one

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section TameDifferent
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F']
variable (K F) in

Lean source · statement

theorem degree_tameDifferentDivisor_of_deg_eq_one {S : Finset (Place K F')}
    (hdeg1 : ∀ w ∈ S, (w.deg : ℤ) = 1) :
    Divisor.degree (tameDifferentDivisor K F S)
      = ∑ w ∈ S, ((w.ramificationIndex F : ℤ) - 1)

theorem

tameDifferentDivisor_subset_unramified

L268 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.tameDifferentDivisor_subset_unramified

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section TameDifferent
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F']
variable (K F) in

Lean source · statement

theorem tameDifferentDivisor_subset_unramified {S T : Finset (Place K F')}
    (hST : S ⊆ T) (hunram : ∀ w ∈ T, w ∉ S → w.ramificationIndex F = 1) :
    tameDifferentDivisor K F T = tameDifferentDivisor K F S

theorem

tameDifferentDivisor_eq_of_unramified_compl

L274 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.tameDifferentDivisor_eq_of_unramified_compl

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section TameDifferent
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F']
variable (K F) in

Lean source · statement

theorem tameDifferentDivisor_eq_of_unramified_compl {S T : Finset (Place K F')}
    (hS : ∀ w : Place K F', w ∉ S → w.ramificationIndex F = 1)
    (hT : ∀ w : Place K F', w ∉ T → w.ramificationIndex F = 1) :
    tameDifferentDivisor K F S = tameDifferentDivisor K F T

theorem

degree_tameDifferentDivisor_disjUnion

L287 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.degree_tameDifferentDivisor_disjUnion

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section TameDifferent
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F']
variable (K F) in

Lean source · statement

theorem degree_tameDifferentDivisor_disjUnion {S T : Finset (Place K F')}
    (hdisj : Disjoint S T) :
    Divisor.degree (tameDifferentDivisor K F (S.disjUnion T hdisj))
      = Divisor.degree (tameDifferentDivisor K F S)
        + Divisor.degree (tameDifferentDivisor K F T)

theorem

hurwitzDifferentAssembly_of_tameDifferent

L301 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.hurwitzDifferentAssembly_of_tameDifferent

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K F']

Lean source · statement

theorem hurwitzDifferentAssembly_of_tameDifferent {S : Finset (Place K F')} {d : ℚ}
    (hH : HurwitzCanonicalDecomposition K F F' (tameDifferentDivisor K F S))
    (hsum : ((∑ w ∈ S, ((w.ramificationIndex F : ℤ) - 1) * (w.deg : ℤ) : ℤ) : ℚ) = d) :
    ∃ 𝔡 : Divisor K F',
      HurwitzCanonicalDecomposition K F F' 𝔡 ∧ (Divisor.degree 𝔡 : ℚ) = d

theorem

canonicalDifferentDegree_of_tameDifferent

L308 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.canonicalDifferentDegree_of_tameDifferent

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K F']

Lean source · statement

theorem canonicalDifferentDegree_of_tameDifferent {S : Finset (Place K F')} {d : ℚ}
    (hH : HurwitzCanonicalDecomposition K F F' (tameDifferentDivisor K F S))
    (hsum : ((∑ w ∈ S, ((w.ramificationIndex F : ℤ) - 1) * (w.deg : ℤ) : ℤ) : ℚ) = d) :
    CanonicalDifferentDegree K F F' d

theorem

sum_eq_of_canonicalDifferentDegree_of_tameDifferentHurwitz

L315 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.sum_eq_of_canonicalDifferentDegree_of_tameDifferentHurwitz

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K F']

Lean source · statement

theorem sum_eq_of_canonicalDifferentDegree_of_tameDifferentHurwitz
    [HasCanonicalDivisor (K := K) (F := F)] [HasCanonicalDivisor (K := K) (F := F')]
    {ω : Ω[F⁄K]} (hω : ω ≠ 0) {ω' : Ω[F'⁄K]} (hω' : ω' ≠ 0)
    {S : Finset (Place K F')} {d : ℚ}
    (hH : HurwitzCanonicalDecomposition K F F' (tameDifferentDivisor K F S))
    (hCD : CanonicalDifferentDegree K F F' d) :
    ((∑ w ∈ S, ((w.ramificationIndex F : ℤ) - 1) * (w.deg : ℤ) : ℤ) : ℚ) = d

theorem

sum_eq_of_hurwitz_tameDifferent

L325 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.sum_eq_of_hurwitz_tameDifferent

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K F']

Lean source · statement

theorem sum_eq_of_hurwitz_tameDifferent
    [HasCanonicalDivisor (K := K) (F := F)] [HasCanonicalDivisor (K := K) (F := F')]
    {ω : Ω[F⁄K]} (hω : ω ≠ 0) {ω' : Ω[F'⁄K]} (hω' : ω' ≠ 0)
    {S₁ S₂ : Finset (Place K F')}
    (h₁ : HurwitzCanonicalDecomposition K F F' (tameDifferentDivisor K F S₁))
    (h₂ : HurwitzCanonicalDecomposition K F F' (tameDifferentDivisor K F S₂)) :
    ∑ w ∈ S₁, ((w.ramificationIndex F : ℤ) - 1) * (w.deg : ℤ)
      = ∑ w ∈ S₂, ((w.ramificationIndex F : ℤ) - 1) * (w.deg : ℤ)

theorem

tameDifferentDivisor_apply_of_mem

L348 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.tameDifferentDivisor_apply_of_mem

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section TameApply
variable (K : Type*) {F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F']

Lean source · statement

theorem tameDifferentDivisor_apply_of_mem {S : Finset (Place K F')} {w : Place K F'}
    (hw : w ∈ S) :
    (tameDifferentDivisor K F S) w = (w.ramificationIndex F : ℤ) - 1

theorem

tameDifferentDivisor_apply_of_notMem

L356 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.tameDifferentDivisor_apply_of_notMem

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section TameApply
variable (K : Type*) {F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F']

Lean source · statement

theorem tameDifferentDivisor_apply_of_notMem {S : Finset (Place K F')} {w : Place K F'}
    (hw : w ∉ S) :
    (tameDifferentDivisor K F S) w = 0

def

LocalHurwitzExponent

L372 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.LocalHurwitzExponent

Documentation

The local differential-order relation with the specified different divisor.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section LocalExponent
variable (K F F' : Type*) [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K F']

Lean source · statement

def LocalHurwitzExponent (ω₀ : Ω[F⁄K]) (ω₀' : Ω[F'⁄K]) (𝔡 : Divisor K F') : Prop

theorem

canonicalDivisorOf_eq_of_localHurwitzExponent

L379 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.canonicalDivisorOf_eq_of_localHurwitzExponent

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section LocalExponent
variable (K F F' : Type*) [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K F']
variable {K F F'}

Lean source · statement

theorem canonicalDivisorOf_eq_of_localHurwitzExponent
    [HasCanonicalDivisor (K := K) (F := F)] [HasCanonicalDivisor (K := K) (F := F')]
    {ω₀ : Ω[F⁄K]} (hω₀ : ω₀ ≠ 0) {ω₀' : Ω[F'⁄K]} (hω₀' : ω₀' ≠ 0)
    {𝔡 : Divisor K F'} (hL : LocalHurwitzExponent K F F' ω₀ ω₀' 𝔡) :
    canonicalDivisorOf (K := K) hω₀'
      = Divisor.pullback F' (canonicalDivisorOf (K := K) hω₀) + 𝔡

theorem

localHurwitzExponent_of_canonicalDivisorOf_eq

L389 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.localHurwitzExponent_of_canonicalDivisorOf_eq

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section LocalExponent
variable (K F F' : Type*) [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K F']
variable {K F F'}

Lean source · statement

theorem localHurwitzExponent_of_canonicalDivisorOf_eq
    [HasCanonicalDivisor (K := K) (F := F)] [HasCanonicalDivisor (K := K) (F := F')]
    {ω₀ : Ω[F⁄K]} (hω₀ : ω₀ ≠ 0) {ω₀' : Ω[F'⁄K]} (hω₀' : ω₀' ≠ 0)
    {𝔡 : Divisor K F'}
    (hexact : canonicalDivisorOf (K := K) hω₀'
      = Divisor.pullback F' (canonicalDivisorOf (K := K) hω₀) + 𝔡) :
    LocalHurwitzExponent K F F' ω₀ ω₀' 𝔡

def

CanonicalDivisorVariationPrincipal

L407 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.CanonicalDivisorVariationPrincipal

Documentation

Any two canonical divisors differ by a principal divisor.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section VariationPrincipal
variable (K F : Type*) [Field K] [Field F] [Algebra K F]

Lean source · statement

def CanonicalDivisorVariationPrincipal : Prop

theorem

hurwitzCanonicalDecomposition_of_localHurwitzExponent

L421 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.hurwitzCanonicalDecomposition_of_localHurwitzExponent

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section CoreEngine
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K F']

Lean source · statement

theorem hurwitzCanonicalDecomposition_of_localHurwitzExponent
    {ω₀ : Ω[F⁄K]} (hω₀ : ω₀ ≠ 0) {ω₀' : Ω[F'⁄K]} (hω₀' : ω₀' ≠ 0)
    {𝔡 : Divisor K F'} (hL : LocalHurwitzExponent K F F' ω₀ ω₀' 𝔡)
    (hVF : CanonicalDivisorVariationPrincipal K F)
    (hVF' : CanonicalDivisorVariationPrincipal K F') :
    HurwitzCanonicalDecomposition K F F' 𝔡

theorem

canonicalDivisorVariationPrincipal_cover_of_hurwitzCanonicalDecomposition

L439 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.canonicalDivisorVariationPrincipal_cover_of_hurwitzCanonicalDecomposition

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section CoreEngine
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K F']

Lean source · statement

theorem canonicalDivisorVariationPrincipal_cover_of_hurwitzCanonicalDecomposition
    [HasCanonicalDivisor (K := K) (F := F)] [HasCanonicalDivisor (K := K) (F := F')]
    {ω₀ : Ω[F⁄K]} (hω₀ : ω₀ ≠ 0)
    {𝔡 : Divisor K F'}
    (hH : HurwitzCanonicalDecomposition K F F' 𝔡)
    {ω₁' : Ω[F'⁄K]} (hω₁' : ω₁' ≠ 0) {ω₂' : Ω[F'⁄K]} (hω₂' : ω₂' ≠ 0) :
    (canonicalDivisorOf (K := K) hω₁' - canonicalDivisorOf (K := K) hω₂').IsPrincipal

theorem

localHurwitzExponent_tameDifferent_iff

L463 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.localHurwitzExponent_tameDifferent_iff

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section TameSpecialization
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']

Lean source · statement

theorem localHurwitzExponent_tameDifferent_iff {ω₀ : Ω[F⁄K]} {ω₀' : Ω[F'⁄K]}
    {S : Finset (Place K F')} :
    LocalHurwitzExponent K F F' ω₀ ω₀' (tameDifferentDivisor K F S)
      ↔ (∀ w ∈ S, w.ordDifferential ω₀'
            = (w.ramificationIndex F : ℤ) * (w.restrict F).ordDifferential ω₀
              + ((w.ramificationIndex F : ℤ) - 1))
        ∧ (∀ w ∉ S, w.ordDifferential ω₀'
            = (w.ramificationIndex F : ℤ) * (w.restrict F).ordDifferential ω₀)

theorem

localHurwitzExponent_tameDifferent_of_universal

L481 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.localHurwitzExponent_tameDifferent_of_universal

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section TameSpecialization
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']

Lean source · statement

theorem localHurwitzExponent_tameDifferent_of_universal {ω₀ : Ω[F⁄K]} {ω₀' : Ω[F'⁄K]}
    {S : Finset (Place K F')}
    (hram : ∀ w : Place K F', w ∉ S → w.ramificationIndex F = 1)
    (huniv : ∀ w : Place K F', w.ordDifferential ω₀'
        = (w.ramificationIndex F : ℤ) * (w.restrict F).ordDifferential ω₀
          + ((w.ramificationIndex F : ℤ) - 1)) :
    LocalHurwitzExponent K F F' ω₀ ω₀' (tameDifferentDivisor K F S)

theorem

differentialCoeff_ne_zero'

L527 ↗

AlgebraicCurve.Place.differentialCoeff_ne_zero'

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section RankOne
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
open scoped _root_.AlgebraicCurve.Place in

Lean source · statement

theorem _root_.AlgebraicCurve.Place.differentialCoeff_ne_zero' (v : Place K F)
  [v.DCoordGenerates]
    [Nontrivial Ω[F⁄K]] {ω : Ω[F⁄K]} (hω : ω ≠ 0) :
    v.differentialCoeff ω ≠ 0

theorem

exists_smul_eq

L542 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.IsCurveOver.exists_smul_eq

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section RankOne
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve
open scoped _root_.AlgebraicCurve.IsCurveOver in

Lean source · statement

theorem IsCurveOver.exists_smul_eq [IsCurveOver K F]
    {ω₁ : Ω[F⁄K]} (hω₁ : ω₁ ≠ 0) {ω₂ : Ω[F⁄K]} (hω₂ : ω₂ ≠ 0) :
    ∃ c : F, c ≠ 0 ∧ ω₂ = c • ω₁

theorem

ordDifferential_smul_sub

L551 ↗

AlgebraicCurve.Place.ordDifferential_smul_sub

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section RankOne
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve
namespace Place
open scoped _root_.AlgebraicCurve.Place in

Lean source · statement

theorem _root_.AlgebraicCurve.Place.ordDifferential_smul_sub (v : Place K F)
  [v.DCoordGenerates]
    [Nontrivial Ω[F⁄K]] {c : F} (hc : c ≠ 0) {ω : Ω[F⁄K]} (hω : ω ≠ 0) :
    v.ordDifferential (c • ω) - v.ordDifferential ω = v.ord c

theorem

canonicalDivisorOf_smul_sub_isPrincipal

L565 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.canonicalDivisorOf_smul_sub_isPrincipal

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section VariationDischarge
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · full declaration

theorem canonicalDivisorOf_smul_sub_isPrincipal
    [HasCanonicalDivisor (K := K) (F := F)]
    [∀ v : Place K F, v.DCoordGenerates] [Nontrivial Ω[F⁄K]]
    {c : F} (hc : c ≠ 0) {ω : Ω[F⁄K]} (hω : ω ≠ 0) :
    (canonicalDivisorOf (K := K) (show c • ω ≠ 0 from smul_ne_zero hc hω)
      - canonicalDivisorOf (K := K) hω).IsPrincipal :=
  ⟨c, hc, fun v => by
    rw [Finsupp.sub_apply, canonicalDivisorOf_apply, canonicalDivisorOf_apply,
      v.ordDifferential_smul_sub hc hω]⟩

theorem

canonicalDivisorVariationPrincipal_of_isCurveOver

L575 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.canonicalDivisorVariationPrincipal_of_isCurveOver

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section VariationDischarge
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem canonicalDivisorVariationPrincipal_of_isCurveOver
    [IsCurveOver K F] [∀ v : Place K F, v.DCoordGenerates] :
    CanonicalDivisorVariationPrincipal K F

theorem

hurwitzCanonicalDecomposition_of_localHurwitzExponent_of_isCurveOver

L590 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.hurwitzCanonicalDecomposition_of_localHurwitzExponent_of_isCurveOver

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section VFreeEngine
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']

Lean source · statement

theorem hurwitzCanonicalDecomposition_of_localHurwitzExponent_of_isCurveOver
    [IsCurveOver K F] [∀ v : Place K F, v.DCoordGenerates]
    [IsCurveOver K F'] [∀ w : Place K F', w.DCoordGenerates]
    {ω₀ : Ω[F⁄K]} (hω₀ : ω₀ ≠ 0) {ω₀' : Ω[F'⁄K]} (hω₀' : ω₀' ≠ 0)
    {𝔡 : Divisor K F'} (hL : LocalHurwitzExponent K F F' ω₀ ω₀' 𝔡) :
    HurwitzCanonicalDecomposition K F F' 𝔡

abbrev

kaehlerMap

L615 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.kaehlerMap

Documentation

The linear map on Kähler differentials induced by the function-field extension.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section KaehlerMap
variable (K F F' : Type*) [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']

Lean source · statement

abbrev kaehlerMap : Ω[F⁄K] →ₗ[F] Ω[F'⁄K]

theorem

kaehlerMap_dCoord

L620 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.kaehlerMap_dCoord

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section KaehlerMap
variable (K F F' : Type*) [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
variable {K F F'}

Lean source · statement

theorem kaehlerMap_dCoord (v : Place K F) :
    kaehlerMap K F F' v.dCoord
      = KaehlerDifferential.D K F' (algebraMap F F' v.uniformizer)

theorem

kaehlerMap_eq_smul_dCoordImage

L625 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.kaehlerMap_eq_smul_dCoordImage

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section KaehlerMap
variable (K F F' : Type*) [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
variable {K F F'}

Lean source · statement

theorem kaehlerMap_eq_smul_dCoordImage (v : Place K F) [v.DCoordGenerates] (ω : Ω[F⁄K]) :
    kaehlerMap K F F' ω
      = (algebraMap F F' (v.differentialCoeff ω))
          • KaehlerDifferential.D K F' (algebraMap F F' v.uniformizer)

def

restrictDCoord

L643 ↗

AlgebraicCurve.Place.restrictDCoord

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section RestrictDCoord
variable {K : Type*} (F : Type*) {F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']
namespace Place
open scoped _root_.AlgebraicCurve.Place in

Lean source · statement

def _root_.AlgebraicCurve.Place.restrictDCoord (w : Place K F') : Ω[F'⁄K]

theorem

restrictDCoord_eq_kaehlerMap

L649 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.Place.restrictDCoord_eq_kaehlerMap

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section RestrictDCoord
variable {K : Type*} (F : Type*) {F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']
open _root_.AlgebraicCurve
open scoped _root_.AlgebraicCurve.Place in

Lean source · statement

theorem Place.restrictDCoord_eq_kaehlerMap (w : Place K F') :
    w.restrictDCoord F = kaehlerMap K F F' (w.restrict F).dCoord

def

TameLocalDifferentExponent

L656 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.TameLocalDifferentExponent

Documentation

The nonvanishing and valuation formula for the local differential coefficient.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section RestrictDCoord
variable {K : Type*} (F : Type*) {F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']
open _root_.AlgebraicCurve
variable (K F')

Lean source · statement

def TameLocalDifferentExponent : Prop

theorem

differentialCoeff_kaehlerMap_eq

L669 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.differentialCoeff_kaehlerMap_eq

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section LFromTame
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']

Lean source · statement

theorem differentialCoeff_kaehlerMap_eq (w : Place K F') [w.DCoordGenerates]
    [(w.restrict F).DCoordGenerates] [Nontrivial Ω[F'⁄K]] (ω₀ : Ω[F⁄K]) :
    w.differentialCoeff (kaehlerMap K F F' ω₀)
      = algebraMap F F' ((w.restrict F).differentialCoeff ω₀)
          * w.differentialCoeff (w.restrictDCoord F)

theorem

ordDifferential_kaehlerMap_eq

L677 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.ordDifferential_kaehlerMap_eq

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section LFromTame
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']

Lean source · statement

theorem ordDifferential_kaehlerMap_eq (w : Place K F') [w.DCoordGenerates]
    [(w.restrict F).DCoordGenerates] [Nontrivial Ω[F⁄K]] [Nontrivial Ω[F'⁄K]]
    {ω₀ : Ω[F⁄K]} (hω₀ : ω₀ ≠ 0)
    (htame : w.differentialCoeff (w.restrictDCoord F) ≠ 0) :
    w.ordDifferential (kaehlerMap K F F' ω₀)
      = (w.ramificationIndex F : ℤ) * (w.restrict F).ordDifferential ω₀
          + w.ord (w.differentialCoeff (w.restrictDCoord F))

theorem

kaehlerMap_ne_zero_of_tameAt

L692 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.kaehlerMap_ne_zero_of_tameAt

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section LFromTame
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']

Lean source · statement

theorem kaehlerMap_ne_zero_of_tameAt [Nontrivial Ω[F⁄K]] [Nontrivial Ω[F'⁄K]]
    (w : Place K F') [w.DCoordGenerates] [(w.restrict F).DCoordGenerates]
    {ω₀ : Ω[F⁄K]} (hω₀ : ω₀ ≠ 0)
    (htame : w.differentialCoeff (w.restrictDCoord F) ≠ 0) :
    kaehlerMap K F F' ω₀ ≠ 0

theorem

ordDifferential_kaehlerMap_universal

L707 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.ordDifferential_kaehlerMap_universal

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section LFromTame
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']

Lean source · statement

theorem ordDifferential_kaehlerMap_universal
    [IsCurveOver K F] [∀ v : Place K F, v.DCoordGenerates]
    [IsCurveOver K F'] [∀ w : Place K F', w.DCoordGenerates]
    (htame : TameLocalDifferentExponent K F F')
    {ω₀ : Ω[F⁄K]} (hω₀ : ω₀ ≠ 0) (w : Place K F') :
    w.ordDifferential (kaehlerMap K F F' ω₀)
      = (w.ramificationIndex F : ℤ) * (w.restrict F).ordDifferential ω₀
          + ((w.ramificationIndex F : ℤ) - 1)

theorem

localHurwitzExponent_kaehlerMap_of_tameLocalDifferent

L717 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.localHurwitzExponent_kaehlerMap_of_tameLocalDifferent

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section LFromTame
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']

Lean source · statement

theorem localHurwitzExponent_kaehlerMap_of_tameLocalDifferent
    [IsCurveOver K F] [∀ v : Place K F, v.DCoordGenerates]
    [IsCurveOver K F'] [∀ w : Place K F', w.DCoordGenerates]
    (htame : TameLocalDifferentExponent K F F')
    {ω₀ : Ω[F⁄K]} (hω₀ : ω₀ ≠ 0)
    {S : Finset (Place K F')} (hram : ∀ w : Place K F', w ∉ S → w.ramificationIndex F = 1) :
    LocalHurwitzExponent K F F' ω₀ (kaehlerMap K F F' ω₀) (tameDifferentDivisor K F S)

theorem

kaehlerMap_ne_zero_of_tameLocalDifferent

L727 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.kaehlerMap_ne_zero_of_tameLocalDifferent

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section LFromTame
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']

Lean source · statement

theorem kaehlerMap_ne_zero_of_tameLocalDifferent
    [IsCurveOver K F] [∀ v : Place K F, v.DCoordGenerates]
    [IsCurveOver K F'] [∀ w : Place K F', w.DCoordGenerates]
    (htame : TameLocalDifferentExponent K F F') (w₀ : Place K F')
    {ω₀ : Ω[F⁄K]} (hω₀ : ω₀ ≠ 0) :
    kaehlerMap K F F' ω₀ ≠ 0

theorem

hurwitzCanonicalDecomposition_of_tameLocalDifferent

L743 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.hurwitzCanonicalDecomposition_of_tameLocalDifferent

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section HurwitzFromTame
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']

Lean source · statement

theorem hurwitzCanonicalDecomposition_of_tameLocalDifferent
    [IsCurveOver K F] [∀ v : Place K F, v.DCoordGenerates]
    [IsCurveOver K F'] [∀ w : Place K F', w.DCoordGenerates]
    (htame : TameLocalDifferentExponent K F F') (w₀ : Place K F')
    {S : Finset (Place K F')} (hram : ∀ w : Place K F', w ∉ S → w.ramificationIndex F = 1) :
    HurwitzCanonicalDecomposition K F F' (tameDifferentDivisor K F S)

theorem

ord_algebraMap'

L789 ↗

AlgebraicCurve.Place.ord_algebraMap'

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
open IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg mem_iff_ord_nonneg
section Helpers
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

Lean source · statement

theorem _root_.AlgebraicCurve.Place.ord_algebraMap' (c : K) : v.ord (algebraMap K F c) = 0

theorem

ord_natCast'

L800 ↗

AlgebraicCurve.Place.ord_natCast'

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
open IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg mem_iff_ord_nonneg
section Helpers
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place

Lean source · statement

theorem _root_.AlgebraicCurve.Place.ord_natCast' (n : ℕ) : v.ord (n : F) = 0

theorem

ord_pow'

L805 ↗

AlgebraicCurve.Place.ord_pow'

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
open IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg mem_iff_ord_nonneg
section Helpers
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place

Lean source · statement

theorem _root_.AlgebraicCurve.Place.ord_pow' (f : F) (n : ℕ) : v.ord (f ^ n) = n * v.ord f

theorem

ord_neg'

L811 ↗

AlgebraicCurve.Place.ord_neg'

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
open IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg mem_iff_ord_nonneg
section Helpers
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place

Lean source · statement

theorem _root_.AlgebraicCurve.Place.ord_neg' (f : F) : v.ord (-f) = v.ord f

theorem

ord_add_eq_min'

L824 ↗

AlgebraicCurve.Place.ord_add_eq_min'

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
open IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg mem_iff_ord_nonneg
section Helpers
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place

Lean source · statement

theorem _root_.AlgebraicCurve.Place.ord_add_eq_min' {f g : F} (hf : f ≠ 0) (hg : g ≠ 0)
    (h : v.ord f ≠ v.ord g) : v.ord (f + g) = min (v.ord f) (v.ord g)

theorem

differentialCoeff_add'

L847 ↗

AlgebraicCurve.Place.differentialCoeff_add'

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
open IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg mem_iff_ord_nonneg
section Helpers
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place

Lean source · statement

theorem _root_.AlgebraicCurve.Place.differentialCoeff_add' [v.DCoordGenerates] [Nontrivial
  Ω[F⁄K]]
    (ω₁ ω₂ : Ω[F⁄K]) :
    v.differentialCoeff (ω₁ + ω₂) = v.differentialCoeff ω₁ + v.differentialCoeff ω₂

theorem

exists_ord_eq_zero_mul_uniformizer_zpow

L856 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.Place.exists_ord_eq_zero_mul_uniformizer_zpow

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
open IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg mem_iff_ord_nonneg
section Helpers
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place

Lean source · statement

theorem exists_ord_eq_zero_mul_uniformizer_zpow {f : F} (hf : f ≠ 0) :
    ∃ u : F, u ≠ 0 ∧ v.ord u = 0 ∧ f = u * v.uniformizer ^ (v.ord f)

theorem

differentialCoeff_D_uniformizer_pow

L872 ↗

AlgebraicCurve.Place.differentialCoeff_D_uniformizer_pow

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
open IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg mem_iff_ord_nonneg
section PowerRule
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
  (v : Place K F) [v.DCoordGenerates] [Nontrivial Ω[F⁄K]]

Lean source · statement

theorem _root_.AlgebraicCurve.Place.differentialCoeff_D_uniformizer_pow (n : ℕ) :
    v.differentialCoeff (KaehlerDifferential.D K F (v.uniformizer ^ n))
      = (n : F) * v.uniformizer ^ (n - 1)

theorem

ord_differentialCoeff_D_uniformizer_pow

L882 ↗

AlgebraicCurve.Place.ord_differentialCoeff_D_uniformizer_pow

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
open IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg mem_iff_ord_nonneg
section PowerRule
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
  (v : Place K F) [v.DCoordGenerates] [Nontrivial Ω[F⁄K]]
open _root_.AlgebraicCurve.Place

Lean source · statement

theorem _root_.AlgebraicCurve.Place.ord_differentialCoeff_D_uniformizer_pow {n : ℕ} (hn :
  (n : F) ≠ 0) :
    v.ord (v.differentialCoeff (KaehlerDifferential.D K F (v.uniformizer ^ n)))
      = (n : ℤ) - 1

theorem

differentialCoeff_D_uniformizer_pow_ne_zero

L894 ↗

AlgebraicCurve.Place.differentialCoeff_D_uniformizer_pow_ne_zero

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
open IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg mem_iff_ord_nonneg
section PowerRule
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
  (v : Place K F) [v.DCoordGenerates] [Nontrivial Ω[F⁄K]]
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place

Lean source · statement

theorem _root_.AlgebraicCurve.Place.differentialCoeff_D_uniformizer_pow_ne_zero {n : ℕ} (hn
  : (n : F) ≠ 0) :
    v.differentialCoeff (KaehlerDifferential.D K F (v.uniformizer ^ n)) ≠ 0

theorem

differentialCoeff_D_mul

L908 ↗

AlgebraicCurve.Place.differentialCoeff_D_mul

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
open IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg mem_iff_ord_nonneg
section LeibnizDecomp
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
  (v : Place K F) [v.DCoordGenerates] [Nontrivial Ω[F⁄K]]

Lean source · statement

theorem _root_.AlgebraicCurve.Place.differentialCoeff_D_mul (a b : F) :
    v.differentialCoeff (KaehlerDifferential.D K F (a * b))
      = a * v.differentialCoeff (KaehlerDifferential.D K F b)
        + b * v.differentialCoeff (KaehlerDifferential.D K F a)

theorem

ord_differentialCoeff_D_of_unit_mul_uniformizer_pow

L917 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.Place.ord_differentialCoeff_D_of_unit_mul_uniformizer_pow

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
open IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg mem_iff_ord_nonneg
section LeibnizDecomp
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
  (v : Place K F) [v.DCoordGenerates] [Nontrivial Ω[F⁄K]]
open _root_.AlgebraicCurve.Place

Lean source · statement

theorem ord_differentialCoeff_D_of_unit_mul_uniformizer_pow {u : F} (hune : u ≠ 0)
    (hu : v.ord u = 0) {n : ℕ} (hn : (n : F) ≠ 0)
    (hreg : v.differentialCoeff (KaehlerDifferential.D K F u) = 0
        ∨ 0 ≤ v.ord (v.differentialCoeff (KaehlerDifferential.D K F u))) :
    v.differentialCoeff (KaehlerDifferential.D K F (u * v.uniformizer ^ n)) ≠ 0
    ∧ v.ord (v.differentialCoeff (KaehlerDifferential.D K F (u * v.uniformizer ^ n)))
        = (n : ℤ) - 1

def

LocalUnitDerivativeRegular

L966 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.LocalUnitDerivativeRegular

Documentation

The differential coefficient of a nonzero local unit is zero or has nonnegative order.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
open IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section Discharge
variable (K F : Type*) [Field K] [Field F] [Algebra K F]

Lean source · statement

def LocalUnitDerivativeRegular : Prop

theorem

ord_differentialCoeff_D_of_ord_eq

L975 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.ord_differentialCoeff_D_of_ord_eq

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
open IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section Discharge
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable {K F}
variable {F' : Type*} [Field F'] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']

Lean source · statement

theorem ord_differentialCoeff_D_of_ord_eq (w : Place K F') [w.DCoordGenerates]
    [Nontrivial Ω[F'⁄K]] (hreg : LocalUnitDerivativeRegular K F')
    {f : F'} (hf : f ≠ 0) {n : ℕ} (hn : (n : F') ≠ 0)
    (hord : w.ord f = (n : ℤ)) :
    w.differentialCoeff (KaehlerDifferential.D K F' f) ≠ 0
    ∧ w.ord (w.differentialCoeff (KaehlerDifferential.D K F' f)) = (n : ℤ) - 1

theorem

tameLocalDifferentExponent_of_localUnitDerivativeRegular

L989 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.tameLocalDifferentExponent_of_localUnitDerivativeRegular

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
open IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section Discharge
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable {K F}
variable {F' : Type*} [Field F'] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']

Lean source · statement

theorem tameLocalDifferentExponent_of_localUnitDerivativeRegular
    [∀ w : Place K F', w.DCoordGenerates] [Nontrivial Ω[F'⁄K]]
    (hreg : LocalUnitDerivativeRegular K F')
    (htame : ∀ w : Place K F', ((w.ramificationIndex F : ℕ) : F') ≠ 0) :
    TameLocalDifferentExponent K F F'

theorem

ramificationIndex_cast_ne_zero_of_charZero

L1004 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.ramificationIndex_cast_ne_zero_of_charZero

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
open IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section Discharge
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable {K F}
variable {F' : Type*} [Field F'] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']
omit [Algebra K F] [IsScalarTower K F F'] in

Lean source · statement

theorem ramificationIndex_cast_ne_zero_of_charZero [CharZero K] (w : Place K F') :
    ((w.ramificationIndex F : ℕ) : F') ≠ 0

theorem

tameLocalDifferentExponent_of_localUnitDerivativeRegular_charZero

L1011 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.tameLocalDifferentExponent_of_localUnitDerivativeRegular_charZero

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
open IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section Discharge
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable {K F}
variable {F' : Type*} [Field F'] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']

Lean source · statement

theorem tameLocalDifferentExponent_of_localUnitDerivativeRegular_charZero [CharZero K]
    [∀ w : Place K F', w.DCoordGenerates] [Nontrivial Ω[F'⁄K]]
    (hreg : LocalUnitDerivativeRegular K F') :
    TameLocalDifferentExponent K F F'

theorem

ord_differentialCoeff_D_algebraMap_uniformizer

L1046 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.ord_differentialCoeff_D_algebraMap_uniformizer

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
open IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section RHEngine
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F']

Lean source · statement

theorem ord_differentialCoeff_D_algebraMap_uniformizer
    [∀ w : Place K F', w.DCoordGenerates] [Nontrivial Ω[F'⁄K]]
    (hreg : ∀ (w : Place K F') (u : F'), u ≠ 0 → w.ord u = 0 →
      w.differentialCoeff (KaehlerDifferential.D K F' u) = 0
        ∨ 0 ≤ w.ord (w.differentialCoeff (KaehlerDifferential.D K F' u)))
    (w : Place K F') (hw : ((w.ramificationIndex F : ℕ) : F') ≠ 0) :
    w.differentialCoeff (KaehlerDifferential.D K F' (algebraMap F F' (w.restrict F).uniformizer)) ≠
      0 ∧
      w.ord (w.differentialCoeff
        (KaehlerDifferential.D K F' (algebraMap F F' (w.restrict F).uniformizer)))
          = (w.ramificationIndex F : ℤ) - 1

theorem

tameLocalDifferentExponent_of_hreg

L1065 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.tameLocalDifferentExponent_of_hreg

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
open IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section RHEngine
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F']

Lean source · statement

theorem tameLocalDifferentExponent_of_hreg
    [∀ w : Place K F', w.DCoordGenerates] [Nontrivial Ω[F'⁄K]]
    (hreg : ∀ (w : Place K F') (u : F'), u ≠ 0 → w.ord u = 0 →
      w.differentialCoeff (KaehlerDifferential.D K F' u) = 0
        ∨ 0 ≤ w.ord (w.differentialCoeff (KaehlerDifferential.D K F' u)))
    (htame : ∀ w : Place K F', ((w.ramificationIndex F : ℕ) : F') ≠ 0) :
    TameLocalDifferentExponent K F F'

theorem

nontrivial_kaehler_of_isCurveOver'

L1078 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.nontrivial_kaehler_of_isCurveOver'

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
open IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section RHEngine
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F']
variable [IsCurveOver K F] [∀ v : Place K F, v.DCoordGenerates]
  [IsCurveOver K F'] [∀ w : Place K F', w.DCoordGenerates]
omit [Algebra.IsIntegral F F'] [∀ w : Place K F', w.DCoordGenerates] in

Lean source · statement

theorem nontrivial_kaehler_of_isCurveOver' : Nontrivial Ω[F'⁄K]

theorem

ordDifferential_map_eq_port

L1081 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.ordDifferential_map_eq_port

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
open IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section RHEngine
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F']
variable [IsCurveOver K F] [∀ v : Place K F, v.DCoordGenerates]
  [IsCurveOver K F'] [∀ w : Place K F', w.DCoordGenerates]

Lean source · statement

theorem ordDifferential_map_eq_port
    (hreg : ∀ (w : Place K F') (u : F'), u ≠ 0 → w.ord u = 0 →
      w.differentialCoeff (KaehlerDifferential.D K F' u) = 0
        ∨ 0 ≤ w.ord (w.differentialCoeff (KaehlerDifferential.D K F' u)))
    (htame : ∀ w : Place K F', ((w.ramificationIndex F : ℕ) : F') ≠ 0)
    {ω₀ : Ω[F⁄K]} (hω₀ : ω₀ ≠ 0) (w : Place K F') :
    w.ordDifferential (KaehlerDifferential.map K K F F' ω₀)
      = (w.ramificationIndex F : ℤ) * (w.restrict F).ordDifferential ω₀
          + ((w.ramificationIndex F : ℤ) - 1)

theorem

map_ne_zero_of_tame

L1093 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.map_ne_zero_of_tame

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
open IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section RHEngine
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F']
variable [IsCurveOver K F] [∀ v : Place K F, v.DCoordGenerates]
  [IsCurveOver K F'] [∀ w : Place K F', w.DCoordGenerates]

Lean source · statement

theorem map_ne_zero_of_tame
    (hreg : ∀ (w : Place K F') (u : F'), u ≠ 0 → w.ord u = 0 →
      w.differentialCoeff (KaehlerDifferential.D K F' u) = 0
        ∨ 0 ≤ w.ord (w.differentialCoeff (KaehlerDifferential.D K F' u)))
    (htame : ∀ w : Place K F', ((w.ramificationIndex F : ℕ) : F') ≠ 0)
    (w₀ : Place K F') {ω₀ : Ω[F⁄K]} (hω₀ : ω₀ ≠ 0) :
    KaehlerDifferential.map K K F F' ω₀ ≠ 0

theorem

exists_finset_unramified_off

L1104 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.exists_finset_unramified_off

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
open IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section RHEngine
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F']
variable [IsCurveOver K F] [∀ v : Place K F, v.DCoordGenerates]
  [IsCurveOver K F'] [∀ w : Place K F', w.DCoordGenerates]

Lean source · statement

theorem exists_finset_unramified_off
    [HasCanonicalDivisor (K := K) (F := F)] [HasCanonicalDivisor (K := K) (F := F')]
    (hreg : ∀ (w : Place K F') (u : F'), u ≠ 0 → w.ord u = 0 →
      w.differentialCoeff (KaehlerDifferential.D K F' u) = 0
        ∨ 0 ≤ w.ord (w.differentialCoeff (KaehlerDifferential.D K F' u)))
    (htame : ∀ w : Place K F', ((w.ramificationIndex F : ℕ) : F') ≠ 0)
    {ω₀ : Ω[F⁄K]} (hω₀ : ω₀ ≠ 0) (hω₀' : KaehlerDifferential.map K K F F' ω₀ ≠ 0) :
    ∃ S : Finset (Place K F'), ∀ w : Place K F', w ∉ S → w.ramificationIndex F = 1

theorem

canonicalDivisorOf_map_eq

L1135 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.canonicalDivisorOf_map_eq

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
open IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section RHEngine
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F']
variable [IsCurveOver K F] [∀ v : Place K F, v.DCoordGenerates]
  [IsCurveOver K F'] [∀ w : Place K F', w.DCoordGenerates]

Lean source · statement

theorem canonicalDivisorOf_map_eq
    [HasCanonicalDivisor (K := K) (F := F)] [HasCanonicalDivisor (K := K) (F := F')]
    (hreg : ∀ (w : Place K F') (u : F'), u ≠ 0 → w.ord u = 0 →
      w.differentialCoeff (KaehlerDifferential.D K F' u) = 0
        ∨ 0 ≤ w.ord (w.differentialCoeff (KaehlerDifferential.D K F' u)))
    (htame : ∀ w : Place K F', ((w.ramificationIndex F : ℕ) : F') ≠ 0)
    {ω₀ : Ω[F⁄K]} (hω₀ : ω₀ ≠ 0) (hω₀' : KaehlerDifferential.map K K F F' ω₀ ≠ 0)
    {S : Finset (Place K F')} (hS : ∀ w : Place K F', w ∉ S → w.ramificationIndex F = 1) :
    canonicalDivisorOf (K := K) hω₀'
      = Divisor.pullback F' (canonicalDivisorOf (K := K) hω₀) + tameDifferentDivisor K F S

theorem

degree_canonicalDivisorOf_map

L1150 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.degree_canonicalDivisorOf_map

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
open IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section RHEngine
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F']
variable [IsCurveOver K F] [∀ v : Place K F, v.DCoordGenerates]
  [IsCurveOver K F'] [∀ w : Place K F', w.DCoordGenerates]

Lean source · statement

theorem degree_canonicalDivisorOf_map
    [HasCanonicalDivisor (K := K) (F := F)] [HasCanonicalDivisor (K := K) (F := F')]
    [FiniteDimensional F F'] [Algebra.IsSeparable F F']
    (hreg : ∀ (w : Place K F') (u : F'), u ≠ 0 → w.ord u = 0 →
      w.differentialCoeff (KaehlerDifferential.D K F' u) = 0
        ∨ 0 ≤ w.ord (w.differentialCoeff (KaehlerDifferential.D K F' u)))
    (htame : ∀ w : Place K F', ((w.ramificationIndex F : ℕ) : F') ≠ 0)
    {ω₀ : Ω[F⁄K]} (hω₀ : ω₀ ≠ 0) (hω₀' : KaehlerDifferential.map K K F F' ω₀ ≠ 0) :
    Divisor.degree (canonicalDivisorOf (K := K) hω₀')
      = (Module.finrank F F' : ℤ) * Divisor.degree (canonicalDivisorOf (K := K) hω₀)
        + ∑ᶠ w : Place K F', ((w.ramificationIndex F : ℤ) - 1) * (w.deg : ℤ)

theorem

two_mul_genus_sub_two_eq_of_degree_canonical

L1174 ↗

AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq.AlgebraicCurve.two_mul_genus_sub_two_eq_of_degree_canonical

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
open IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section RHEngine
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F']
variable [IsCurveOver K F] [∀ v : Place K F, v.DCoordGenerates]
  [IsCurveOver K F'] [∀ w : Place K F', w.DCoordGenerates]

Lean source · statement

theorem two_mul_genus_sub_two_eq_of_degree_canonical
    [HasCanonicalDivisor (K := K) (F := F)] [HasCanonicalDivisor (K := K) (F := F')]
    [FiniteDimensional F F'] [Algebra.IsSeparable F F']
    (hreg : ∀ (w : Place K F') (u : F'), u ≠ 0 → w.ord u = 0 →
      w.differentialCoeff (KaehlerDifferential.D K F' u) = 0
        ∨ 0 ≤ w.ord (w.differentialCoeff (KaehlerDifferential.D K F' u)))
    (htame : ∀ w : Place K F', ((w.ramificationIndex F : ℕ) : F') ≠ 0)
    {ω₀ : Ω[F⁄K]} (hω₀ : ω₀ ≠ 0) (hω₀' : KaehlerDifferential.map K K F F' ω₀ ≠ 0)
    (hK : Divisor.degree (canonicalDivisorOf (K := K) hω₀) = 2 * (genus K F : ℤ) - 2)
    (hK' : Divisor.degree (canonicalDivisorOf (K := K) hω₀') = 2 * (genus K F' : ℤ) - 2) :
    2 * (genus K F' : ℤ) - 2
      = (Module.finrank F F' : ℤ) * (2 * (genus K F : ℤ) - 2)
        + ∑ᶠ w : Place K F', ((w.ramificationIndex F : ℤ) - 1) * (w.deg : ℤ)

theorem

ordDifferential_map_eq

L1200 ↗

AlgebraicCurve.ordDifferential_map_eq

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.OrdDifferential_map_eq
open IsDedekindDomain WithZero
open _root_.AlgebraicCurves.Differentials.Proofs in
open _root_.AlgebraicCurve hiding
  Place.ord_nonneg_of_mem
  Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg in
open OrdDifferential_map_eq.AlgebraicCurve in

Lean source · statement

theorem _root_.AlgebraicCurve.ordDifferential_map_eq {K : Type*} {F : Type*} {F' : Type*} [Field K]
  [Field F] [Field F'] [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']
    [IsCurveOver K F] [∀ v : Place K F, v.DCoordGenerates] [IsCurveOver K F'] [∀ w : Place K F',
      w.DCoordGenerates]
    (hreg : ∀ (w : Place K F') (u : F'), u ≠ 0 → w.ord u = 0 →
      w.differentialCoeff (KaehlerDifferential.D K F' u) = 0
        ∨ 0 ≤ w.ord (w.differentialCoeff (KaehlerDifferential.D K F' u)))
    (htame : ∀ w : Place K F', ((w.ramificationIndex F : ℕ) : F') ≠ 0)
    {ω₀ : Ω[F⁄K]} (hω₀ : ω₀ ≠ 0) (w : Place K F') :
    w.ordDifferential (KaehlerDifferential.map K K F F' ω₀)
      = (w.ramificationIndex F : ℤ) * (w.restrict F).ordDifferential ω₀
          + ((w.ramificationIndex F : ℤ) - 1)

Module documentation

Ord Differential map eq

Declarations