Module

Exists_wittVector_lift_of_normalFormOrder.lean

Nyll.AlgebraicCurves.FunctionFields.Exists_wittVector_lift_of_normalFormOrder

110 declarations indexed from sourceView source ↗

Module documentation

Exists witt Vector lift of normal Form Order

Imports4

Mathlib.Algebra.Module.TransferInstance
Mathlib.RingTheory.WittVector.Complete
Mathlib.RingTheory.WittVector.Truncated
Nyll.AlgebraicCurves.FunctionFields.Exists_lift_normalForm_structureConstants_of_smallExtension

Imported by1

Nyll.AlgebraicCurves.FunctionFields.All

structure

Table

L37 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.Table

Documentation

Structure constants of a commutative unital multiplication table.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra

Lean source · full declaration

structure Table (R : Type*) [CommRing R] (N : ℕ) where
  /-- The structure constants for multiplication in the indexed basis. -/
  γ : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R
  /-- The zeroth basis vector acts as the multiplicative identity. -/
  unit : ∀ j k, γ 0 j k = if j = k then 1 else 0
  /-- The structure constants are symmetric in the two multiplicands. -/
  comm : ∀ i j k, γ i j k = γ j i k
  /-- The structure constants satisfy the associativity equations. -/
  assoc : ∀ i j l m, ∑ k, γ i j k * γ k l m = ∑ k, γ j l k * γ i k m

def

cst

L50 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.cst

Documentation

The product of coordinate vectors determined by structure constants.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}

Lean source · statement

def cst (γ : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R) (x y : Fin (N + 1) → R) :
    Fin (N + 1) → R

theorem

cst_apply

L54 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.cst_apply

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}

Lean source · statement

theorem cst_apply (γ : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R) (x y : Fin (N + 1) → R)
    (m : Fin (N + 1)) : cst γ x y m = ∑ i, ∑ j, x i * y j * γ i j m

theorem

sum3_rot

L57 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.sum3_rot

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}

Lean source · statement

theorem sum3_rot (f : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R) :
    ∑ q, ∑ l, ∑ t, f q l t = ∑ l, ∑ t, ∑ q, f q l t

theorem

sum4_rot

L62 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.sum4_rot

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}

Lean source · statement

theorem sum4_rot (f : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R) :
    ∑ q, ∑ t, ∑ k, ∑ l, f q t k l = ∑ k, ∑ l, ∑ t, ∑ q, f q t k l

theorem

cst_cst_left

L73 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.cst_cst_left

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}

Lean source · statement

theorem cst_cst_left (γ : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R)
    (a b c : Fin (N + 1) → R) (s : Fin (N + 1)) :
    cst γ (cst γ a b) c s = ∑ k, ∑ l, ∑ t, a k * b l * c t * ∑ q, γ k l q * γ q t s

theorem

cst_cst_right

L82 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.cst_cst_right

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}

Lean source · statement

theorem cst_cst_right (γ : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R)
    (a b c : Fin (N + 1) → R) (s : Fin (N + 1)) :
    cst γ a (cst γ b c) s = ∑ k, ∑ l, ∑ t, a k * b l * c t * ∑ q, γ l t q * γ k q s

theorem

cst_comm_of

L92 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.cst_comm_of

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}

Lean source · statement

theorem cst_comm_of (γ : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R)
    (hc : ∀ i j k, γ i j k = γ j i k) (a b : Fin (N + 1) → R) : cst γ a b = cst γ b a

theorem

cst_add_left

L99 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.cst_add_left

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}

Lean source · statement

theorem cst_add_left (γ : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R) (a a' b : Fin (N + 1) → R) :
    cst γ (a + a') b = cst γ a b + cst γ a' b

theorem

cst_add_right

L104 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.cst_add_right

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}

Lean source · statement

theorem cst_add_right (γ : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R) (a b b' : Fin (N + 1) → R) :
    cst γ a (b + b') = cst γ a b + cst γ a b'

theorem

cst_smul_left

L109 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.cst_smul_left

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}

Lean source · statement

theorem cst_smul_left (γ : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R) (z : R)
    (a b : Fin (N + 1) → R) : cst γ (z • a) b = z • cst γ a b

theorem

cst_zero_left

L114 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.cst_zero_left

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}

Lean source · statement

theorem cst_zero_left (γ : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R) (b : Fin (N + 1) → R) :
    cst γ 0 b = 0

theorem

cst_single_single

L118 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.cst_single_single

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}

Lean source · full declaration

theorem cst_single_single (γ : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R) (i j : Fin (N + 1)) :
    cst γ (Pi.single i 1) (Pi.single j 1) = fun m => γ i j m := by
  funext m
  rw [cst_apply, Finset.sum_eq_single i, Finset.sum_eq_single j]
  · simp
  · intro b _ hb; simp [Pi.single_eq_of_ne hb]
  · intro h; exact absurd (Finset.mem_univ j) h
  · intro b _ hb; simp [Pi.single_eq_of_ne hb]
  · intro h; exact absurd (Finset.mem_univ i) h

theorem

cst_unit_left

L128 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.cst_unit_left

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}

Lean source · full declaration

theorem cst_unit_left (γ : Fin (N + 1) → Fin (N + 1) → Fin (N + 1) → R)
    (h1 : ∀ j k, γ 0 j k = if j = k then 1 else 0) (b : Fin (N + 1) → R) :
    cst γ (Pi.single 0 1) b = b := by
  funext m
  rw [cst_apply, Finset.sum_eq_single 0]
  · simp only [Pi.single_eq_same, one_mul, h1]
    rw [Finset.sum_eq_single m]
    · simp
    · intro j _ hj; simp [hj]
    · intro h; exact absurd (Finset.mem_univ m) h
  · intro i _ hi; simp [Pi.single_eq_of_ne hi]
  · intro h; exact absurd (Finset.mem_univ (0 : Fin (N + 1))) h

structure

TAlg

L142 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.TAlg

Documentation

The algebra with the given multiplication table.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}

Lean source · full declaration

structure TAlg (T : Table R N) where
  /-- The coordinates of an algebra element in the indexed basis. -/
  coord : Fin (N + 1) → R

theorem

ext

L150 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.TAlg.ext

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · statement

theorem ext {x y : TAlg T} (h : x.coord = y.coord) : x = y

def

equiv

L154 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.TAlg.equiv

Documentation

The coordinate equivalence of the table algebra.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · full declaration

def equiv : TAlg T ≃ (Fin (N + 1) → R) where
  toFun := coord
  invFun := TAlg.mk
  left_inv _ := rfl
  right_inv _ := rfl

instance

(anonymous instance)

L160 ↗

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · statement

instance : AddCommGroup (TAlg T)

instance

instModule

L162 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.TAlg.instModule

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · statement

instance instModule : Module R (TAlg T)

theorem

coord_add

