NYLL
Module

IsSeparable_of_algHom_apply_eq_pow_of_transcendental.lean

Nyll.AlgebraicCurves.Foundations.FieldTheory.IsSeparable_of_algHom_apply_eq_pow_of_transcendental
6 declarations indexed from sourceView source ↗

Module documentation

Is Separable of alg Hom apply eq pow of transcendental

Imports2
  • Mathlib.FieldTheory.IsAlgClosed.Basic
  • Mathlib.FieldTheory.RatFunc.Basic
Imported by2

Declarations

theorem

apply_coeff_minpoly_eq

L33 ↗
AlgebraicCurves.Foundations.FieldTheory.Proofs.IsSeparable_of_algHom_apply_eq_pow_of_transcendental.HDescent.apply_coeff_minpoly_eq
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IsSeparable_of_algHom_apply_eq_pow_of_transcendental
open Polynomial
namespace HDescent
section Part1
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem apply_coeff_minpoly_eq {L : IntermediateField K F} (σ₁ σ₂ : F →+* F)
    (hL : ∀ x ∈ L, ∃ y ∈ L, σ₁ x = σ₂ y)
    (g : F) (hgint : IsIntegral L g) (hg : σ₁ g = σ₂ g) (i : ℕ) :
    σ₁ ((minpoly L g).coeff i : F) = σ₂ ((minpoly L g).coeff i : F)
theorem

exists_mem_adjoin_apply_eq_iterateFrobenius

L86 ↗
AlgebraicCurves.Foundations.FieldTheory.Proofs.IsSeparable_of_algHom_apply_eq_pow_of_transcendental.HDescent.exists_mem_adjoin_apply_eq_iterateFrobenius
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IsSeparable_of_algHom_apply_eq_pow_of_transcendental
open Polynomial
namespace HDescent
section Part1
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem exists_mem_adjoin_apply_eq_iterateFrobenius {p : ℕ} [Fact p.Prime] [CharP F p] (r : ℕ)
    (φ : F →ₐ[K] F) (t : F) (hφt : φ t = t ^ p ^ r) (hK : ∀ a : K, ∃ b : K, b ^ p ^ r = a) :
    ∀ x ∈ IntermediateField.adjoin K ({t} : Set F), ∃ y ∈ IntermediateField.adjoin K ({t} : Set F),
      (φ : F →+* F) x = iterateFrobenius F p r y
theorem

ringHom_aeval

L116 ↗
AlgebraicCurves.Foundations.FieldTheory.Proofs.IsSeparable_of_algHom_apply_eq_pow_of_transcendental.HDescent.ringHom_aeval
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IsSeparable_of_algHom_apply_eq_pow_of_transcendental
open Polynomial
namespace HDescent
section Part2
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem ringHom_aeval (σ : F →+* F) (τ : K →+* K)
    (hστ : ∀ a : K, σ (algebraMap K F a) = algebraMap K F (τ a)) (x : F) (a : K[X]) :
    σ (aeval x a) = aeval (σ x) (a.map τ)
theorem

aeval_mem_closure

L123 ↗
AlgebraicCurves.Foundations.FieldTheory.Proofs.IsSeparable_of_algHom_apply_eq_pow_of_transcendental.HDescent.aeval_mem_closure
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IsSeparable_of_algHom_apply_eq_pow_of_transcendental
open Polynomial
namespace HDescent
section Part2
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem aeval_mem_closure (t : F) (a : K[X]) (S : Subfield F) (ht : t ∈ S)
    (ha : ∀ i, algebraMap K F (a.coeff i) ∈ S) : aeval t a ∈ S
theorem

mem_closure_of_apply_eq_pow

L130 ↗
AlgebraicCurves.Foundations.FieldTheory.Proofs.IsSeparable_of_algHom_apply_eq_pow_of_transcendental.HDescent.mem_closure_of_apply_eq_pow
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IsSeparable_of_algHom_apply_eq_pow_of_transcendental
open Polynomial
namespace HDescent
section Part2
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem mem_closure_of_apply_eq_pow {p : ℕ} [Fact p.Prime] [CharP F p] (r : ℕ)
    (φ : F →ₐ[K] F) (t : F) (ht : Transcendental K t) (hφt : φ t = t ^ p ^ r)
    {c : F} (hc : c ∈ IntermediateField.adjoin K ({t} : Set F)) (hφc : φ c = c ^ p ^ r) :
    c ∈ Subfield.closure ({x : F | x ^ p ^ r = x} ∪ {t})
theorem

of_algHom_apply_eq_pow_of_transcendental

L201 ↗
IsSeparable.of_algHom_apply_eq_pow_of_transcendental
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IsSeparable_of_algHom_apply_eq_pow_of_transcendental
open Polynomial
open HDescent in
Lean source · statement
theorem _root_.IsSeparable.of_algHom_apply_eq_pow_of_transcendental
    {K F : Type*} [Field K] [Field F] [Algebra K F] [IsAlgClosed K]
    (p r : ℕ) [Fact p.Prime] [CharP F p] (_hr : 0 < r)
    (φ : F →ₐ[K] F) (t : F) (ht : Transcendental K t) (hφt : φ t = t ^ p ^ r)
    (hsep : Algebra.IsSeparable (IntermediateField.adjoin K ({t} : Set F)) F)
    (g : F) (hg : φ g = g ^ p ^ r) :
    IsSeparable (Subfield.closure ({c : F | c ^ p ^ r = c} ∪ {t})) g

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