NYLL
Module

Kw_cart_C_pow_pred_smul_D.lean

Nyll.AlgebraicCurves.Differentials.Kw_cart_C_pow_pred_smul_D
13 declarations indexed from sourceView source ↗

Module documentation

Kw cart C pow pred smul D

Imports2
Imported by3

Declarations

def

CC

L37 ↗
AlgebraicCurves.Differentials.Proofs.Kw_cart_C_pow_pred_smul_D.CartMintSol.CC
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Kw_cart_C_pow_pred_smul_D
noncomputable section
open AlgebraicCurve.KwPke AlgebraicCurve.KwCart AlgebraicCurve.KwCfx
namespace CartMintSol
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP F ℓ]
variable (t : F) (hdt : KaehlerDifferential.D K F t ≠ 0)
  (hspan : Submodule.span F {KaehlerDifferential.D K F t} = ⊤)
  (hsep : ∀ x : F, IsSeparable (kw_pke_expansionField (ℓ := ℓ) t).toSubfield x)
  (hdeg : (minpoly (kw_pke_pthPowers F ℓ) t).natDegree = ℓ)
Lean source · statement
def CC : Ω[F⁄K] →+ Ω[F⁄K]
theorem

CC_apply

L41 ↗
AlgebraicCurves.Differentials.Proofs.Kw_cart_C_pow_pred_smul_D.CartMintSol.CC_apply
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Kw_cart_C_pow_pred_smul_D
noncomputable section
open AlgebraicCurve.KwPke AlgebraicCurve.KwCart AlgebraicCurve.KwCfx
namespace CartMintSol
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP F ℓ]
variable (t : F) (hdt : KaehlerDifferential.D K F t ≠ 0)
  (hspan : Submodule.span F {KaehlerDifferential.D K F t} = ⊤)
  (hsep : ∀ x : F, IsSeparable (kw_pke_expansionField (ℓ := ℓ) t).toSubfield x)
  (hdeg : (minpoly (kw_pke_pthPowers F ℓ) t).natDegree = ℓ)
Lean source · statement
theorem CC_apply (ω : Ω[F⁄K]) :
    CC t hdt hspan hsep hdeg ω = kw_cart_C (K := K) t hdt hspan hsep hdeg ω
theorem

CC_semilinear

L44 ↗
AlgebraicCurves.Differentials.Proofs.Kw_cart_C_pow_pred_smul_D.CartMintSol.CC_semilinear
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Kw_cart_C_pow_pred_smul_D
noncomputable section
open AlgebraicCurve.KwPke AlgebraicCurve.KwCart AlgebraicCurve.KwCfx
namespace CartMintSol
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP F ℓ]
variable (t : F) (hdt : KaehlerDifferential.D K F t ≠ 0)
  (hspan : Submodule.span F {KaehlerDifferential.D K F t} = ⊤)
  (hsep : ∀ x : F, IsSeparable (kw_pke_expansionField (ℓ := ℓ) t).toSubfield x)
  (hdeg : (minpoly (kw_pke_pthPowers F ℓ) t).natDegree = ℓ)
Lean source · statement
theorem CC_semilinear (a : F) (ω : Ω[F⁄K]) :
    CC t hdt hspan hsep hdeg (a ^ ℓ • ω) = a • CC t hdt hspan hsep hdeg ω
theorem

repr_pow_basis

L48 ↗
AlgebraicCurves.Differentials.Proofs.Kw_cart_C_pow_pred_smul_D.CartMintSol.repr_pow_basis
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Kw_cart_C_pow_pred_smul_D
noncomputable section
open AlgebraicCurve.KwPke AlgebraicCurve.KwCart AlgebraicCurve.KwCfx
namespace CartMintSol
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP F ℓ]
variable (t : F) (hdt : KaehlerDifferential.D K F t ≠ 0)
  (hspan : Submodule.span F {KaehlerDifferential.D K F t} = ⊤)
  (hsep : ∀ x : F, IsSeparable (kw_pke_expansionField (ℓ := ℓ) t).toSubfield x)
  (hdeg : (minpoly (kw_pke_pthPowers F ℓ) t).natDegree = ℓ)
Lean source · full declaration
theorem repr_pow_basis {k : ℕ} (hk : k < ℓ) :
    kw_cart_repr t hsep hdeg (t ^ k)
      = fun j : Fin ℓ => if j = ⟨k, hk⟩ then 1 else 0 := by
  refine kw_cart_repr_unique t hsep hdeg ?_
  rw [Finset.sum_eq_single (⟨k, hk⟩ : Fin ℓ)]
  · simp
  · intro j _ hj
    simp [hj]
  · intro hmem
    exact absurd (Finset.mem_univ _) hmem
theorem

repr_pow_top_eq_zero

