Module

Exists_aeval_sub_mem_smul_of_isMaximal_of_isIntegrallyClosed.lean

Nyll.AlgebraicCurves.FunctionFields.Exists_aeval_sub_mem_smul_of_isMaximal_of_isIntegrallyClosed

5 declarations indexed from sourceView source ↗

Module documentation

Exists aeval sub mem smul of is Maximal of is Integrally Closed

Imports54

Mathlib.Algebra.Algebra.Defs
Mathlib.Algebra.Algebra.Basic
Mathlib.Algebra.Field.Defs
Mathlib.Algebra.GroupWithZero.Associated
Mathlib.Algebra.BigOperators.Group.Finset.Defs
Mathlib.Algebra.BigOperators.Group.Finset.Basic
Mathlib.Algebra.Module.Submodule.Defs
Mathlib.Algebra.Module.Submodule.Lattice
Mathlib.Algebra.Module.Submodule.RestrictScalars
Mathlib.Algebra.Polynomial.Basic
Mathlib.Algebra.Polynomial.Eval.Defs
Mathlib.Algebra.Polynomial.Eval.Coeff
Mathlib.Algebra.Polynomial.AlgebraMap
Mathlib.Algebra.Polynomial.Div
Mathlib.Algebra.Polynomial.Degree.Operations
Mathlib.Algebra.Polynomial.FieldDivision
Mathlib.Algebra.Polynomial.RingDivision
Mathlib.Algebra.Polynomial.Monomial
Mathlib.Algebra.Polynomial.Monic
Mathlib.Data.Fin.Embedding
Mathlib.Data.Finset.Range
Mathlib.Data.Finset.Dedup
Mathlib.Data.Finset.Lattice.Fold
Mathlib.Data.Fintype.EquivFin
Mathlib.Data.Multiset.Count
Mathlib.Data.Multiset.MapFold
Mathlib.FieldTheory.IsAlgClosed.Basic
Mathlib.LinearAlgebra.Span.Defs
Mathlib.Logic.Function.Basic
Mathlib.RingTheory.DedekindDomain.Basic
Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Mathlib.RingTheory.Ideal.Defs
Mathlib.RingTheory.Ideal.Basic
Mathlib.RingTheory.Ideal.Lattice
Mathlib.RingTheory.Ideal.Span
Mathlib.RingTheory.Ideal.Prime
Mathlib.RingTheory.Ideal.Maximal
Mathlib.RingTheory.Ideal.Maps
Mathlib.RingTheory.Ideal.Operations
Mathlib.RingTheory.Ideal.Quotient.Basic
Mathlib.RingTheory.Ideal.Quotient.Defs
Mathlib.RingTheory.Finiteness.Defs
Mathlib.RingTheory.IntegralClosure.IsIntegral.Defs
Mathlib.RingTheory.IntegralClosure.Algebra.Defs
Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Mathlib.RingTheory.Noetherian.Basic
Mathlib.RingTheory.Polynomial.Basic
Mathlib.RingTheory.PrincipalIdealDomain
Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Mathlib.Tactic.Ring.RingNF
Mathlib.Tactic.LinearCombination
Mathlib.Tactic.Choose

Imported by2

theorem

eq_span_sup_sq

L89 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_aeval_sub_mem_smul_of_isMaximal_of_isIntegrallyClosed.FibreMonogenicSol.eq_span_sup_sq

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs
namespace Exists_aeval_sub_mem_smul_of_isMaximal_of_isIntegrallyClosed
open Polynomial UniqueFactorizationMonoid
universe u v
noncomputable section
namespace FibreMonogenicSol
section Local
variable {B : Type v} [CommRing B] [IsDedekindDomain B]

Lean source · statement

theorem eq_span_sup_sq (Q : Ideal B) [Q.IsPrime] (hQ0 : Q ≠ ⊥) (t : B) (ht : t ∈ Q)
    (ht2 : t ∉ Q ^ 2) : Ideal.span {t} ⊔ Q ^ 2 = Q

theorem

pow_le_span_pow_sup

