NYLL
Module

CartierOperator_existsUnique.lean

Nyll.AlgebraicCurves.Differentials.CartierOperator_existsUnique
6 declarations indexed from sourceView source ↗

Module documentation

Cartier Operator exists Unique

Imports6
Imported by3

Declarations

theorem

hsep_of_pDigits

L43 ↗
AlgebraicCurves.Differentials.Proofs.CartierOperator_existsUnique.AlgebraicCurve.CartierOperatorConstruction.hsep_of_pDigits
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.CartierOperator_existsUnique
attribute [-simp] AlgebraicCurve.KwCfx.kw_cfx_tau_coe AlgebraicCurve.kw_hwcd_dlog_zero
  AlgebraicCurve.kw_hwcd_mem_regularDifferentials_iff AlgebraicCurve.kw_hwcd_dlog_one
universe u v
open KaehlerDifferential AlgebraicCurve.KwPke AlgebraicCurve.KwCart
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CartierOperatorConstruction
open _root_.AlgebraicCurve
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
variable (p : ℕ) [hp : Fact p.Prime] [CharP F p]
Lean source · statement
theorem hsep_of_pDigits {t : F}
    (hdig : ∀ g : F, ∃ a : Fin p → F, g = ∑ i : Fin p, a i ^ p * t ^ (i : ℕ)) :
    ∀ x : F, IsSeparable (kw_pke_expansionField (ℓ := p) t).toSubfield x
theorem

exists_cartierOperator

L58 ↗
AlgebraicCurves.Differentials.Proofs.CartierOperator_existsUnique.AlgebraicCurve.CartierOperatorConstruction.exists_cartierOperator
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.CartierOperator_existsUnique
attribute [-simp] AlgebraicCurve.KwCfx.kw_cfx_tau_coe AlgebraicCurve.kw_hwcd_dlog_zero
  AlgebraicCurve.kw_hwcd_mem_regularDifferentials_iff AlgebraicCurve.kw_hwcd_dlog_one
universe u v
open KaehlerDifferential AlgebraicCurve.KwPke AlgebraicCurve.KwCart
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CartierOperatorConstruction
open _root_.AlgebraicCurve
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
variable (p : ℕ) [hp : Fact p.Prime] [CharP F p]
Lean source · statement
theorem exists_cartierOperator [IsCurveOver K F] {t : F} (hdt : D K F t ≠ 0)
    (hdig : ∀ g : F, ∃ a : Fin p → F, g = ∑ i : Fin p, a i ^ p * t ^ (i : ℕ)) :
    ∃ C : Ω[F⁄K] →+ Ω[F⁄K],
      (∀ (f : F) (ω : Ω[F⁄K]), C (f ^ p • ω) = f • C ω) ∧
      (∀ f : F, C (D K F f) = 0) ∧
      (∀ f : F, C (f ^ (p - 1) • D K F f) = D K F f)
theorem

cartier_pow_smul_D_eq_zero

L87 ↗
AlgebraicCurves.Differentials.Proofs.CartierOperator_existsUnique.AlgebraicCurve.CartierOperatorConstruction.cartier_pow_smul_D_eq_zero
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.CartierOperator_existsUnique
attribute [-simp] AlgebraicCurve.KwCfx.kw_cfx_tau_coe AlgebraicCurve.kw_hwcd_dlog_zero
  AlgebraicCurve.kw_hwcd_mem_regularDifferentials_iff AlgebraicCurve.kw_hwcd_dlog_one
universe u v
open KaehlerDifferential AlgebraicCurve.KwPke AlgebraicCurve.KwCart
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CartierOperatorConstruction
open _root_.AlgebraicCurve
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
variable (p : ℕ) [hp : Fact p.Prime] [CharP F p]
section Unique
variable (C : Ω[F⁄K] →+ Ω[F⁄K])
  (hC₁ : ∀ (f : F) (ω : Ω[F⁄K]), C (f ^ p • ω) = f • C ω)
  (hC₂ : ∀ f : F, C (D K F f) = 0)
  (hC₃ : ∀ f : F, C (f ^ (p - 1) • D K F f) = D K F f)
include hC₁ hC₂ in
Lean source · statement
theorem cartier_pow_smul_D_eq_zero (t : F) {i : ℕ} (hi : i + 1 < p) :
    C (t ^ i • D K F t) = 0
theorem

cartier_digits

