FieldArithmetic.Chapter06.exists_generalNormalization_generatorInvariant
Generator-sensitive Noether normalization over an arbitrary field.
For a tuple of n elements, this simultaneously constructs an algebraically independent normalizing tuple and exactly n - r retained original generators. The retained generators together with the normalizing tuple generate the original algebra, and every element of the original algebra is integral over the algebra generated by the normalizing tuple.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace FieldArithmetic
namespace Chapter06
open Algebra Function MvPolynomial
variable {K : Type*} [Field K]Lean source · full declaration
theorem exists_generalNormalization_generatorInvariant
{A : Type*} [CommRing A] [Nontrivial A] [Algebra K A] :
∀ {n : ℕ} (x : Fin n → A),
∃ r : ℕ, r ≤ n ∧
∃ t : Fin r → A,
AlgebraicIndependent K t ∧
∃ J : Finset (Fin n),
J.card = n - r ∧
Algebra.adjoin K
(Set.range t ∪ x '' (J : Set (Fin n))) =
Algebra.adjoin K (Set.range x) ∧
∀ y ∈ Algebra.adjoin K (Set.range x),
IsIntegral (Algebra.adjoin K (Set.range t)) y
| 0, x => by
refine
⟨0, le_rfl, x, algebraicIndependent_empty_type, ∅, ?_, ?_, ?_⟩
· simp
· simp
· exact isIntegral_of_mem_adjoin_range_self x
| n + 1, x => by
by_cases hx : AlgebraicIndependent K x
· refine ⟨n + 1, le_rfl, x, hx, ∅, ?_, ?_, ?_⟩
· simp
· simp
· exact isIntegral_of_mem_adjoin_range_self x
· have hnotinj :
¬ Function.Injective
(aeval x : MvPolynomial (Fin (n + 1)) K →ₐ[K] A) := by
intro hinj
exact hx (algebraicIndependent_iff_injective_aeval.mpr hinj)
obtain ⟨P, Q, hPQ, hne⟩ :=
Function.not_injective_iff.mp hnotinj
let F : MvPolynomial (Fin (n + 1)) K := P - Q
have hF : F ≠ 0 := sub_ne_zero.mpr hne
have hrel : aeval x F = 0 := by
dsimp only [F]
rw [map_sub, hPQ, sub_self]
obtain ⟨m, -, hstepAdjoin, hstepIntegral⟩ :=
exists_generatorReducing_powerTail x hF hrel
let tail : Fin n → A :=
fun i => x i.succ - x 0 ^ m i
have hstepAdjoin' :
Algebra.adjoin K (Set.range x) =
Algebra.adjoin K (Set.range tail ∪ {x 0}) := by
simpa only [tail] using hstepAdjoin
have hstepIntegral' :
∀ y ∈ Algebra.adjoin K (Set.range x),
IsIntegral (Algebra.adjoin K (Set.range tail)) y := by
simpa only [tail] using hstepIntegral
obtain
⟨r, hr, t, htind, J', hJ'card, hIHadjoin, hIHintegral⟩ :=
exists_generalNormalization_generatorInvariant tail
let J : Finset (Fin (n + 1)) :=
insert 0 (J'.image Fin.succ)
refine
⟨r, hr.trans (Nat.le_succ n), t, htind, J, ?_, ?_, ?_⟩
· have hzero :
(0 : Fin (n + 1)) ∉ J'.image Fin.succ := by
simp
have himageCard :
(J'.image Fin.succ).card = J'.card :=
Finset.card_image_of_injective J' (Fin.succ_injective n)
change (insert 0 (J'.image Fin.succ)).card = n + 1 - r
rw [Finset.card_insert_of_notMem hzero, himageCard, hJ'card]
omega
· let oldSet : Set A :=
Set.range t ∪ tail '' (J' : Set (Fin n))
let newSet : Set A :=
Set.range t ∪ x '' (J : Set (Fin (n + 1)))
have hadjoinSelected :
Algebra.adjoin K newSet =
Algebra.adjoin K (oldSet ∪ {x 0}) := by
apply le_antisymm
· rw [Algebra.adjoin_le_iff]
intro y hy
change
y ∈ Set.range t ∪ x '' (J : Set (Fin (n + 1)))
at hy
rcases hy with hy | ⟨i, hiJ, rfl⟩
· apply Algebra.subset_adjoin
exact Or.inl (Or.inl hy)
· change i ∈ insert 0 (J'.image Fin.succ) at hiJ
rcases Finset.mem_insert.mp hiJ with rfl | hiJ
· apply Algebra.subset_adjoin
exact Or.inr rfl
· obtain ⟨j, hjJ, rfl⟩ :=
Finset.mem_image.mp hiJ
have htail :
tail j ∈
Algebra.adjoin K (oldSet ∪ {x 0}) := by
apply Algebra.subset_adjoin
exact Or.inl (Or.inr ⟨j, hjJ, rfl⟩)
have hzero :
x 0 ∈
Algebra.adjoin K (oldSet ∪ {x 0}) := by
apply Algebra.subset_adjoin
exact Or.inr rfl
rw [show x j.succ = tail j + x 0 ^ m j by
simp [tail]]
exact
(Algebra.adjoin K (oldSet ∪ {x 0})).add_mem
htail
((Algebra.adjoin K (oldSet ∪ {x 0})).pow_mem
hzero (m j))
· rw [Algebra.adjoin_le_iff]
intro y hy
change
y ∈
(Set.range t ∪ tail '' (J' : Set (Fin n))) ∪
{x 0}
at hy
rcases hy with (hy | rfl)
· rcases hy with hy | ⟨j, hjJ, rfl⟩
· apply Algebra.subset_adjoin
exact Or.inl hy
· change j ∈ J' at hjJ
have hxsucc :
x j.succ ∈ Algebra.adjoin K newSet := by
apply Algebra.subset_adjoin
apply Or.inr
refine ⟨j.succ, ?_, rfl⟩
change j.succ ∈
insert 0 (J'.image Fin.succ)
exact
Finset.mem_insert_of_mem
(Finset.mem_image.mpr ⟨j, hjJ, rfl⟩)
have hzero :
x 0 ∈ Algebra.adjoin K newSet := by
apply Algebra.subset_adjoin
apply Or.inr
refine ⟨0, ?_, rfl⟩
change (0 : Fin (n + 1)) ∈
insert 0 (J'.image Fin.succ)
simp
change
x j.succ - x 0 ^ m j ∈
Algebra.adjoin K newSet
exact
(Algebra.adjoin K newSet).sub_mem
hxsucc
((Algebra.adjoin K newSet).pow_mem hzero (m j))
· apply Algebra.subset_adjoin
apply Or.inr
refine ⟨0, ?_, rfl⟩
change (0 : Fin (n + 1)) ∈
insert 0 (J'.image Fin.succ)
simp
have hIHadjoin' :
Algebra.adjoin K oldSet =
Algebra.adjoin K (Set.range tail) := by
simpa only [oldSet] using hIHadjoin
change
Algebra.adjoin K newSet =
Algebra.adjoin K (Set.range x)
calc
Algebra.adjoin K newSet =
Algebra.adjoin K (oldSet ∪ {x 0}) :=
hadjoinSelected
_ =
Algebra.adjoin K oldSet ⊔
Algebra.adjoin K {x 0} :=
Algebra.adjoin_union oldSet {x 0}
_ =
Algebra.adjoin K (Set.range tail) ⊔
Algebra.adjoin K {x 0} := by
rw [hIHadjoin']
_ =
Algebra.adjoin K (Set.range tail ∪ {x 0}) :=
(Algebra.adjoin_union (Set.range tail) {x 0}).symm
_ = Algebra.adjoin K (Set.range x) :=
hstepAdjoin'.symm
· let B : Subalgebra K A :=
Algebra.adjoin K (Set.range t)
let S : Subalgebra K A :=
Algebra.adjoin K (Set.range tail)
have ht_mem_S : ∀ i, t i ∈ S := by
intro i
change t i ∈ Algebra.adjoin K (Set.range tail)
rw [← hIHadjoin]
exact
Algebra.subset_adjoin
(Set.mem_union_left _ ⟨i, rfl⟩)
have hBS : B ≤ S := by
rw [Algebra.adjoin_le_iff]
rintro y ⟨i, rfl⟩
exact ht_mem_S i
let : Algebra B S :=
(Subalgebra.inclusion hBS).toAlgebra
have : IsScalarTower B S A :=
IsScalarTower.of_algebraMap_eq fun _ => rfl
let : Algebra.IsIntegral B S :=
⟨fun z =>
(isIntegral_algebraMap_iff
(R := B) (A := S) (B := A)).mp
(hIHintegral z z.property)⟩
intro y hy
exact isIntegral_trans y (hstepIntegral' y hy)