NYLL
Module

Place_isSeparable_adjoin_of_ord_eq_one.lean

Nyll.AlgebraicCurves.Places.Place_isSeparable_adjoin_of_ord_eq_one
23 declarations indexed from sourceView source ↗

Module documentation

Place is Separable adjoin of ord eq one

Imports9
Imported by11

Declarations

def

frobeniusSubfield

L59 ↗
AlgebraicCurves.Places.Proofs.PlaceSeparableAdjoinOrdOne.AlgebraicCurve.SEPEngine.frobeniusSubfield
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceSeparableAdjoinOrdOne
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
  instIsScalarTowerResidueFieldRestrictPushforward
  instAlgebraResidueFieldRestrictPushforward
  instIsLocalHomRestrictInclusion
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  AlgebraicCurve.Divisor.mapRestrict_single AlgebraicCurve.Divisor.pushforward_single
  AlgebraicCurve.Place.coe_restrictInclusion AlgebraicCurve.Place.mem_fiber
  AlgebraicCurve.Place.restrict_toValuationSubring AlgebraicCurve.Divisor.degree_pushforward
  AlgebraicCurve.Place.restrictResidueMap_residue AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom
  AlgebraicCurve.Pic0.coe_pullbackDegZeroHom
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SEPEngine
open _root_.AlgebraicCurve
open IntermediateField Polynomial
Lean source · statement
def frobeniusSubfield (M : Type*) [Field M] (p : ℕ) [ExpChar M p] : Subfield M
theorem

mem_frobeniusSubfield_iff

L62 ↗
AlgebraicCurves.Places.Proofs.PlaceSeparableAdjoinOrdOne.AlgebraicCurve.SEPEngine.mem_frobeniusSubfield_iff
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceSeparableAdjoinOrdOne
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
  instIsScalarTowerResidueFieldRestrictPushforward
  instAlgebraResidueFieldRestrictPushforward
  instIsLocalHomRestrictInclusion
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  AlgebraicCurve.Divisor.mapRestrict_single AlgebraicCurve.Divisor.pushforward_single
  AlgebraicCurve.Place.coe_restrictInclusion AlgebraicCurve.Place.mem_fiber
  AlgebraicCurve.Place.restrict_toValuationSubring AlgebraicCurve.Divisor.degree_pushforward
  AlgebraicCurve.Place.restrictResidueMap_residue AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom
  AlgebraicCurve.Pic0.coe_pullbackDegZeroHom
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SEPEngine
open _root_.AlgebraicCurve
open IntermediateField Polynomial
Lean source · statement
theorem mem_frobeniusSubfield_iff {M : Type*} [Field M] (p : ℕ) [ExpChar M p] {a : M} :
    a ∈ frobeniusSubfield M p ↔ ∃ b : M, b ^ p = a
theorem

pow_mem_frobeniusSubfield

L66 ↗
AlgebraicCurves.Places.Proofs.PlaceSeparableAdjoinOrdOne.AlgebraicCurve.SEPEngine.pow_mem_frobeniusSubfield
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceSeparableAdjoinOrdOne
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
  instIsScalarTowerResidueFieldRestrictPushforward
  instAlgebraResidueFieldRestrictPushforward
  instIsLocalHomRestrictInclusion
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  AlgebraicCurve.Divisor.mapRestrict_single AlgebraicCurve.Divisor.pushforward_single
  AlgebraicCurve.Place.coe_restrictInclusion AlgebraicCurve.Place.mem_fiber
  AlgebraicCurve.Place.restrict_toValuationSubring AlgebraicCurve.Divisor.degree_pushforward
  AlgebraicCurve.Place.restrictResidueMap_residue AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom
  AlgebraicCurve.Pic0.coe_pullbackDegZeroHom
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SEPEngine
open _root_.AlgebraicCurve
open IntermediateField Polynomial
Lean source · statement
theorem pow_mem_frobeniusSubfield {M : Type*} [Field M] (p : ℕ) [ExpChar M p] (a : M) :
    a ^ p ∈ frobeniusSubfield M p
def

frobeniusRingEquivRange

L69 ↗
AlgebraicCurves.Places.Proofs.PlaceSeparableAdjoinOrdOne.AlgebraicCurve.SEPEngine.frobeniusRingEquivRange
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceSeparableAdjoinOrdOne
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
  instIsScalarTowerResidueFieldRestrictPushforward
  instAlgebraResidueFieldRestrictPushforward
  instIsLocalHomRestrictInclusion
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  AlgebraicCurve.Divisor.mapRestrict_single AlgebraicCurve.Divisor.pushforward_single
  AlgebraicCurve.Place.coe_restrictInclusion AlgebraicCurve.Place.mem_fiber
  AlgebraicCurve.Place.restrict_toValuationSubring AlgebraicCurve.Divisor.degree_pushforward
  AlgebraicCurve.Place.restrictResidueMap_residue AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom
  AlgebraicCurve.Pic0.coe_pullbackDegZeroHom
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SEPEngine
open _root_.AlgebraicCurve
open IntermediateField Polynomial
Lean source · statement
def frobeniusRingEquivRange (M : Type*) [Field M] (p : ℕ) [ExpChar M p] :
    M ≃+* frobeniusSubfield M p
theorem

frobeniusRingEquivRange_apply

