Module

Derivation_add_mulLeft_pow_char.lean

Nyll.AlgebraicCurves.Differentials.Kaehler.Derivation_add_mulLeft_pow_char

47 declarations indexed from sourceView source ↗

Module documentation

Derivation add mul Left pow char

Imports9

Mathlib.RingTheory.Derivation.Basic
Mathlib.Algebra.Polynomial.Basic
Mathlib.Algebra.Polynomial.Derivative
Mathlib.Algebra.Polynomial.Eval.Defs
Mathlib.Data.Int.GCD
Mathlib.Data.Nat.Choose.Dvd
Mathlib.Algebra.Module.NatInt
Mathlib.GroupTheory.GroupAction.Ring
Mathlib.Algebra.GroupWithZero.Action.Defs

Imported by2

def

sseq

L37 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char.Star2B.sseq

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v
namespace Star2B
variable {R : Type u} {F : Type v} [CommRing R] [CommRing F] [Algebra R F]

Lean source · full declaration

def sseq (d : Derivation R F F) (a : F) : ℕ → F
  | 0 => 1
  | m + 1 => d (sseq d a m) + a * sseq d a m

lemma

sseq_zero

L41 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char.Star2B.sseq_zero

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v
namespace Star2B
variable {R : Type u} {F : Type v} [CommRing R] [CommRing F] [Algebra R F]

Lean source · statement

lemma sseq_zero (d : Derivation R F F) (a : F) : sseq d a 0 = 1

lemma

sseq_succ

L43 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char.Star2B.sseq_succ

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v
namespace Star2B
variable {R : Type u} {F : Type v} [CommRing R] [CommRing F] [Algebra R F]

Lean source · statement

lemma sseq_succ (d : Derivation R F F) (a : F) (m : ℕ) :
    sseq d a (m + 1) = d (sseq d a m) + a * sseq d a m

lemma

mul_app

L46 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char.Star2B.mul_app

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v
namespace Star2B
variable {R : Type u} {F : Type v} [CommRing R] [CommRing F] [Algebra R F]

Lean source · statement

lemma mul_app (f g : F →ₗ[R] F) (x : F) : (f * g) x = f (g x)

lemma

mulLeft_app

L48 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char.Star2B.mulLeft_app

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v
namespace Star2B
variable {R : Type u} {F : Type v} [CommRing R] [CommRing F] [Algebra R F]

Lean source · statement

lemma mulLeft_app (a x : F) : LinearMap.mulLeft R a x = a * x

lemma

dtl_app

L50 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char.Star2B.dtl_app

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v
namespace Star2B
variable {R : Type u} {F : Type v} [CommRing R] [CommRing F] [Algebra R F]

Lean source · statement

lemma dtl_app (d : Derivation R F F) (x : F) : d.toLinearMap x = d x

lemma

key

L52 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char.Star2B.key

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v
namespace Star2B
variable {R : Type u} {F : Type v} [CommRing R] [CommRing F] [Algebra R F]

Lean source · statement

lemma key (d : Derivation R F F) (a s : F) (i : ℕ) :
    (d.toLinearMap + LinearMap.mulLeft R a) * (LinearMap.mulLeft R s * d.toLinearMap ^ i)
      = LinearMap.mulLeft R s * d.toLinearMap ^ (i + 1)
        + LinearMap.mulLeft R (d s + a * s) * d.toLinearMap ^ i

lemma

struct

L61 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char.Star2B.struct

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v
namespace Star2B
variable {R : Type u} {F : Type v} [CommRing R] [CommRing F] [Algebra R F]

Lean source · statement

lemma struct (d : Derivation R F F) (a : F) (n : ℕ) :
    (d.toLinearMap + LinearMap.mulLeft R a) ^ n
      = ∑ i ∈ Finset.range (n + 1),
          n.choose i • (LinearMap.mulLeft R (sseq d a (n - i)) * d.toLinearMap ^ i)

lemma

char_nsmul_zero

L103 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char.Star2B.char_nsmul_zero

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v
namespace Star2B
variable {R : Type u} {F : Type v} [CommRing R] [CommRing F] [Algebra R F]

Lean source · statement

lemma char_nsmul_zero (p : ℕ) [CharP F p] (x : F →ₗ[R] F) : p • x = 0

theorem

iterate_form

L107 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char.Star2B.iterate_form

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v
namespace Star2B
variable {R : Type u} {F : Type v} [CommRing R] [CommRing F] [Algebra R F]

Lean source · statement

