Module

ValuationSubring_mem_adjoin_singleton_of_isIntegral_of_separable_minpoly.lean

Nyll.AlgebraicCurves.Valuations.ValuationSubring_mem_adjoin_singleton_of_isIntegral_of_separable_minpoly

7 declarations indexed from sourceView source ↗

Module documentation

Valuation Subring mem adjoin singleton of is Integral of separable minpoly

Imports7

Mathlib.RingTheory.Valuation.ValuationSubring
Mathlib.RingTheory.Valuation.Integral
Mathlib.RingTheory.Valuation.LocalSubring
Mathlib.RingTheory.Discriminant
Mathlib.FieldTheory.SeparableDegree
Mathlib.Algebra.Polynomial.Splits
Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Imported by2

theorem

integers

L38 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_mem_adjoin_singleton_of_isIntegral_of_separable_minpoly.Ws50V1.integers

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_mem_adjoin_singleton_of_isIntegral_of_separable_minpoly
open Polynomial
namespace Ws50V1
section RootDiff
variable {κ E : Type*} [Field κ] [Field E] [Algebra κ E] (B : ValuationSubring E)

Lean source · full declaration

theorem integers : B.valuation.Integers B where
  hom_inj := Subtype.val_injective
  map_le_one := B.valuation_le_one
  exists_of_le_one := fun x hx => ⟨⟨x, (B.valuation_le_one_iff x).mp hx⟩, rfl⟩

theorem

mem_of_isIntegral

L43 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_mem_adjoin_singleton_of_isIntegral_of_separable_minpoly.Ws50V1.mem_of_isIntegral

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_mem_adjoin_singleton_of_isIntegral_of_separable_minpoly
open Polynomial
namespace Ws50V1
section RootDiff
variable {κ E : Type*} [Field κ] [Field E] [Algebra κ E] (B : ValuationSubring E)

Lean source · statement

theorem mem_of_isIntegral (hκ : ∀ a : κ, algebraMap κ E a ∈ B) {s : E} (hs : IsIntegral κ s) : s ∈
  B

theorem

aeval_mem

L55 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_mem_adjoin_singleton_of_isIntegral_of_separable_minpoly.Ws50V1.aeval_mem

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_mem_adjoin_singleton_of_isIntegral_of_separable_minpoly
open Polynomial
namespace Ws50V1
section RootDiff
variable {κ E : Type*} [Field κ] [Field E] [Algebra κ E] (B : ValuationSubring E)

Lean source · statement

theorem aeval_mem (hκ : ∀ a : κ, algebraMap κ E a ∈ B) (q : κ[X]) {s : E} (hs : s ∈ B) : aeval s q
  ∈ B

theorem

eq_one_of_prod_map_eq_one

L65 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_mem_adjoin_singleton_of_isIntegral_of_separable_minpoly.Ws50V1.eq_one_of_prod_map_eq_one

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_mem_adjoin_singleton_of_isIntegral_of_separable_minpoly
open Polynomial
namespace Ws50V1
section RootDiff
variable {κ E : Type*} [Field κ] [Field E] [Algebra κ E] (B : ValuationSubring E)

Lean source · statement

theorem eq_one_of_prod_map_eq_one {ι M : Type*} [CommMonoid M] [PartialOrder M] [IsOrderedMonoid M]
    (s : Multiset ι) (f : ι → M) (hle : ∀ a ∈ s, f a ≤ 1) (hprod : (s.map f).prod = 1) {a : ι} (ha
      : a ∈ s) :
    f a = 1

theorem

valuation_sub_eq_one

L82 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_mem_adjoin_singleton_of_isIntegral_of_separable_minpoly.Ws50V1.valuation_sub_eq_one

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_mem_adjoin_singleton_of_isIntegral_of_separable_minpoly
open Polynomial
namespace Ws50V1
section RootDiff
variable {κ E : Type*} [Field κ] [Field E] [Algebra κ E] (B : ValuationSubring E)

Lean source · statement

theorem valuation_sub_eq_one (hκ : ∀ a : κ, algebraMap κ E a ∈ B)
    {g : κ[X]} (hg : g.Monic) (hsep : g.Separable) (hsplit : (g.map (algebraMap κ E)).Splits)
    {r r' : E} (hr : r ∈ (g.map (algebraMap κ E)).roots) (hr' : r' ∈ (g.map (algebraMap κ E)).roots)
    (hne : r ≠ r') : B.valuation (r - r') = 1

theorem

exists_unit_eq_discr

L128 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_mem_adjoin_singleton_of_isIntegral_of_separable_minpoly.Ws50V1.exists_unit_eq_discr

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_mem_adjoin_singleton_of_isIntegral_of_separable_minpoly
open Polynomial
namespace Ws50V1
section Main
variable {κ F L : Type*} [Field κ] [Field F] [Field L] [Algebra κ F] [Algebra F L] [Algebra κ L]
  [IsScalarTower κ F L] (𝒪 : ValuationSubring F) [Algebra 𝒪 L] [IsScalarTower 𝒪 F L]

Lean source · statement

theorem exists_unit_eq_discr (hκ : ∀ a : κ, algebraMap κ F a ∈ 𝒪)
    (c : L) (hc : IsIntegral κ c) (hsep : (minpoly κ c).Separable)
    (pb : PowerBasis F L) (hpb : pb.gen = c) [FiniteDimensional F L] [Algebra.IsSeparable F L] :
    ∃ u : 𝒪ˣ, algebraMap 𝒪 F u = Algebra.discr F pb.basis

theorem

mem_adjoin_singleton_of_isIntegral_of_separable_minpoly

L205 ↗

ValuationSubring.mem_adjoin_singleton_of_isIntegral_of_separable_minpoly

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_mem_adjoin_singleton_of_isIntegral_of_separable_minpoly
open Polynomial
open Ws50V1 in

Lean source · statement

theorem _root_.ValuationSubring.mem_adjoin_singleton_of_isIntegral_of_separable_minpoly
    {κ F L : Type*} [Field κ] [Field F] [Field L] [Algebra κ F] [Algebra F L] [Algebra κ L]
      [IsScalarTower κ F L]
    (𝒪 : ValuationSubring F) [Algebra 𝒪 L] [IsScalarTower 𝒪 F L]
    (hκ : ∀ a : κ, algebraMap κ F a ∈ 𝒪)
    (c : L) (hc : IsIntegral κ c) (hsep : (minpoly κ c).Separable)
    (hgen : IntermediateField.adjoin F ({c} : Set L) = ⊤)
    (z : L) (hz : IsIntegral 𝒪 z) :
    z ∈ Algebra.adjoin 𝒪 ({c} : Set L)

Module documentation

Valuation Subring mem adjoin singleton of is Integral of separable minpoly

Declarations

integers

mem_of_isIntegral

aeval_mem

eq_one_of_prod_map_eq_one

valuation_sub_eq_one

exists_unit_eq_discr

mem_adjoin_singleton_of_isIntegral_of_separable_minpoly