NYLL
Module

Finite_and_card_torsion_le_pow_finrank.lean

Nyll.AlgebraicCurves.FunctionFields.Finite_and_card_torsion_le_pow_finrank
16 declarations indexed from sourceView source ↗

Module documentation

Finite and card torsion le pow finrank

Imports15
Imported by2

Declarations

theorem

charP_F

L49 ↗
AlgebraicCurves.FunctionFields.Proofs.Finite_and_card_torsion_le_pow_finrank.AlgebraicCurve.PayoffDev.charP_F
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Finite_and_card_torsion_le_pow_finrank
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace PayoffDev
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem charP_F (p : ℕ) [CharP K p] : CharP F p
theorem

nsmul_eq_cast_smul

L52 ↗
AlgebraicCurves.FunctionFields.Proofs.Finite_and_card_torsion_le_pow_finrank.AlgebraicCurve.PayoffDev.nsmul_eq_cast_smul
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Finite_and_card_torsion_le_pow_finrank
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace PayoffDev
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem nsmul_eq_cast_smul {M : Type*} [AddCommGroup M] [Module F M] (n : ℕ) (ω : M) :
    n • ω = (n : F) • ω
theorem

pkill

L55 ↗
AlgebraicCurves.FunctionFields.Proofs.Finite_and_card_torsion_le_pow_finrank.AlgebraicCurve.PayoffDev.pkill
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Finite_and_card_torsion_le_pow_finrank
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace PayoffDev
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem pkill (p : ℕ) [Fact p.Prime] [CharP K p] {M : Type*} [AddCommGroup M]
    [Module F M] (ω : M) : p • ω = 0
theorem

D_pow_char

L60 ↗
AlgebraicCurves.FunctionFields.Proofs.Finite_and_card_torsion_le_pow_finrank.AlgebraicCurve.PayoffDev.D_pow_char
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Finite_and_card_torsion_le_pow_finrank
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace PayoffDev
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem D_pow_char (p : ℕ) [Fact p.Prime] [CharP K p] (a : F) :
    D K F (a ^ p) = 0
theorem

natCast_pow_char

L64 ↗
AlgebraicCurves.FunctionFields.Proofs.Finite_and_card_torsion_le_pow_finrank.AlgebraicCurve.PayoffDev.natCast_pow_char
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Finite_and_card_torsion_le_pow_finrank
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace PayoffDev
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem natCast_pow_char (p : ℕ) [Fact p.Prime] [CharP K p] (m : ℕ) :
    ((m : F)) ^ p = (m : F)
theorem

dlog_mul

L71 ↗
AlgebraicCurves.FunctionFields.Proofs.Finite_and_card_torsion_le_pow_finrank.AlgebraicCurve.PayoffDev.dlog_mul
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Finite_and_card_torsion_le_pow_finrank
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace PayoffDev
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem dlog_mul {g h : F} (hg : g ≠ 0) (hh : h ≠ 0) :
    (g * h)⁻¹ • D K F (g * h) = g⁻¹ • D K F g + h⁻¹ • D K F h
theorem

dlog_inv

L80 ↗
AlgebraicCurves.FunctionFields.Proofs.Finite_and_card_torsion_le_pow_finrank.AlgebraicCurve.PayoffDev.dlog_inv
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Finite_and_card_torsion_le_pow_finrank
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace PayoffDev
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem dlog_inv {g : F} (hg : g ≠ 0) :
    (g⁻¹)⁻¹ • D K F g⁻¹ = -(g⁻¹ • D K F g)
theorem

dlog_fixed

L88 ↗
AlgebraicCurves.FunctionFields.Proofs.Finite_and_card_torsion_le_pow_finrank.AlgebraicCurve.PayoffDev.dlog_fixed
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Finite_and_card_torsion_le_pow_finrank
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace PayoffDev
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem dlog_fixed (p : ℕ) [Fact p.Prime] (C : Ω[F⁄K] →+ Ω[F⁄K])
    (hsemi : ∀ (f : F) (η : Ω[F⁄K]), C (f ^ p • η) = f • C η)
    (hdlog : ∀ f : F, C (f ^ (p - 1) • D K F f) = D K F f) (g : F) :
    C (g⁻¹ • D K F g) = g⁻¹ • D K F g
theorem

exists_pow_eq_of_D_eq_zero