L164 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.TAlg.coord_add

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · statement

theorem coord_add (x y : TAlg T) : (x + y).coord = x.coord + y.coord

theorem

coord_zero

L165 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.TAlg.coord_zero

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · statement

theorem coord_zero : (0 : TAlg T).coord = 0

theorem

coord_neg

L166 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.TAlg.coord_neg

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · statement

theorem coord_neg (x : TAlg T) : (-x).coord = -x.coord

theorem

coord_sub

L167 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.TAlg.coord_sub

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · statement

theorem coord_sub (x y : TAlg T) : (x - y).coord = x.coord - y.coord

theorem

coord_smul

L168 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.TAlg.coord_smul

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · statement

theorem coord_smul (z : R) (x : TAlg T) : (z • x).coord = z • x.coord

theorem

coord_mk

L169 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.TAlg.coord_mk

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · statement

theorem coord_mk (v : Fin (N + 1) → R) : (TAlg.mk v : TAlg T).coord = v

def

linearEquiv

L172 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.TAlg.linearEquiv

Documentation

The linear coordinate equivalence of the table algebra.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · statement

def linearEquiv : TAlg T ≃ₗ[R] (Fin (N + 1) → R)

theorem

linearEquiv_apply

L177 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.TAlg.linearEquiv_apply

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · statement

theorem linearEquiv_apply (x : TAlg T) : linearEquiv T x = x.coord

theorem

linearEquiv_symm_apply

L178 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.TAlg.linearEquiv_symm_apply

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · statement

theorem linearEquiv_symm_apply (v : Fin (N + 1) → R) : (linearEquiv T).symm v =
  TAlg.mk v

theorem

coord_sum

L182 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.TAlg.coord_sum

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · statement

theorem coord_sum {ι : Type*} (s : Finset ι) (f : ι → TAlg T) :
    (∑ i ∈ s, f i).coord = ∑ i ∈ s, (f i).coord

instance

(anonymous instance)

L187 ↗

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · statement

instance : Mul (TAlg T)

instance

(anonymous instance)

L189 ↗

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · statement

instance : One (TAlg T)

theorem

coord_mul

L191 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.TAlg.coord_mul

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · statement

theorem coord_mul (x y : TAlg T) : (x * y).coord = cst T.γ x.coord y.coord

theorem

coord_one

L192 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.TAlg.coord_one

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · statement

theorem coord_one : (1 : TAlg T).coord = Pi.single 0 1

theorem

mul_comm'

L194 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.TAlg.mul_comm'

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · statement

theorem mul_comm' (x y : TAlg T) : x * y = y * x

theorem

mul_assoc'

L197 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.TAlg.mul_assoc'

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · statement

theorem mul_assoc' (x y z : TAlg T) : x * y * z = x * (y * z)

theorem

one_mul'

L206 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.TAlg.one_mul'

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · statement

theorem one_mul' (x : TAlg T) : 1 * x = x

instance

instCommRing

L209 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.TAlg.instCommRing

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · full declaration

instance instCommRing : CommRing (TAlg T) where
  __ := (inferInstance : AddCommGroup (TAlg T))
  mul := (· * ·)
  one := 1
  mul_assoc := mul_assoc' T
  one_mul := one_mul' T
  mul_one x := by rw [mul_comm']; exact one_mul' T x
  zero_mul x := by ext1; simp only [coord_mul, coord_zero]; exact cst_zero_left _ _
  mul_zero x := by rw [mul_comm']; ext1; simp only [coord_mul, coord_zero]; exact cst_zero_left _ _
  left_distrib x y z := by ext1; simp only [coord_mul, coord_add]; exact cst_add_right _ _ _ _
  right_distrib x y z := by ext1; simp only [coord_mul, coord_add]; exact cst_add_left _ _ _ _
  mul_comm := mul_comm' T

theorem

smul_mul_assoc'

L222 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.TAlg.smul_mul_assoc'

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · statement

theorem smul_mul_assoc' (z : R) (x y : TAlg T) : (z • x) * y = z • (x * y)

instance

instAlgebra

L225 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.TAlg.instAlgebra

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · statement

instance instAlgebra : Algebra R (TAlg T)

def

basis

L230 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.TAlg.basis

Documentation

The coordinate basis of the table algebra.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · statement

def basis : Module.Basis (Fin (N + 1)) R (TAlg T)

theorem

basis_apply

L232 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.TAlg.basis_apply

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · statement

theorem basis_apply (i : Fin (N + 1)) : basis T i = TAlg.mk (Pi.single i 1)

theorem

coord_basis

L235 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.TAlg.coord_basis

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · statement

theorem coord_basis (i : Fin (N + 1)) : (basis T i).coord = Pi.single i 1

theorem

basis_repr_apply

L238 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.TAlg.basis_repr_apply

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · statement

theorem basis_repr_apply (x : TAlg T) (k : Fin (N + 1)) : (basis T).repr x k = x.coord k

theorem

basis_zero

L241 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.TAlg.basis_zero

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · statement

theorem basis_zero : basis T 0 = 1

theorem

basis_mul_basis_coord

L244 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.TAlg.basis_mul_basis_coord

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · full declaration

theorem basis_mul_basis_coord (i j : Fin (N + 1)) :
    (basis T i * basis T j).coord = fun m => T.γ i j m := by
  rw [coord_mul, coord_basis, coord_basis, cst_single_single]

theorem

repr_basis_mul_basis

L248 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.TAlg.repr_basis_mul_basis

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · statement

theorem repr_basis_mul_basis (i j k : Fin (N + 1)) :
    (basis T).repr (basis T i * basis T j) k = T.γ i j k

theorem

algebraMap_coord

L252 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.TAlg.algebraMap_coord

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · statement

theorem algebraMap_coord (f : R) : (algebraMap R (TAlg T) f).coord = Pi.single 0 f

theorem

eq_sum_coord_smul_basis

L255 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.TAlg.eq_sum_coord_smul_basis

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
namespace TAlg
variable (T : Table R N)

Lean source · statement

theorem eq_sum_coord_smul_basis (x : TAlg T) : x = ∑ i, x.coord i • basis T i

theorem

repr_mul_unit

L265 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.repr_mul_unit

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
section OfBasis
variable {C : Type*} [CommRing C] [Algebra R C] (e : Module.Basis (Fin (N + 1)) R C)

Lean source · full declaration

theorem repr_mul_unit (he : e 0 = 1) (j k : Fin (N + 1)) :
    e.repr (e 0 * e j) k = if j = k then 1 else 0 := by
  rw [he, one_mul, e.repr_self, Finsupp.single_apply]

theorem

repr_mul_comm

L269 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.repr_mul_comm

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
section OfBasis
variable {C : Type*} [CommRing C] [Algebra R C] (e : Module.Basis (Fin (N + 1)) R C)

Lean source · statement

theorem repr_mul_comm (i j k : Fin (N + 1)) : e.repr (e i * e j) k = e.repr (e j * e i) k

theorem

repr_mul_expand_left

L272 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.repr_mul_expand_left

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
section OfBasis
variable {C : Type*} [CommRing C] [Algebra R C] (e : Module.Basis (Fin (N + 1)) R C)

Lean source · statement

theorem repr_mul_expand_left (i j l m : Fin (N + 1)) :
    e.repr (e i * e j * e l) m = ∑ k, e.repr (e i * e j) k * e.repr (e k * e l) m

theorem

repr_mul_expand_right

L279 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.repr_mul_expand_right

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
section OfBasis
variable {C : Type*} [CommRing C] [Algebra R C] (e : Module.Basis (Fin (N + 1)) R C)

Lean source · statement

theorem repr_mul_expand_right (i j l m : Fin (N + 1)) :
    e.repr (e i * (e j * e l)) m = ∑ k, e.repr (e j * e l) k * e.repr (e i * e k) m

theorem

repr_mul_assoc

L286 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.repr_mul_assoc

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
section OfBasis
variable {C : Type*} [CommRing C] [Algebra R C] (e : Module.Basis (Fin (N + 1)) R C)

Lean source · statement

theorem repr_mul_assoc (i j l m : Fin (N + 1)) :
    ∑ k, e.repr (e i * e j) k * e.repr (e k * e l) m =
      ∑ k, e.repr (e j * e l) k * e.repr (e i * e k) m

def

tableOfBasis

L292 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.tableOfBasis

Documentation

The multiplication table in a basis whose first vector is the unit.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
section OfBasis
variable {C : Type*} [CommRing C] [Algebra R C] (e : Module.Basis (Fin (N + 1)) R C)

Lean source · full declaration

def tableOfBasis (he : e 0 = 1) : Table R N where
  γ i j k := e.repr (e i * e j) k
  unit := repr_mul_unit e he
  comm := repr_mul_comm e
  assoc := repr_mul_assoc e

theorem

tableOfBasis_γ

L298 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.tableOfBasis_γ

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}
section OfBasis
variable {C : Type*} [CommRing C] [Algebra R C] (e : Module.Basis (Fin (N + 1)) R C)

Lean source · statement

theorem tableOfBasis_γ (he : e 0 = 1) (i j k : Fin (N + 1)) :
    (tableOfBasis e he).γ i j k = e.repr (e i * e j) k

def

map

L304 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.Table.map

Documentation

Apply a ring homomorphism to the structure constants of a multiplication table.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}