L75 ↗
AlgebraicCurves.Places.Proofs.PlaceSeparableAdjoinOrdOne.AlgebraicCurve.SEPEngine.frobeniusRingEquivRange_apply
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceSeparableAdjoinOrdOne
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
  instIsScalarTowerResidueFieldRestrictPushforward
  instAlgebraResidueFieldRestrictPushforward
  instIsLocalHomRestrictInclusion
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  AlgebraicCurve.Divisor.mapRestrict_single AlgebraicCurve.Divisor.pushforward_single
  AlgebraicCurve.Place.coe_restrictInclusion AlgebraicCurve.Place.mem_fiber
  AlgebraicCurve.Place.restrict_toValuationSubring AlgebraicCurve.Divisor.degree_pushforward
  AlgebraicCurve.Place.restrictResidueMap_residue AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom
  AlgebraicCurve.Pic0.coe_pullbackDegZeroHom
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SEPEngine
open _root_.AlgebraicCurve
open IntermediateField Polynomial
Lean source · statement
theorem frobeniusRingEquivRange_apply (M : Type*) [Field M] (p : ℕ) [ExpChar M p]
    (a : M) : ((frobeniusRingEquivRange M p a : frobeniusSubfield M p) : M) = a ^ p
abbrev

frobeniusSubfieldImageInM

L82 ↗
AlgebraicCurves.Places.Proofs.PlaceSeparableAdjoinOrdOne.AlgebraicCurve.SEPEngine.frobeniusSubfieldImageInM
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceSeparableAdjoinOrdOne
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
  instIsScalarTowerResidueFieldRestrictPushforward
  instAlgebraResidueFieldRestrictPushforward
  instIsLocalHomRestrictInclusion
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  AlgebraicCurve.Divisor.mapRestrict_single AlgebraicCurve.Divisor.pushforward_single
  AlgebraicCurve.Place.coe_restrictInclusion AlgebraicCurve.Place.mem_fiber
  AlgebraicCurve.Place.restrict_toValuationSubring AlgebraicCurve.Divisor.degree_pushforward
  AlgebraicCurve.Place.restrictResidueMap_residue AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom
  AlgebraicCurve.Pic0.coe_pullbackDegZeroHom
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SEPEngine
open _root_.AlgebraicCurve
open IntermediateField Polynomial
section Transport
variable {E M : Type*} [Field E] [Field M] [Algebra E M] (p : ℕ) [ExpChar E p] [ExpChar M p]
Lean source · statement
abbrev frobeniusSubfieldImageInM : Subfield M
theorem

frobeniusSubfieldImageInM_le_algebraMapRange

L85 ↗
AlgebraicCurves.Places.Proofs.PlaceSeparableAdjoinOrdOne.AlgebraicCurve.SEPEngine.frobeniusSubfieldImageInM_le_algebraMapRange
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceSeparableAdjoinOrdOne
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
  instIsScalarTowerResidueFieldRestrictPushforward
  instAlgebraResidueFieldRestrictPushforward
  instIsLocalHomRestrictInclusion
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  AlgebraicCurve.Divisor.mapRestrict_single AlgebraicCurve.Divisor.pushforward_single
  AlgebraicCurve.Place.coe_restrictInclusion AlgebraicCurve.Place.mem_fiber
  AlgebraicCurve.Place.restrict_toValuationSubring AlgebraicCurve.Divisor.degree_pushforward
  AlgebraicCurve.Place.restrictResidueMap_residue AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom
  AlgebraicCurve.Pic0.coe_pullbackDegZeroHom
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SEPEngine
open _root_.AlgebraicCurve
open IntermediateField Polynomial
section Transport
variable {E M : Type*} [Field E] [Field M] [Algebra E M] (p : ℕ) [ExpChar E p] [ExpChar M p]
omit [ExpChar M p] in
Lean source · statement
theorem frobeniusSubfieldImageInM_le_algebraMapRange :
    frobeniusSubfieldImageInM (E := E) (M := M) p ≤ (algebraMap E M).fieldRange
theorem

frobeniusSubfieldImageInM_le_frobeniusSubfield

L89 ↗
AlgebraicCurves.Places.Proofs.PlaceSeparableAdjoinOrdOne.AlgebraicCurve.SEPEngine.frobeniusSubfieldImageInM_le_frobeniusSubfield
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceSeparableAdjoinOrdOne
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
  instIsScalarTowerResidueFieldRestrictPushforward
  instAlgebraResidueFieldRestrictPushforward
  instIsLocalHomRestrictInclusion
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  AlgebraicCurve.Divisor.mapRestrict_single AlgebraicCurve.Divisor.pushforward_single
  AlgebraicCurve.Place.coe_restrictInclusion AlgebraicCurve.Place.mem_fiber
  AlgebraicCurve.Place.restrict_toValuationSubring AlgebraicCurve.Divisor.degree_pushforward
  AlgebraicCurve.Place.restrictResidueMap_residue AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom
  AlgebraicCurve.Pic0.coe_pullbackDegZeroHom
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SEPEngine
open _root_.AlgebraicCurve
open IntermediateField Polynomial
section Transport
variable {E M : Type*} [Field E] [Field M] [Algebra E M] (p : ℕ) [ExpChar E p] [ExpChar M p]
Lean source · statement
theorem frobeniusSubfieldImageInM_le_frobeniusSubfield :
    frobeniusSubfieldImageInM (E := E) (M := M) p ≤ frobeniusSubfield M p
theorem

comap_frobenius_frobeniusSubfield