L107 ↗
AlgebraicCurves.FunctionFields.Proofs.Finite_and_card_torsion_le_pow_finrank.AlgebraicCurve.PayoffDev.exists_pow_eq_of_D_eq_zero
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Finite_and_card_torsion_le_pow_finrank
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace PayoffDev
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem exists_pow_eq_of_D_eq_zero [IsCurveOver K F] (p : ℕ) [Fact p.Prime]
    [CharP K p] [PerfectField K] (x : F)
    [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
    {r : F} (hr : D K F r = 0) : ∃ s : F, r = s ^ p
theorem

nsmul_mod

L182 ↗
AlgebraicCurves.FunctionFields.Proofs.Finite_and_card_torsion_le_pow_finrank.AlgebraicCurve.PayoffDev.nsmul_mod
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Finite_and_card_torsion_le_pow_finrank
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace PayoffDev
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem nsmul_mod {M : Type*} [AddCommGroup M] (p : ℕ) (hkill : ∀ ω : M, p • ω = 0)
    (n : ℕ) (ω : M) : n • ω = (n % p) • ω
theorem

neg_eq_pred_nsmul

L187 ↗
AlgebraicCurves.FunctionFields.Proofs.Finite_and_card_torsion_le_pow_finrank.AlgebraicCurve.PayoffDev.neg_eq_pred_nsmul
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Finite_and_card_torsion_le_pow_finrank
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace PayoffDev
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem neg_eq_pred_nsmul {M : Type*} [AddCommGroup M] (p : ℕ) (hp : 0 < p)
    (hkill : ∀ ω : M, p • ω = 0) (ω : M) : -ω = (p - 1) • ω
theorem

finite_and_card_le_of_rawIndep_le

L196 ↗
AlgebraicCurves.FunctionFields.Proofs.Finite_and_card_torsion_le_pow_finrank.AlgebraicCurve.PayoffDev.finite_and_card_le_of_rawIndep_le
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Finite_and_card_torsion_le_pow_finrank
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace PayoffDev
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem finite_and_card_le_of_rawIndep_le {M : Type*} [AddCommGroup M]
    (p n : ℕ) (hp : p.Prime) (hkill : ∀ ω : M, p • ω = 0) (S : Set M)
    (hind : ∀ (m : ℕ) (w : Fin m → M), (∀ i, w i ∈ S) →
      (∀ c : Fin m → ℕ, (∑ i, c i • w i) = 0 → ∀ i, p ∣ c i) → m ≤ n) :
    S.Finite ∧ Nat.card S ≤ p ^ n
def

dlogSet

L284 ↗
AlgebraicCurves.FunctionFields.Proofs.Finite_and_card_torsion_le_pow_finrank.AlgebraicCurve.PayoffDev.dlogSet
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Finite_and_card_torsion_le_pow_finrank
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace PayoffDev
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in
Lean source · statement
def dlogSet (p : ℕ) : Set Ω[F⁄K]
theorem

finite_and_card_torsion_le_pow_finrank_X

L287 ↗
AlgebraicCurves.FunctionFields.Proofs.Finite_and_card_torsion_le_pow_finrank.AlgebraicCurve.PayoffDev.finite_and_card_torsion_le_pow_finrank_X
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Finite_and_card_torsion_le_pow_finrank
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace PayoffDev
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in
Lean source · statement
theorem finite_and_card_torsion_le_pow_finrank_X [IsCurveOver K F] (p : ℕ)
    [Fact p.Prime] [CharP K p] [PerfectField K]
    [FiniteDimensional K (regularDiffs K F)]
    (x : F) [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
    (C : Ω[F⁄K] →+ Ω[F⁄K])
    (hsemi : ∀ (f : F) (η : Ω[F⁄K]), C (f ^ p • η) = f • C η)
    (hdlog : ∀ f : F, C (f ^ (p - 1) • D K F f) = D K F f) :
    Finite (Pic0.torsion K F p) ∧
      Nat.card (Pic0.torsion K F p) ≤ p ^ Module.finrank K (regularDiffs K F)
theorem

finite_and_card_torsion_le_pow_finrank_unconditional_X

L427 ↗
AlgebraicCurves.FunctionFields.Proofs.Finite_and_card_torsion_le_pow_finrank.AlgebraicCurve.PayoffDev.finite_and_card_torsion_le_pow_finrank_unconditional_X
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Finite_and_card_torsion_le_pow_finrank
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace PayoffDev
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in
Lean source · statement
theorem finite_and_card_torsion_le_pow_finrank_unconditional_X [IsCurveOver K F]
    (p : ℕ) [Fact p.Prime] [CharP K p] [PerfectField K]
    [FiniteDimensional K (regularDiffs K F)]
    (x : F) [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F] :
    Finite (Pic0.torsion K F p) ∧
      Nat.card (Pic0.torsion K F p) ≤ p ^ Module.finrank K (regularDiffs K F)
theorem

finite_and_card_torsion_le_pow_finrank

L442 ↗
AlgebraicCurve.finite_and_card_torsion_le_pow_finrank
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Finite_and_card_torsion_le_pow_finrank
noncomputable section
open KaehlerDifferential
universe u v
Lean source · statement
theorem _root_.AlgebraicCurve.finite_and_card_torsion_le_pow_finrank
    {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
    [AlgebraicCurve.IsCurveOver K F] (p : ℕ) [Fact p.Prime] [CharP K p] [PerfectField K]
    [FiniteDimensional K (AlgebraicCurve.regularDiffs K F)]
    (x : F) [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F] :
    Finite (AlgebraicCurve.Pic0.torsion K F p) ∧
      Nat.card (AlgebraicCurve.Pic0.torsion K F p) ≤
        p ^ Module.finrank K (AlgebraicCurve.regularDiffs K F)

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