Module

Algebra_finite_integralClosure_adjoin_singleton_of_isAlgClosed.lean

Nyll.AlgebraicCurves.Foundations.FieldTheory.Algebra_finite_integralClosure_adjoin_singleton_of_isAlgClosed

9 declarations indexed from sourceView source ↗

Module documentation

Algebra finite integral Closure adjoin singleton of is Alg Closed

Imports23

Mathlib.Algebra.Algebra.Subalgebra.Tower
Mathlib.Algebra.Algebra.Tower
Mathlib.Algebra.CharP.Frobenius
Mathlib.Algebra.CharP.Lemmas
Mathlib.Algebra.Group.Pointwise.Set.Scalar
Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Mathlib.FieldTheory.IsAlgClosed.Basic
Mathlib.FieldTheory.PurelyInseparable.Basic
Mathlib.FieldTheory.PurelyInseparable.Exponent
Mathlib.FieldTheory.SeparableClosure
Mathlib.LinearAlgebra.Span.Basic
Mathlib.RingTheory.Adjoin.FG
Mathlib.RingTheory.Algebraic.Basic
Mathlib.RingTheory.DedekindDomain.IntegralClosure
Mathlib.RingTheory.Finiteness.Basic
Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Mathlib.RingTheory.Noetherian.Basic
Mathlib.RingTheory.Noetherian.Defs
Mathlib.RingTheory.Polynomial.RationalRoot
Mathlib.Tactic.Choose

Imported by1

Nyll.AlgebraicCurves.Foundations.FieldTheory.All

theorem

isNoetherianRing_adjoin

L54 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.Algebra_finite_integralClosure_adjoin_singleton_of_isAlgClosed.FiniteIntegralClosureAdjoinSingleton.isNoetherianRing_adjoin

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace Algebra_finite_integralClosure_adjoin_singleton_of_isAlgClosed
open Polynomial IntermediateField
open scoped IntermediateField.algebraAdjoinAdjoin Pointwise
namespace FiniteIntegralClosureAdjoinSingleton
variable {k F : Type*} [Field k] [Field F] [Algebra k F]

Lean source · statement

theorem isNoetherianRing_adjoin (y : F) :
    IsNoetherianRing (Algebra.adjoin k ({y} : Set F))

theorem

fg_of_image_le

L58 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.Algebra_finite_integralClosure_adjoin_singleton_of_isAlgClosed.FiniteIntegralClosureAdjoinSingleton.fg_of_image_le

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace Algebra_finite_integralClosure_adjoin_singleton_of_isAlgClosed
open Polynomial IntermediateField
open scoped IntermediateField.algebraAdjoinAdjoin Pointwise
namespace FiniteIntegralClosureAdjoinSingleton
variable {k F : Type*} [Field k] [Field F] [Algebra k F]

Lean source · statement