L94 ↗
AlgebraicCurves.Places.Proofs.PlaceSeparableAdjoinOrdOne.AlgebraicCurve.SEPEngine.comap_frobenius_frobeniusSubfield
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceSeparableAdjoinOrdOne
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
  instIsScalarTowerResidueFieldRestrictPushforward
  instAlgebraResidueFieldRestrictPushforward
  instIsLocalHomRestrictInclusion
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  AlgebraicCurve.Divisor.mapRestrict_single AlgebraicCurve.Divisor.pushforward_single
  AlgebraicCurve.Place.coe_restrictInclusion AlgebraicCurve.Place.mem_fiber
  AlgebraicCurve.Place.restrict_toValuationSubring AlgebraicCurve.Divisor.degree_pushforward
  AlgebraicCurve.Place.restrictResidueMap_residue AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom
  AlgebraicCurve.Pic0.coe_pullbackDegZeroHom
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SEPEngine
open _root_.AlgebraicCurve
open IntermediateField Polynomial
section Transport
variable {E M : Type*} [Field E] [Field M] [Algebra E M] (p : ℕ) [ExpChar E p] [ExpChar M p]
Lean source · statement
theorem comap_frobenius_frobeniusSubfield :
    (frobeniusSubfield M p).comap (frobenius M p) = ⊤
theorem

comap_frobenius_frobeniusSubfieldImageInM

L100 ↗
AlgebraicCurves.Places.Proofs.PlaceSeparableAdjoinOrdOne.AlgebraicCurve.SEPEngine.comap_frobenius_frobeniusSubfieldImageInM
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceSeparableAdjoinOrdOne
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
  instIsScalarTowerResidueFieldRestrictPushforward
  instAlgebraResidueFieldRestrictPushforward
  instIsLocalHomRestrictInclusion
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  AlgebraicCurve.Divisor.mapRestrict_single AlgebraicCurve.Divisor.pushforward_single
  AlgebraicCurve.Place.coe_restrictInclusion AlgebraicCurve.Place.mem_fiber
  AlgebraicCurve.Place.restrict_toValuationSubring AlgebraicCurve.Divisor.degree_pushforward
  AlgebraicCurve.Place.restrictResidueMap_residue AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom
  AlgebraicCurve.Pic0.coe_pullbackDegZeroHom
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SEPEngine
open _root_.AlgebraicCurve
open IntermediateField Polynomial
section Transport
variable {E M : Type*} [Field E] [Field M] [Algebra E M] (p : ℕ) [ExpChar E p] [ExpChar M p]
Lean source · statement
theorem comap_frobenius_frobeniusSubfieldImageInM :
    (frobeniusSubfieldImageInM (E := E) (M := M) p).comap (frobenius M p) =
      (algebraMap E M).fieldRange
theorem

finrank_algebraMapRange_eq

L109 ↗
AlgebraicCurves.Places.Proofs.PlaceSeparableAdjoinOrdOne.AlgebraicCurve.SEPEngine.finrank_algebraMapRange_eq
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceSeparableAdjoinOrdOne
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
  instIsScalarTowerResidueFieldRestrictPushforward
  instAlgebraResidueFieldRestrictPushforward
  instIsLocalHomRestrictInclusion
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  AlgebraicCurve.Divisor.mapRestrict_single AlgebraicCurve.Divisor.pushforward_single
  AlgebraicCurve.Place.coe_restrictInclusion AlgebraicCurve.Place.mem_fiber
  AlgebraicCurve.Place.restrict_toValuationSubring AlgebraicCurve.Divisor.degree_pushforward
  AlgebraicCurve.Place.restrictResidueMap_residue AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom
  AlgebraicCurve.Pic0.coe_pullbackDegZeroHom
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SEPEngine
open _root_.AlgebraicCurve
open IntermediateField Polynomial
section Transport
variable {E M : Type*} [Field E] [Field M] [Algebra E M] (p : ℕ) [ExpChar E p] [ExpChar M p]
Lean source · statement
theorem finrank_algebraMapRange_eq :
    Module.finrank (↥(algebraMap E M).fieldRange) M = Module.finrank E M
theorem

finrank_frobeniusSubfield_eq

L122 ↗
AlgebraicCurves.Places.Proofs.PlaceSeparableAdjoinOrdOne.AlgebraicCurve.SEPEngine.finrank_frobeniusSubfield_eq
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceSeparableAdjoinOrdOne
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
  instIsScalarTowerResidueFieldRestrictPushforward
  instAlgebraResidueFieldRestrictPushforward
  instIsLocalHomRestrictInclusion
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  AlgebraicCurve.Divisor.mapRestrict_single AlgebraicCurve.Divisor.pushforward_single
  AlgebraicCurve.Place.coe_restrictInclusion AlgebraicCurve.Place.mem_fiber
  AlgebraicCurve.Place.restrict_toValuationSubring AlgebraicCurve.Divisor.degree_pushforward
  AlgebraicCurve.Place.restrictResidueMap_residue AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom
  AlgebraicCurve.Pic0.coe_pullbackDegZeroHom
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SEPEngine
open _root_.AlgebraicCurve
open IntermediateField Polynomial
section Transport
variable {E M : Type*} [Field E] [Field M] [Algebra E M] (p : ℕ) [ExpChar E p] [ExpChar M p]
Lean source · statement
theorem finrank_frobeniusSubfield_eq [FiniteDimensional E M]
    [FiniteDimensional (frobeniusSubfield E p) E] :
    Module.finrank (frobeniusSubfield M p) M = Module.finrank (frobeniusSubfield E p) E
