NYLL
Module

Mathlib_FieldTheory_RatFuncImperfectionDegree.lean

Nyll.AlgebraicCurves.Foundations.FieldTheory.Mathlib_FieldTheory_RatFuncImperfectionDegree
32 declarations indexed from sourceView source ↗

Module documentation

Mathlib Field Theory Rat Func Imperfection Degree

Imports18
  • Mathlib.FieldTheory.RatFunc.IntermediateField
  • Mathlib.FieldTheory.RatFunc.Degree
  • Mathlib.FieldTheory.RatFunc.AsPolynomial
  • Mathlib.FieldTheory.RatFunc.Basic
  • Mathlib.FieldTheory.Relrank
  • Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
  • Mathlib.FieldTheory.IntermediateField.Basic
  • Mathlib.Algebra.Field.Subfield.Basic
  • Mathlib.LinearAlgebra.Dimension.Finrank
  • Mathlib.LinearAlgebra.Dimension.Finite
  • Mathlib.RingTheory.PowerBasis
  • Mathlib.Algebra.Polynomial.Expand
  • Mathlib.FieldTheory.Perfect
  • Mathlib.FieldTheory.Separable
  • Mathlib.Algebra.Field.ZMod
  • Mathlib.Data.ZMod.Basic
  • Mathlib.Data.ZMod.Defs
  • Mathlib.Tactic.Ring.RingNF
Imported by2

Declarations

theorem

finrank_toSubfield_eq

L44 ↗
IntermediateField.finrank_toSubfield_eq
Source context 4 commands

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

noncomputable section
open Polynomial
section Bridges
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem IntermediateField.finrank_toSubfield_eq (E : IntermediateField K L) :
    Module.finrank E.toSubfield L = Module.finrank E L
theorem

aeval_mem_adjoin_singleton

L51 ↗
IntermediateField.aeval_mem_adjoin_singleton
Source context 4 commands

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

noncomputable section
open Polynomial
section Bridges
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem IntermediateField.aeval_mem_adjoin_singleton (y : L) (r : Polynomial K) :
    Polynomial.aeval y r ∈ IntermediateField.adjoin K {y}
theorem

finrank_fieldRange_algebraMap

L56 ↗
Source context 4 commands

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

noncomputable section
open Polynomial
section Bridges
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem finrank_fieldRange_algebraMap (K L : Type*) [Field K] [Field L] [Algebra K L] :
    Module.finrank (algebraMap K L).fieldRange L = Module.finrank K L
theorem

finrank_map_ringEquiv

L65 ↗
Subfield.finrank_map_ringEquiv
Source context 3 commands

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