theorem iterate_form (p : ℕ) [Fact p.Prime] [CharP F p] (d : Derivation R F F) (a : F) :
    (d.toLinearMap + LinearMap.mulLeft R a) ^ p
      = d.toLinearMap ^ p + LinearMap.mulLeft R (sseq d a p)

theorem

head_b_of_collapse

L120 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char.Star2B.head_b_of_collapse

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v
namespace Star2B
variable {R : Type u} {F : Type v} [CommRing R] [CommRing F] [Algebra R F]

Lean source · statement

theorem head_b_of_collapse (p : ℕ) [Fact p.Prime] [CharP F p] (d : Derivation R F F) (a : F)
    (hcollapse : sseq d a p = a ^ p + (d.toLinearMap ^ (p - 1)) a) :
    (d.toLinearMap + LinearMap.mulLeft R a) ^ p
      = d.toLinearMap ^ p + LinearMap.mulLeft R (a ^ p + (d.toLinearMap ^ (p - 1)) a)

lemma

mul_app2

L134 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char.Star2B.mul_app2

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v
namespace Star2B
variable {R : Type u} {F : Type v} [CommRing R] [CommRing F] [Algebra R F]
section layer2
open Polynomial

Lean source · statement

lemma mul_app2 (f g : F →ₗ[R] F) (x : F) : (f * g) x = f (g x)

lemma

mulLeft_app2

L136 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char.Star2B.mulLeft_app2

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v
namespace Star2B
variable {R : Type u} {F : Type v} [CommRing R] [CommRing F] [Algebra R F]
section layer2
open Polynomial

Lean source · statement

lemma mulLeft_app2 (a x : F) : LinearMap.mulLeft R a x = a * x

lemma

dtl_app2

L138 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char.Star2B.dtl_app2

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v
namespace Star2B
variable {R : Type u} {F : Type v} [CommRing R] [CommRing F] [Algebra R F]
section layer2
open Polynomial

Lean source · statement

lemma dtl_app2 (d : Derivation R F F) (x : F) : d.toLinearMap x = d x

lemma

mulLeft_mul2

L140 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char.Star2B.mulLeft_mul2

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v
namespace Star2B
variable {R : Type u} {F : Type v} [CommRing R] [CommRing F] [Algebra R F]
section layer2
open Polynomial

Lean source · statement

lemma mulLeft_mul2 (a b : F) :
    LinearMap.mulLeft R a * LinearMap.mulLeft R b = LinearMap.mulLeft R (a * b)

lemma

dm_rel2

L144 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char.Star2B.dm_rel2

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v
namespace Star2B
variable {R : Type u} {F : Type v} [CommRing R] [CommRing F] [Algebra R F]
section layer2
open Polynomial

Lean source · statement

lemma dm_rel2 (d : Derivation R F F) (b : F) :
    d.toLinearMap * LinearMap.mulLeft R b
      = LinearMap.mulLeft R b * d.toLinearMap + LinearMap.mulLeft R (d b)

lemma

mulLeft_pow'

L152 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char.Star2B.mulLeft_pow'

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v
namespace Star2B
variable {R : Type u} {F : Type v} [CommRing R] [CommRing F] [Algebra R F]
section layer2
open Polynomial

Lean source · statement

lemma mulLeft_pow' (a : F) (n : ℕ) :
    (LinearMap.mulLeft R a) ^ n = LinearMap.mulLeft R (a ^ n)

def

zpoly

L158 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char.Star2B.zpoly

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v
namespace Star2B
variable {R : Type u} {F : Type v} [CommRing R] [CommRing F] [Algebra R F]
section layer2
open Polynomial

Lean source · statement

def zpoly (d : Derivation R F F) (a : F) :
    Polynomial (F →ₗ[R] F)

lemma

deriv_pow_noncomm

L162 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char.Star2B.deriv_pow_noncomm

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v
namespace Star2B
variable {R : Type u} {F : Type v} [CommRing R] [CommRing F] [Algebra R F]
section layer2
open Polynomial

Lean source · statement

lemma deriv_pow_noncomm {A : Type*} [Ring A] (z : Polynomial A) (n : ℕ) :
    derivative (z ^ n)
      = ∑ i ∈ Finset.range n, z ^ i * derivative z * z ^ (n - 1 - i)

lemma

deriv_zpoly

L177 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char.Star2B.deriv_zpoly

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v
namespace Star2B
variable {R : Type u} {F : Type v} [CommRing R] [CommRing F] [Algebra R F]
section layer2
open Polynomial

Lean source · statement

lemma deriv_zpoly (d : Derivation R F F) (a : F) :
    derivative (zpoly d a) = C (LinearMap.mulLeft R a)

def

adSeq

