NYLL
Module

Algebra_exists_monic_irreducible_map_algebraicClosure_hypersurfaceModel_of_forall_isSeparable.lean

Nyll.AlgebraicCurves.Foundations.FieldTheory.Algebra_exists_monic_irreducible_map_algebraicClosure_hypersurfaceModel_of_forall_isSeparable
7 declarations indexed from sourceView source ↗

Module documentation

Algebra exists monic irreducible map algebraic Closure hypersurface Model of forall is

Separable

Imports6
Imported by2

Declarations

theorem

exists_isSeparable_pow

L40 ↗
AlgebraicCurves.Foundations.FieldTheory.Proofs.SeparableHypersurfaceModel.P2mHypModel.exists_isSeparable_pow
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs.SeparableHypersurfaceModel
universe u v w
open _root_.Polynomial
open scoped IntermediateField
namespace P2mHypModel
section SepPow
variable {F E : Type*} [Field F] [Field E] [Algebra F E]
Lean source · statement
theorem exists_isSeparable_pow (q : ℕ) [ExpChar F q] {t : E} (ht : IsIntegral F t) :
    ∃ n : ℕ, IsSeparable F (t ^ q ^ n)
theorem

isSeparable_pow_add

L49 ↗
AlgebraicCurves.Foundations.FieldTheory.Proofs.SeparableHypersurfaceModel.P2mHypModel.isSeparable_pow_add
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs.SeparableHypersurfaceModel
universe u v w
open _root_.Polynomial
open scoped IntermediateField
namespace P2mHypModel
section SepPow
variable {F E : Type*} [Field F] [Field E] [Algebra F E]
Lean source · statement
theorem isSeparable_pow_add (q : ℕ) [ExpChar F q] {t : E} {n : ℕ} (h : IsSeparable F (t ^ q ^ n))
  (m : ℕ) :
    IsSeparable F (t ^ q ^ (n + m))
theorem

coe_adjoin_range_eq_range

L67 ↗
AlgebraicCurves.Foundations.FieldTheory.Proofs.SeparableHypersurfaceModel.P2mHypModel.coe_adjoin_range_eq_range
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs.SeparableHypersurfaceModel
universe u v w
open _root_.Polynomial
open scoped IntermediateField
namespace P2mHypModel
section FracRange
variable {k R L K : Type*} [Field k] [CommRing R] [IsDomain R] [Field L] [Field K]
  [Algebra k R] [Algebra R L] [Algebra k L] [IsScalarTower k R L]
  [Algebra R K] [IsFractionRing R K] [Algebra K L] [IsScalarTower R K L]
omit [IsDomain R] in
Lean source · statement
theorem coe_adjoin_range_eq_range :
    (IntermediateField.adjoin k (Set.range (algebraMap R L)) : Set L) = Set.range (algebraMap K L)
theorem

forall_isSeparable_mem_range

L87 ↗
AlgebraicCurves.Foundations.FieldTheory.Proofs.SeparableHypersurfaceModel.P2mHypModel.forall_isSeparable_mem_range
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs.SeparableHypersurfaceModel
universe u v w
open _root_.Polynomial
open scoped IntermediateField
namespace P2mHypModel
section FracRange
variable {k R L K : Type*} [Field k] [CommRing R] [IsDomain R] [Field L] [Field K]
  [Algebra k R] [Algebra R L] [Algebra k L] [IsScalarTower k R L]
  [Algebra R K] [IsFractionRing R K] [Algebra K L] [IsScalarTower R K L]
omit [IsDomain R] in
Lean source · statement
theorem forall_isSeparable_mem_range
    (hgi : ∀ θ : L, IsSeparable (IntermediateField.adjoin k (Set.range (algebraMap R L))) θ →
      θ ∈ IntermediateField.adjoin k (Set.range (algebraMap R L))) :
    ∀ θ : L, IsSeparable K θ → θ ∈ (algebraMap K L).range
theorem

exists_ne_zero_map_eq_C_mul

L122 ↗
AlgebraicCurves.Foundations.FieldTheory.Proofs.SeparableHypersurfaceModel.P2mHypModel.exists_ne_zero_map_eq_C_mul
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs.SeparableHypersurfaceModel
universe u v w
open _root_.Polynomial
open scoped IntermediateField
namespace P2mHypModel
section Denom
Lean source · statement
theorem exists_ne_zero_map_eq_C_mul {R K : Type*} [CommRing R] [IsDomain R] [Field K] [Algebra R K]
    [IsFractionRing R K] {d : ℕ} (p : MvPolynomial (Fin d) K) :
    ∃ ρ : R, ρ ≠ 0 ∧ ∃ p₀ : MvPolynomial (Fin d) R,
      MvPolynomial.map (algebraMap R K) p₀ = MvPolynomial.C (algebraMap R K ρ) * p