Lean source · full declaration

def Table.map {R' : Type*} [CommRing R'] (T : Table R N) (f : R →+* R') : Table R' N where
  γ i j k := f (T.γ i j k)
  unit j k := by rw [T.unit]; split_ifs <;> simp
  comm i j k := by rw [T.comm]
  assoc i j l m := by
    have h := congrArg f (T.assoc i j l m)
    simpa only [map_sum, map_mul] using h

theorem

map_γ

L312 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.Table.map_γ

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section TableAlgebra
variable {R : Type*} [CommRing R] {N : ℕ}

Lean source · statement

theorem Table.map_γ {R' : Type*} [CommRing R'] (T : Table R N) (f : R →+* R')
    (i j k : Fin (N + 1)) : (T.map f).γ i j k = f (T.γ i j k)

def

rho

L324 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.rho

Documentation

The constant-coefficient homomorphism on truncated Witt vectors.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Witt
variable (p : ℕ) [hp : Fact p.Prime] (K : Type*) [Field K] [CharP K p] [PerfectRing K p]
local notation "𝕎" => WittVector p

Lean source · statement

def rho (m : ℕ) : TruncatedWittVector p (m + 1) K →+* K

theorem

rho_truncate

L333 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.rho_truncate

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Witt
variable (p : ℕ) [hp : Fact p.Prime] (K : Type*) [Field K] [CharP K p] [PerfectRing K p]
local notation "𝕎" => WittVector p
omit [CharP K p] [PerfectRing K p] in

Lean source · statement

theorem rho_truncate (m : ℕ) (x : 𝕎 K) :
    rho p K m (WittVector.truncate (m + 1) x) = x.coeff 0

theorem

rho_apply

L337 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.rho_apply

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Witt
variable (p : ℕ) [hp : Fact p.Prime] (K : Type*) [Field K] [CharP K p] [PerfectRing K p]
local notation "𝕎" => WittVector p
omit [CharP K p] [PerfectRing K p] in

Lean source · statement

theorem rho_apply (m : ℕ) (x : TruncatedWittVector p (m + 1) K) : rho p K m x = x.coeff 0

theorem

rho_surjective

L342 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.rho_surjective

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Witt
variable (p : ℕ) [hp : Fact p.Prime] (K : Type*) [Field K] [CharP K p] [PerfectRing K p]
local notation "𝕎" => WittVector p
omit [CharP K p] [PerfectRing K p] in

Lean source · statement

theorem rho_surjective (m : ℕ) : Function.Surjective (rho p K m)

theorem

rho_zero_injective

L346 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.rho_zero_injective

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Witt
variable (p : ℕ) [hp : Fact p.Prime] (K : Type*) [Field K] [CharP K p] [PerfectRing K p]
local notation "𝕎" => WittVector p
omit [CharP K p] [PerfectRing K p] in

Lean source · statement

theorem rho_zero_injective : Function.Injective (rho p K 0)

def

rhoZeroEquiv

L356 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.rhoZeroEquiv

Documentation

The ring equivalence identifying length-one truncated Witt vectors with the coefficient field.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Witt
variable (p : ℕ) [hp : Fact p.Prime] (K : Type*) [Field K] [CharP K p] [PerfectRing K p]
local notation "𝕎" => WittVector p

Lean source · statement

def rhoZeroEquiv : TruncatedWittVector p 1 K ≃+* K

theorem

rhoZeroEquiv_apply

L359 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.rhoZeroEquiv_apply

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Witt
variable (p : ℕ) [hp : Fact p.Prime] (K : Type*) [Field K] [CharP K p] [PerfectRing K p]
local notation "𝕎" => WittVector p
omit [CharP K p] [PerfectRing K p] in

Lean source · statement

theorem rhoZeroEquiv_apply (x : TruncatedWittVector p 1 K) : rhoZeroEquiv p K x = rho p K 0 x

abbrev

piT

L362 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.piT

Documentation

The homomorphism discarding the last coordinate of a truncated Witt vector.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Witt
variable (p : ℕ) [hp : Fact p.Prime] (K : Type*) [Field K] [CharP K p] [PerfectRing K p]
local notation "𝕎" => WittVector p

Lean source · statement

abbrev piT (m : ℕ) : TruncatedWittVector p (m + 2) K →+* TruncatedWittVector p (m + 1) K

theorem

piT_surjective

L365 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.piT_surjective

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Witt
variable (p : ℕ) [hp : Fact p.Prime] (K : Type*) [Field K] [CharP K p] [PerfectRing K p]
local notation "𝕎" => WittVector p
omit [CharP K p] [PerfectRing K p] in

Lean source · statement

theorem piT_surjective (m : ℕ) : Function.Surjective (piT p K m)

theorem

rho_piT

L368 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.rho_piT

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Witt
variable (p : ℕ) [hp : Fact p.Prime] (K : Type*) [Field K] [CharP K p] [PerfectRing K p]
local notation "𝕎" => WittVector p
omit [CharP K p] [PerfectRing K p] in

Lean source · statement

theorem rho_piT (m : ℕ) (a : TruncatedWittVector p (m + 2) K) :
    rho p K m (piT p K m a) = rho p K (m + 1) a

theorem

truncate_p_pow_mul_eq_zero

L373 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.truncate_p_pow_mul_eq_zero

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Witt
variable (p : ℕ) [hp : Fact p.Prime] (K : Type*) [Field K] [CharP K p] [PerfectRing K p]
local notation "𝕎" => WittVector p

Lean source · statement

theorem truncate_p_pow_mul_eq_zero (m : ℕ) (D : 𝕎 K) :
    WittVector.truncate (m + 2) ((p : 𝕎 K) ^ (m + 2) * D) = 0

theorem

piT_eq_zero_iff

L379 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.piT_eq_zero_iff

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Witt
variable (p : ℕ) [hp : Fact p.Prime] (K : Type*) [Field K] [CharP K p] [PerfectRing K p]
local notation "𝕎" => WittVector p

Lean source · statement

theorem piT_eq_zero_iff (m : ℕ) (a : TruncatedWittVector p (m + 2) K) :
    piT p K m a = 0 ↔ ((p : TruncatedWittVector p (m + 2) K) ^ (m + 1)) ∣ a

theorem

exists_eq_p_mul_of_rho_piT_eq_zero

L408 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.exists_eq_p_mul_of_rho_piT_eq_zero

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Witt
variable (p : ℕ) [hp : Fact p.Prime] (K : Type*) [Field K] [CharP K p] [PerfectRing K p]
local notation "𝕎" => WittVector p

Lean source · statement

theorem exists_eq_p_mul_of_rho_piT_eq_zero (m : ℕ) (a : TruncatedWittVector p (m + 2) K)
    (h : rho p K m (piT p K m a) = 0) :
    ∃ D : 𝕎 K, a = WittVector.truncate (m + 2) ((p : 𝕎 K) * D)

theorem

p_pow_mul_eq_zero_of_rho_piT_eq_zero

L418 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.p_pow_mul_eq_zero_of_rho_piT_eq_zero

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Witt
variable (p : ℕ) [hp : Fact p.Prime] (K : Type*) [Field K] [CharP K p] [PerfectRing K p]
local notation "𝕎" => WittVector p

Lean source · statement

theorem p_pow_mul_eq_zero_of_rho_piT_eq_zero (m : ℕ) (a : TruncatedWittVector p (m + 2) K)
    (h : rho p K m (piT p K m a) = 0) :
    (p : TruncatedWittVector p (m + 2) K) ^ (m + 1) * a = 0

theorem

isNilpotent_of_rho_piT_eq_zero

L428 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.isNilpotent_of_rho_piT_eq_zero

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Witt
variable (p : ℕ) [hp : Fact p.Prime] (K : Type*) [Field K] [CharP K p] [PerfectRing K p]
local notation "𝕎" => WittVector p

Lean source · statement

theorem isNilpotent_of_rho_piT_eq_zero (m : ℕ) (a : TruncatedWittVector p (m + 2) K)
    (h : rho p K m (piT p K m a) = 0) : IsNilpotent a

theorem

truncate_le_refl

L435 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.truncate_le_refl

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Witt
variable (p : ℕ) [hp : Fact p.Prime] (K : Type*) [Field K] [CharP K p] [PerfectRing K p]
local notation "𝕎" => WittVector p
omit [CharP K p] [PerfectRing K p] in

Lean source · statement

theorem truncate_le_refl {m : ℕ} (x : TruncatedWittVector p m K) :
    TruncatedWittVector.truncate (le_refl m) x = x

theorem

eq_of_forall_map_truncate

L440 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.eq_of_forall_map_truncate

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Witt
variable (p : ℕ) [hp : Fact p.Prime] (K : Type*) [Field K] [CharP K p] [PerfectRing K p]
local notation "𝕎" => WittVector p
omit [CharP K p] [PerfectRing K p] in

Lean source · statement

theorem eq_of_forall_map_truncate {P Q : (𝕎 K)[X]}
    (h : ∀ m : ℕ, P.map (WittVector.truncate (m + 1)) = Q.map (WittVector.truncate (m + 1))) :
    P = Q

theorem

constantCoeff_eq_rho_comp_truncate

L449 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.constantCoeff_eq_rho_comp_truncate

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Witt
variable (p : ℕ) [hp : Fact p.Prime] (K : Type*) [Field K] [CharP K p] [PerfectRing K p]
local notation "𝕎" => WittVector p
omit [CharP K p] [PerfectRing K p] in

Lean source · statement

theorem constantCoeff_eq_rho_comp_truncate :
    (WittVector.constantCoeff : 𝕎 K →+* K) = (rho p K 0).comp (WittVector.truncate (0 + 1))

structure

Datum

L464 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.Datum

Documentation

Normal-form basis data, with degree bounds and specified behavior at infinity.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Tower
variable {p : ℕ} [hp : Fact p.Prime] {K : Type u} [Field K] [IsAlgClosed K] [CharP K p]
  {n : ℕ} {B : Type v} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [Algebra K[X] B]
local notation "𝕎" => WittVector p

Lean source · full declaration

structure Datum (K : Type u) [Field K] (n : ℕ) (B : Type v) [CommRing B] [Algebra K[X] B] where
  /-- The basis of the algebra over the polynomial ring. -/
  b : Module.Basis (Fin (n + 1)) K[X] B
  /-- The degree assigned to each basis vector. -/
  d : Fin (n + 1) → ℕ
  /-- The zeroth basis vector is the multiplicative identity. -/
  hb0 : b 0 = 1
  /-- The zeroth basis vector has degree zero. -/
  hd0 : d 0 = 0
  /-- Every other basis vector has degree one or two. -/
  hd : ∀ i, i ≠ 0 → d i = 1 ∨ d i = 2
  /-- The degrees of the multiplication coefficients satisfy the assigned degree bounds. -/
  hdeg : ∀ i j k, i ≠ 0 → j ≠ 0 → ((b.repr (b i * b j)) k).natDegree ≤ d i + d j - d k
  /-- An invertible evaluation matrix splits the leading multiplication constants at infinity. -/
  hinf : ∃ τ : Fin (n + 1) → Fin (n + 1) → K,
      IsUnit (Matrix.det (Matrix.of τ)) ∧ (∀ j, τ j 0 = 1) ∧
      ∀ j i i', i ≠ 0 → i' ≠ 0 →
        τ j i * τ j i' = ∑ k, ((b.repr (b i * b i')) k).coeff (d i + d i' - d k) * τ j k

structure

Good

L487 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.Good

Documentation

The multiplication, degree, and reduction conditions required of a truncated Witt-vector lift.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Tower
variable {p : ℕ} [hp : Fact p.Prime] {K : Type u} [Field K] [IsAlgClosed K] [CharP K p]
  {n : ℕ} {B : Type v} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [Algebra K[X] B]
local notation "𝕎" => WittVector p
variable (p) (D : Datum K n B)

Lean source · full declaration

structure Good (m : ℕ)
    (γ : Fin (n + 1) → Fin (n + 1) → Fin (n + 1) → (TruncatedWittVector p (m + 1) K)[X]) :
    Prop where
  /-- The lifted zeroth basis vector acts as the multiplicative identity. -/
  unit : ∀ j k, γ 0 j k = if j = k then 1 else 0
  /-- The lifted multiplication constants are commutative. -/
  comm : ∀ i j k, γ i j k = γ j i k
  /-- The lifted multiplication constants satisfy associativity. -/
  assoc : ∀ i j l m', ∑ k, γ i j k * γ k l m' = ∑ k, γ j l k * γ i k m'
  /-- The lifted coefficients obey the original degree bounds. -/
  deg : ∀ i j k, i ≠ 0 → j ≠ 0 → (γ i j k).natDegree ≤ D.d i + D.d j - D.d k
  /-- Reduction of the lifted coefficients recovers the original multiplication table. -/
  red : ∀ i j k, (γ i j k).map (rho p K m) = D.b.repr (D.b i * D.b j) k

def

table0

L502 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.table0

Documentation

The multiplication table over length-one Witt vectors transported from the original basis.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Tower
variable {p : ℕ} [hp : Fact p.Prime] {K : Type u} [Field K] [IsAlgClosed K] [CharP K p]
  {n : ℕ} {B : Type v} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [Algebra K[X] B]
local notation "𝕎" => WittVector p
variable (p) (D : Datum K n B)

Lean source · statement

def table0 : Table ((TruncatedWittVector p 1 K)[X]) n

theorem

table0_γ

L507 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.table0_γ

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Tower
variable {p : ℕ} [hp : Fact p.Prime] {K : Type u} [Field K] [IsAlgClosed K] [CharP K p]
  {n : ℕ} {B : Type v} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [Algebra K[X] B]
local notation "𝕎" => WittVector p
variable (p) (D : Datum K n B)
omit [IsDomain B] [IsIntegrallyClosed B] in
omit [IsAlgClosed K] [CharP K p] in

Lean source · statement

theorem table0_γ (i j k : Fin (n + 1)) :
    (table0 p D).γ i j k =
      (D.b.repr (D.b i * D.b j) k).map
        ((rhoZeroEquiv p K).symm : K ≃+* TruncatedWittVector p 1 K).toRingHom

theorem

good_table0

L513 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.good_table0

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Tower
variable {p : ℕ} [hp : Fact p.Prime] {K : Type u} [Field K] [IsAlgClosed K] [CharP K p]
  {n : ℕ} {B : Type v} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [Algebra K[X] B]
local notation "𝕎" => WittVector p
variable (p) (D : Datum K n B)
omit [IsDomain B] [IsIntegrallyClosed B] in
omit [IsAlgClosed K] [CharP K p] in

Lean source · full declaration

theorem good_table0 : Good p D 0 (table0 p D).γ where
  unit := (table0 p D).unit
  comm := (table0 p D).comm
  assoc := (table0 p D).assoc
  deg i j k hi hj := by
    rw [table0_γ, Polynomial.natDegree_map_eq_of_injective (RingEquiv.injective _)]
    exact D.hdeg i j k hi hj
  red i j k := by
    rw [table0_γ, Polynomial.map_map]
    have : (rho p K 0).comp
        ((rhoZeroEquiv p K).symm : K ≃+* TruncatedWittVector p 1 K).toRingHom = RingHom.id K := by
      ext x
      change rhoZeroEquiv p K ((rhoZeroEquiv p K).symm x) = x
      exact RingEquiv.apply_symm_apply _ _
    rw [this, Polynomial.map_id]

theorem

exists_step

L529 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.exists_step

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Tower
variable {p : ℕ} [hp : Fact p.Prime] {K : Type u} [Field K] [IsAlgClosed K] [CharP K p]
  {n : ℕ} {B : Type v} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [Algebra K[X] B]
local notation "𝕎" => WittVector p
variable (p) (D : Datum K n B)

Lean source · statement

theorem exists_step (m : ℕ)
    (γ : Fin (n + 1) → Fin (n + 1) → Fin (n + 1) → (TruncatedWittVector p (m + 1) K)[X])
    (hγ : Good p D m γ) :
    ∃ γ' : Fin (n + 1) → Fin (n + 1) → Fin (n + 1) → (TruncatedWittVector p (m + 2) K)[X],
      Good p D (m + 1) γ' ∧ ∀ i j k, (γ' i j k).map (piT p K m) = γ i j k