L182 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char.Star2B.adSeq

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v
namespace Star2B
variable {R : Type u} {F : Type v} [CommRing R] [CommRing F] [Algebra R F]
section layer2
open Polynomial

Lean source · full declaration

def adSeq (z w : Polynomial (F →ₗ[R] F)) : ℕ → Polynomial (F →ₗ[R] F)
  | 0 => w
  | n + 1 => z * adSeq z w n - adSeq z w n * z

lemma

adSeq_zero

L186 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char.Star2B.adSeq_zero

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v
namespace Star2B
variable {R : Type u} {F : Type v} [CommRing R] [CommRing F] [Algebra R F]
section layer2
open Polynomial

Lean source · statement

lemma adSeq_zero (z w : Polynomial (F →ₗ[R] F)) : adSeq z w 0 = w

lemma

adSeq_succ

L188 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char.Star2B.adSeq_succ

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v
namespace Star2B
variable {R : Type u} {F : Type v} [CommRing R] [CommRing F] [Algebra R F]
section layer2
open Polynomial

Lean source · statement

lemma adSeq_succ (z w : Polynomial (F →ₗ[R] F)) (n : ℕ) :
    adSeq z w (n + 1) = z * adSeq z w n - adSeq z w n * z

lemma

ad_step

L191 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char.Star2B.ad_step

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v
namespace Star2B
variable {R : Type u} {F : Type v} [CommRing R] [CommRing F] [Algebra R F]
section layer2
open Polynomial

Lean source · statement

lemma ad_step (d : Derivation R F F) (a c : F) :
    zpoly d a * C (LinearMap.mulLeft R c) - C (LinearMap.mulLeft R c) * zpoly d a
      = C (LinearMap.mulLeft R (d c))

lemma

adSeq_deg

L215 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char.Star2B.adSeq_deg

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v
namespace Star2B
variable {R : Type u} {F : Type v} [CommRing R] [CommRing F] [Algebra R F]
section layer2
open Polynomial

Lean source · statement

lemma adSeq_deg (d : Derivation R F F) (a b : F) (k : ℕ) :
    adSeq (zpoly d a) (C (LinearMap.mulLeft R b)) k
      = C (LinearMap.mulLeft R ((d.toLinearMap ^ k) b))

lemma

adSeq_expand

L226 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char.Star2B.adSeq_expand

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v
namespace Star2B
variable {R : Type u} {F : Type v} [CommRing R] [CommRing F] [Algebra R F]
section layer2
open Polynomial

Lean source · statement

lemma adSeq_expand (z w : Polynomial (F →ₗ[R] F)) (n : ℕ) :
    adSeq z w n
      = ∑ i ∈ Finset.range (n + 1),
          ((-1 : ℤ) ^ i * (n.choose i : ℤ)) • (z ^ (n - i) * w * z ^ i)

lemma

signed_choose_int

L283 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char.Star2B.signed_choose_int

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v
namespace Star2B
variable {R : Type u} {F : Type v} [CommRing R] [CommRing F] [Algebra R F]
section layer2
open Polynomial

Lean source · statement

lemma signed_choose_int (p : ℕ) (hp : p.Prime) :
    ∀ i, i ≤ p - 1 → (p : ℤ) ∣ ((-1 : ℤ) ^ i * (((p-1).choose i) : ℤ) - 1)

lemma

mulLeft_add2

L306 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char.Star2B.mulLeft_add2

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v
namespace Star2B
variable {R : Type u} {F : Type v} [CommRing R] [CommRing F] [Algebra R F]
section layer2
open Polynomial

Lean source · statement

lemma mulLeft_add2 (a b : F) :
    LinearMap.mulLeft R (a + b) = LinearMap.mulLeft R a + LinearMap.mulLeft R b

lemma

z_natDegree_le

L310 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char.Star2B.z_natDegree_le

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v
namespace Star2B
variable {R : Type u} {F : Type v} [CommRing R] [CommRing F] [Algebra R F]
section layer2
open Polynomial

Lean source · statement

lemma z_natDegree_le (d : Derivation R F F) (a : F) : (zpoly d a).natDegree ≤ 1

lemma

W_pow_natDegree_le

L317 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char.Star2B.W_pow_natDegree_le

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v
namespace Star2B
variable {R : Type u} {F : Type v} [CommRing R] [CommRing F] [Algebra R F]
section layer2
open Polynomial

Lean source · statement

lemma W_pow_natDegree_le (d : Derivation R F F) (a : F) (n : ℕ) :
    ((zpoly d a) ^ n).natDegree ≤ n

lemma

W_coeff_top