theorem

main

L147 ↗
AlgebraicCurves.Foundations.FieldTheory.Proofs.SeparableHypersurfaceModel.P2mHypModel.main
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs.SeparableHypersurfaceModel
universe u v w
open _root_.Polynomial
open scoped IntermediateField
namespace P2mHypModel
section Main
variable (k : Type u) [Field k] {R : Type v} {C : Type w} [CommRing R] [IsDomain R] [Algebra k R]
    [Algebra.FiniteType k R] [CommRing C] [IsDomain C] [Algebra k C] [Algebra R C]
    [IsScalarTower k R C] [Algebra.FiniteType R C] [FaithfulSMul R C]
omit [Algebra.FiniteType k R] in
Lean source · statement
theorem main
    (hgi : ∀ θ : FractionRing C,
      IsSeparable (IntermediateField.adjoin k (Set.range (algebraMap R (FractionRing C)))) θ →
      θ ∈ IntermediateField.adjoin k (Set.range (algebraMap R (FractionRing C)))) :
    ∃ r : R, r ≠ 0 ∧ ∃ (d : ℕ) (z : Fin d → C) (w : C) (F : Polynomial (MvPolynomial (Fin d) R))
      (g : MvPolynomial (Fin d) R),
      AlgebraicIndependent R z ∧ F.Monic ∧
      F.eval₂ (MvPolynomial.aeval z : MvPolynomial (Fin d) R →ₐ[R] C).toRingHom w = 0 ∧
      Irreducible (F.map (MvPolynomial.map (algebraMap R (AlgebraicClosure (FractionRing R))))) ∧
      g ≠ 0 ∧
      (∀ c : C, ∃ m M : ℕ, 0 < M ∧
        ((MvPolynomial.aeval z g) ^ m * c) ^ M ∈ Algebra.adjoin R (insert w (Set.range z))) ∧
      (∀ c : C, ∃ n : ℕ, IsIntegral (Algebra.adjoin R (Set.range z)) (r ^ n • c))
theorem

exists_monic_irreducible_map_algebraicClosure_hypersurfaceModel_of_forall_isSeparable

L687 ↗
Algebra.exists_monic_irreducible_map_algebraicClosure_hypersurfaceModel_of_forall_isSeparable
Source context 6 commands

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

section ProofImplementation
namespace Algebra
open _root_.AlgebraicCurves.Foundations.FieldTheory.Proofs.SeparableHypersurfaceModel
universe u v w
open _root_.Polynomial
open scoped _root_.IntermediateField
Lean source · statement
theorem exists_monic_irreducible_map_algebraicClosure_hypersurfaceModel_of_forall_isSeparable
    (k : Type u) [Field k] {R : Type v} {C : Type w} [CommRing R] [IsDomain R] [Algebra k R]
    [Algebra.FiniteType k R] [CommRing C] [IsDomain C] [Algebra k C] [Algebra R C]
    [IsScalarTower k R C] [Algebra.FiniteType R C] [FaithfulSMul R C]
    (hgi : ∀ θ : FractionRing C,
      IsSeparable (IntermediateField.adjoin k (Set.range (algebraMap R (FractionRing C)))) θ →
      θ ∈ IntermediateField.adjoin k (Set.range (algebraMap R (FractionRing C)))) :
    ∃ r : R, r ≠ 0 ∧ ∃ (d : ℕ) (z : Fin d → C) (w : C) (F : Polynomial (MvPolynomial (Fin d) R))
      (g : MvPolynomial (Fin d) R),
      AlgebraicIndependent R z ∧ F.Monic ∧
      F.eval₂ (MvPolynomial.aeval z : MvPolynomial (Fin d) R →ₐ[R] C).toRingHom w = 0 ∧
      Irreducible (F.map (MvPolynomial.map (algebraMap R (AlgebraicClosure (FractionRing R))))) ∧
      g ≠ 0 ∧
      (∀ c : C, ∃ m M : ℕ, 0 < M ∧
        ((MvPolynomial.aeval z g) ^ m * c) ^ M ∈ Algebra.adjoin R (insert w (Set.range z))) ∧
      (∀ c : C, ∃ n : ℕ, IsIntegral (Algebra.adjoin R (Set.range z)) (r ^ n • c))

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