noncomputable section
open Polynomial
section Transport
Lean source · statement
theorem Subfield.finrank_map_ringEquiv {F F' : Type*} [Field F] [Field F'] (A : Subfield F)
    (e : F ≃+* F') :
    Module.finrank (A.map (e : F →+* F')) F' = Module.finrank A F
theorem

map_fieldRange_frobenius

L77 ↗
Source context 4 commands

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

noncomputable section
open Polynomial
section Transport
variable {F F' : Type*} [Field F] [Field F'] (ℓ : ℕ) [Fact ℓ.Prime]
Lean source · statement
theorem map_fieldRange_frobenius [CharP F ℓ] [CharP F' ℓ] (e : F ≃+* F') :
    ((frobenius F ℓ).fieldRange).map (e : F →+* F') = (frobenius F' ℓ).fieldRange
theorem

finrank_fieldRange_frobenius_eq_of_ringEquiv

L89 ↗
Source context 4 commands

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

noncomputable section
open Polynomial
section Transport
variable {F F' : Type*} [Field F] [Field F'] (ℓ : ℕ) [Fact ℓ.Prime]
Lean source · statement
theorem finrank_fieldRange_frobenius_eq_of_ringEquiv [CharP F ℓ] [CharP F' ℓ] (e : F ≃+* F') :
    Module.finrank (frobenius F ℓ).fieldRange F
      = Module.finrank (frobenius F' ℓ).fieldRange F'
theorem

finrank_fieldRange_frobenius_eq_of_finiteDimensional

L101 ↗
Source context 5 commands

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

noncomputable section
open Polynomial
section Engine
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable (ℓ : ℕ) [Fact ℓ.Prime] [CharP K ℓ] [CharP F ℓ]
Lean source · statement
theorem finrank_fieldRange_frobenius_eq_of_finiteDimensional [FiniteDimensional K F] :
    Module.finrank (frobenius F ℓ).fieldRange F
      = Module.finrank (frobenius K ℓ).fieldRange K
theorem

finrank_fieldRange_frobenius_eq_of_isSeparable

L145 ↗
Source context 5 commands

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

noncomputable section
open Polynomial
section Engine
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable (ℓ : ℕ) [Fact ℓ.Prime] [CharP K ℓ] [CharP F ℓ]
Lean source · statement
theorem finrank_fieldRange_frobenius_eq_of_isSeparable [FiniteDimensional K F]
    [Algebra.IsSeparable K F] :
    Module.finrank (frobenius F ℓ).fieldRange F
      = Module.finrank (frobenius K ℓ).fieldRange K
theorem

num_X_pow

L160 ↗
RatFunc.num_X_pow
Source context 5 commands

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

noncomputable section
open Polynomial
namespace RatFunc
section AnyField
variable (K : Type*) [Field K]
Lean source · statement
theorem num_X_pow (n : ℕ) : (RatFunc.X ^ n : RatFunc K).num = Polynomial.X ^ n
theorem

denom_X_pow

L163 ↗
RatFunc.denom_X_pow
Source context 5 commands

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

noncomputable section
open Polynomial
namespace RatFunc
section AnyField
variable (K : Type*) [Field K]
Lean source · statement
theorem denom_X_pow (n : ℕ) : (RatFunc.X ^ n : RatFunc K).denom = 1
theorem

intDegree_X_pow

L166 ↗
RatFunc.intDegree_X_pow
Source context 5 commands

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

noncomputable section
open Polynomial
namespace RatFunc
section AnyField
variable (K : Type*) [Field K]
Lean source · statement
theorem intDegree_X_pow (n : ℕ) : (RatFunc.X ^ n : RatFunc K).intDegree = n
theorem

X_pow_ne_C

L170 ↗
RatFunc.X_pow_ne_C
Source context 5 commands

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

noncomputable section
open Polynomial
namespace RatFunc
section AnyField
variable (K : Type*) [Field K]
Lean source · statement
theorem X_pow_ne_C {n : ℕ} (hn : n ≠ 0) (c : K) : (RatFunc.X ^ n : RatFunc K) ≠ RatFunc.C c
theorem

finrank_adjoin_X_pow

L176 ↗
RatFunc.finrank_adjoin_X_pow
Source context 5 commands

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

noncomputable section
open Polynomial
namespace RatFunc
section AnyField
variable (K : Type*) [Field K]
Lean source · statement
theorem finrank_adjoin_X_pow (n : ℕ) :
    Module.finrank (IntermediateField.adjoin K {(RatFunc.X ^ n : RatFunc K)}) (RatFunc K)
      = n
theorem

isIntegral_adjoin_X_pow

L183 ↗
RatFunc.isIntegral_adjoin_X_pow
Source context 5 commands

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

noncomputable section
open Polynomial
namespace RatFunc
section AnyField
variable (K : Type*) [Field K]
Lean source · statement
theorem isIntegral_adjoin_X_pow (n : ℕ) (hn : n ≠ 0) :
    IsIntegral (IntermediateField.adjoin K {(RatFunc.X ^ n : RatFunc K)})
      (RatFunc.X : RatFunc K)
def

powerBasisAdjoinXPow

L191 ↗
RatFunc.powerBasisAdjoinXPow
Documentation

The power basis of the rational function field over the field generated by a nonzero power of its variable.

Source context 5 commands

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

noncomputable section
open Polynomial
namespace RatFunc
section AnyField
variable (K : Type*) [Field K]
Lean source · statement
def powerBasisAdjoinXPow (n : ℕ) (hn : n ≠ 0) :
    PowerBasis (IntermediateField.adjoin K {(RatFunc.X ^ n : RatFunc K)}) (RatFunc K)
theorem

powerBasisAdjoinXPow_gen

L197 ↗
RatFunc.powerBasisAdjoinXPow_gen
Source context 5 commands

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

noncomputable section
open Polynomial
namespace RatFunc
section AnyField
variable (K : Type*) [Field K]
Lean source · statement
theorem powerBasisAdjoinXPow_gen (n : ℕ) (hn : n ≠ 0) :
    (powerBasisAdjoinXPow K n hn).gen = RatFunc.X
theorem

powerBasisAdjoinXPow_dim

L203 ↗
RatFunc.powerBasisAdjoinXPow_dim
Source context 5 commands

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

noncomputable section
open Polynomial
namespace RatFunc
section AnyField
variable (K : Type*) [Field K]
Lean source · statement
theorem powerBasisAdjoinXPow_dim (n : ℕ) (hn : n ≠ 0) :
    (powerBasisAdjoinXPow K n hn).dim = n
theorem

powerBasisAdjoinXPow_basis_apply

L207 ↗
RatFunc.powerBasisAdjoinXPow_basis_apply
Source context 5 commands

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

noncomputable section
open Polynomial
namespace RatFunc
section AnyField
variable (K : Type*) [Field K]
Lean source · statement
theorem powerBasisAdjoinXPow_basis_apply (n : ℕ) (hn : n ≠ 0)
    (i : Fin (powerBasisAdjoinXPow K n hn).dim) :
    (powerBasisAdjoinXPow K n hn).basis i = (RatFunc.X : RatFunc K) ^ (i : ℕ)
theorem

intDegree_pow

L218 ↗
RatFunc.intDegree_pow
Source context 5 commands

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

noncomputable section
open Polynomial
namespace RatFunc
section NotAPower
variable (K : Type*) [Field K]
Lean source · statement
theorem intDegree_pow (x : RatFunc K) (hx : x ≠ 0) (n : ℕ) :
    (x ^ n).intDegree = n * x.intDegree
theorem

pow_ne_X

L227 ↗
RatFunc.pow_ne_X
Source context 5 commands

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

noncomputable section
open Polynomial
namespace RatFunc
section NotAPower
variable (K : Type*) [Field K]
Lean source · statement
theorem pow_ne_X {n : ℕ} (hn : 2 ≤ n) (g : RatFunc K) : g ^ n ≠ RatFunc.X
theorem

X_notMem_fieldRange_frobenius

L240 ↗
RatFunc.X_notMem_fieldRange_frobenius
Source context 6 commands

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

noncomputable section
open Polynomial
namespace RatFunc
section NotAPower
variable (K : Type*) [Field K]
variable (ℓ : ℕ) [Fact ℓ.Prime] [CharP K ℓ]
Lean source · statement
theorem X_notMem_fieldRange_frobenius :
    (RatFunc.X : RatFunc K) ∉ (frobenius (RatFunc K) ℓ).fieldRange
theorem

fieldRange_frobenius_ne_top

L246 ↗
RatFunc.fieldRange_frobenius_ne_top
Source context 6 commands

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

noncomputable section
open Polynomial
namespace RatFunc
section NotAPower
variable (K : Type*) [Field K]
variable (ℓ : ℕ) [Fact ℓ.Prime] [CharP K ℓ]
Lean source · statement
theorem fieldRange_frobenius_ne_top :
    (frobenius (RatFunc K) ℓ).fieldRange ≠ ⊤
theorem

pow_char_aeval_X

L257 ↗
RatFunc.pow_char_aeval_X
Source context 5 commands

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

noncomputable section
open Polynomial
namespace RatFunc
section PerfectConstants
variable (K : Type*) [Field K] (ℓ : ℕ) [Fact ℓ.Prime] [CharP K ℓ]
Lean source · statement
theorem pow_char_aeval_X (r : Polynomial K) :
    (Polynomial.aeval (RatFunc.X : RatFunc K) r) ^ ℓ
      = Polynomial.aeval ((RatFunc.X ^ ℓ : RatFunc K)) (r.map (frobenius K ℓ))
theorem

mem_fieldRange_frobenius_iff

L265 ↗
RatFunc.mem_fieldRange_frobenius_iff
Source context 6 commands

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

noncomputable section
open Polynomial
namespace RatFunc
section PerfectConstants
variable (K : Type*) [Field K] (ℓ : ℕ) [Fact ℓ.Prime] [CharP K ℓ]
variable [PerfectRing K ℓ]
Lean source · statement
theorem mem_fieldRange_frobenius_iff (z : RatFunc K) :
    z ∈ (frobenius (RatFunc K) ℓ).fieldRange
      ↔ z ∈ IntermediateField.adjoin K {(RatFunc.X ^ ℓ : RatFunc K)}
theorem

fieldRange_frobenius_eq_toSubfield_adjoin

L296 ↗
RatFunc.fieldRange_frobenius_eq_toSubfield_adjoin
Source context 6 commands

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

noncomputable section
open Polynomial
namespace RatFunc
section PerfectConstants
variable (K : Type*) [Field K] (ℓ : ℕ) [Fact ℓ.Prime] [CharP K ℓ]
variable [PerfectRing K ℓ]
Lean source · statement
theorem fieldRange_frobenius_eq_toSubfield_adjoin :
    (frobenius (RatFunc K) ℓ).fieldRange
      = (IntermediateField.adjoin K {(RatFunc.X ^ ℓ : RatFunc K)}).toSubfield
theorem

finrank_fieldRange_frobenius

L303 ↗
RatFunc.finrank_fieldRange_frobenius
Source context 6 commands

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

noncomputable section
open Polynomial
namespace RatFunc
section PerfectConstants
variable (K : Type*) [Field K] (ℓ : ℕ) [Fact ℓ.Prime] [CharP K ℓ]
variable [PerfectRing K ℓ]
Lean source · statement
theorem finrank_fieldRange_frobenius :
    Module.finrank (frobenius (RatFunc K) ℓ).fieldRange (RatFunc K) = ℓ
theorem

finrank_fieldRange_of_forall_pow

L317 ↗
AlgHom.finrank_fieldRange_of_forall_pow
Source context 5 commands

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

noncomputable section
open Polynomial
section Consumer
variable {K₀ F : Type*} [Field K₀] [Field F] [Algebra K₀ F]
variable {ℓ : ℕ} [Fact ℓ.Prime] [CharP F ℓ]
Lean source · statement
theorem AlgHom.finrank_fieldRange_of_forall_pow (φ : F →ₐ[K₀] F) (hφ : ∀ x, φ x = x ^ ℓ) :
    Module.finrank φ.fieldRange F = Module.finrank (frobenius F ℓ).fieldRange F
theorem

finrank_fieldRange_eq_char_of_ringEquiv_ratFunc

L323 ↗
AlgHom.finrank_fieldRange_eq_char_of_ringEquiv_ratFunc
Source context 5 commands

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

noncomputable section
open Polynomial
section Consumer
variable {K₀ F : Type*} [Field K₀] [Field F] [Algebra K₀ F]
variable {ℓ : ℕ} [Fact ℓ.Prime] [CharP F ℓ]
Lean source · statement
theorem AlgHom.finrank_fieldRange_eq_char_of_ringEquiv_ratFunc {K : Type*} [Field K]
    [CharP K ℓ] [PerfectRing K ℓ] (e : F ≃+* RatFunc K) (φ : F →ₐ[K₀] F)
    (hφ : ∀ x, φ x = x ^ ℓ) :
    Module.finrank φ.fieldRange F = ℓ
theorem

finrank_fieldRange_eq_char_of_finiteDimensional

L331 ↗
AlgHom.finrank_fieldRange_eq_char_of_finiteDimensional
Source context 5 commands

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

noncomputable section
open Polynomial
section Consumer
variable {K₀ F : Type*} [Field K₀] [Field F] [Algebra K₀ F]
variable {ℓ : ℕ} [Fact ℓ.Prime] [CharP F ℓ]
Lean source · statement
theorem AlgHom.finrank_fieldRange_eq_char_of_finiteDimensional {K F₀ : Type*} [Field K]
    [Field F₀] [Algebra F₀ F] [FiniteDimensional F₀ F] [CharP K ℓ] [CharP F₀ ℓ]
    [PerfectRing K ℓ] (e : F₀ ≃+* RatFunc K) (φ : F →ₐ[K₀] F) (hφ : ∀ x, φ x = x ^ ℓ) :
    Module.finrank φ.fieldRange F = ℓ
theorem

finrank_fieldRange_frobenius_two

L344 ↗
RatFunc.finrank_fieldRange_frobenius_two
Source context 3 commands

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

noncomputable section
open Polynomial
section Gates
Lean source · statement
theorem RatFunc.finrank_fieldRange_frobenius_two :
    Module.finrank (frobenius (RatFunc (ZMod 2)) 2).fieldRange (RatFunc (ZMod 2)) = 2
theorem

gate_finrank_ne_one

L348 ↗
RatFunc.gate_finrank_ne_one
Source context 3 commands

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

noncomputable section
open Polynomial
section Gates
Lean source · statement
theorem RatFunc.gate_finrank_ne_one :
    Module.finrank (frobenius (RatFunc (ZMod 2)) 2).fieldRange (RatFunc (ZMod 2)) ≠ 1
theorem

gate_engine_self

L353 ↗
RatFunc.gate_engine_self
Source context 3 commands

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

noncomputable section
open Polynomial
section Gates
Lean source · statement
theorem RatFunc.gate_engine_self :
    Module.finrank (frobenius (RatFunc (ZMod 2)) 2).fieldRange (RatFunc (ZMod 2)) = 2

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