def

stage

L548 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.stage

Documentation

The recursively chosen compatible multiplication coefficients at every truncation level.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Tower
variable {p : ℕ} [hp : Fact p.Prime] {K : Type u} [Field K] [IsAlgClosed K] [CharP K p]
  {n : ℕ} {B : Type v} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [Algebra K[X] B]
local notation "𝕎" => WittVector p
variable (p) (D : Datum K n B)

Lean source · full declaration

def stage : (m : ℕ) →
    {γ : Fin (n + 1) → Fin (n + 1) → Fin (n + 1) → (TruncatedWittVector p (m + 1) K)[X] //
      Good p D m γ}
  | 0 => ⟨(table0 p D).γ, good_table0 p D⟩
  | m + 1 => ⟨(exists_step p D m (stage m).1 (stage m).2).choose,
      (exists_step p D m (stage m).1 (stage m).2).choose_spec.1⟩

theorem

stage_succ_map

L555 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.stage_succ_map

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Tower
variable {p : ℕ} [hp : Fact p.Prime] {K : Type u} [Field K] [IsAlgClosed K] [CharP K p]
  {n : ℕ} {B : Type v} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [Algebra K[X] B]
local notation "𝕎" => WittVector p
variable (p) (D : Datum K n B)

Lean source · statement