theorem

pDigits_linearIndependent

L163 ↗
AlgebraicCurves.Places.Proofs.PlaceSeparableAdjoinOrdOne.AlgebraicCurve.SEPEngine.pDigits_linearIndependent
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceSeparableAdjoinOrdOne
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
  instIsScalarTowerResidueFieldRestrictPushforward
  instAlgebraResidueFieldRestrictPushforward
  instIsLocalHomRestrictInclusion
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  AlgebraicCurve.Divisor.mapRestrict_single AlgebraicCurve.Divisor.pushforward_single
  AlgebraicCurve.Place.coe_restrictInclusion AlgebraicCurve.Place.mem_fiber
  AlgebraicCurve.Place.restrict_toValuationSubring AlgebraicCurve.Divisor.degree_pushforward
  AlgebraicCurve.Place.restrictResidueMap_residue AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom
  AlgebraicCurve.Pic0.coe_pullbackDegZeroHom
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SEPEngine
open _root_.AlgebraicCurve
open IntermediateField Polynomial
section LinearIndependence
variable {M : Type*} [Field M] (p : ℕ) [hp : Fact p.Prime] [CharP M p]
Lean source · full declaration
theorem pDigits_linearIndependent {t : M} (htp : ∀ a : M, a ^ p ≠ t) :
    haveI : ExpChar M p := ExpChar.prime hp.out
    LinearIndependent (frobeniusSubfield M p)
      (fun i : Fin p ↦ (t ^ (i : ℕ) : M)) := by
  have : ExpChar M p := ExpChar.prime hp.out
  have htp' : ∀ c : frobeniusSubfield M p, c ^ p ≠
      (⟨t ^ p, pow_mem_frobeniusSubfield p t⟩ : frobeniusSubfield M p) := by
    rintro ⟨_, b, rfl⟩ hcp
    refine htp b ((frobenius M p).injective ?_)
    have hcp' := congrArg (fun z : frobeniusSubfield M p ↦ (z : M)) hcp
    push_cast at hcp'
    simpa only [frobenius_def] using hcp'
  have hirr : Irreducible (X ^ p - C (⟨t ^ p, pow_mem_frobeniusSubfield p t⟩ :
      frobeniusSubfield M p)) :=
    X_pow_sub_C_irreducible_of_prime hp.out htp'
  have hroot : (aeval (R := ↥(frobeniusSubfield M p)) t)
      (X ^ p - C (⟨t ^ p, pow_mem_frobeniusSubfield p t⟩ : frobeniusSubfield M p)) = 0 := by
    simp only [map_sub, map_pow, aeval_X, aeval_C]
    exact sub_self _
  have hmon : (X ^ p - C (⟨t ^ p, pow_mem_frobeniusSubfield p t⟩ :
      frobeniusSubfield M p)).Monic := monic_X_pow_sub_C _ hp.out.ne_zero
  have hmp : X ^ p - C (⟨t ^ p, pow_mem_frobeniusSubfield p t⟩ : frobeniusSubfield M p) =
      minpoly (↥(frobeniusSubfield M p)) t :=
    minpoly.eq_of_irreducible_of_monic hirr hroot hmon
  have hdeg : (minpoly (↥(frobeniusSubfield M p)) t).natDegree = p := by
    rw [← hmp, natDegree_X_pow_sub_C]
  have hli := linearIndependent_pow (K := ↥(frobeniusSubfield M p)) t
  rw [hdeg] at hli
  exact hli
abbrev

genT

L202 ↗
AlgebraicCurves.Places.Proofs.PlaceSeparableAdjoinOrdOne.AlgebraicCurve.SEPEngine.genT
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceSeparableAdjoinOrdOne
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
  instIsScalarTowerResidueFieldRestrictPushforward
  instAlgebraResidueFieldRestrictPushforward
  instIsLocalHomRestrictInclusion
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  AlgebraicCurve.Divisor.mapRestrict_single AlgebraicCurve.Divisor.pushforward_single
  AlgebraicCurve.Place.coe_restrictInclusion AlgebraicCurve.Place.mem_fiber
  AlgebraicCurve.Place.restrict_toValuationSubring AlgebraicCurve.Divisor.degree_pushforward
  AlgebraicCurve.Place.restrictResidueMap_residue AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom
  AlgebraicCurve.Pic0.coe_pullbackDegZeroHom
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SEPEngine
open _root_.AlgebraicCurve
open IntermediateField Polynomial
section AdjoinIndex
open scoped IntermediateField
variable {K M : Type*} [Field K] [Field M] [Algebra K M]
  (p : ℕ) [hp : Fact p.Prime] [CharP K p]
Lean source · statement
abbrev genT (t : M) : ↥K⟮t⟯
theorem

genT_not_pow

L204 ↗
AlgebraicCurves.Places.Proofs.PlaceSeparableAdjoinOrdOne.AlgebraicCurve.SEPEngine.genT_not_pow
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceSeparableAdjoinOrdOne
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
  instIsScalarTowerResidueFieldRestrictPushforward
  instAlgebraResidueFieldRestrictPushforward
  instIsLocalHomRestrictInclusion
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  AlgebraicCurve.Divisor.mapRestrict_single AlgebraicCurve.Divisor.pushforward_single
  AlgebraicCurve.Place.coe_restrictInclusion AlgebraicCurve.Place.mem_fiber
  AlgebraicCurve.Place.restrict_toValuationSubring AlgebraicCurve.Divisor.degree_pushforward
  AlgebraicCurve.Place.restrictResidueMap_residue AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom
  AlgebraicCurve.Pic0.coe_pullbackDegZeroHom
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SEPEngine
open _root_.AlgebraicCurve
open IntermediateField Polynomial
section AdjoinIndex
open scoped IntermediateField
variable {K M : Type*} [Field K] [Field M] [Algebra K M]
  (p : ℕ) [hp : Fact p.Prime] [CharP K p]
