NYLL
Module

Place_ordDiff_pullbackDiff_of_natCast_ramificationIndexAlong_ne_zero.lean

Nyll.AlgebraicCurves.Places.Place_ordDiff_pullbackDiff_of_natCast_ramificationIndexAlong_ne_zero
14 declarations indexed from sourceView source ↗

Module documentation

Place ord Diff pullback Diff of nat Cast ramification Index Along ne zero

Imports11
Imported by1

Declarations

theorem

pullbackDiff_smul'

L39 ↗
AlgebraicCurves.Places.Proofs.Place_ordDiff_pullbackDiff_of_natCast_ramificationIndexAlong_ne_zero.FtameBuild.pullbackDiff_smul'
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ordDiff_pullbackDiff_of_natCast_ramificationIndexAlong_ne_zero
open _root_.AlgebraicCurve
open _root_.KaehlerDifferential
namespace FtameBuild
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
Lean source · statement
theorem pullbackDiff_smul' (φ : F →ₐ[K] F') (g : F) (ω : Ω[F⁄K]) :
    pullbackDiff φ (g • ω) = φ g • pullbackDiff φ ω
theorem

ramificationIndexAlong_pos

L47 ↗
AlgebraicCurves.Places.Proofs.Place_ordDiff_pullbackDiff_of_natCast_ramificationIndexAlong_ne_zero.FtameBuild.ramificationIndexAlong_pos
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ordDiff_pullbackDiff_of_natCast_ramificationIndexAlong_ne_zero
open _root_.AlgebraicCurve
open _root_.KaehlerDifferential
namespace FtameBuild
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
Lean source · statement
theorem ramificationIndexAlong_pos (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
    (w' : Place K F') : 0 < Place.ramificationIndexAlong φ w'
theorem

ordDiff_pullbackDiff_of_local

L54 ↗
AlgebraicCurves.Places.Proofs.Place_ordDiff_pullbackDiff_of_natCast_ramificationIndexAlong_ne_zero.FtameBuild.ordDiff_pullbackDiff_of_local
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ordDiff_pullbackDiff_of_natCast_ramificationIndexAlong_ne_zero
open _root_.AlgebraicCurve
open _root_.KaehlerDifferential
namespace FtameBuild
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
Lean source · statement
theorem ordDiff_pullbackDiff_of_local (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
    (w' : Place K F') {ω : Ω[F⁄K]} (hω : ω ≠ 0)
    (hspan : ∃ g : F, ω = g • D K F (w'.restrictAlong φ hφ).uniformizer_alt)
    (hadd : ∀ (a : F') (η : Ω[F'⁄K]), a ≠ 0 → η ≠ 0 →
      w'.ordDiff (a • η) = w'.ord a + w'.ordDiff η)
    (hDt : D K F' (φ (w'.restrictAlong φ hφ).uniformizer_alt) ≠ 0)
    (hR6a : w'.ordDiff (D K F' (φ (w'.restrictAlong φ hφ).uniformizer_alt))
      = (Place.ramificationIndexAlong φ w' : ℤ) - 1) :
    w'.ordDiff (pullbackDiff φ ω)
      = (Place.ramificationIndexAlong φ w' : ℤ) * (w'.restrictAlong φ hφ).ordDiff ω
        + ((Place.ramificationIndexAlong φ w' : ℤ) - 1)
theorem

ord_phi_uniformizer

L86 ↗
AlgebraicCurves.Places.Proofs.Place_ordDiff_pullbackDiff_of_natCast_ramificationIndexAlong_ne_zero.FtameBuild.ord_phi_uniformizer
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ordDiff_pullbackDiff_of_natCast_ramificationIndexAlong_ne_zero
open _root_.AlgebraicCurve
open _root_.KaehlerDifferential
namespace FtameBuild
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
section Discharge
variable [PerfectField K]
variable (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (w' : Place K F')
omit [PerfectField K] in
Lean source · statement
theorem ord_phi_uniformizer :
    w'.ord (φ (w'.restrictAlong φ hφ).uniformizer_alt) = (Place.ramificationIndexAlong φ w' : ℤ)
theorem

ord_phi_uniformizer_ne_zero

L92 ↗
AlgebraicCurves.Places.Proofs.Place_ordDiff_pullbackDiff_of_natCast_ramificationIndexAlong_ne_zero.FtameBuild.ord_phi_uniformizer_ne_zero
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ordDiff_pullbackDiff_of_natCast_ramificationIndexAlong_ne_zero
open _root_.AlgebraicCurve
open _root_.KaehlerDifferential
namespace FtameBuild
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
section Discharge
variable [PerfectField K]
variable (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (w' : Place K F')
omit [PerfectField K] in
Lean source · statement
theorem ord_phi_uniformizer_ne_zero :
    w'.ord (φ (w'.restrictAlong φ hφ).uniformizer_alt) ≠ 0
theorem

hadd

L97 ↗
AlgebraicCurves.Places.Proofs.Place_ordDiff_pullbackDiff_of_natCast_ramificationIndexAlong_ne_zero.FtameBuild.hadd
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ordDiff_pullbackDiff_of_natCast_ramificationIndexAlong_ne_zero
open _root_.AlgebraicCurve
open _root_.KaehlerDifferential
namespace FtameBuild
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
section Discharge
variable [PerfectField K]
variable (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (w' : Place K F')
Lean source · statement
theorem hadd (x : F') [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F')) F'] :
    ∀ (a : F') (η : Ω[F'⁄K]), a ≠ 0 → η ≠ 0 → w'.ordDiff (a • η) = w'.ord a + w'.ordDiff η
theorem

hspan

L103 ↗
AlgebraicCurves.Places.Proofs.Place_ordDiff_pullbackDiff_of_natCast_ramificationIndexAlong_ne_zero.FtameBuild.hspan
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ordDiff_pullbackDiff_of_natCast_ramificationIndexAlong_ne_zero
open _root_.AlgebraicCurve
open _root_.KaehlerDifferential
namespace FtameBuild
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
section Discharge
variable [PerfectField K]
variable (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (w' : Place K F')
Lean source · statement
theorem hspan (x₀ : F) [Algebra.IsAlgebraic (IntermediateField.adjoin K ({x₀} : Set F)) F]
    (ω : Ω[F⁄K]) : ∃ g : F, ω = g • D K F (w'.restrictAlong φ hφ).uniformizer_alt
theorem

ord_algebraMap_eq_zero

L113 ↗
AlgebraicCurves.Places.Proofs.Place_ordDiff_pullbackDiff_of_natCast_ramificationIndexAlong_ne_zero.FtameBuild.ord_algebraMap_eq_zero
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ordDiff_pullbackDiff_of_natCast_ramificationIndexAlong_ne_zero
open _root_.AlgebraicCurve
open _root_.KaehlerDifferential
namespace FtameBuild
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
section Discharge
variable [PerfectField K]
variable (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (w' : Place K F')
omit [PerfectField K] in
Lean source · statement
theorem ord_algebraMap_eq_zero {c : K} (hc : c ≠ 0) :
    w'.ord (algebraMap K F' c) = 0
theorem

diffCoeff_eq_of_eq_smul

L125 ↗
AlgebraicCurves.Places.Proofs.Place_ordDiff_pullbackDiff_of_natCast_ramificationIndexAlong_ne_zero.FtameBuild.diffCoeff_eq_of_eq_smul
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ordDiff_pullbackDiff_of_natCast_ramificationIndexAlong_ne_zero
open _root_.AlgebraicCurve
open _root_.KaehlerDifferential
namespace FtameBuild
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
section Discharge
variable [PerfectField K]
variable (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (w' : Place K F')
omit [PerfectField K] in
Lean source · statement
theorem diffCoeff_eq_of_eq_smul {t : F'} (hDt : D K F' t ≠ 0) {ω : Ω[F'⁄K]} {g : F'}
    (h : ω = g • D K F' t) : Place.diffCoeff t ω = g
theorem

exists_good_coeff

L134 ↗
AlgebraicCurves.Places.Proofs.Place_ordDiff_pullbackDiff_of_natCast_ramificationIndexAlong_ne_zero.FtameBuild.exists_good_coeff
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ordDiff_pullbackDiff_of_natCast_ramificationIndexAlong_ne_zero
open _root_.AlgebraicCurve
open _root_.KaehlerDifferential
namespace FtameBuild
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
section Discharge
variable [PerfectField K]
variable (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (w' : Place K F')
Lean source · statement
theorem exists_good_coeff (x : F')
    [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F')) F']
    (he : ((Place.ramificationIndexAlong φ w' : ℕ) : K) ≠ 0) :
    ∃ g₀ : F', g₀ ≠ 0 ∧
      D K F' (φ (w'.restrictAlong φ hφ).uniformizer_alt) = g₀ • D K F' w'.uniformizer_alt ∧
      w'.ord g₀ = (Place.ramificationIndexAlong φ w' : ℤ) - 1
theorem

hDt_of_tame

L223 ↗
AlgebraicCurves.Places.Proofs.Place_ordDiff_pullbackDiff_of_natCast_ramificationIndexAlong_ne_zero.FtameBuild.hDt_of_tame
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ordDiff_pullbackDiff_of_natCast_ramificationIndexAlong_ne_zero
open _root_.AlgebraicCurve
open _root_.KaehlerDifferential
namespace FtameBuild
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
section Discharge
variable [PerfectField K]
variable (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (w' : Place K F')
Lean source · statement
theorem hDt_of_tame (x : F')
    [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F')) F']
    (he : ((Place.ramificationIndexAlong φ w' : ℕ) : K) ≠ 0) :
    D K F' (φ (w'.restrictAlong φ hφ).uniformizer_alt) ≠ 0
theorem

hR6a_of_tame

L239 ↗
AlgebraicCurves.Places.Proofs.Place_ordDiff_pullbackDiff_of_natCast_ramificationIndexAlong_ne_zero.FtameBuild.hR6a_of_tame
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ordDiff_pullbackDiff_of_natCast_ramificationIndexAlong_ne_zero
open _root_.AlgebraicCurve
open _root_.KaehlerDifferential
namespace FtameBuild
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
section Discharge
variable [PerfectField K]
variable (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (w' : Place K F')
Lean source · statement
theorem hR6a_of_tame (x : F')
    [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F')) F']
    (he : ((Place.ramificationIndexAlong φ w' : ℕ) : K) ≠ 0) :
    w'.ordDiff (D K F' (φ (w'.restrictAlong φ hφ).uniformizer_alt))
      = (Place.ramificationIndexAlong φ w' : ℤ) - 1
theorem

solution_impl

L265 ↗
AlgebraicCurves.Places.Proofs.Place_ordDiff_pullbackDiff_of_natCast_ramificationIndexAlong_ne_zero.AlgebraicCurve.Place.solution_impl
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ordDiff_pullbackDiff_of_natCast_ramificationIndexAlong_ne_zero
open _root_.AlgebraicCurve
open _root_.KaehlerDifferential
open scoped _root_.AlgebraicCurve _root_.AlgebraicCurve.Place in
Lean source · statement
theorem AlgebraicCurve.Place.solution_impl
    {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
    [PerfectField K]
    (x₀ : F) [Algebra.IsAlgebraic (IntermediateField.adjoin K ({x₀} : Set F)) F]
    (x : F') [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F')) F']
    (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (w' : Place K F') {ω : Ω[F⁄K]}
    (hω : ω ≠ 0)
    (he : ((Place.ramificationIndexAlong φ w' : ℕ) : K) ≠ 0) :
    w'.ordDiff (pullbackDiff φ ω)
      = (Place.ramificationIndexAlong φ w' : ℤ) * (w'.restrictAlong φ hφ).ordDiff ω
        + ((Place.ramificationIndexAlong φ w' : ℤ) - 1)
theorem

ordDiff_pullbackDiff_of_natCast_ramificationIndexAlong_ne_zero

L280 ↗
AlgebraicCurve.Place.ordDiff_pullbackDiff_of_natCast_ramificationIndexAlong_ne_zero
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ordDiff_pullbackDiff_of_natCast_ramificationIndexAlong_ne_zero
open _root_.AlgebraicCurve
open _root_.KaehlerDifferential
Lean source · statement
theorem _root_.AlgebraicCurve.Place.ordDiff_pullbackDiff_of_natCast_ramificationIndexAlong_ne_zero
  {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
    [PerfectField K]
    (x₀ : F) [Algebra.IsAlgebraic (IntermediateField.adjoin K ({x₀} : Set F)) F]
    (x : F') [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F')) F']
    (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (w' : Place K F') {ω : Ω[F⁄K]}
    (hω : ω ≠ 0)
    (he : ((Place.ramificationIndexAlong φ w' : ℕ) : K) ≠ 0) :
    w'.ordDiff (pullbackDiff φ ω)
      = (Place.ramificationIndexAlong φ w' : ℤ) * (w'.restrictAlong φ hφ).ordDiff ω
        + ((Place.ramificationIndexAlong φ w' : ℤ) - 1)

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