Field generation by a parameter tuple and one primitive coordinate, and the resulting fraction-field structure on the image ring.
theorem
CCDN.primitive_parameter_tuple_adjoin_top
{K : Type u_1}
{F : Type u_2}
[Field K]
[Field F]
[Algebra K F]
{m : ℕ}
(u : Fin m → F)
(v : F)
(hprim : (↥(IntermediateField.adjoin K (Set.range u)))⟮v⟯ = ⊤)
:
If v generates F over the subfield generated by the tuple u, then the extended tuple
(v, u 0, u 1, …) generates F over K.
theorem
CCDN.isFractionRing_of_generating_tuple
{K : Type u_1}
{A : Type u_2}
{F : Type u_3}
{σ : Type u_4}
[Field K]
[CommRing A]
[Field F]
[Algebra K A]
[Algebra K F]
(φ : A →ₐ[K] F)
(hφ : Function.Injective ⇑φ)
(a : σ → A)
(ha : IntermediateField.adjoin K (Set.range fun (i : σ) => φ (a i)) = ⊤)
:
have this := φ.toAlgebra;
IsFractionRing A F
An injective algebra map into a field realizes that field as the fraction field whenever a tuple of source elements generates it as a field.