L102 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_aeval_sub_mem_smul_of_isMaximal_of_isIntegrallyClosed.FibreMonogenicSol.pow_le_span_pow_sup

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs
namespace Exists_aeval_sub_mem_smul_of_isMaximal_of_isIntegrallyClosed
open Polynomial UniqueFactorizationMonoid
universe u v
noncomputable section
namespace FibreMonogenicSol
section Local
variable {B : Type v} [CommRing B] [IsDedekindDomain B]

Lean source · statement

theorem pow_le_span_pow_sup (Q : Ideal B) [Q.IsPrime] (hQ0 : Q ≠ ⊥) (t : B) (ht : t ∈ Q)
    (ht2 : t ∉ Q ^ 2) (k : ℕ) : Q ^ k ≤ Ideal.span {t ^ k} ⊔ Q ^ (k + 1)

theorem

exists_expansion

L121 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_aeval_sub_mem_smul_of_isMaximal_of_isIntegrallyClosed.FibreMonogenicSol.exists_expansion

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs
namespace Exists_aeval_sub_mem_smul_of_isMaximal_of_isIntegrallyClosed
open Polynomial UniqueFactorizationMonoid
universe u v
noncomputable section
namespace FibreMonogenicSol
section Local
variable {B : Type v} [CommRing B] [IsDedekindDomain B]

Lean source · statement

theorem exists_expansion (Q : Ideal B) [Q.IsPrime] (hQ0 : Q ≠ ⊥) (t : B) (ht : t ∈ Q)
    (ht2 : t ∉ Q ^ 2) {K : Type u} [Field K] (φ : K →+* B)
    (hres : ∀ b : B, ∃ a : K, b - φ a ∈ Q) (b : B) (k : ℕ) :
    ∃ a : ℕ → K, b - ∑ i ∈ Finset.range k, φ (a i) * t ^ i ∈ Q ^ k

theorem

main

L156 ↗

AlgebraicCurves.FunctionFields.Proofs.Exists_aeval_sub_mem_smul_of_isMaximal_of_isIntegrallyClosed.FibreMonogenicSol.main

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs
namespace Exists_aeval_sub_mem_smul_of_isMaximal_of_isIntegrallyClosed
open Polynomial UniqueFactorizationMonoid
universe u v
noncomputable section
namespace FibreMonogenicSol
section Main
variable {K : Type u} [Field K] [IsAlgClosed K] {B : Type v} [CommRing B] [IsDomain B]
  [IsIntegrallyClosed B] [Algebra K[X] B] [Module.Finite K[X] B] [FaithfulSMul K[X] B]

Lean source · statement

theorem main (P : Ideal K[X]) (hP : P.IsMaximal) :
    ∃ y : B, ∀ z : B, ∃ q : Polynomial K[X], z - aeval y q ∈ P • (⊤ : Submodule K[X] B)

theorem

exists_aeval_sub_mem_smul_of_isMaximal_of_isIntegrallyClosed

L341 ↗

AlgebraicCurve.exists_aeval_sub_mem_smul_of_isMaximal_of_isIntegrallyClosed

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs
namespace Exists_aeval_sub_mem_smul_of_isMaximal_of_isIntegrallyClosed
open Polynomial UniqueFactorizationMonoid
universe u v

Lean source · statement

theorem _root_.AlgebraicCurve.exists_aeval_sub_mem_smul_of_isMaximal_of_isIntegrallyClosed
    (K : Type u) [Field K] [IsAlgClosed K] (B : Type v) [CommRing B] [IsDomain B]
    [IsIntegrallyClosed B] [Algebra K[X] B] [Module.Finite K[X] B] [FaithfulSMul K[X] B]
    (P : Ideal K[X]) (hP : P.IsMaximal) :
    ∃ y : B, ∀ z : B, ∃ q : Polynomial K[X], z - aeval y q ∈ P • (⊤ : Submodule K[X] B)

Module documentation

Exists aeval sub mem smul of is Maximal of is Integrally Closed

Declarations

eq_span_sup_sq

pow_le_span_pow_sup

exists_expansion

main

exists_aeval_sub_mem_smul_of_isMaximal_of_isIntegrallyClosed