omit [CharP K p] in
Lean source · statement
theorem genT_not_pow (t : M) (htr : Transcendental K t) (a : ↥K⟮t⟯) :
    a ^ p ≠ genT t
theorem

adjoin_genT_over_frobeniusSubfield

L241 ↗
AlgebraicCurves.Places.Proofs.PlaceSeparableAdjoinOrdOne.AlgebraicCurve.SEPEngine.adjoin_genT_over_frobeniusSubfield
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceSeparableAdjoinOrdOne
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
  instIsScalarTowerResidueFieldRestrictPushforward
  instAlgebraResidueFieldRestrictPushforward
  instIsLocalHomRestrictInclusion
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  AlgebraicCurve.Divisor.mapRestrict_single AlgebraicCurve.Divisor.pushforward_single
  AlgebraicCurve.Place.coe_restrictInclusion AlgebraicCurve.Place.mem_fiber
  AlgebraicCurve.Place.restrict_toValuationSubring AlgebraicCurve.Divisor.degree_pushforward
  AlgebraicCurve.Place.restrictResidueMap_residue AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom
  AlgebraicCurve.Pic0.coe_pullbackDegZeroHom
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SEPEngine
open _root_.AlgebraicCurve
open IntermediateField Polynomial
section AdjoinIndex
open scoped IntermediateField
variable {K M : Type*} [Field K] [Field M] [Algebra K M]
  (p : ℕ) [hp : Fact p.Prime] [CharP K p]