theorem fg_of_image_le {A A' : Subalgebra k F} (φ : F →+* F) (hφ : Function.Injective φ)
    (hlift : ∀ a' ∈ A', ∃ a ∈ A, φ a = a') [IsNoetherianRing A']
    (M' : Submodule A' F) (hM' : M'.FG) (B : Submodule A F) (hB : ∀ b ∈ B, φ b ∈ M') :
    B.FG

theorem

fg_toSubmodule_integralClosure_of_isSeparable

L126 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.Algebra_finite_integralClosure_adjoin_singleton_of_isAlgClosed.FiniteIntegralClosureAdjoinSingleton.fg_toSubmodule_integralClosure_of_isSeparable

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace Algebra_finite_integralClosure_adjoin_singleton_of_isAlgClosed
open Polynomial IntermediateField
open scoped IntermediateField.algebraAdjoinAdjoin Pointwise
namespace FiniteIntegralClosureAdjoinSingleton
variable {k F : Type*} [Field k] [Field F] [Algebra k F]
section WithX
variable (x : F)

Lean source · statement

theorem fg_toSubmodule_integralClosure_of_isSeparable (hx : Transcendental k x)
    (E : IntermediateField 𝓚 F) [FiniteDimensional 𝓚 E] [Algebra.IsSeparable 𝓚 E] :
    (Subalgebra.toSubmodule (integralClosure 𝓐 E)).FG

theorem

exists_fg_of_isSeparable

L138 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.Algebra_finite_integralClosure_adjoin_singleton_of_isAlgClosed.FiniteIntegralClosureAdjoinSingleton.exists_fg_of_isSeparable

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace Algebra_finite_integralClosure_adjoin_singleton_of_isAlgClosed
open Polynomial IntermediateField
open scoped IntermediateField.algebraAdjoinAdjoin Pointwise
namespace FiniteIntegralClosureAdjoinSingleton
variable {k F : Type*} [Field k] [Field F] [Algebra k F]
section WithX
variable (x : F)

Lean source · statement

theorem exists_fg_of_isSeparable (hx : Transcendental k x)
    (E : IntermediateField 𝓚 F) [FiniteDimensional 𝓚 E] [Algebra.IsSeparable 𝓚 E] :
    ∃ N : Submodule 𝓐 F, N.FG ∧ ∀ f : F, f ∈ E → IsIntegral 𝓐 f → f ∈ N

theorem

exists_pow_mem_separableClosure

L151 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.Algebra_finite_integralClosure_adjoin_singleton_of_isAlgClosed.FiniteIntegralClosureAdjoinSingleton.exists_pow_mem_separableClosure

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace Algebra_finite_integralClosure_adjoin_singleton_of_isAlgClosed
open Polynomial IntermediateField
open scoped IntermediateField.algebraAdjoinAdjoin Pointwise
namespace FiniteIntegralClosureAdjoinSingleton
variable {k F : Type*} [Field k] [Field F] [Algebra k F]
section WithX
variable (x : F)

Lean source · statement

theorem exists_pow_mem_separableClosure [FiniteDimensional 𝓚 F] :
    ∃ p e : ℕ, ExpChar F p ∧ ∀ f : F, f ^ p ^ e ∈ separableClosure 𝓚 F

theorem

exists_pow_eq_of_mem_adjoin_pow

L162 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.Algebra_finite_integralClosure_adjoin_singleton_of_isAlgClosed.FiniteIntegralClosureAdjoinSingleton.exists_pow_eq_of_mem_adjoin_pow

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace Algebra_finite_integralClosure_adjoin_singleton_of_isAlgClosed
open Polynomial IntermediateField
open scoped IntermediateField.algebraAdjoinAdjoin Pointwise
namespace FiniteIntegralClosureAdjoinSingleton
variable {k F : Type*} [Field k] [Field F] [Algebra k F]
section WithX
variable (x : F)

Lean source · statement

theorem exists_pow_eq_of_mem_adjoin_pow [IsAlgClosed k] (p e : ℕ) [ExpChar F p]
    {a' : F} (ha' : a' ∈ Algebra.adjoin k ({x ^ p ^ e} : Set F)) :
    ∃ a ∈ 𝓐, a ^ p ^ e = a'

theorem

exists_fg_adjoin_pow_of_fg

L181 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.Algebra_finite_integralClosure_adjoin_singleton_of_isAlgClosed.FiniteIntegralClosureAdjoinSingleton.exists_fg_adjoin_pow_of_fg

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace Algebra_finite_integralClosure_adjoin_singleton_of_isAlgClosed
open Polynomial IntermediateField
open scoped IntermediateField.algebraAdjoinAdjoin Pointwise
namespace FiniteIntegralClosureAdjoinSingleton
variable {k F : Type*} [Field k] [Field F] [Algebra k F]
section WithX
variable (x : F)

Lean source · statement

theorem exists_fg_adjoin_pow_of_fg (q : ℕ) (hq : 0 < q) (N : Submodule 𝓐 F) (hN : N.FG) :
    ∃ M' : Submodule (Algebra.adjoin k ({x ^ q} : Set F)) F,
      M'.FG ∧ ∀ f ∈ N, f ∈ M'

theorem

fg_toSubmodule_integralClosure

L236 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.Algebra_finite_integralClosure_adjoin_singleton_of_isAlgClosed.FiniteIntegralClosureAdjoinSingleton.fg_toSubmodule_integralClosure

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace Algebra_finite_integralClosure_adjoin_singleton_of_isAlgClosed
open Polynomial IntermediateField
open scoped IntermediateField.algebraAdjoinAdjoin Pointwise
namespace FiniteIntegralClosureAdjoinSingleton
variable {k F : Type*} [Field k] [Field F] [Algebra k F]
section WithX
variable (x : F)

Lean source · statement

theorem fg_toSubmodule_integralClosure [IsAlgClosed k] (hx : Transcendental k x)
    (hfd : FiniteDimensional 𝓚 F) :
    (Subalgebra.toSubmodule (integralClosure 𝓐 F)).FG

theorem

finite_integralClosure_adjoin_singleton_of_isAlgClosed

L261 ↗

Algebra.finite_integralClosure_adjoin_singleton_of_isAlgClosed

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace Algebra_finite_integralClosure_adjoin_singleton_of_isAlgClosed
open Polynomial IntermediateField
open scoped IntermediateField.algebraAdjoinAdjoin Pointwise

Lean source · statement

theorem _root_.Algebra.finite_integralClosure_adjoin_singleton_of_isAlgClosed
    {k F : Type*} [Field k] [IsAlgClosed k] [Field F] [Algebra k F] (x : F)
    (hx : Transcendental k x)
    (hfd : FiniteDimensional (IntermediateField.adjoin k ({x} : Set F)) F) :
    Module.Finite (Algebra.adjoin k ({x} : Set F))
      (integralClosure (Algebra.adjoin k ({x} : Set F)) F)

Module documentation

Algebra finite integral Closure adjoin singleton of is Alg Closed

Declarations