theorem stage_succ_map (m : ℕ) (i j k : Fin (n + 1)) :
    ((stage p D (m + 1)).1 i j k).map (piT p K m) = (stage p D m).1 i j k

theorem

stage_compat

L559 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.stage_compat

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Tower
variable {p : ℕ} [hp : Fact p.Prime] {K : Type u} [Field K] [IsAlgClosed K] [CharP K p]
  {n : ℕ} {B : Type v} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [Algebra K[X] B]
local notation "𝕎" => WittVector p
variable (p) (D : Datum K n B)

Lean source · full declaration

theorem stage_compat (c : ℕ) : ∀ (e : ℕ) (i j k : Fin (n + 1)),
    ((stage p D (c + e)).1 i j k).map
        (TruncatedWittVector.truncate (by omega : c + 1 ≤ c + e + 1)) = (stage p D c).1 i j k
  | 0, i, j, k => by
    have : TruncatedWittVector.truncate (p := p) (R := K) (le_refl (c + 1)) = RingHom.id _ := by
      ext1 x; exact truncate_le_refl p K x
    change ((stage p D c).1 i j k).map (TruncatedWittVector.truncate (le_refl (c + 1))) = _
    rw [this, Polynomial.map_id]
  | e + 1, i, j, k => by
    have h1 : c + 1 ≤ c + e + 1 := by omega
    have h2 : c + e + 1 ≤ c + e + 2 := by omega
    change ((stage p D (c + e + 1)).1 i j k).map (TruncatedWittVector.truncate (h1.trans h2)) = _
    rw [← TruncatedWittVector.truncate_comp h1 h2, ← Polynomial.map_map]
    have h3 : ((stage p D (c + e + 1)).1 i j k).map (TruncatedWittVector.truncate h2) =
        (stage p D (c + e)).1 i j k := stage_succ_map p D (c + e) i j k
    rw [h3]
    exact stage_compat c e i j k