Lean source · full declaration
theorem adjoin_genT_over_frobeniusSubfield [PerfectField K] (t : M) :
    haveI : ExpChar (↥K⟮t⟯) p :=
      expChar_of_injective_algebraMap (algebraMap K _).injective p
    (IntermediateField.adjoin (↥(frobeniusSubfield (↥K⟮t⟯) p)) {genT t} :
        IntermediateField _ (↥K⟮t⟯)) = ⊤ := by
  have : ExpChar (↥K⟮t⟯) p :=
    expChar_of_injective_algebraMap (algebraMap K _).injective p
  rw [eq_top_iff]
  intro x _
  obtain ⟨r, s, hrs⟩ := (IntermediateField.mem_adjoin_simple_iff K _).mp x.2
  have hrs' : x = aeval (genT t) r / aeval (genT t) s := by
    apply Subtype.ext
    rw [hrs]
    push_cast
    exact congrArg₂ _
      (IntermediateField.AdjoinSimple.coe_aeval_gen_apply (F := K) (α := t) r).symm
      (IntermediateField.AdjoinSimple.coe_aeval_gen_apply (F := K) (α := t) s).symm
  rw [hrs']
  have hK : ∀ c : K, (algebraMap K (↥K⟮t⟯)) c ∈ (frobeniusSubfield (↥K⟮t⟯) p : Subfield _) := by
    intro c
    obtain ⟨c', hc'⟩ := (frobeniusEquiv K p).surjective c
    exact ⟨algebraMap K _ c', by
      rw [← hc']; simp only [frobenius_def, map_pow, frobeniusEquiv_apply, frobenius_def]⟩
  have haeval : ∀ q : K[X], aeval (genT t) q ∈
      (IntermediateField.adjoin (↥(frobeniusSubfield (↥K⟮t⟯) p)) {genT t} :
        IntermediateField _ (↥K⟮t⟯)) := by
    intro q
    induction q using Polynomial.induction_on with
    | C c =>
      simp only [aeval_C]
      exact IntermediateField.algebraMap_mem _ (⟨_, hK c⟩ : ↥(frobeniusSubfield (↥K⟮t⟯) p))
    | add f g hf hg => simpa only [map_add] using add_mem hf hg
    | monomial n c _ =>
      simp only [map_mul, aeval_C, map_pow, aeval_X]
      exact mul_mem (IntermediateField.algebraMap_mem _
          (⟨_, hK c⟩ : ↥(frobeniusSubfield (↥K⟮t⟯) p)))
        (pow_mem (IntermediateField.mem_adjoin_simple_self _ _) _)
  exact div_mem (haeval r) (haeval s)
theorem

finrank_frobeniusSubfield_adjoin_transcendental

L280 ↗
AlgebraicCurves.Places.Proofs.PlaceSeparableAdjoinOrdOne.AlgebraicCurve.SEPEngine.finrank_frobeniusSubfield_adjoin_transcendental
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceSeparableAdjoinOrdOne
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
  instIsScalarTowerResidueFieldRestrictPushforward
  instAlgebraResidueFieldRestrictPushforward
  instIsLocalHomRestrictInclusion
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  AlgebraicCurve.Divisor.mapRestrict_single AlgebraicCurve.Divisor.pushforward_single
  AlgebraicCurve.Place.coe_restrictInclusion AlgebraicCurve.Place.mem_fiber
  AlgebraicCurve.Place.restrict_toValuationSubring AlgebraicCurve.Divisor.degree_pushforward
  AlgebraicCurve.Place.restrictResidueMap_residue AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom
  AlgebraicCurve.Pic0.coe_pullbackDegZeroHom
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SEPEngine
open _root_.AlgebraicCurve
open IntermediateField Polynomial
section AdjoinIndex
open scoped IntermediateField
variable {K M : Type*} [Field K] [Field M] [Algebra K M]
  (p : ℕ) [hp : Fact p.Prime] [CharP K p]
Lean source · full declaration
theorem finrank_frobeniusSubfield_adjoin_transcendental [PerfectField K]
    {t : M} (htr : Transcendental K t) :
    haveI : ExpChar (↥(IntermediateField.adjoin K ({t} : Set M))) p :=
      expChar_of_injective_algebraMap (algebraMap K _).injective p
    Module.finrank
      (frobeniusSubfield (↥(IntermediateField.adjoin K ({t} : Set M))) p)
      (↥(IntermediateField.adjoin K ({t} : Set M))) = p := by
  have : ExpChar (↥K⟮t⟯) p :=
    expChar_of_injective_algebraMap (algebraMap K _).injective p
  have : CharP (↥K⟮t⟯) p :=
    charP_of_injective_algebraMap (algebraMap K _).injective p
  let t' : ↥K⟮t⟯ := genT t
  let tp : ↥(frobeniusSubfield (↥K⟮t⟯) p) := ⟨t' ^ p, pow_mem_frobeniusSubfield p t'⟩
  have hint : IsIntegral (↥(frobeniusSubfield (↥K⟮t⟯) p)) t' := by
    refine ⟨X ^ p - C tp, monic_X_pow_sub_C _ hp.out.ne_zero, ?_⟩
    simp only [eval₂_sub, eval₂_X_pow, eval₂_C]
    exact sub_eq_zero.mpr rfl
  have hfd : FiniteDimensional (↥(frobeniusSubfield (↥K⟮t⟯) p)) (↥K⟮t⟯) := by
    have h1 := adjoin_genT_over_frobeniusSubfield (K := K) (M := M) p t
    have h2 := IntermediateField.adjoin.finiteDimensional hint
    rw [show t' = genT t from rfl, h1] at h2
    exact (IntermediateField.topEquiv (F := ↥(frobeniusSubfield (↥K⟮t⟯) p))
      (E := ↥K⟮t⟯)).toLinearEquiv.finiteDimensional
  have hli := pDigits_linearIndependent (M := ↥K⟮t⟯) p (t := t') (genT_not_pow p t htr)
  refine le_antisymm ?_
    (by simpa only [Fintype.card_fin] using hli.fintype_card_le_finrank)
  have htop := adjoin_genT_over_frobeniusSubfield (K := K) (M := M) p t
  calc Module.finrank _ (↥K⟮t⟯)
      = Module.finrank (↥(frobeniusSubfield (↥K⟮t⟯) p))
          (↥(IntermediateField.adjoin (↥(frobeniusSubfield (↥K⟮t⟯) p)) {t'} :
            IntermediateField _ (↥K⟮t⟯))) := by
        rw [show t' = genT t from rfl, htop, IntermediateField.finrank_top']
    _ = (minpoly (↥(frobeniusSubfield (↥K⟮t⟯) p)) t').natDegree :=
        IntermediateField.adjoin.finrank hint
    _ ≤ (X ^ p - C tp).natDegree :=
        Polynomial.natDegree_le_of_dvd (minpoly.dvd _ _ (by
          simp only [map_sub, map_pow, aeval_X, aeval_C]; exact sub_eq_zero.mpr rfl))
          (monic_X_pow_sub_C _ hp.out.ne_zero).ne_zero
    _ = p := natDegree_X_pow_sub_C
theorem

finrank_frobeniusSubfield_eq_of_transcendental

L322 ↗
AlgebraicCurves.Places.Proofs.PlaceSeparableAdjoinOrdOne.AlgebraicCurve.SEPEngine.finrank_frobeniusSubfield_eq_of_transcendental
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceSeparableAdjoinOrdOne
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
  instIsScalarTowerResidueFieldRestrictPushforward
  instAlgebraResidueFieldRestrictPushforward
  instIsLocalHomRestrictInclusion
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  AlgebraicCurve.Divisor.mapRestrict_single AlgebraicCurve.Divisor.pushforward_single
  AlgebraicCurve.Place.coe_restrictInclusion AlgebraicCurve.Place.mem_fiber
  AlgebraicCurve.Place.restrict_toValuationSubring AlgebraicCurve.Divisor.degree_pushforward
  AlgebraicCurve.Place.restrictResidueMap_residue AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom
  AlgebraicCurve.Pic0.coe_pullbackDegZeroHom
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SEPEngine
open _root_.AlgebraicCurve
open IntermediateField Polynomial
Lean source · full declaration
theorem finrank_frobeniusSubfield_eq_of_transcendental {K M : Type*} [Field K] [Field M]
    [Algebra K M] [PerfectField K] (p : ℕ) [hp : Fact p.Prime] [CharP K p]
    (t : M) (htr : Transcendental K t)
    [FiniteDimensional (IntermediateField.adjoin K ({t} : Set M)) M] :
    haveI : ExpChar M p := expChar_of_injective_algebraMap (algebraMap K M).injective p
    Module.finrank (frobeniusSubfield M p) M = p := by
  have : ExpChar M p := expChar_of_injective_algebraMap (algebraMap K M).injective p
  have : ExpChar (↥(IntermediateField.adjoin K ({t} : Set M))) p :=
    expChar_of_injective_algebraMap (algebraMap K _).injective p
  have : FiniteDimensional
      (frobeniusSubfield (↥(IntermediateField.adjoin K ({t} : Set M))) p)
      (↥(IntermediateField.adjoin K ({t} : Set M))) :=
    FiniteDimensional.of_finrank_pos (by
      rw [finrank_frobeniusSubfield_adjoin_transcendental p htr]; exact hp.out.pos)
  rw [finrank_frobeniusSubfield_eq (E := ↥(IntermediateField.adjoin K ({t} : Set M))) p,
    finrank_frobeniusSubfield_adjoin_transcendental p htr]
theorem

pDigits_exists_of_finrank_eq

L343 ↗
AlgebraicCurves.Places.Proofs.PlaceSeparableAdjoinOrdOne.AlgebraicCurve.SEPEngine.pDigits_exists_of_finrank_eq
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceSeparableAdjoinOrdOne
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
  instIsScalarTowerResidueFieldRestrictPushforward
  instAlgebraResidueFieldRestrictPushforward
  instIsLocalHomRestrictInclusion
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  AlgebraicCurve.Divisor.mapRestrict_single AlgebraicCurve.Divisor.pushforward_single
  AlgebraicCurve.Place.coe_restrictInclusion AlgebraicCurve.Place.mem_fiber
  AlgebraicCurve.Place.restrict_toValuationSubring AlgebraicCurve.Divisor.degree_pushforward
  AlgebraicCurve.Place.restrictResidueMap_residue AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom
  AlgebraicCurve.Pic0.coe_pullbackDegZeroHom
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SEPEngine
open _root_.AlgebraicCurve
open IntermediateField Polynomial
section PDigitsExists
variable {M : Type*} [Field M] (p : ℕ) [hp : Fact p.Prime] [CharP M p]
Lean source · full declaration
theorem pDigits_exists_of_finrank_eq
    (hfr : haveI : ExpChar M p := ExpChar.prime hp.out
      Module.finrank (frobeniusSubfield M p) M = p)
    {t : M} (htp : ∀ a : M, a ^ p ≠ t) (g : M) :
    ∃ a : Fin p → M, g = ∑ i : Fin p, a i ^ p * t ^ (i : ℕ) := by
  have : ExpChar M p := ExpChar.prime hp.out
  have hlin := pDigits_linearIndependent p htp
  let b : Module.Basis (Fin p) (frobeniusSubfield M p) M :=
    basisOfLinearIndependentOfCardEqFinrank hlin (by rw [hfr, Fintype.card_fin])
  have hbapply : ∀ i : Fin p, (b i : M) = t ^ (i : ℕ) := fun i ↦
    congrFun (coe_basisOfLinearIndependentOfCardEqFinrank hlin
      (by rw [hfr, Fintype.card_fin])) i
  refine ⟨fun i ↦ (frobeniusRingEquivRange M p).symm (b.repr g i), ?_⟩
  conv_lhs => rw [← b.sum_repr g]
  refine Finset.sum_congr rfl fun i _ ↦ ?_
  rw [hbapply i, ← frobeniusRingEquivRange_apply M p, RingEquiv.apply_symm_apply]
  rfl
theorem

not_pow_of_ord_eq_one

L372 ↗
AlgebraicCurves.Places.Proofs.PlaceSeparableAdjoinOrdOne.AlgebraicCurve.SEPEngine.not_pow_of_ord_eq_one
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceSeparableAdjoinOrdOne
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
  instIsScalarTowerResidueFieldRestrictPushforward
  instAlgebraResidueFieldRestrictPushforward
  instIsLocalHomRestrictInclusion
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  AlgebraicCurve.Divisor.mapRestrict_single AlgebraicCurve.Divisor.pushforward_single
  AlgebraicCurve.Place.coe_restrictInclusion AlgebraicCurve.Place.mem_fiber
  AlgebraicCurve.Place.restrict_toValuationSubring AlgebraicCurve.Divisor.degree_pushforward
  AlgebraicCurve.Place.restrictResidueMap_residue AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom
  AlgebraicCurve.Pic0.coe_pullbackDegZeroHom
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SEPEngine
open _root_.AlgebraicCurve
open KaehlerDifferential IntermediateField
Lean source · statement
theorem not_pow_of_ord_eq_one {K F : Type*} [Field K] [Field F] [Algebra K F]
    (v : AlgebraicCurve.Place K F) {t : F} (ht : v.ord t = 1) {p : ℕ} (hp : 2 ≤ p) (a : F) :
    a ^ p ≠ t
theorem

D_pow_eq_zero

L381 ↗
AlgebraicCurves.Places.Proofs.PlaceSeparableAdjoinOrdOne.AlgebraicCurve.SEPEngine.D_pow_eq_zero
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceSeparableAdjoinOrdOne
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
  instIsScalarTowerResidueFieldRestrictPushforward
  instAlgebraResidueFieldRestrictPushforward
  instIsLocalHomRestrictInclusion
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  AlgebraicCurve.Divisor.mapRestrict_single AlgebraicCurve.Divisor.pushforward_single
  AlgebraicCurve.Place.coe_restrictInclusion AlgebraicCurve.Place.mem_fiber
  AlgebraicCurve.Place.restrict_toValuationSubring AlgebraicCurve.Divisor.degree_pushforward
  AlgebraicCurve.Place.restrictResidueMap_residue AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom
  AlgebraicCurve.Pic0.coe_pullbackDegZeroHom
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SEPEngine
open _root_.AlgebraicCurve
open KaehlerDifferential IntermediateField
Lean source · statement
theorem D_pow_eq_zero {E M : Type*} [CommRing E] [CommRing M]
    [Algebra E M] (p : ℕ) [Fact p.Prime] [CharP M p] (a : M) :
    D E M (a ^ p) = 0
theorem

isSeparable_of_not_pow_mem_range

L386 ↗
AlgebraicCurves.Places.Proofs.PlaceSeparableAdjoinOrdOne.AlgebraicCurve.SEPEngine.isSeparable_of_not_pow_mem_range
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceSeparableAdjoinOrdOne
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
  instIsScalarTowerResidueFieldRestrictPushforward
  instAlgebraResidueFieldRestrictPushforward
  instIsLocalHomRestrictInclusion
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  AlgebraicCurve.Divisor.mapRestrict_single AlgebraicCurve.Divisor.pushforward_single
  AlgebraicCurve.Place.coe_restrictInclusion AlgebraicCurve.Place.mem_fiber
  AlgebraicCurve.Place.restrict_toValuationSubring AlgebraicCurve.Divisor.degree_pushforward
  AlgebraicCurve.Place.restrictResidueMap_residue AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom
  AlgebraicCurve.Pic0.coe_pullbackDegZeroHom
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace SEPEngine
open _root_.AlgebraicCurve
open KaehlerDifferential IntermediateField
Lean source · full declaration
theorem isSeparable_of_not_pow_mem_range {E M : Type*} [Field E] [Field M]
    [Algebra E M] (p : ℕ) [hp : Fact p.Prime] [CharP M p]
    [FiniteDimensional E M]
    (hfr : haveI : ExpChar M p := ExpChar.prime hp.out
      Module.finrank (frobeniusSubfield M p) M = p)
    {t : M} (htE : t ∈ (algebraMap E M).range) (htp : ∀ a : M, a ^ p ≠ t) :
    Algebra.IsSeparable E M := by
  have : ExpChar M p := ExpChar.prime hp.out
  obtain ⟨tE, rfl⟩ := htE
  have hDt : D E M (algebraMap E M tE) = 0 := (D E M).map_algebraMap tE
  have hDzero : ∀ m : M, D E M m = 0 := by
    intro m
    obtain ⟨a, rfl⟩ := pDigits_exists_of_finrank_eq p hfr htp m
    rw [map_sum]
    refine Finset.sum_eq_zero fun i _ ↦ ?_
    rw [Derivation.leibniz, D_pow_eq_zero p (a i),
      smul_zero, add_zero, Derivation.leibniz_pow, hDt, smul_zero,
      ← Nat.cast_smul_eq_nsmul M, smul_zero, smul_zero]
  have hsubsingleton : Subsingleton (Ω[M⁄E]) := by
    refine ⟨fun ω₁ ω₂ ↦ ?_⟩
    have htop : (⊤ : Submodule M (Ω[M⁄E])) = ⊥ := by
      rw [← KaehlerDifferential.span_range_derivation, Submodule.span_eq_bot]
      rintro _ ⟨m, rfl⟩; exact hDzero m
    have h1 : ω₁ ∈ (⊥ : Submodule M (Ω[M⁄E])) := htop ▸ Submodule.mem_top
    have h2 : ω₂ ∈ (⊥ : Submodule M (Ω[M⁄E])) := htop ▸ Submodule.mem_top
    rw [Submodule.mem_bot] at h1 h2; rw [h1, h2]
  have : Algebra.FormallyUnramified E M := ⟨hsubsingleton⟩
  exact Algebra.FormallyUnramified.isSeparable E M
theorem

isSeparable_adjoin_of_ord_eq_one

L421 ↗
AlgebraicCurve.Place.isSeparable_adjoin_of_ord_eq_one
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceSeparableAdjoinOrdOne
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
  instIsScalarTowerResidueFieldRestrictPushforward
  instAlgebraResidueFieldRestrictPushforward
  instIsLocalHomRestrictInclusion
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  AlgebraicCurve.Divisor.mapRestrict_single AlgebraicCurve.Divisor.pushforward_single
  AlgebraicCurve.Place.coe_restrictInclusion AlgebraicCurve.Place.mem_fiber
  AlgebraicCurve.Place.restrict_toValuationSubring AlgebraicCurve.Divisor.degree_pushforward
  AlgebraicCurve.Place.restrictResidueMap_residue AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom
  AlgebraicCurve.Pic0.coe_pullbackDegZeroHom
noncomputable section
open _root_.AlgebraicCurve
  _root_.AlgebraicCurves.Places.Proofs.PlaceSeparableAdjoinOrdOne.AlgebraicCurve
  AlgebraicCurve.SEPEngine IntermediateField in
open scoped IntermediateField in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.isSeparable_adjoin_of_ord_eq_one {K F : Type*} [Field K]
  [Field F] [Algebra K F] [PerfectField K] (x : F)
    [Algebra.IsAlgebraic (IntermediateField.adjoin K ({x} : Set F)) F]
    (v : AlgebraicCurve.Place K F) {t : F} (ht : v.ord t = 1) :
    Algebra.IsSeparable (IntermediateField.adjoin K ({t} : Set F)) F

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