The algebraic core of the primitive normalization

The abstract form of the primitive normalization ([GR84, Chapter 3, §1]; the second alternative of [Fre17, Ch. I, 8.2]): let R be a domain of characteristic zero (the base 𝒪_d; integral closedness enters only in the division argument, through minpoly.isIntegrallyClosed_dvd), S a domain which is finite over R through an injective ring map f (the quotient 𝒪_n / P with the Noether normalization), both algebras over an infinite field C (the constants ℂ) compatibly with f. Given finitely many elements ξ_i of S (the classes of the fibre coordinates) with a distinguished ξ_{i₀}:

• there are constants c_j ∈ C, c_{i₀} = 1, such that γ := ∑ c_j ξ_j is a primitive element: the field Frac S is generated over Frac R by γ (PrimitiveLinear.lean, exists_linear_primitive_of_isIntegral, applied in Frac S / Frac R);
• the minimal polynomial Q := minpoly R γ is monic and irreducible in R[T] (Mathlib's minpoly.irreducible for domains) and Q(γ) = 0;
• every ξ_i lies in Frac R (γ) = Frac R [γ] (γ is algebraic), so clearing denominators gives A ∈ R ∖ 0 and B_i ∈ R[T] with A · ξ_i = B_i(γ) in S (IsLocalization.integerNormalization, the injectivity of S → Frac S, a common denominator).

The statement is in ring-map form (Polynomial.eval₂ f), with no Algebra R S instance, because it is applied to a quotient of 𝒪_n whose ring structure is not reducibly the one an R-algebra instance built from f would carry (the algebra structure is introduced locally inside the proof by RingHom.toAlgebra).

theorem Analytic.exists_linear_primitive_relations {R : Type u_1} {S : Type u_2} [CommRing R] [IsDomain R] [CharZero R] [CommRing S] [IsDomain S] {C : Type u_3} [Field C] [Algebra C R] [Algebra C S] (f : R →+* S) (hf : f.Finite) (hinj : Function.Injective ⇑f) (hC : ∀ (c : C), f ((algebraMap C R) c) = (algebraMap C S) c) {ι : Type u_4} (s : Finset ι) (ξ : ι → S) {i₀ : ι} (hi₀ : i₀ ∈ s) : ∃ (c : ι → C), c i₀ = 1 ∧ (∀ i ∉ s, c i = 0) ∧ ∃ (Q : Polynomial R), Q.Monic ∧ Irreducible Q ∧ Polynomial.eval₂ f (∑ j ∈ s, (algebraMap C S) (c j) * ξ j) Q = 0 ∧ ∃ (A : R), A ≠ 0 ∧ ∀ i ∈ s, ∃ (B : Polynomial R), f A * ξ i = Polynomial.eval₂ f (∑ j ∈ s, (algebraMap C S) (c j) * ξ j) B

The algebraic core of the primitive normalization (the second alternative of [Fre17, Ch. I, 8.2], over a d-dimensional base): for a domain S finite over the domain R (characteristic 0) through an injective f : R →+* S, both C-algebras compatibly (C an field), and a finite family ξ_i ∈ S (i ∈ s, i₀ ∈ s), there are constants c : ι → C with c i₀ = 1, c = 0 off s, such that with γ := ∑ c_j ξ_j: the minimal polynomial Q of γ over R is monic irreducible with Q(γ) = 0, and some A ∈ R ∖ 0 has A · ξ_i = B_i(γ) for polynomials B_i ∈ R[T], every i ∈ s.