def

wlim

L578 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.wlim

Documentation

The Witt vector assembled from the compatible coefficients at all truncation levels.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Tower
variable {p : ℕ} [hp : Fact p.Prime] {K : Type u} [Field K] [IsAlgClosed K] [CharP K p]
  {n : ℕ} {B : Type v} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [Algebra K[X] B]
local notation "𝕎" => WittVector p
variable (p) (D : Datum K n B)

Lean source · statement

def wlim (i j k : Fin (n + 1)) (t : ℕ) : 𝕎 K

theorem

coeff_stage_eq

L581 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.coeff_stage_eq

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Tower
variable {p : ℕ} [hp : Fact p.Prime] {K : Type u} [Field K] [IsAlgClosed K] [CharP K p]
  {n : ℕ} {B : Type v} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [Algebra K[X] B]
local notation "𝕎" => WittVector p
variable (p) (D : Datum K n B)

Lean source · full declaration

theorem coeff_stage_eq (c e : ℕ) (i j k : Fin (n + 1)) (t : ℕ) :
    TruncatedWittVector.coeff ⟨c, by omega⟩ (((stage p D (c + e)).1 i j k).coeff t) =
      TruncatedWittVector.coeff (Fin.last c) (((stage p D c).1 i j k).coeff t) := by
  have h := congrArg (fun P : (TruncatedWittVector p (c + 1) K)[X] =>
    TruncatedWittVector.coeff (Fin.last c) (P.coeff t)) (stage_compat p D c e i j k)
  simp only [Polynomial.coeff_map, TruncatedWittVector.coeff_truncate] at h
  exact h

theorem

truncate_wlim

L589 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.truncate_wlim

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Tower
variable {p : ℕ} [hp : Fact p.Prime] {K : Type u} [Field K] [IsAlgClosed K] [CharP K p]
  {n : ℕ} {B : Type v} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [Algebra K[X] B]
local notation "𝕎" => WittVector p
variable (p) (D : Datum K n B)

Lean source · statement

theorem truncate_wlim (m : ℕ) (i j k : Fin (n + 1)) (t : ℕ) :
    WittVector.truncate (m + 1) (wlim p D i j k t) = ((stage p D m).1 i j k).coeff t

def

Γlim

L597 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.Γlim

Documentation

The limiting polynomial multiplication coefficient with its bounded range of degrees.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Tower
variable {p : ℕ} [hp : Fact p.Prime] {K : Type u} [Field K] [IsAlgClosed K] [CharP K p]
  {n : ℕ} {B : Type v} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [Algebra K[X] B]
local notation "𝕎" => WittVector p
variable (p) (D : Datum K n B)

Lean source · statement

def Γlim (i j k : Fin (n + 1)) : (𝕎 K)[X]

theorem

coeff_Γlim

L600 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.coeff_Γlim

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Tower
variable {p : ℕ} [hp : Fact p.Prime] {K : Type u} [Field K] [IsAlgClosed K] [CharP K p]
  {n : ℕ} {B : Type v} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [Algebra K[X] B]
local notation "𝕎" => WittVector p
variable (p) (D : Datum K n B)

Lean source · full declaration

theorem coeff_Γlim (i j k : Fin (n + 1)) (t : ℕ) :
    (Γlim p D i j k).coeff t = if t < 5 then wlim p D i j k t else 0 := by
  rw [Γlim, Polynomial.finsetSum_coeff]
  simp only [Polynomial.coeff_C_mul_X_pow]
  split_ifs with ht
  · rw [Finset.sum_eq_single t]
    · rw [ite_eq_left rfl]
    · intro s _ hs; rw [ite_eq_right (Ne.symm hs)]
    · intro h; exact absurd (Finset.mem_range.2 ht) h
  · refine Finset.sum_eq_zero fun s hs => ?_
    rw [ite_eq_right]
    rintro rfl
    exact ht (Finset.mem_range.1 hs)

theorem

natDegree_stage_le

L614 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.natDegree_stage_le

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Tower
variable {p : ℕ} [hp : Fact p.Prime] {K : Type u} [Field K] [IsAlgClosed K] [CharP K p]
  {n : ℕ} {B : Type v} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [Algebra K[X] B]
local notation "𝕎" => WittVector p
variable (p) (D : Datum K n B)

Lean source · statement

theorem natDegree_stage_le (m : ℕ) (i j k : Fin (n + 1)) :
    ((stage p D m).1 i j k).natDegree ≤ 4

theorem

map_truncate_Γlim

L626 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.map_truncate_Γlim

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Tower
variable {p : ℕ} [hp : Fact p.Prime] {K : Type u} [Field K] [IsAlgClosed K] [CharP K p]
  {n : ℕ} {B : Type v} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [Algebra K[X] B]
local notation "𝕎" => WittVector p
variable (p) (D : Datum K n B)

Lean source · statement

theorem map_truncate_Γlim (m : ℕ) (i j k : Fin (n + 1)) :
    (Γlim p D i j k).map (WittVector.truncate (m + 1)) = (stage p D m).1 i j k

def

tableLim

L640 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.tableLim

Documentation