L322 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char.Star2B.W_coeff_top

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v
namespace Star2B
variable {R : Type u} {F : Type v} [CommRing R] [CommRing F] [Algebra R F]
section layer2
open Polynomial

Lean source · statement

lemma W_coeff_top (d : Derivation R F F) (a : F) (n : ℕ) :
    ((zpoly d a) ^ n).coeff n = (LinearMap.mulLeft R a) ^ n

lemma

W_coeff_zero'

L337 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char.Star2B.W_coeff_zero'

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v
namespace Star2B
variable {R : Type u} {F : Type v} [CommRing R] [CommRing F] [Algebra R F]
section layer2
open Polynomial

Lean source · statement

lemma W_coeff_zero' (d : Derivation R F F) (a : F) (n : ℕ) :
    ((zpoly d a) ^ n).coeff 0 = d.toLinearMap ^ n

lemma

char_nsmul2

L348 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char.Star2B.char_nsmul2

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v
namespace Star2B
variable {R : Type u} {F : Type v} [CommRing R] [CommRing F] [Algebra R F]
section layer2
open Polynomial
section primepart
variable (p : ℕ) [Fact p.Prime] [CharP F p]
omit [Fact p.Prime] in

Lean source · statement

lemma char_nsmul2 (f : F →ₗ[R] F) : p • f = 0

lemma

charP_nsmul_P

L352 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char.Star2B.charP_nsmul_P

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v
namespace Star2B
variable {R : Type u} {F : Type v} [CommRing R] [CommRing F] [Algebra R F]
section layer2
open Polynomial
section primepart
variable (p : ℕ) [Fact p.Prime] [CharP F p]
omit [Fact p.Prime] in

Lean source · statement

lemma charP_nsmul_P (x : Polynomial (F →ₗ[R] F)) : p • x = 0

lemma

zsmul_eq_self_of_dvd

L356 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char.Star2B.zsmul_eq_self_of_dvd

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v
namespace Star2B
variable {R : Type u} {F : Type v} [CommRing R] [CommRing F] [Algebra R F]
section layer2
open Polynomial
section primepart
variable (p : ℕ) [Fact p.Prime] [CharP F p]
omit [Fact p.Prime] in

Lean source · statement

lemma zsmul_eq_self_of_dvd (c : ℤ) (hdvd : (p : ℤ) ∣ (c - 1))
    (x : Polynomial (F →ₗ[R] F)) : c • x = x

lemma

nsmul_cancelA

L364 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char.Star2B.nsmul_cancelA

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v
namespace Star2B
variable {R : Type u} {F : Type v} [CommRing R] [CommRing F] [Algebra R F]
section layer2
open Polynomial
section primepart
variable (p : ℕ) [Fact p.Prime] [CharP F p]

Lean source · statement

lemma nsmul_cancelA (k : ℕ) (hk : ¬ (p ∣ k)) (x : F →ₗ[R] F) (hx : k • x = 0) :
    x = 0

lemma

adSeq_expand_prime

L381 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char.Star2B.adSeq_expand_prime

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v
namespace Star2B
variable {R : Type u} {F : Type v} [CommRing R] [CommRing F] [Algebra R F]
section layer2
open Polynomial
section primepart
variable (p : ℕ) [Fact p.Prime] [CharP F p]

Lean source · statement

lemma adSeq_expand_prime (z w : Polynomial (F →ₗ[R] F)) :
    adSeq z w (p - 1) = ∑ i ∈ Finset.range p, z ^ (p - 1 - i) * w * z ^ i

lemma

deriv_W

L390 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char.Star2B.deriv_W

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v
namespace Star2B
variable {R : Type u} {F : Type v} [CommRing R] [CommRing F] [Algebra R F]
section layer2
open Polynomial
section primepart
variable (p : ℕ) [Fact p.Prime] [CharP F p]

Lean source · statement

lemma deriv_W (d : Derivation R F F) (a : F) :
    derivative ((zpoly d a) ^ p)
      = C (LinearMap.mulLeft R ((d.toLinearMap ^ (p - 1)) a))

lemma

W_coeff_succ

L405 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char.Star2B.W_coeff_succ

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v
namespace Star2B
variable {R : Type u} {F : Type v} [CommRing R] [CommRing F] [Algebra R F]
section layer2
open Polynomial
section primepart
variable (p : ℕ) [Fact p.Prime] [CharP F p]

Lean source · statement

lemma W_coeff_succ (d : Derivation R F F) (a : F) (n : ℕ) :
    ((zpoly d a) ^ p).coeff (n + 1) * ((n : F →ₗ[R] F) + 1)
      = (C (LinearMap.mulLeft R ((d.toLinearMap ^ (p - 1)) a))).coeff n