L59 ↗
AlgebraicCurves.Differentials.Proofs.Kw_cart_C_pow_pred_smul_D.CartMintSol.repr_pow_top_eq_zero
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Kw_cart_C_pow_pred_smul_D
noncomputable section
open AlgebraicCurve.KwPke AlgebraicCurve.KwCart AlgebraicCurve.KwCfx
namespace CartMintSol
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP F ℓ]
variable (t : F) (hdt : KaehlerDifferential.D K F t ≠ 0)
  (hspan : Submodule.span F {KaehlerDifferential.D K F t} = ⊤)
  (hsep : ∀ x : F, IsSeparable (kw_pke_expansionField (ℓ := ℓ) t).toSubfield x)
  (hdeg : (minpoly (kw_pke_pthPowers F ℓ) t).natDegree = ℓ)
Lean source · full declaration
theorem repr_pow_top_eq_zero {k : ℕ} (hk : k + 1 < ℓ) :
    kw_cart_repr t hsep hdeg (t ^ k)
      ⟨ℓ - 1, by have := hℓ.out.pos; omega⟩ = 0 := by
  have hklt : k < ℓ := by omega
  rw [repr_pow_basis t hsep hdeg hklt]
  have hne : (⟨ℓ - 1, by have := hℓ.out.pos; omega⟩ : Fin ℓ) ≠ ⟨k, hklt⟩ := by
    intro he
    have hv : ℓ - 1 = k := by injection he
    omega
  exact ite_eq_right hne
theorem

root_zero

L70 ↗
AlgebraicCurves.Differentials.Proofs.Kw_cart_C_pow_pred_smul_D.CartMintSol.root_zero
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Kw_cart_C_pow_pred_smul_D
noncomputable section
open AlgebraicCurve.KwPke AlgebraicCurve.KwCart AlgebraicCurve.KwCfx
namespace CartMintSol
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP F ℓ]
variable (t : F) (hdt : KaehlerDifferential.D K F t ≠ 0)
  (hspan : Submodule.span F {KaehlerDifferential.D K F t} = ⊤)
  (hsep : ∀ x : F, IsSeparable (kw_pke_expansionField (ℓ := ℓ) t).toSubfield x)
  (hdeg : (minpoly (kw_pke_pthPowers F ℓ) t).natDegree = ℓ)
Lean source · statement
theorem root_zero : kw_cart_root (0 : kw_pke_pthPowers F ℓ) = 0
theorem

C_pow_smul_Dt

L73 ↗
AlgebraicCurves.Differentials.Proofs.Kw_cart_C_pow_pred_smul_D.CartMintSol.C_pow_smul_Dt
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Kw_cart_C_pow_pred_smul_D
noncomputable section
open AlgebraicCurve.KwPke AlgebraicCurve.KwCart AlgebraicCurve.KwCfx
namespace CartMintSol
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP F ℓ]
variable (t : F) (hdt : KaehlerDifferential.D K F t ≠ 0)
  (hspan : Submodule.span F {KaehlerDifferential.D K F t} = ⊤)
  (hsep : ∀ x : F, IsSeparable (kw_pke_expansionField (ℓ := ℓ) t).toSubfield x)
  (hdeg : (minpoly (kw_pke_pthPowers F ℓ) t).natDegree = ℓ)
Lean source · statement
theorem C_pow_smul_Dt {k : ℕ} (hk : k + 1 < ℓ) :
    kw_cart_C (K := K) t hdt hspan hsep hdeg
      (t ^ k • KaehlerDifferential.D K F t) = 0
theorem

C_D_eq_zero

L81 ↗
AlgebraicCurves.Differentials.Proofs.Kw_cart_C_pow_pred_smul_D.CartMintSol.C_D_eq_zero
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Kw_cart_C_pow_pred_smul_D
noncomputable section
open AlgebraicCurve.KwPke AlgebraicCurve.KwCart AlgebraicCurve.KwCfx
namespace CartMintSol
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP F ℓ]
variable (t : F) (hdt : KaehlerDifferential.D K F t ≠ 0)
  (hspan : Submodule.span F {KaehlerDifferential.D K F t} = ⊤)
  (hsep : ∀ x : F, IsSeparable (kw_pke_expansionField (ℓ := ℓ) t).toSubfield x)
  (hdeg : (minpoly (kw_pke_pthPowers F ℓ) t).natDegree = ℓ)
Lean source · statement
theorem C_D_eq_zero (f : F) :
    kw_cart_C (K := K) t hdt hspan hsep hdeg (KaehlerDifferential.D K F f) = 0
theorem

C_pow_pred_smul_D

L99 ↗
AlgebraicCurves.Differentials.Proofs.Kw_cart_C_pow_pred_smul_D.CartMintSol.C_pow_pred_smul_D
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Kw_cart_C_pow_pred_smul_D
noncomputable section
open AlgebraicCurve.KwPke AlgebraicCurve.KwCart AlgebraicCurve.KwCfx
namespace CartMintSol
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP F ℓ]
variable (t : F) (hdt : KaehlerDifferential.D K F t ≠ 0)
  (hspan : Submodule.span F {KaehlerDifferential.D K F t} = ⊤)
  (hsep : ∀ x : F, IsSeparable (kw_pke_expansionField (ℓ := ℓ) t).toSubfield x)
  (hdeg : (minpoly (kw_pke_pthPowers F ℓ) t).natDegree = ℓ)