L101 ↗
AlgebraicCurves.Differentials.Proofs.CartierOperator_existsUnique.AlgebraicCurve.CartierOperatorConstruction.cartier_digits
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.CartierOperator_existsUnique
attribute [-simp] AlgebraicCurve.KwCfx.kw_cfx_tau_coe AlgebraicCurve.kw_hwcd_dlog_zero
  AlgebraicCurve.kw_hwcd_mem_regularDifferentials_iff AlgebraicCurve.kw_hwcd_dlog_one
universe u v
open KaehlerDifferential AlgebraicCurve.KwPke AlgebraicCurve.KwCart
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CartierOperatorConstruction
open _root_.AlgebraicCurve
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
variable (p : ℕ) [hp : Fact p.Prime] [CharP F p]
section Unique
variable (C : Ω[F⁄K] →+ Ω[F⁄K])
  (hC₁ : ∀ (f : F) (ω : Ω[F⁄K]), C (f ^ p • ω) = f • C ω)
  (hC₂ : ∀ f : F, C (D K F f) = 0)
  (hC₃ : ∀ f : F, C (f ^ (p - 1) • D K F f) = D K F f)
include hC₁ hC₂ hC₃ in
Lean source · statement
theorem cartier_digits (t : F) (a : Fin p → F) :
    C ((∑ i : Fin p, a i ^ p * t ^ (i : ℕ)) • D K F t) =
      a ⟨p - 1, Nat.sub_lt hp.out.pos Nat.one_pos⟩ • D K F t
theorem

unique_of_pDigits

L116 ↗
AlgebraicCurves.Differentials.Proofs.CartierOperator_existsUnique.AlgebraicCurve.CartierOperatorConstruction.unique_of_pDigits
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.CartierOperator_existsUnique
attribute [-simp] AlgebraicCurve.KwCfx.kw_cfx_tau_coe AlgebraicCurve.kw_hwcd_dlog_zero
  AlgebraicCurve.kw_hwcd_mem_regularDifferentials_iff AlgebraicCurve.kw_hwcd_dlog_one
universe u v
open KaehlerDifferential AlgebraicCurve.KwPke AlgebraicCurve.KwCart
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CartierOperatorConstruction
open _root_.AlgebraicCurve
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
variable (p : ℕ) [hp : Fact p.Prime] [CharP F p]
Lean source · statement
theorem unique_of_pDigits [IsCurveOver K F] {t : F} (hdt : D K F t ≠ 0)
    (hdig : ∀ g : F, ∃ a : Fin p → F, g = ∑ i : Fin p, a i ^ p * t ^ (i : ℕ))
    (C C' : Ω[F⁄K] →+ Ω[F⁄K])
    (hC₁ : ∀ (f : F) (ω : Ω[F⁄K]), C (f ^ p • ω) = f • C ω)
    (hC₂ : ∀ f : F, C (D K F f) = 0)
    (hC₃ : ∀ f : F, C (f ^ (p - 1) • D K F f) = D K F f)
    (hC'₁ : ∀ (f : F) (ω : Ω[F⁄K]), C' (f ^ p • ω) = f • C' ω)
    (hC'₂ : ∀ f : F, C' (D K F f) = 0)
    (hC'₃ : ∀ f : F, C' (f ^ (p - 1) • D K F f) = D K F f) : C = C'
theorem

cartierOperator_existsUnique

L138 ↗
AlgebraicCurve.cartierOperator_existsUnique
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.CartierOperator_existsUnique
attribute [-simp] AlgebraicCurve.KwCfx.kw_cfx_tau_coe AlgebraicCurve.kw_hwcd_dlog_zero
  AlgebraicCurve.kw_hwcd_mem_regularDifferentials_iff AlgebraicCurve.kw_hwcd_dlog_one
universe u v
open KaehlerDifferential AlgebraicCurve.KwPke AlgebraicCurve.KwCart
open AlgebraicCurve.CartierOperatorConstruction in
Lean source · statement
theorem _root_.AlgebraicCurve.cartierOperator_existsUnique {K : Type u} {F : Type v} [Field K]
  [Field F]
    [Algebra K F] [AlgebraicCurve.IsCurveOver K F] (p : ℕ) [Fact p.Prime] [CharP K p]
    [PerfectField K] (x : F) [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F] :
    ∃! C : Ω[F⁄K] →+ Ω[F⁄K],
      (∀ (f : F) (ω : Ω[F⁄K]), C (f ^ p • ω) = f • C ω) ∧
      (∀ f : F, C (KaehlerDifferential.D K F f) = 0) ∧
      (∀ f : F, C (f ^ (p - 1) • KaehlerDifferential.D K F f) = KaehlerDifferential.D K F f)

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