The multiplication table over Witt-vector polynomials obtained from the compatible truncations.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Tower
variable {p : ℕ} [hp : Fact p.Prime] {K : Type u} [Field K] [IsAlgClosed K] [CharP K p]
  {n : ℕ} {B : Type v} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [Algebra K[X] B]
local notation "𝕎" => WittVector p
variable (p) (D : Datum K n B)

Lean source · full declaration

def tableLim : Table ((𝕎 K)[X]) n where
  γ := Γlim p D
  unit j k := by
    apply eq_of_forall_map_truncate p K
    intro m
    rw [map_truncate_Γlim, (stage p D m).2.unit]
    split_ifs <;> simp
  comm i j k := by
    apply eq_of_forall_map_truncate p K
    intro m
    rw [map_truncate_Γlim, map_truncate_Γlim, (stage p D m).2.comm]
  assoc i j l m' := by
    apply eq_of_forall_map_truncate p K
    intro m
    simp only [Polynomial.map_sum, Polynomial.map_mul, map_truncate_Γlim]
    exact (stage p D m).2.assoc i j l m'

theorem

tableLim_γ

L657 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.tableLim_γ

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Tower
variable {p : ℕ} [hp : Fact p.Prime] {K : Type u} [Field K] [IsAlgClosed K] [CharP K p]
  {n : ℕ} {B : Type v} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [Algebra K[X] B]
local notation "𝕎" => WittVector p
variable (p) (D : Datum K n B)

Lean source · statement

theorem tableLim_γ (i j k : Fin (n + 1)) : (tableLim p D).γ i j k = Γlim p D i j k

theorem

natDegree_Γlim_le

L659 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.natDegree_Γlim_le

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Tower
variable {p : ℕ} [hp : Fact p.Prime] {K : Type u} [Field K] [IsAlgClosed K] [CharP K p]
  {n : ℕ} {B : Type v} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [Algebra K[X] B]
local notation "𝕎" => WittVector p
variable (p) (D : Datum K n B)

Lean source · statement

theorem natDegree_Γlim_le (i j k : Fin (n + 1)) (hi : i ≠ 0) (hj : j ≠ 0) :
    (Γlim p D i j k).natDegree ≤ D.d i + D.d j - D.d k

theorem

map_constantCoeff_Γlim

L673 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.map_constantCoeff_Γlim

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Tower
variable {p : ℕ} [hp : Fact p.Prime] {K : Type u} [Field K] [IsAlgClosed K] [CharP K p]
  {n : ℕ} {B : Type v} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [Algebra K[X] B]
local notation "𝕎" => WittVector p
variable (p) (D : Datum K n B)

Lean source · statement

theorem map_constantCoeff_Γlim (i j k : Fin (n + 1)) :
    (Γlim p D i j k).map (WittVector.constantCoeff : 𝕎 K →+* K) = D.b.repr (D.b i * D.b j) k

abbrev

red

L678 ↗

WittLiftNF.red

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Tower
variable {p : ℕ} [hp : Fact p.Prime] {K : Type u} [Field K] [IsAlgClosed K] [CharP K p]
  {n : ℕ} {B : Type v} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [Algebra K[X] B]
local notation "𝕎" => WittVector p
variable (p) (D : Datum K n B)

Lean source · statement

abbrev _root_.WittLiftNF.red : (𝕎 K)[X] →+* K[X]

theorem

red_apply

L683 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.red_apply

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Tower
variable {p : ℕ} [hp : Fact p.Prime] {K : Type u} [Field K] [IsAlgClosed K] [CharP K p]
  {n : ℕ} {B : Type v} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [Algebra K[X] B]
local notation "𝕎" => WittVector p
variable (p) (D : Datum K n B)
open _root_.WittLiftNF
omit [IsAlgClosed K] [CharP K p] in

Lean source · statement

theorem red_apply (f : (𝕎 K)[X]) : red p f = f.map (WittVector.constantCoeff : 𝕎 K →+* K)

theorem

red_Γlim

L685 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.red_Γlim

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Tower
variable {p : ℕ} [hp : Fact p.Prime] {K : Type u} [Field K] [IsAlgClosed K] [CharP K p]
  {n : ℕ} {B : Type v} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [Algebra K[X] B]
local notation "𝕎" => WittVector p
variable (p) (D : Datum K n B)
open _root_.WittLiftNF

Lean source · statement

theorem red_Γlim (i j k : Fin (n + 1)) :
    red p ((tableLim p D).γ i j k) = D.b.repr (D.b i * D.b j) k

def

piFun

L692 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.piFun

Documentation

The reduction map on coordinates from the lifted algebra to the original basis algebra.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Tower
variable {p : ℕ} [hp : Fact p.Prime] {K : Type u} [Field K] [IsAlgClosed K] [CharP K p]
  {n : ℕ} {B : Type v} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [Algebra K[X] B]
local notation "𝕎" => WittVector p
variable (p) (D : Datum K n B)
open _root_.WittLiftNF
open scoped TAlg

Lean source · statement

def piFun (x : TAlg (tableLim p D)) : B

theorem

piFun_add

L694 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.piFun_add

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Tower
variable {p : ℕ} [hp : Fact p.Prime] {K : Type u} [Field K] [IsAlgClosed K] [CharP K p]
  {n : ℕ} {B : Type v} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [Algebra K[X] B]
local notation "𝕎" => WittVector p
variable (p) (D : Datum K n B)
open _root_.WittLiftNF
open scoped TAlg

Lean source · statement

theorem piFun_add (x y : TAlg (tableLim p D)) : piFun p D (x + y) = piFun p D x + piFun p D y

theorem

piFun_single

L697 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.piFun_single

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Tower
variable {p : ℕ} [hp : Fact p.Prime] {K : Type u} [Field K] [IsAlgClosed K] [CharP K p]
  {n : ℕ} {B : Type v} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [Algebra K[X] B]
local notation "𝕎" => WittVector p
variable (p) (D : Datum K n B)
open _root_.WittLiftNF
open scoped TAlg

Lean source · statement

theorem piFun_single (i : Fin (n + 1)) (f : (𝕎 K)[X]) :
    piFun p D (TAlg.mk (Pi.single i f)) = red p f • D.b i

theorem

piFun_one

L704 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.piFun_one

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Tower
variable {p : ℕ} [hp : Fact p.Prime] {K : Type u} [Field K] [IsAlgClosed K] [CharP K p]
  {n : ℕ} {B : Type v} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [Algebra K[X] B]
local notation "𝕎" => WittVector p
variable (p) (D : Datum K n B)
open _root_.WittLiftNF
open scoped TAlg

Lean source · statement

theorem piFun_one : piFun p D 1 = 1

theorem

b_mul_b

L708 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.b_mul_b

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Tower
variable {p : ℕ} [hp : Fact p.Prime] {K : Type u} [Field K] [IsAlgClosed K] [CharP K p]
  {n : ℕ} {B : Type v} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [Algebra K[X] B]