Lean source · statement
theorem C_pow_pred_smul_D (g : F) :
    kw_cart_C (K := K) t hdt hspan hsep hdeg
      (g ^ (ℓ - 1) • KaehlerDifferential.D K F g) = KaehlerDifferential.D K F g
theorem

C_dlog_fixed_all

L114 ↗
AlgebraicCurves.Differentials.Proofs.Kw_cart_C_pow_pred_smul_D.CartMintSol.C_dlog_fixed_all
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Kw_cart_C_pow_pred_smul_D
noncomputable section
open AlgebraicCurve.KwPke AlgebraicCurve.KwCart AlgebraicCurve.KwCfx
namespace CartMintSol
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP F ℓ]
variable (t : F) (hdt : KaehlerDifferential.D K F t ≠ 0)
  (hspan : Submodule.span F {KaehlerDifferential.D K F t} = ⊤)
  (hsep : ∀ x : F, IsSeparable (kw_pke_expansionField (ℓ := ℓ) t).toSubfield x)
  (hdeg : (minpoly (kw_pke_pthPowers F ℓ) t).natDegree = ℓ)
Lean source · statement
theorem C_dlog_fixed_all (g : F) :
    kw_cart_C (K := K) t hdt hspan hsep hdeg
      (g⁻¹ • KaehlerDifferential.D K F g) = g⁻¹ • KaehlerDifferential.D K F g
theorem

C_pow_smul_D_eq_zero

L122 ↗
AlgebraicCurves.Differentials.Proofs.Kw_cart_C_pow_pred_smul_D.CartMintSol.C_pow_smul_D_eq_zero
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Kw_cart_C_pow_pred_smul_D
noncomputable section
open AlgebraicCurve.KwPke AlgebraicCurve.KwCart AlgebraicCurve.KwCfx
namespace CartMintSol
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP F ℓ]
variable (t : F) (hdt : KaehlerDifferential.D K F t ≠ 0)
  (hspan : Submodule.span F {KaehlerDifferential.D K F t} = ⊤)
  (hsep : ∀ x : F, IsSeparable (kw_pke_expansionField (ℓ := ℓ) t).toSubfield x)
  (hdeg : (minpoly (kw_pke_pthPowers F ℓ) t).natDegree = ℓ)
Lean source · statement
theorem C_pow_smul_D_eq_zero (g : F) {i : ℕ} (hi : i + 1 < ℓ) :
    kw_cart_C (K := K) t hdt hspan hsep hdeg
      (g ^ i • KaehlerDifferential.D K F g) = 0
theorem

C_digits

L140 ↗
AlgebraicCurves.Differentials.Proofs.Kw_cart_C_pow_pred_smul_D.CartMintSol.C_digits
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Kw_cart_C_pow_pred_smul_D
noncomputable section
open AlgebraicCurve.KwPke AlgebraicCurve.KwCart AlgebraicCurve.KwCfx
namespace CartMintSol
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP F ℓ]
variable (t : F) (hdt : KaehlerDifferential.D K F t ≠ 0)
  (hspan : Submodule.span F {KaehlerDifferential.D K F t} = ⊤)
  (hsep : ∀ x : F, IsSeparable (kw_pke_expansionField (ℓ := ℓ) t).toSubfield x)
  (hdeg : (minpoly (kw_pke_pthPowers F ℓ) t).natDegree = ℓ)
Lean source · statement
theorem C_digits (g : F) (a : Fin ℓ → F) :
    kw_cart_C (K := K) t hdt hspan hsep hdeg
      ((∑ i : Fin ℓ, a i ^ ℓ * g ^ (i : ℕ)) • KaehlerDifferential.D K F g) =
      a ⟨ℓ - 1, Nat.sub_lt (Fact.out : ℓ.Prime).pos Nat.one_pos⟩ •
        KaehlerDifferential.D K F g
theorem

kw_cart_C_pow_pred_smul_D

L161 ↗
AlgebraicCurve.kw_cart_C_pow_pred_smul_D
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Kw_cart_C_pow_pred_smul_D
noncomputable section
open AlgebraicCurve.KwPke AlgebraicCurve.KwCart AlgebraicCurve.KwCfx
Lean source · statement
theorem _root_.AlgebraicCurve.kw_cart_C_pow_pred_smul_D {K F : Type*} [Field K] [Field F]
    [Algebra K F] {ℓ : ℕ} [Fact ℓ.Prime] [CharP F ℓ] (t : F)
    (hdt : KaehlerDifferential.D K F t ≠ 0)
    (hspan : Submodule.span F {KaehlerDifferential.D K F t} = ⊤)
    (hsep : ∀ x : F,
      IsSeparable (AlgebraicCurve.KwPke.kw_pke_expansionField (ℓ := ℓ) t).toSubfield x)
    (hdeg : (minpoly (AlgebraicCurve.KwPke.kw_pke_pthPowers F ℓ) t).natDegree = ℓ)
    (g : F) :
    AlgebraicCurve.KwCart.kw_cart_C (K := K) t hdt hspan hsep hdeg
      (g ^ (ℓ - 1) • KaehlerDifferential.D K F g) = KaehlerDifferential.D K F g

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