Module

PthPowerKernel.lean

Nyll.AlgebraicCurves.Differentials.PthPowerKernel

10 declarations indexed from sourceView source ↗

Module documentation

Pth Power Kernel

Imports16

Mathlib.Algebra.CharP.Algebra
Mathlib.Algebra.CharP.Frobenius
Mathlib.Algebra.GroupWithZero.Associated
Mathlib.Algebra.Polynomial.Monic
Mathlib.Algebra.Polynomial.RingDivision
Mathlib.Algebra.Polynomial.Degree.Domain
Mathlib.Algebra.Polynomial.Degree.Operations
Mathlib.FieldTheory.Minpoly.Field
Mathlib.FieldTheory.Separable
Mathlib.FieldTheory.Perfect
Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Mathlib.RingTheory.PowerBasis
Mathlib.RingTheory.Kaehler.Basic
Mathlib.LinearAlgebra.LinearIndependent.Defs
Mathlib.Tactic.Choose
Mathlib.Tactic.Ring.RingNF

Imported by4

theorem

kw_pke_mem_of_isSeparable_of_pow_mem

L41 ↗

AlgebraicCurve.KwPke.kw_pke_mem_of_isSeparable_of_pow_mem

Source context 3 commands

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

open Polynomial IntermediateField
noncomputable section
namespace AlgebraicCurve.KwPke

Lean source · statement

theorem kw_pke_mem_of_isSeparable_of_pow_mem
    {F : Type*} [Field F] {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP F ℓ]
    (B : Subfield F) {x : F} (hxp : x ^ ℓ ∈ B) (hsep : IsSeparable B x) :
    x ∈ B

def

kw_pke_pthPowers

L95 ↗

AlgebraicCurve.KwPke.kw_pke_pthPowers

Documentation

The subfield of ℓ-th powers, defined as the image of Frobenius.

Source context 5 commands

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

open Polynomial IntermediateField
noncomputable section
namespace AlgebraicCurve.KwPke
section PthPowers
variable (F : Type*) [Field F] (ℓ : ℕ) [hℓ : Fact ℓ.Prime] [CharP F ℓ]

Lean source · statement

def kw_pke_pthPowers : Subfield F

theorem

kw_pke_mem_pthPowers_iff

L97 ↗

AlgebraicCurve.KwPke.kw_pke_mem_pthPowers_iff

Source context 5 commands

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

open Polynomial IntermediateField
noncomputable section
namespace AlgebraicCurve.KwPke
section PthPowers
variable (F : Type*) [Field F] (ℓ : ℕ) [hℓ : Fact ℓ.Prime] [CharP F ℓ]

Lean source · statement

theorem kw_pke_mem_pthPowers_iff {y : F} :
    y ∈ kw_pke_pthPowers F ℓ ↔ ∃ g : F, g ^ ℓ = y

theorem

kw_pke_prime_field_pow

L101 ↗

AlgebraicCurve.KwPke.kw_pke_prime_field_pow

Source context 5 commands

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

open Polynomial IntermediateField
noncomputable section
namespace AlgebraicCurve.KwPke
section PthPowers
variable (F : Type*) [Field F] (ℓ : ℕ) [hℓ : Fact ℓ.Prime] [CharP F ℓ]

Lean source · statement

theorem kw_pke_prime_field_pow (n : ℕ) : ((n : F)) ∈ kw_pke_pthPowers F ℓ

abbrev

kw_pke_expansionField

L118 ↗

AlgebraicCurve.KwPke.kw_pke_expansionField

Documentation

The intermediate field generated by t over the subfield of ℓ-th powers.

Source context 5 commands

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

open Polynomial IntermediateField
noncomputable section
namespace AlgebraicCurve.KwPke
section Expansion
variable {F : Type*} [Field F] {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP F ℓ]

Lean source · statement

abbrev kw_pke_expansionField (t : F) :
    IntermediateField (kw_pke_pthPowers F ℓ) F

theorem

kw_pke_hsep_of_isSeparable_adjoin

L124 ↗

AlgebraicCurve.KwPke.kw_pke_hsep_of_isSeparable_adjoin

Documentation

A separable extension of K(t) remains separable over the field generated by the ℓ-th powers and t, when the constant field is perfect.

Source context 5 commands

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

open Polynomial IntermediateField
noncomputable section
namespace AlgebraicCurve.KwPke
section Expansion
variable {F : Type*} [Field F] {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP F ℓ]

Lean source · statement

theorem kw_pke_hsep_of_isSeparable_adjoin
    {K : Type*} [Field K] [Algebra K F] [PerfectField K]
    (t : F) (hsepK : Algebra.IsSeparable (IntermediateField.adjoin K ({t} : Set F)) F) :
    ∀ x : F, IsSeparable (kw_pke_expansionField (ℓ := ℓ) t).toSubfield x

theorem

kw_pke_mem_expansionField

L166 ↗

AlgebraicCurve.KwPke.kw_pke_mem_expansionField

Source context 5 commands

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

open Polynomial IntermediateField
noncomputable section
namespace AlgebraicCurve.KwPke
section Expansion
variable {F : Type*} [Field F] {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP F ℓ]

Lean source · statement

theorem kw_pke_mem_expansionField (t : F)
    (hsep : ∀ x : F, IsSeparable (kw_pke_expansionField (ℓ := ℓ) t).toSubfield x)
    (x : F) : x ∈ (kw_pke_expansionField (ℓ := ℓ) t).toSubfield

theorem

kw_pke_isIntegral_gen

L174 ↗

AlgebraicCurve.KwPke.kw_pke_isIntegral_gen

Source context 5 commands

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

open Polynomial IntermediateField
noncomputable section
namespace AlgebraicCurve.KwPke
section Expansion
variable {F : Type*} [Field F] {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP F ℓ]

Lean source · statement

theorem kw_pke_isIntegral_gen (t : F) :
    IsIntegral (kw_pke_pthPowers F ℓ) t

theorem

kw_pke_minpoly_natDegree_le

L183 ↗

AlgebraicCurve.KwPke.kw_pke_minpoly_natDegree_le

Source context 5 commands

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

open Polynomial IntermediateField
noncomputable section
namespace AlgebraicCurve.KwPke
section Expansion
variable {F : Type*} [Field F] {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP F ℓ]

Lean source · statement

theorem kw_pke_minpoly_natDegree_le (t : F) :
    (minpoly (kw_pke_pthPowers F ℓ) t).natDegree ≤ ℓ

theorem

kw_pke_ker_d_pthPower

L204 ↗

AlgebraicCurve.KwPke.kw_pke_ker_d_pthPower

Source context 6 commands

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

open Polynomial IntermediateField
noncomputable section
namespace AlgebraicCurve.KwPke
section Expansion
variable {F : Type*} [Field F] {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP F ℓ]
variable {K : Type*} [Field K] [Algebra K F]

Lean source · statement

theorem kw_pke_ker_d_pthPower (t : F)
    (hsep : ∀ x : F, IsSeparable (kw_pke_expansionField (ℓ := ℓ) t).toSubfield x)
    (hdt : KaehlerDifferential.D K F t ≠ 0)
    {f : F} (hdf : KaehlerDifferential.D K F f = 0) :
    ∃ g : F, f = g ^ ℓ

Module documentation

Pth Power Kernel

Declarations