lemma

W_coeff_one

L410 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char.Star2B.W_coeff_one

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v
namespace Star2B
variable {R : Type u} {F : Type v} [CommRing R] [CommRing F] [Algebra R F]
section layer2
open Polynomial
section primepart
variable (p : ℕ) [Fact p.Prime] [CharP F p]

Lean source · statement

lemma W_coeff_one (d : Derivation R F F) (a : F) :
    ((zpoly d a) ^ p).coeff 1 = LinearMap.mulLeft R ((d.toLinearMap ^ (p - 1)) a)

lemma

W_coeff_mid

L415 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char.Star2B.W_coeff_mid

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v
namespace Star2B
variable {R : Type u} {F : Type v} [CommRing R] [CommRing F] [Algebra R F]
section layer2
open Polynomial
section primepart
variable (p : ℕ) [Fact p.Prime] [CharP F p]

Lean source · statement

lemma W_coeff_mid (d : Derivation R F F) (a : F) (n : ℕ)
    (h1 : 1 ≤ n) (h2 : n + 1 ≤ p - 1) : ((zpoly d a) ^ p).coeff (n + 1) = 0

def

evalOne

L427 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char.Star2B.evalOne

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v
namespace Star2B
variable {R : Type u} {F : Type v} [CommRing R] [CommRing F] [Algebra R F]
section layer2
open Polynomial
section primepart
variable (p : ℕ) [Fact p.Prime] [CharP F p]

Lean source · statement

def evalOne : Polynomial (F →ₗ[R] F) →+* (F →ₗ[R] F)

lemma

evalOne_apply

L430 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char.Star2B.evalOne_apply

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v
namespace Star2B
variable {R : Type u} {F : Type v} [CommRing R] [CommRing F] [Algebra R F]
section layer2
open Polynomial
section primepart
variable (p : ℕ) [Fact p.Prime] [CharP F p]

Lean source · statement

lemma evalOne_apply (q : Polynomial (F →ₗ[R] F)) :
    evalOne (R := R) (F := F) q = Polynomial.eval₂ (RingHom.id _) 1 q

lemma

evalOne_z

L433 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char.Star2B.evalOne_z

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v
namespace Star2B
variable {R : Type u} {F : Type v} [CommRing R] [CommRing F] [Algebra R F]
section layer2
open Polynomial
section primepart
variable (p : ℕ) [Fact p.Prime] [CharP F p]

Lean source · statement

lemma evalOne_z (d : Derivation R F F) (a : F) :
    evalOne (zpoly d a) = d.toLinearMap + LinearMap.mulLeft R a

lemma

evalOne_W_sum

L439 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char.Star2B.evalOne_W_sum

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v
namespace Star2B
variable {R : Type u} {F : Type v} [CommRing R] [CommRing F] [Algebra R F]
section layer2
open Polynomial
section primepart
variable (p : ℕ) [Fact p.Prime] [CharP F p]

Lean source · statement

lemma evalOne_W_sum (d : Derivation R F F) (a : F) :
    evalOne ((zpoly d a) ^ p)
      = d.toLinearMap ^ p + (LinearMap.mulLeft R a) ^ p
        + LinearMap.mulLeft R ((d.toLinearMap ^ (p - 1)) a)

theorem

hochschild_full

L473 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char.Star2B.hochschild_full

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v
namespace Star2B
variable {R : Type u} {F : Type v} [CommRing R] [CommRing F] [Algebra R F]
section layer2
open Polynomial
section primepart
variable (p : ℕ) [Fact p.Prime] [CharP F p]

Lean source · statement

theorem hochschild_full (d : Derivation R F F) (a : F) :
    (d.toLinearMap + LinearMap.mulLeft R a) ^ p
      = d.toLinearMap ^ p + LinearMap.mulLeft R (a ^ p + (d.toLinearMap ^ (p - 1)) a)

theorem

add_mulLeft_pow_char

L489 ↗

Derivation.add_mulLeft_pow_char

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs.Derivation_add_mulLeft_pow_char
universe u v

Lean source · statement

theorem _root_.Derivation.add_mulLeft_pow_char {R : Type u} {F : Type v} [CommRing R] [CommRing F]
    [Algebra R F] (p : ℕ) [Fact p.Prime] [CharP F p] (d : Derivation R F F) (a : F) :
    (d.toLinearMap + LinearMap.mulLeft R a) ^ p
      = d.toLinearMap ^ p + LinearMap.mulLeft R (a ^ p + (d.toLinearMap ^ (p - 1)) a)

Module documentation

Derivation add mul Left pow char

Declarations