local notation "𝕎" => WittVector p
variable (p) (D : Datum K n B)
open _root_.WittLiftNF
open scoped TAlg
omit [IsAlgClosed K] [IsDomain B] [IsIntegrallyClosed B] in

Lean source · statement

theorem b_mul_b (i j : Fin (n + 1)) :
    D.b i * D.b j = ∑ m, D.b.repr (D.b i * D.b j) m • D.b m

theorem

piFun_mul

L712 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.piFun_mul

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Tower
variable {p : ℕ} [hp : Fact p.Prime] {K : Type u} [Field K] [IsAlgClosed K] [CharP K p]
  {n : ℕ} {B : Type v} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [Algebra K[X] B]
local notation "𝕎" => WittVector p
variable (p) (D : Datum K n B)
open _root_.WittLiftNF
open scoped TAlg

Lean source · statement

theorem piFun_mul (x y : TAlg (tableLim p D)) :
    piFun p D (x * y) = piFun p D x * piFun p D y

def

piB

L738 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.piB

Documentation

The ring homomorphism reducing the lifted algebra to the original algebra.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Tower
variable {p : ℕ} [hp : Fact p.Prime] {K : Type u} [Field K] [IsAlgClosed K] [CharP K p]
  {n : ℕ} {B : Type v} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [Algebra K[X] B]
local notation "𝕎" => WittVector p
variable (p) (D : Datum K n B)
open _root_.WittLiftNF
open scoped TAlg

Lean source · full declaration

def piB : TAlg (tableLim p D) →+* B where
  toFun := piFun p D
  map_one' := piFun_one p D
  map_mul' := piFun_mul p D
  map_zero' := by simp [piFun]
  map_add' := piFun_add p D

theorem

piB_apply

L745 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.piB_apply

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Tower
variable {p : ℕ} [hp : Fact p.Prime] {K : Type u} [Field K] [IsAlgClosed K] [CharP K p]
  {n : ℕ} {B : Type v} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [Algebra K[X] B]
local notation "𝕎" => WittVector p
variable (p) (D : Datum K n B)
open _root_.WittLiftNF
open scoped TAlg

Lean source · statement

theorem piB_apply (x : TAlg (tableLim p D)) : piB p D x = ∑ i, red p (x.coord i) • D.b i

theorem

piB_algebraMap

L747 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.piB_algebraMap

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Tower
variable {p : ℕ} [hp : Fact p.Prime] {K : Type u} [Field K] [IsAlgClosed K] [CharP K p]
  {n : ℕ} {B : Type v} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [Algebra K[X] B]
local notation "𝕎" => WittVector p
variable (p) (D : Datum K n B)
open _root_.WittLiftNF
open scoped TAlg

Lean source · statement

theorem piB_algebraMap (f : (𝕎 K)[X]) :
    piB p D (algebraMap (𝕎 K)[X] (TAlg (tableLim p D)) f) =
      algebraMap K[X] B (f.map (WittVector.constantCoeff : 𝕎 K →+* K))

theorem

piB_basis

L757 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.piB_basis

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Tower
variable {p : ℕ} [hp : Fact p.Prime] {K : Type u} [Field K] [IsAlgClosed K] [CharP K p]
  {n : ℕ} {B : Type v} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [Algebra K[X] B]
local notation "𝕎" => WittVector p
variable (p) (D : Datum K n B)
open _root_.WittLiftNF
open scoped TAlg

Lean source · statement

theorem piB_basis (i : Fin (n + 1)) : piB p D (TAlg.basis (tableLim p D) i) = D.b i

theorem

natDegree_repr_basis_mul

L762 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.natDegree_repr_basis_mul

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
noncomputable section
namespace WittLiftNF
section Tower
variable {p : ℕ} [hp : Fact p.Prime] {K : Type u} [Field K] [IsAlgClosed K] [CharP K p]
  {n : ℕ} {B : Type v} [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [Algebra K[X] B]
local notation "𝕎" => WittVector p
variable (p) (D : Datum K n B)
open _root_.WittLiftNF
open scoped TAlg

Lean source · statement

theorem natDegree_repr_basis_mul (i j k : Fin (n + 1)) (hi : i ≠ 0) (hj : j ≠ 0) :
    ((TAlg.basis (tableLim p D)).repr
        (TAlg.basis (tableLim p D) i * TAlg.basis (tableLim p D) j) k).natDegree ≤
      D.d i + D.d j - D.d k

theorem

exists_wittVector_lift_of_normalFormOrder

L777 ↗

AlgebraicCurve.exists_wittVector_lift_of_normalFormOrder

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_wittVector_lift_of_normalFormOrder
open Polynomial
universe u v
open Exists_wittVector_lift_of_normalFormOrder.WittLiftNF in
open scoped Exists_wittVector_lift_of_normalFormOrder.WittLiftNF.TAlg in

Lean source · statement

theorem _root_.AlgebraicCurve.exists_wittVector_lift_of_normalFormOrder
    (p : ℕ) [Fact p.Prime] (K : Type u) [Field K] [IsAlgClosed K] [CharP K p]
    (n : ℕ) (B : Type v) [CommRing B] [IsDomain B] [IsIntegrallyClosed B]
    [Algebra K[X] B] (b : Module.Basis (Fin (n + 1)) K[X] B) (d : Fin (n + 1) → ℕ)
    (hb0 : b 0 = 1) (hd0 : d 0 = 0) (hd : ∀ i, i ≠ 0 → d i = 1 ∨ d i = 2)
    (hdeg : ∀ i j k, i ≠ 0 → j ≠ 0 → ((b.repr (b i * b j)) k).natDegree ≤ d i + d j - d k)
    (hinf : ∃ τ : Fin (n + 1) → Fin (n + 1) → K,
      IsUnit (Matrix.det (Matrix.of τ)) ∧
      (∀ j, τ j 0 = 1) ∧
      ∀ j i i', i ≠ 0 → i' ≠ 0 →
        τ j i * τ j i' = ∑ k, ((b.repr (b i * b i')) k).coeff (d i + d i' - d k) * τ j k) :
    ∃ (Bt : Type u) (_ : CommRing Bt) (_ : Algebra (WittVector p K)[X] Bt)
      (bt : Module.Basis (Fin (n + 1)) (WittVector p K)[X] Bt) (π : Bt →+* B),
      bt 0 = 1 ∧
      (∀ i j k, i ≠ 0 → j ≠ 0 → ((bt.repr (bt i * bt j)) k).natDegree ≤ d i + d j - d k) ∧
      (∀ f : (WittVector p K)[X],
        π (algebraMap (WittVector p K)[X] Bt f) =
          algebraMap K[X] B (f.map (WittVector.constantCoeff : WittVector p K →+* K))) ∧
      (∀ i, π (bt i) = b i)

Module documentation

Exists witt Vector lift of normal Form Order

Declarations