Module

IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent.lean

Nyll.AlgebraicCurves.Foundations.FieldTheory.IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent

33 declarations indexed from sourceView source ↗

Module documentation

Intermediate Field mem adjoin sum mul of is Separable of algebraic Independent

Imports18

Mathlib.FieldTheory.SeparableDegree
Mathlib.FieldTheory.PrimitiveElement
Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure
Mathlib.RingTheory.Localization.Module
Mathlib.RingTheory.Polynomial.RationalRoot
Mathlib.RingTheory.Polynomial.Resultant.Basic
Mathlib.LinearAlgebra.Lagrange
Mathlib.Algebra.Polynomial.Lifts
Mathlib.RingTheory.Polynomial.UniqueFactorization
Mathlib.Data.Fin.Tuple.Basic
Mathlib.Data.Fintype.Pigeonhole
Mathlib.Data.Nat.Find
Mathlib.Tactic.Choose
Mathlib.Tactic.Convert
Mathlib.Tactic.LinearCombination
Mathlib.Tactic.Ring.RingNF
Mathlib.Tactic.Set

Imported by2

theorem

isSeparable_transport

L50 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent.P2mFieldBertini.isSeparable_transport

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent
open Polynomial
namespace P2mFieldBertini
section Transport
variable {R₁ R₂ L L' : Type*} [Field R₁] [Field R₂] [Field L] [Field L']
  [Algebra R₁ L] [Algebra R₂ L']

Lean source · statement

theorem isSeparable_transport (e : R₁ ≃+* R₂) (σ : L →+* L')
    (he : ∀ r, algebraMap R₂ L' (e r) = σ (algebraMap R₁ L r)) {y : L}
    (h : IsSeparable R₁ y) : IsSeparable R₂ (σ y)

theorem

isSeparable_of_le

L68 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent.P2mFieldBertini.isSeparable_of_le

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent
open Polynomial
namespace P2mFieldBertini
section TransportSub
variable {k L : Type*} [Field k] [Field L] [Algebra k L]

Lean source · statement

theorem isSeparable_of_le {E₁ E₂ : IntermediateField k L} (h : E₁ ≤ E₂) {y : L}
    (hy : IsSeparable E₁ y) : IsSeparable E₂ y

theorem

transcendental_of_le

L80 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent.P2mFieldBertini.transcendental_of_le

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent
open Polynomial
namespace P2mFieldBertini
section TransportSub
variable {k L : Type*} [Field k] [Field L] [Algebra k L]

Lean source · statement

theorem transcendental_of_le {R A : Type*} [CommRing R] [CommRing A] [Algebra R A]
    {S₁ S₂ : Subalgebra R A} (h : S₁ ≤ S₂) {t : A} (ht : Transcendental S₂ t) :
    Transcendental S₁ t

theorem

transcendental_of_le'

L92 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent.P2mFieldBertini.transcendental_of_le'

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent
open Polynomial
namespace P2mFieldBertini
section TransportSub
variable {k L : Type*} [Field k] [Field L] [Algebra k L]

Lean source · statement

theorem transcendental_of_le' {E₁ E₂ : IntermediateField k L} (h : E₁ ≤ E₂) {t : L}
    (ht : Transcendental E₂ t) : Transcendental E₁ t

theorem

restrictScalars_adjoin_eq

L104 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent.P2mFieldBertini.restrictScalars_adjoin_eq

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent
open Polynomial
namespace P2mFieldBertini
section TransportSub
variable {k L : Type*} [Field k] [Field L] [Algebra k L]

Lean source · statement

theorem restrictScalars_adjoin_eq (K : Type*) [Field K] [Algebra k K] [Algebra K L]
    [IsScalarTower k K L] (S : Set L) :
    (IntermediateField.adjoin K S).restrictScalars k =
      IntermediateField.adjoin k (Set.range (algebraMap K L) ∪ S)

theorem

separable_scaleRoots

L122 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent.P2mFieldBertini.separable_scaleRoots

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent
open Polynomial
namespace P2mFieldBertini

Lean source · statement

theorem separable_scaleRoots {K : Type*} [Field K] {p : K[X]} (hp : p.Separable) {c : K}
    (hc : c ≠ 0) : (p.scaleRoots c).Separable

theorem

mem_adjoin_simple_of_isSeparable_of_transcendental

L141 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent.P2mFieldBertini.mem_adjoin_simple_of_isSeparable_of_transcendental

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent
open Polynomial
namespace P2mFieldBertini
section SC1
variable {F M L : Type*} [Field F] [Field M] [Field L] [Algebra F L] [Algebra M L]
open IntermediateField in

Lean source · statement

theorem mem_adjoin_simple_of_isSeparable_of_transcendental [Infinite F]
    (φ : F →+* M) (hφ : ∀ a, algebraMap M L (φ a) = algebraMap F L a)
    (hsc : ∀ m : M, IsSeparable F (algebraMap M L m) → ∃ a, φ a = m)
    {t : L} (ht : Transcendental M t) {y : L} (hy : y ∈ M⟮t⟯)
    (hsep : IsSeparable F⟮t⟯ y) : y ∈ F⟮t⟯

def

SepClosedIn

L355 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent.P2mFieldBertini.SepClosedIn

Documentation

Every element of the larger intermediate field that is separable over the smaller belongs to it.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent
open Polynomial
namespace P2mFieldBertini
open IntermediateField
variable {k L : Type*} [Field k] [Field L] [Algebra k L]

Lean source · statement

def SepClosedIn (F M : IntermediateField k L) : Prop

theorem

mono_right

L358 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent.P2mFieldBertini.SepClosedIn.mono_right

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent
open Polynomial
namespace P2mFieldBertini
open IntermediateField
variable {k L : Type*} [Field k] [Field L] [Algebra k L]

Lean source · statement

theorem SepClosedIn.mono_right {F M M' : IntermediateField k L} (h : SepClosedIn F M)
    (hM : M' ≤ M) : SepClosedIn F M'

theorem

adjoin_coe_adjoin_union

L361 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent.P2mFieldBertini.adjoin_coe_adjoin_union

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent
open Polynomial
namespace P2mFieldBertini
open IntermediateField
variable {k L : Type*} [Field k] [Field L] [Algebra k L]

Lean source · statement

theorem adjoin_coe_adjoin_union (S T : Set L) :
    adjoin k ((adjoin k S : Set L) ∪ T) = adjoin k (S ∪ T)

theorem

adjoin_transcendental

L365 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent.P2mFieldBertini.SepClosedIn.adjoin_transcendental

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent
open Polynomial
namespace P2mFieldBertini
open IntermediateField
variable {k L : Type*} [Field k] [Field L] [Algebra k L]

Lean source · statement

theorem SepClosedIn.adjoin_transcendental [Infinite k] {F M : IntermediateField k L}
    (hFM : F ≤ M) (h : SepClosedIn F M) {t : L} (ht : Transcendental M t) :
    SepClosedIn ((adjoin F {t}).restrictScalars k) ((adjoin M {t}).restrictScalars k)

theorem

adjoin_transcendental'

L380 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent.P2mFieldBertini.SepClosedIn.adjoin_transcendental'

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent
open Polynomial
namespace P2mFieldBertini
open IntermediateField
variable {k L : Type*} [Field k] [Field L] [Algebra k L]

Lean source · statement

theorem SepClosedIn.adjoin_transcendental' [Infinite k] {S T : Set L}
    (hST : S ⊆ T) (h : SepClosedIn (adjoin k S) (adjoin k T)) {t : L}
    (ht : Transcendental (adjoin k T) t) :
    SepClosedIn (adjoin k (S ∪ {t})) (adjoin k (T ∪ {t}))

theorem

isSeparable_of_isSeparable_bot

L387 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent.P2mFieldBertini.isSeparable_of_isSeparable_bot

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent
open Polynomial
namespace P2mFieldBertini
open IntermediateField
variable {k L : Type*} [Field k] [Field L] [Algebra k L]

Lean source · statement

theorem isSeparable_of_isSeparable_bot {y : L} (h : IsSeparable (⊥ : IntermediateField k L) y) :
    IsSeparable k y

theorem

sepClosedIn_adjoin_image

L404 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent.P2mFieldBertini.sepClosedIn_adjoin_image

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent
open Polynomial
namespace P2mFieldBertini
open IntermediateField
variable {k L : Type*} [Field k] [Field L] [Algebra k L]
section Permanence
variable [Infinite k] (K : Type*) [Field K] [Algebra k K] [Algebra K L] [IsScalarTower k K L]

Lean source · statement

theorem sepClosedIn_adjoin_image
    (hsc : ∀ θ : K, IsSeparable k θ → θ ∈ (⊥ : IntermediateField k K))
    {ι : Type*} (x : ι → L) (hx : AlgebraicIndependent K x) (s : Finset ι) :
    SepClosedIn (adjoin k (x '' ↑s)) (adjoin k (Set.range (algebraMap K L) ∪ x '' ↑s))

theorem

sepClosedIn_adjoin_range

L440 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent.P2mFieldBertini.sepClosedIn_adjoin_range

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent
open Polynomial
namespace P2mFieldBertini
open IntermediateField
variable {k L : Type*} [Field k] [Field L] [Algebra k L]
section Permanence
variable [Infinite k] (K : Type*) [Field K] [Algebra k K] [Algebra K L] [IsScalarTower k K L]

Lean source · statement

theorem sepClosedIn_adjoin_range
    (hsc : ∀ θ : K, IsSeparable k θ → θ ∈ (⊥ : IntermediateField k K))
    {ι : Type*} [Finite ι] (x : ι → L) (hx : AlgebraicIndependent K x) :
    SepClosedIn (adjoin k (Set.range x)) (adjoin k (Set.range (algebraMap K L) ∪ Set.range x))

theorem

linearIndependent_powerBasis_over_adjoin

L455 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent.P2mFieldBertini.linearIndependent_powerBasis_over_adjoin

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent
open Polynomial
namespace P2mFieldBertini
open IntermediateField
variable {k L : Type*} [Field k] [Field L] [Algebra k L]
section FinSep
variable {F E : Type*} [Field F] [Field E] [Algebra F E]
open scoped IntermediateField.algebraAdjoinAdjoin in

Lean source · full declaration

theorem linearIndependent_powerBasis_over_adjoin {ι : Type*} {x : ι → E}
    (hx : AlgebraicIndependent F x) {α : E} (hα : IsIntegral F α) :
    LinearIndependent (adjoin F (Set.range x))
      (fun i => ((adjoin.powerBasis hα).basis i : E)) := by
  classical
  set A : IntermediateField F E := F⟮α⟯
  set pb := adjoin.powerBasis hα
  have : FiniteDimensional F A := adjoin.finiteDimensional hα
  have : Algebra.IsAlgebraic F A := Algebra.IsAlgebraic.of_finite F A
  have hxA : AlgebraicIndependent A x := hx.extendScalars A
  rw [← LinearIndependent.iff_fractionRing (Algebra.adjoin F (Set.range x))
    (adjoin F (Set.range x))]
  rw [linearIndependent_iff']
  intro u g hsum i hi
  let P : _ → MvPolynomial ι F := fun j => hx.aevalEquiv.symm (g j)
  have hgP : ∀ j, (g j : E) = MvPolynomial.aeval x (P j) := by
    intro j
    have : g j = hx.aevalEquiv (P j) := by simp [P]
    conv_lhs => rw [this]
    rfl
  set Q : MvPolynomial ι A :=
    ∑ j ∈ u, MvPolynomial.C (pb.basis j) * MvPolynomial.map (algebraMap F A) (P j) with hQ
  have hQ0 : MvPolynomial.aeval x Q = 0 := by
    rw [hQ, map_sum]
    have : ∀ j ∈ u, MvPolynomial.aeval x (MvPolynomial.C (pb.basis j) *
        MvPolynomial.map (algebraMap F A) (P j)) = (g j : E) * (pb.basis j : E) := by
      intro j _
      rw [map_mul, MvPolynomial.aeval_map_algebraMap, MvPolynomial.aeval_C, hgP, mul_comm]
      rfl
    rw [Finset.sum_congr rfl this]
    simpa [Algebra.smul_def] using hsum
  have hQzero : Q = 0 := hxA.eq_zero_of_aeval_eq_zero Q hQ0
  have hcoeff : ∀ m : ι →₀ ℕ, ∑ j ∈ u, (P j).coeff m • pb.basis j = 0 := by
    intro m
    have := congrArg (fun p : MvPolynomial ι A => p.coeff m) hQzero
    rw [hQ, MvPolynomial.coeff_sum] at this
    change (∑ j ∈ u, (MvPolynomial.C (pb.basis j) *
      (MvPolynomial.map (algebraMap F A)) (P j)).coeff m) = (0 : A) at this
    rw [← this]
    apply Finset.sum_congr rfl
    intro j _
    rw [MvPolynomial.coeff_C_mul, MvPolynomial.coeff_map, Algebra.smul_def, mul_comm]
  have hPzero : ∀ j ∈ u, P j = 0 := by
    intro j hj
    ext m
    have := linearIndependent_iff'.mp pb.basis.linearIndependent u (fun j => (P j).coeff m)
      (hcoeff m) j hj
    simpa using this
  have : g i = hx.aevalEquiv (P i) := by simp [P]
  rw [this, hPzero i hi, map_zero]

theorem

exists_bound_finrank_adjoin_of_fg

L506 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent.P2mFieldBertini.exists_bound_finrank_adjoin_of_fg

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent
open Polynomial
namespace P2mFieldBertini
open IntermediateField
variable {k L : Type*} [Field k] [Field L] [Algebra k L]
section FinSep
variable {F E : Type*} [Field F] [Field E] [Algebra F E]

Lean source · statement

theorem exists_bound_finrank_adjoin_of_fg (hfg : (⊤ : IntermediateField F E).FG) :
    ∃ N : ℕ, ∀ α : E, IsIntegral F α → Module.finrank F F⟮α⟯ ≤ N

theorem

exists_isSeparable_forall_mem_adjoin_of_fg

L529 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent.P2mFieldBertini.exists_isSeparable_forall_mem_adjoin_of_fg

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent
open Polynomial
namespace P2mFieldBertini
open IntermediateField
variable {k L : Type*} [Field k] [Field L] [Algebra k L]
section FinSep
variable {F E : Type*} [Field F] [Field E] [Algebra F E]

Lean source · statement

theorem exists_isSeparable_forall_mem_adjoin_of_fg (hfg : (⊤ : IntermediateField F E).FG) :
    ∃ γ : E, IsSeparable F γ ∧ ∀ θ : E, IsSeparable F θ → θ ∈ F⟮γ⟯

theorem

exists_ne_adjoin_simple_eq

L563 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent.P2mFieldBertini.exists_ne_adjoin_simple_eq

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent
open Polynomial
namespace P2mFieldBertini
open IntermediateField
variable {k L : Type*} [Field k] [Field L] [Algebra k L]
section FinSep
variable {F E : Type*} [Field F] [Field E] [Algebra F E]

Lean source · statement

theorem exists_ne_adjoin_simple_eq {α : Type*} [Infinite α]
    (hfg : (⊤ : IntermediateField F E).FG) (θ : α → E) (hθ : ∀ a, IsSeparable F (θ a)) :
    ∃ a₁ a₂, a₁ ≠ a₂ ∧ F⟮θ a₁⟯ = F⟮θ a₂⟯

theorem

map_adjoin_range_union_singleton

L589 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent.P2mFieldBertini.map_adjoin_range_union_singleton

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent
open Polynomial
namespace P2mFieldBertini
open IntermediateField
variable {k L : Type*} [Field k] [Field L] [Algebra k L]
section Bookkeeping
variable {K : Type*} [Field K] [Algebra k K] [Algebra K L] [IsScalarTower k K L]

Lean source · statement

theorem map_adjoin_range_union_singleton {ι : Type*} (σ : L ≃ₐ[k] L) (x : ι → L) (b : ι → k)
    (hσx : ∀ i, σ (x i) = x i + algebraMap k L (b i)) (ξ ξ' : L) (hσξ : σ ξ = ξ') :
    (adjoin k (Set.range x ∪ {ξ})).map (σ : L →ₐ[k] L) = adjoin k (Set.range x ∪ {ξ'})

theorem

fg_top_of_adjoin_eq_top

L616 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent.P2mFieldBertini.fg_top_of_adjoin_eq_top

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent
open Polynomial
namespace P2mFieldBertini
open IntermediateField
variable {k L : Type*} [Field k] [Field L] [Algebra k L]
section Bookkeeping
variable {K : Type*} [Field K] [Algebra k K] [Algebra K L] [IsScalarTower k K L]

Lean source · statement

theorem fg_top_of_adjoin_eq_top (hfg : (⊤ : IntermediateField k K).FG) {S : Set L}
    (htop : adjoin k (Set.range (algebraMap K L) ∪ S) = ⊤) (E : IntermediateField k L)
    (hS : S ⊆ E) : (⊤ : IntermediateField E L).FG

theorem

mem_of_two_shifts

L637 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent.P2mFieldBertini.mem_of_two_shifts

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent
open Polynomial
namespace P2mFieldBertini
open IntermediateField
variable {k L : Type*} [Field k] [Field L] [Algebra k L]
section Bookkeeping
variable {K : Type*} [Field K] [Algebra k K] [Algebra K L] [IsScalarTower k K L]

Lean source · statement

theorem mem_of_two_shifts (N : IntermediateField k L) {ξ δ : L} {a₁ a₂ : k} (hne : a₁ ≠ a₂)
    (h₁ : ξ + algebraMap k L a₁ * δ ∈ N) (h₂ : ξ + algebraMap k L a₂ * δ ∈ N) :
    ξ ∈ N ∧ δ ∈ N

def

tau

L661 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent.P2mFieldBertini.tau

Documentation

The polynomial algebra automorphism translating each variable by the corresponding scalar.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent
open Polynomial
namespace P2mFieldBertini
open IntermediateField
variable {k L : Type*} [Field k] [Field L] [Algebra k L]
section Omega
variable (k K : Type*) [Field k] [Field K] [Algebra k K] (n : ℕ)

Lean source · statement

def tau (b : Fin (n + 1) → K) :
    MvPolynomial (Fin (n + 1)) K ≃ₐ[K] MvPolynomial (Fin (n + 1)) K

theorem

tau_X

L669 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent.P2mFieldBertini.tau_X

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent
open Polynomial
namespace P2mFieldBertini
open IntermediateField
variable {k L : Type*} [Field k] [Field L] [Algebra k L]
section Omega
variable (k K : Type*) [Field k] [Field K] [Algebra k K] (n : ℕ)

Lean source · statement

theorem tau_X (b : Fin (n + 1) → K) (i : Fin (n + 1)) :
    tau K n b (MvPolynomial.X i) = MvPolynomial.X i + MvPolynomial.C (b i)

def

sigma

L675 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent.P2mFieldBertini.sigma

Documentation

The automorphism of the rational function field induced by translation of the polynomial variables.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent
open Polynomial
namespace P2mFieldBertini
open IntermediateField
variable {k L : Type*} [Field k] [Field L] [Algebra k L]
section Omega
variable (k K : Type*) [Field k] [Field K] [Algebra k K] (n : ℕ)

Lean source · statement

def sigma (b : Fin (n + 1) → K) :
    FractionRing (MvPolynomial (Fin (n + 1)) K) ≃ₐ[k] FractionRing (MvPolynomial (Fin (n + 1)) K)

theorem

sigma_algebraMap

L680 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent.P2mFieldBertini.sigma_algebraMap

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent
open Polynomial
namespace P2mFieldBertini
open IntermediateField
variable {k L : Type*} [Field k] [Field L] [Algebra k L]
section Omega
variable (k K : Type*) [Field k] [Field K] [Algebra k K] (n : ℕ)

Lean source · statement

theorem sigma_algebraMap (b : Fin (n + 1) → K) (p : MvPolynomial (Fin (n + 1)) K) :
    sigma k K n b (algebraMap _ _ p) = algebraMap _ _ (tau K n b p)

theorem

sigma_X

L684 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent.P2mFieldBertini.sigma_X

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent
open Polynomial
namespace P2mFieldBertini
open IntermediateField
variable {k L : Type*} [Field k] [Field L] [Algebra k L]
section Omega
variable (k K : Type*) [Field k] [Field K] [Algebra k K] (n : ℕ)

Lean source · statement

theorem sigma_X (b : Fin (n + 1) → K) (i : Fin (n + 1)) :
    sigma k K n b (algebraMap _ _ (MvPolynomial.X i : MvPolynomial (Fin (n + 1)) K)) =
      algebraMap _ _ (MvPolynomial.X i : MvPolynomial (Fin (n + 1)) K) + algebraMap K _ (b i)

theorem

sigma_algebraMap_K

L690 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent.P2mFieldBertini.sigma_algebraMap_K

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent
open Polynomial
namespace P2mFieldBertini
open IntermediateField
variable {k L : Type*} [Field k] [Field L] [Algebra k L]
section Omega
variable (k K : Type*) [Field k] [Field K] [Algebra k K] (n : ℕ)

Lean source · statement

theorem sigma_algebraMap_K (b : Fin (n + 1) → K) (g : K) :
    sigma k K n b (algebraMap K _ g) = algebraMap K _ g

theorem

adjoin_range_union_range_X_eq_top

L695 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent.P2mFieldBertini.adjoin_range_union_range_X_eq_top

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent
open Polynomial
namespace P2mFieldBertini
open IntermediateField
variable {k L : Type*} [Field k] [Field L] [Algebra k L]
section Omega
variable (k K : Type*) [Field k] [Field K] [Algebra k K] (n : ℕ)

Lean source · full declaration

theorem adjoin_range_union_range_X_eq_top :
    adjoin k (Set.range (algebraMap K (FractionRing (MvPolynomial (Fin (n + 1)) K))) ∪
      Set.range (fun i => algebraMap (MvPolynomial (Fin (n + 1)) K)
        (FractionRing (MvPolynomial (Fin (n + 1)) K)) (MvPolynomial.X i))) = ⊤ := by
  set Ω := FractionRing (MvPolynomial (Fin (n + 1)) K)
  set N := adjoin k (Set.range (algebraMap K Ω) ∪
      Set.range (fun i => algebraMap (MvPolynomial (Fin (n + 1)) K) Ω (MvPolynomial.X i)))
  have hpoly : ∀ p : MvPolynomial (Fin (n + 1)) K, algebraMap _ Ω p ∈ N := by
    intro p
    induction p using MvPolynomial.induction_on with
    | C a =>
      rw [← MvPolynomial.algebraMap_eq, ← IsScalarTower.algebraMap_apply]
      exact subset_adjoin k _ (Or.inl ⟨a, rfl⟩)
    | add p q hp hq => rw [map_add]; exact add_mem hp hq
    | mul_X p i hp =>
      rw [map_mul]
      exact mul_mem hp (subset_adjoin k _ (Or.inr ⟨i, rfl⟩))
  rw [eq_top_iff]
  intro z _
  obtain ⟨p, q, -, rfl⟩ := IsFractionRing.div_surjective (A := MvPolynomial (Fin (n + 1)) K) z
  exact div_mem (hpoly p) (hpoly q)

theorem

transcendental_shift

L723 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent.P2mFieldBertini.transcendental_shift

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent
open Polynomial
namespace P2mFieldBertini
open IntermediateField
variable {k L : Type*} [Field k] [Field L] [Algebra k L]
section ChangeVar
variable {k Ω : Type*} [Field k] [Field Ω] [Algebra k Ω] {n : ℕ}

Lean source · statement

theorem transcendental_shift (x : Fin (n + 1) → Ω) (ξ δ : Ω)
    (hind : AlgebraicIndependent k (Fin.snoc (Fin.snoc x ξ) δ)) {a₁ a₂ : k} (hne : a₁ ≠ a₂) :
    Transcendental (adjoin k (Set.range x ∪ {ξ + algebraMap k Ω a₁ * δ}))
      (ξ + algebraMap k Ω a₂ * δ)

theorem

transcendental_restrictScalars_adjoin

L819 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent.P2mFieldBertini.transcendental_restrictScalars_adjoin

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent
open Polynomial
namespace P2mFieldBertini
open IntermediateField
variable {k L : Type*} [Field k] [Field L] [Algebra k L]
section Final
universe u v
variable {k : Type u} {K : Type v} [Field k] [Field K] [Algebra k K]

Lean source · statement

theorem transcendental_restrictScalars_adjoin {L : Type*} [Field L] [Algebra k L]
    {E : IntermediateField k L} {θ t : L} (hθ : IsIntegral E θ)
    (ht : Transcendental E t) : Transcendental ((adjoin E {θ}).restrictScalars k) t

theorem

fieldBertini

L831 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent.P2mFieldBertini.fieldBertini

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent
open Polynomial
namespace P2mFieldBertini
open IntermediateField
variable {k L : Type*} [Field k] [Field L] [Algebra k L]
section Final
universe u v
variable {k : Type u} {K : Type v} [Field k] [Field K] [Algebra k K]
variable [Infinite k]

Lean source · statement

theorem fieldBertini
    (hfg : (⊤ : IntermediateField k K).FG)
    (hsc : ∀ θ : K, IsSeparable k θ → θ ∈ (⊥ : IntermediateField k K))
    {n : ℕ} (g : Fin (n + 1) → K) (c : Fin (n + 1) → k)
    (x : Fin (n + 1) → FractionRing (MvPolynomial (Fin (n + 1)) K))
    (hx : ∀ i, x i = algebraMap (MvPolynomial (Fin (n + 1)) K) _ (MvPolynomial.X i))
    (hind : AlgebraicIndependent k
      (Fin.snoc (Fin.snoc x (∑ i, algebraMap K _ (g i) * x i)) (algebraMap K _ (∑ i, c i • g i))))
    (θ : FractionRing (MvPolynomial (Fin (n + 1)) K))
    (hθ : IsSeparable
      (IntermediateField.adjoin k (Set.range x ∪ {∑ i, algebraMap K _ (g i) * x i})) θ) :
    θ ∈ IntermediateField.adjoin k (Set.range x ∪ {∑ i, algebraMap K _ (g i) * x i})

theorem

mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent

L958 ↗

IntermediateField.mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IntermediateField_mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent
open Polynomial
universe u v

Lean source · statement

theorem _root_.IntermediateField.mem_adjoin_sum_mul_of_isSeparable_of_algebraicIndependent
    {k : Type u} {K : Type v} [Field k] [Infinite k] [Field K] [Algebra k K]
    (hfg : (⊤ : IntermediateField k K).FG)
    (hsc : ∀ θ : K, IsSeparable k θ → θ ∈ (⊥ : IntermediateField k K))
    {n : ℕ} (g : Fin (n + 1) → K) (c : Fin (n + 1) → k)
    (x : Fin (n + 1) → FractionRing (MvPolynomial (Fin (n + 1)) K))
    (hx : ∀ i, x i = algebraMap (MvPolynomial (Fin (n + 1)) K) _ (MvPolynomial.X i))
    (hind : AlgebraicIndependent k
      (Fin.snoc (Fin.snoc x (∑ i, algebraMap K _ (g i) * x i)) (algebraMap K _ (∑ i, c i • g i))))
    (θ : FractionRing (MvPolynomial (Fin (n + 1)) K))
    (hθ : IsSeparable
      (IntermediateField.adjoin k (Set.range x ∪ {∑ i, algebraMap K _ (g i) * x i})) θ) :
    θ ∈ IntermediateField.adjoin k (Set.range x ∪ {∑ i, algebraMap K _ (g i) * x i})

Module documentation

Intermediate Field mem adjoin sum mul of is Separable of algebraic Independent

Declarations